add(substitution): substitution distributes over applications and explicit substitutions (M2 support)

scripts/audit.sh

@@ -35,7 +35,7 @@ done < <(find theory -name '*.v' -print0 2>/dev/null)
 echo "== Print Assumptions =="
 WORK="$(mktemp -d ./.audit-work.XXXXXX)"
 cp theory/*.v "$WORK"/
-for f in ExecReducer Binding Reduction Metatheory Subsystem Tests; do
+for f in ExecReducer Binding Reduction Metatheory Subsystem Substitution Tests; do
   echo "-- $f"
   out="$(rocq compile -Q "$WORK" LambdaSub "$WORK/$f.v" 2>&1 || true)"
   echo "$out"

theory/Substitution.v

@@ -0,0 +1,66 @@
+From Stdlib Require Import List Bool Arith Lia PeanoNat.
+Import ListNotations.
+From LambdaSub Require Import ExecReducer Binding.
+
+Lemma open_rec_app : forall k u a b,
+  open_rec k u (App a b) = App (open_rec k u a) (open_rec k u b).
+Proof. reflexivity. Qed.
+
+Lemma open_rec_lam : forall k u a,
+  open_rec k u (Lam a) = Lam (open_rec (S k) u a).
+Proof. reflexivity. Qed.
+
+Lemma open_rec_esub : forall k u a b,
+  open_rec k u (ESub a b) = ESub (open_rec (S k) u a) (open_rec k u b).
+Proof. reflexivity. Qed.
+
+Lemma close_rec_app : forall x k a b,
+  close_rec x k (App a b) = App (close_rec x k a) (close_rec x k b).
+Proof. reflexivity. Qed.
+
+Lemma close_rec_lam : forall x k a,
+  close_rec x k (Lam a) = Lam (close_rec x (S k) a).
+Proof. reflexivity. Qed.
+
+Lemma close_rec_esub : forall x k a b,
+  close_rec x k (ESub a b) = ESub (close_rec x (S k) a) (close_rec x k b).
+Proof. reflexivity. Qed.
+
+Lemma subst_app : forall x u a b,
+  subst x u (App a b) = App (subst x u a) (subst x u b).
+Proof. reflexivity. Qed.
+
+Lemma subst_lam : forall x u a,
+  subst x u (Lam a) = Lam (open_rec 1 u (close_rec x 1 a)).
+Proof. reflexivity. Qed.
+
+Lemma subst_esub : forall x u a b,
+  subst x u (ESub a b) = ESub (open_rec 1 u (close_rec x 1 a)) (subst x u b).
+Proof. reflexivity. Qed.
+
+Lemma subst_notin : forall x u t,
+  ~ In x (fvs t) -> occurs 0 t = false -> subst x u t = t.
+Proof.
+  intros x u t Hx Ho. unfold subst.
+  rewrite (close_rec_notin t x 0 Hx).
+  apply open_rec_occurs_false. exact Ho.
+Qed.
+
+Lemma subst_lc_self : forall x u, lc u -> subst x u (FVar x) = u.
+Proof. intros. apply subst_fvar_self. exact H. Qed.
+
+Lemma subst_other : forall x y u, y <> x -> subst x u (FVar y) = FVar y.
+Proof. intros. apply subst_fvar_other. exact H. Qed.
+
+Print Assumptions open_rec_app.
+Print Assumptions open_rec_lam.
+Print Assumptions open_rec_esub.
+Print Assumptions close_rec_app.
+Print Assumptions close_rec_lam.
+Print Assumptions close_rec_esub.
+Print Assumptions subst_app.
+Print Assumptions subst_lam.
+Print Assumptions subst_esub.
+Print Assumptions subst_notin.
+Print Assumptions subst_lc_self.
+Print Assumptions subst_other.