add(binding): locally nameless opening closing lifting and substitution laws (M1 obligations)

scripts/audit.sh

@@ -33,17 +33,19 @@ while IFS= read -r -d '' f; do
 done < <(find theory -name '*.v' -print0 2>/dev/null)
 
 echo "== Print Assumptions =="
-mkdir -p /tmp/opencode/audit
+for f in ExecReducer Binding Reduction; do
-out="$(rocq compile -o /tmp/opencode/audit/ExecReducer.vo theory/ExecReducer.v 2>&1 || true)"
+  echo "-- $f"
-echo "$out"
+  out="$(rocq compile -Q theory LambdaSub "theory/$f.v" 2>&1 || true)"
-if echo "$out" | grep -q "Axioms:"; then
+  echo "$out"
-  echo "unexpected axioms reported" >&2
+  if echo "$out" | grep -q "Axioms:"; then
-  fail=1
+    echo "unexpected axioms reported in $f" >&2
-fi
+    fail=1
-if ! echo "$out" | grep -q "Closed under the global context"; then
+  fi
-  echo "no Closed-under-global-context report found" >&2
+  if ! echo "$out" | grep -q "Closed under the global context"; then
-  fail=1
+    echo "no Closed-under-global-context report found for $f" >&2
-fi
+    fail=1
+  fi
+done
 
 if [ "$fail" -ne 0 ]; then
   echo "AUDIT FAIL"

theory/Binding.v

@@ -0,0 +1,157 @@
+From Stdlib Require Import List Bool Arith Lia PeanoNat.
+Import ListNotations.
+From LambdaSub Require Import ExecReducer.
+
+Fixpoint lc_at (d : nat) (t : trm) : Prop :=
+  match t with
+  | BVar n => n < d
+  | FVar _ => True
+  | App a b => lc_at d a /\ lc_at d b
+  | Lam a => lc_at (S d) a
+  | ESub a b => lc_at (S d) a /\ lc_at d b
+  end.
+
+Definition lc (t : trm) : Prop := lc_at 0 t.
+
+Lemma fvs_lift : forall t k, fvs (lift k t) = fvs t.
+Proof.
+  induction t; intros k; simpl.
+  - destruct (Nat.ltb n k); reflexivity.
+  - reflexivity.
+  - rewrite IHt1, IHt2. reflexivity.
+  - rewrite IHt. reflexivity.
+  - rewrite IHt1, IHt2. reflexivity.
+Qed.
+
+Lemma lift_lc : forall t d, lc_at d t -> lift d t = t.
+Proof.
+  induction t; intros d H; simpl in *.
+  - apply Nat.ltb_lt in H. rewrite H. reflexivity.
+  - reflexivity.
+  - destruct H as [Ha Hb]. rewrite (IHt1 d Ha), (IHt2 d Hb). reflexivity.
+  - rewrite (IHt (S d) H). reflexivity.
+  - destruct H as [Ha Hb]. rewrite (IHt1 (S d) Ha), (IHt2 d Hb). reflexivity.
+Qed.
+
+Lemma lift_0_lc : forall t, lc t -> lift 0 t = t.
+Proof. intros t H. apply lift_lc. exact H. Qed.
+
+Lemma open_rec_bvar : forall k u, open_rec k u (BVar k) = lift k u.
+Proof. intros. simpl. rewrite Nat.eqb_refl. reflexivity. Qed.
+
+Lemma close_rec_fvar : forall x k, close_rec x k (FVar x) = BVar k.
+Proof. intros. simpl. rewrite Nat.eqb_refl. reflexivity. Qed.
+
+Lemma open_rec_occurs_false : forall t u k, occurs k t = false -> open_rec k u t = t.
+Proof.
+  induction t; intros u k H; simpl in *.
+  - rewrite H. reflexivity.
+  - reflexivity.
+  - apply orb_false_iff in H as [Ha Hb].
+    rewrite (IHt1 u k Ha), (IHt2 u k Hb). reflexivity.
+  - rewrite (IHt u (S k) H). reflexivity.
+  - apply orb_false_iff in H as [Ha Hb].
+    rewrite (IHt1 u (S k) Ha), (IHt2 u k Hb). reflexivity.
+Qed.
+
+Lemma close_rec_notin : forall t x k, ~ In x (fvs t) -> close_rec x k t = t.
+Proof.
+  induction t; intros x k H; simpl in *.
+  - reflexivity.
+  - destruct (Nat.eqb a x) eqn:E.
+    + apply Nat.eqb_eq in E. subst a. exfalso. apply H. simpl. left. reflexivity.
+    + reflexivity.
+  - assert (Ha : ~ In x (fvs t1)) by (intro Hi; apply H; apply in_app_iff; left; exact Hi).
+    assert (Hb : ~ In x (fvs t2)) by (intro Hi; apply H; apply in_app_iff; right; exact Hi).
+    rewrite (IHt1 x k Ha), (IHt2 x k Hb). reflexivity.
+  - rewrite (IHt x (S k) H). reflexivity.
+  - assert (Ha : ~ In x (fvs t1)) by (intro Hi; apply H; apply in_app_iff; left; exact Hi).
+    assert (Hb : ~ In x (fvs t2)) by (intro Hi; apply H; apply in_app_iff; right; exact Hi).
+    rewrite (IHt1 x (S k) Ha), (IHt2 x k Hb). reflexivity.
+Qed.
+
+Lemma close_rec_fvs : forall t x k y, In y (fvs (close_rec x k t)) -> In y (fvs t).
+Proof.
+  induction t; intros x k y H; simpl in *.
+  - destruct H.
+  - destruct (Nat.eqb a x) eqn:E.
+    + destruct H.
+    + destruct H as [Hy | Hf]. subst y. simpl. left. reflexivity. destruct Hf.
+  - apply in_app_iff in H as [H|H]; apply in_app_iff.
+    + left. apply (IHt1 x k y). exact H.
+    + right. apply (IHt2 x k y). exact H.
+  - apply (IHt x (S k) y). exact H.
+  - apply in_app_iff in H as [H|H]; apply in_app_iff.
+    + left. apply (IHt1 x (S k) y). exact H.
+    + right. apply (IHt2 x k y). exact H.
+Qed.
+
+Lemma open_rec_bvar_neq : forall n k u, n <> k -> open_rec k u (BVar n) = BVar n.
+Proof.
+  intros n k u H. simpl. destruct (Nat.eqb n k) eqn:E.
+  - apply Nat.eqb_eq in E. contradiction.
+  - reflexivity.
+Qed.
+
+Lemma open_rec_fvs : forall t u k y, In y (fvs (open_rec k u t)) -> In y (fvs u) \/ In y (fvs t).
+Proof.
+  induction t; intros u k y H.
+  - destruct (Nat.eqb n k) eqn:E.
+    + apply Nat.eqb_eq in E. subst n. rewrite (open_rec_bvar k u) in H.
+      left. rewrite <- (fvs_lift u k). exact H.
+    + apply Nat.eqb_neq in E. rewrite (open_rec_bvar_neq n k u E) in H.
+      simpl in H. destruct H.
+  - simpl in H. right. exact H.
+  - simpl in H. apply in_app_iff in H as [H|H].
+    + destruct (IHt1 u k y H) as [Hl|Hr]. left. exact Hl. right. apply in_app_iff. left. exact Hr.
+    + destruct (IHt2 u k y H) as [Hl|Hr]. left. exact Hl. right. apply in_app_iff. right. exact Hr.
+  - simpl in H. destruct (IHt u (S k) y H) as [Hl|Hr]. left. exact Hl. right. exact Hr.
+  - simpl in H. apply in_app_iff in H as [H|H].
+    + destruct (IHt1 u (S k) y H) as [Hl|Hr]. left. exact Hl. right. apply in_app_iff. left. exact Hr.
+    + destruct (IHt2 u k y H) as [Hl|Hr]. left. exact Hl. right. apply in_app_iff. right. exact Hr.
+Qed.
+
+Lemma open_close : forall t x k, occurs k t = false -> open_rec k (FVar x) (close_rec x k t) = t.
+Proof.
+  induction t; intros x k H; simpl in *.
+  - rewrite H. reflexivity.
+  - destruct (Nat.eqb a x) eqn:E.
+    + apply Nat.eqb_eq in E. subst a. rewrite open_rec_bvar. reflexivity.
+    + reflexivity.
+  - apply orb_false_iff in H as [Ha Hb].
+    rewrite (IHt1 x k Ha), (IHt2 x k Hb). reflexivity.
+  - rewrite (IHt x (S k) H). reflexivity.
+  - apply orb_false_iff in H as [Ha Hb].
+    rewrite (IHt1 x (S k) Ha), (IHt2 x k Hb). reflexivity.
+Qed.
+
+Lemma subst_fvar_self : forall x u, lc u -> subst x u (FVar x) = u.
+Proof.
+  intros x u Hu. unfold subst. simpl. rewrite Nat.eqb_refl. simpl.
+  apply lift_0_lc. exact Hu.
+Qed.
+
+Lemma subst_fvar_other : forall x y u, y <> x -> subst x u (FVar y) = FVar y.
+Proof.
+  intros x y u Hxy. unfold subst. simpl. destruct (Nat.eqb y x) eqn:E.
+  - apply Nat.eqb_eq in E. contradiction.
+  - reflexivity.
+Qed.
+
+Lemma subst_fvs : forall x u t y, In y (fvs (subst x u t)) -> In y (fvs u) \/ In y (fvs t).
+Proof.
+  intros x u t y H. unfold subst in H.
+  apply open_rec_fvs in H. destruct H as [H|H]. left. exact H. right.
+  apply close_rec_fvs in H. exact H.
+Qed.
+
+Print Assumptions fvs_lift.
+Print Assumptions lift_lc.
+Print Assumptions open_rec_occurs_false.
+Print Assumptions close_rec_notin.
+Print Assumptions close_rec_fvs.
+Print Assumptions open_rec_fvs.
+Print Assumptions open_close.
+Print Assumptions subst_fvar_self.
+Print Assumptions subst_fvar_other.
+Print Assumptions subst_fvs.