From 96b3cf2ae75ed767cc26dfa3791523b59baec3c1 Mon Sep 17 00:00:00 2001 From: sneeker Date: Tue, 22 Sep 2026 09:50:00 +0200 Subject: [PATCH] add(binding): locally nameless opening closing lifting and substitution laws (M1 obligations) --- scripts/audit.sh | 24 ++++---- theory/Binding.v | 157 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 170 insertions(+), 11 deletions(-) create mode 100644 theory/Binding.v diff --git a/scripts/audit.sh b/scripts/audit.sh index 2c0c386..a7f6d35 100755 --- a/scripts/audit.sh +++ b/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 -out="$(rocq compile -o /tmp/opencode/audit/ExecReducer.vo theory/ExecReducer.v 2>&1 || true)" -echo "$out" -if echo "$out" | grep -q "Axioms:"; then - echo "unexpected axioms reported" >&2 - fail=1 -fi -if ! echo "$out" | grep -q "Closed under the global context"; then - echo "no Closed-under-global-context report found" >&2 - fail=1 -fi +for f in ExecReducer Binding Reduction; do + echo "-- $f" + out="$(rocq compile -Q theory LambdaSub "theory/$f.v" 2>&1 || true)" + echo "$out" + if echo "$out" | grep -q "Axioms:"; then + echo "unexpected axioms reported in $f" >&2 + fail=1 + fi + if ! echo "$out" | grep -q "Closed under the global context"; then + echo "no Closed-under-global-context report found for $f" >&2 + fail=1 + fi +done if [ "$fail" -ne 0 ]; then echo "AUDIT FAIL" diff --git a/theory/Binding.v b/theory/Binding.v new file mode 100644 index 0000000..7598422 --- /dev/null +++ b/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.