add(metatheory): nonempty reduction closure free variable preservation full composition and beta simulation (M2)
This commit is contained in:
1 file changed
+236
@@ -0,0 +1,236 @@
|
|||||||
|
From Stdlib Require Import List Bool Arith Lia PeanoNat.
|
||||||
|
Import ListNotations.
|
||||||
|
From LambdaSub Require Import ExecReducer Binding Reduction.
|
||||||
|
|
||||||
|
Inductive Plus (R : trm -> trm -> Prop) : trm -> trm -> Prop :=
|
||||||
|
| plus1 : forall t u, R t u -> Plus R t u
|
||||||
|
| plusS : forall t u v, R t u -> Plus R u v -> Plus R t v.
|
||||||
|
|
||||||
|
Lemma Plus_red1_context : forall C a b, Plus red1 a b -> Plus red1 (plug C a) (plug C b).
|
||||||
|
Proof.
|
||||||
|
intros C a b H. induction H.
|
||||||
|
- destruct H as [r Hr]. apply plus1. exists r. apply rctx. exact Hr.
|
||||||
|
- destruct H as [r Hr]. apply plusS with (u := plug C u).
|
||||||
|
+ exists r. apply rctx. exact Hr.
|
||||||
|
+ exact IHPlus.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Fixpoint occurs_count (n : nat) (t : trm) : nat :=
|
||||||
|
match t with
|
||||||
|
| BVar m => if Nat.eqb m n then 1 else 0
|
||||||
|
| FVar _ => 0
|
||||||
|
| App a b => occurs_count n a + occurs_count n b
|
||||||
|
| Lam a => occurs_count (S n) a
|
||||||
|
| ESub a b => occurs_count (S n) a + occurs_count n b
|
||||||
|
end.
|
||||||
|
|
||||||
|
Lemma occurs_count_zero : forall t k, occurs_count k t = 0 -> occurs k t = false.
|
||||||
|
Proof.
|
||||||
|
induction t; intros k H; simpl in *.
|
||||||
|
- destruct (Nat.eqb n k) eqn:E; [discriminate H | reflexivity].
|
||||||
|
- reflexivity.
|
||||||
|
- assert (Ha : occurs_count k t1 = 0) by lia.
|
||||||
|
assert (Hb : occurs_count k t2 = 0) by lia.
|
||||||
|
rewrite (IHt1 k Ha), (IHt2 k Hb). reflexivity.
|
||||||
|
- apply IHt. exact H.
|
||||||
|
- assert (Ha : occurs_count (S k) t1 = 0) by lia.
|
||||||
|
assert (Hb : occurs_count k t2 = 0) by lia.
|
||||||
|
rewrite (IHt1 (S k) Ha), (IHt2 k Hb). reflexivity.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma occurs_count_false : forall t k, occurs k t = false -> occurs_count k t = 0.
|
||||||
|
Proof.
|
||||||
|
induction t; intros k H; simpl in *.
|
||||||
|
- rewrite H. reflexivity.
|
||||||
|
- reflexivity.
|
||||||
|
- apply orb_false_iff in H as [Ha Hb].
|
||||||
|
rewrite (IHt1 k Ha), (IHt2 k Hb). reflexivity.
|
||||||
|
- apply IHt. exact H.
|
||||||
|
- apply orb_false_iff in H as [Ha Hb].
|
||||||
|
rewrite (IHt1 (S k) Ha), (IHt2 k Hb). reflexivity.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma occurs_count_pos : forall t n, occurs n t = true -> occurs_count n t > 0.
|
||||||
|
Proof.
|
||||||
|
intros t n H. destruct (Nat.eq_dec (occurs_count n t) 0) as [Hz|Hnz].
|
||||||
|
- exfalso. apply occurs_count_zero in Hz. rewrite Hz in H. discriminate H.
|
||||||
|
- lia.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma occurs_lift_self : forall t k, occurs k (lift k t) = false.
|
||||||
|
Proof.
|
||||||
|
induction t; intros k; simpl.
|
||||||
|
- destruct (Nat.ltb n k) eqn:E.
|
||||||
|
+ apply Nat.ltb_lt in E. apply Nat.eqb_neq. lia.
|
||||||
|
+ apply Nat.ltb_ge in E. apply Nat.eqb_neq. lia.
|
||||||
|
- reflexivity.
|
||||||
|
- rewrite IHt1, IHt2. reflexivity.
|
||||||
|
- apply IHt.
|
||||||
|
- rewrite IHt1, IHt2. reflexivity.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma zdecs_nonempty : forall t k, occurs k t = true -> exists C, In C (zdecs t k).
|
||||||
|
Proof.
|
||||||
|
induction t; intros k H; simpl in *.
|
||||||
|
- destruct (Nat.eqb n k) eqn:E.
|
||||||
|
+ exists ZTop. simpl. left. reflexivity.
|
||||||
|
+ discriminate H.
|
||||||
|
- discriminate H.
|
||||||
|
- apply orb_true_iff in H as [H|H].
|
||||||
|
+ destruct (IHt1 k H) as [C HC]. exists (ZAppL C t2). simpl.
|
||||||
|
apply in_app_iff. left. apply in_map_iff. exists C. split. reflexivity. exact HC.
|
||||||
|
+ destruct (IHt2 k H) as [C HC]. exists (ZAppR t1 C). simpl.
|
||||||
|
apply in_app_iff. right. apply in_map_iff. exists C. split. reflexivity. exact HC.
|
||||||
|
- destruct (IHt (S k) H) as [C HC]. exists (ZLam C). simpl.
|
||||||
|
apply in_map_iff. exists C. split. reflexivity. exact HC.
|
||||||
|
- apply orb_true_iff in H as [H|H].
|
||||||
|
+ destruct (IHt1 (S k) H) as [C HC]. exists (ZESubL C t2). simpl.
|
||||||
|
apply in_app_iff. left. apply in_map_iff. exists C. split. reflexivity. exact HC.
|
||||||
|
+ destruct (IHt2 k H) as [C HC]. exists (ZESubR t1 C). simpl.
|
||||||
|
apply in_app_iff. right. apply in_map_iff. exists C. split. reflexivity. exact HC.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma occurs_count_zfill_plug : forall C k u,
|
||||||
|
occurs_count k (zfill C k) = S (occurs_count k (zplug_lift C k u)).
|
||||||
|
Proof.
|
||||||
|
induction C; intros k u; simpl.
|
||||||
|
- rewrite Nat.eqb_refl. simpl.
|
||||||
|
rewrite (occurs_count_false (lift k u) k (occurs_lift_self u k)). reflexivity.
|
||||||
|
- rewrite (IHC k u). reflexivity.
|
||||||
|
- rewrite (IHC k u). rewrite Nat.add_succ_r. reflexivity.
|
||||||
|
- rewrite (IHC (S k) u). reflexivity.
|
||||||
|
- rewrite (IHC (S k) u). reflexivity.
|
||||||
|
- rewrite (IHC k u). rewrite Nat.add_succ_r. reflexivity.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma open_rec_zplug_lift : forall C k u,
|
||||||
|
open_rec k u (zplug_lift C k u) = open_rec k u (zfill C k).
|
||||||
|
Proof.
|
||||||
|
induction C; intros k u; simpl.
|
||||||
|
- rewrite (open_rec_occurs_false (lift k u) u k (occurs_lift_self u k)).
|
||||||
|
rewrite Nat.eqb_refl. reflexivity.
|
||||||
|
- rewrite (IHC k u). reflexivity.
|
||||||
|
- rewrite (IHC k u). reflexivity.
|
||||||
|
- rewrite (IHC (S k) u). reflexivity.
|
||||||
|
- rewrite (IHC (S k) u). reflexivity.
|
||||||
|
- rewrite (IHC k u). reflexivity.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma full_comp_aux : forall n body u, occurs_count 0 body <= n ->
|
||||||
|
Plus red1 (ESub body u) (open_rec 0 u body).
|
||||||
|
Proof.
|
||||||
|
induction n as [| n IH]; intros body u Hn.
|
||||||
|
- assert (Hc : occurs_count 0 body = 0) by lia.
|
||||||
|
assert (Ho : occurs0 body = false) by (apply occurs_count_zero; exact Hc).
|
||||||
|
rewrite (open_rec_occurs_false body u 0 Ho).
|
||||||
|
apply plus1. exists RGc. apply red1r_root. apply rGc. exact Ho.
|
||||||
|
- destruct (occurs0 body) eqn:E.
|
||||||
|
+ destruct (zdecs_nonempty body 0 E) as [C HC].
|
||||||
|
assert (Hbody : zfill C 0 = body) by (apply zdecs_sound; exact HC).
|
||||||
|
assert (Hlt : occurs_count 0 (zplug_lift C 0 u) < occurs_count 0 body).
|
||||||
|
{ rewrite <- Hbody. rewrite (occurs_count_zfill_plug C 0 u). lia. }
|
||||||
|
assert (Hle : occurs_count 0 (zplug_lift C 0 u) <= n) by lia.
|
||||||
|
apply plusS with (u := ESub (zplug_lift C 0 u) u).
|
||||||
|
* exists RR. apply red1r_root. apply rR. exact Hbody.
|
||||||
|
* rewrite <- Hbody. rewrite <- (open_rec_zplug_lift C 0 u).
|
||||||
|
apply IH. exact Hle.
|
||||||
|
+ rewrite (open_rec_occurs_false body u 0 E).
|
||||||
|
apply plus1. exists RGc. apply red1r_root. apply rGc. exact E.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma lemma_2_2_full_comp : forall body u, Plus red1 (ESub body u) (open_rec 0 u body).
|
||||||
|
Proof. intros. apply (full_comp_aux (occurs_count 0 body) body u). lia. Qed.
|
||||||
|
|
||||||
|
Lemma fvs_zplug_lift : forall C k u y,
|
||||||
|
In y (fvs (zplug_lift C k u)) -> In y (fvs u) \/ In y (fvs (zfill C k)).
|
||||||
|
Proof.
|
||||||
|
induction C; intros k u y H; simpl in *.
|
||||||
|
- left. rewrite <- (fvs_lift u k). exact H.
|
||||||
|
- apply in_app_iff in H as [H|H].
|
||||||
|
+ destruct (IHC k u y H) as [Hl|Hr]. left; exact Hl.
|
||||||
|
right; apply in_app_iff; left; exact Hr.
|
||||||
|
+ right; apply in_app_iff; right; exact H.
|
||||||
|
- apply in_app_iff in H as [H|H].
|
||||||
|
+ right; apply in_app_iff; left; exact H.
|
||||||
|
+ destruct (IHC k u y H) as [Hl|Hr]. left; exact Hl.
|
||||||
|
right; apply in_app_iff; right; exact Hr.
|
||||||
|
- destruct (IHC (S k) u y H) as [Hl|Hr]. left; exact Hl. right; exact Hr.
|
||||||
|
- apply in_app_iff in H as [H|H].
|
||||||
|
+ destruct (IHC (S k) u y H) as [Hl|Hr]. left; exact Hl.
|
||||||
|
right; apply in_app_iff; left; exact Hr.
|
||||||
|
+ right; apply in_app_iff; right; exact H.
|
||||||
|
- apply in_app_iff in H as [H|H].
|
||||||
|
+ right; apply in_app_iff; left; exact H.
|
||||||
|
+ destruct (IHC k u y H) as [Hl|Hr]. left; exact Hl.
|
||||||
|
right; apply in_app_iff; right; exact Hr.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma plug_fv_mono : forall C a s, incl (fvs a) (fvs s) -> incl (fvs (plug C a)) (fvs (plug C s)).
|
||||||
|
Proof.
|
||||||
|
induction C; intros a s H; unfold incl in *; simpl in *.
|
||||||
|
- apply H.
|
||||||
|
- intros y Hy. apply in_app_iff in Hy as [Hy|Hy].
|
||||||
|
+ apply in_app_iff; left; apply (IHC a s H); exact Hy.
|
||||||
|
+ apply in_app_iff; right; exact Hy.
|
||||||
|
- intros y Hy. apply in_app_iff in Hy as [Hy|Hy].
|
||||||
|
+ apply in_app_iff; left; exact Hy.
|
||||||
|
+ apply in_app_iff; right; apply (IHC a s H); exact Hy.
|
||||||
|
- intros y Hy. apply (IHC a s H); exact Hy.
|
||||||
|
- intros y Hy. apply in_app_iff in Hy as [Hy|Hy].
|
||||||
|
+ apply in_app_iff; left; apply (IHC a s H); exact Hy.
|
||||||
|
+ apply in_app_iff; right; exact Hy.
|
||||||
|
- intros y Hy. apply in_app_iff in Hy as [Hy|Hy].
|
||||||
|
+ apply in_app_iff; left; exact Hy.
|
||||||
|
+ apply in_app_iff; right; apply (IHC a s H); exact Hy.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma red1_root_fv : forall r t t', red1_root r t t' -> incl (fvs t') (fvs t).
|
||||||
|
Proof.
|
||||||
|
intros r t t' HR. destruct HR.
|
||||||
|
- simpl. unfold incl. intros y Hy. exact Hy.
|
||||||
|
- simpl. unfold incl. intros y Hy. apply in_app_iff. left. exact Hy.
|
||||||
|
- simpl. unfold incl. intros y Hy. apply in_app_iff in Hy as [Hy|Hy].
|
||||||
|
+ destruct (fvs_zplug_lift C 0 u y Hy) as [Hu|Hb].
|
||||||
|
* apply in_app_iff. right. exact Hu.
|
||||||
|
* apply in_app_iff. left. rewrite <- H. exact Hb.
|
||||||
|
+ apply in_app_iff. right. exact Hy.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma red1r_fv : forall r a b, red1r r a b -> incl (fvs b) (fvs a).
|
||||||
|
Proof.
|
||||||
|
intros r a b H. induction H.
|
||||||
|
- apply red1_root_fv with (r := r). assumption.
|
||||||
|
- apply plug_fv_mono. assumption.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma lemma_2_1_fv_preserved : forall t t', red1 t t' -> incl (fvs t') (fvs t).
|
||||||
|
Proof. intros t t' [r Hr]. apply red1r_fv with r. exact Hr. Qed.
|
||||||
|
|
||||||
|
Inductive beta1 : trm -> trm -> Prop :=
|
||||||
|
| beta_root : forall body u, beta1 (App (Lam body) u) (open_rec 0 u body)
|
||||||
|
| beta_ctx : forall C t t', beta1 t t' -> beta1 (plug C t) (plug C t').
|
||||||
|
|
||||||
|
Lemma lemma_2_3_beta_sim : forall a b, beta1 a b -> Plus red1 a b.
|
||||||
|
Proof.
|
||||||
|
intros a b H. induction H.
|
||||||
|
- apply plusS with (u := ESub body u).
|
||||||
|
+ exists RB. apply red1r_root. apply rB.
|
||||||
|
+ apply lemma_2_2_full_comp.
|
||||||
|
- apply Plus_red1_context. exact IHbeta1.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Print Assumptions Plus_red1_context.
|
||||||
|
Print Assumptions occurs_count_zero.
|
||||||
|
Print Assumptions occurs_count_false.
|
||||||
|
Print Assumptions occurs_count_pos.
|
||||||
|
Print Assumptions occurs_lift_self.
|
||||||
|
Print Assumptions zdecs_nonempty.
|
||||||
|
Print Assumptions occurs_count_zfill_plug.
|
||||||
|
Print Assumptions open_rec_zplug_lift.
|
||||||
|
Print Assumptions lemma_2_2_full_comp.
|
||||||
|
Print Assumptions fvs_zplug_lift.
|
||||||
|
Print Assumptions plug_fv_mono.
|
||||||
|
Print Assumptions red1_root_fv.
|
||||||
|
Print Assumptions red1r_fv.
|
||||||
|
Print Assumptions lemma_2_1_fv_preserved.
|
||||||
|
Print Assumptions lemma_2_3_beta_sim.
|
||||||
Reference in new issue
Block a user