add(binding): locally nameless opening closing lifting and substitution laws (M1 obligations)
This commit is contained in:
2 files changed
+168
-9
No files matched your search
+11
-9
@@ -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
|
||||
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" >&2
|
||||
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
|
||||
fi
|
||||
done
|
||||
|
||||
if [ "$fail" -ne 0 ]; then
|
||||
echo "AUDIT FAIL"
|
||||
|
||||
@@ -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.
|
||||
Reference in new issue
Block a user