161 lines
5.7 KiB
V
161 lines
5.7 KiB
V
From Stdlib Require Import List Bool Arith Lia PeanoNat.
|
|
Import ListNotations.
|
|
From Stdlib Require Import Wf_nat.
|
|
From LambdaSub Require Import ExecReducer Binding Reduction Metatheory Closure.
|
|
|
|
Inductive red_sub_root : trm -> trm -> Prop :=
|
|
| rs_gc : forall body u, occurs0 body = false -> red_sub_root (ESub body u) body
|
|
| rs_r : forall C body u, zfill C 0 = body ->
|
|
red_sub_root (ESub body u) (ESub (zplug_lift C 0 u) u).
|
|
|
|
Inductive red_sub : trm -> trm -> Prop :=
|
|
| red_sub_base : forall t t', red_sub_root t t' -> red_sub t t'
|
|
| red_sub_ctx : forall C t t', red_sub t t' -> red_sub (plug C t) (plug C t').
|
|
|
|
Lemma red_sub_root_to_red1 : forall t t', red_sub_root t t' -> red1 t t'.
|
|
Proof.
|
|
intros t t' H. destruct H.
|
|
- exists RGc. apply red1r_root. apply rGc. exact H.
|
|
- exists RR. apply red1r_root. apply rR. exact H.
|
|
Qed.
|
|
|
|
Lemma red_sub_to_red1 : forall t t', red_sub t t' -> red1 t t'.
|
|
Proof.
|
|
intros t t' H. induction H.
|
|
- apply red_sub_root_to_red1. exact H.
|
|
- destruct IHred_sub as [r Hr]. exists r. apply rctx. exact Hr.
|
|
Qed.
|
|
|
|
Lemma red_sub_context : forall C t t', red_sub t t' -> red_sub (plug C t) (plug C t').
|
|
Proof. intros. apply red_sub_ctx. exact H. Qed.
|
|
|
|
Lemma red_sub_gc : forall body u, occurs0 body = false -> red_sub (ESub body u) body.
|
|
Proof. intros. apply red_sub_base. apply rs_gc. exact H. Qed.
|
|
|
|
Lemma red_sub_r : forall C body u, zfill C 0 = body ->
|
|
red_sub (ESub body u) (ESub (zplug_lift C 0 u) u).
|
|
Proof. intros. apply red_sub_base. apply rs_r. exact H. Qed.
|
|
|
|
Print Assumptions red_sub_root_to_red1.
|
|
Print Assumptions red_sub_to_red1.
|
|
Print Assumptions red_sub_context.
|
|
|
|
Lemma occurs_zfill : forall C k, occurs k (zfill C k) = true.
|
|
Proof.
|
|
induction C; intros k; simpl.
|
|
- rewrite Nat.eqb_refl. reflexivity.
|
|
- rewrite IHC. reflexivity.
|
|
- rewrite IHC. rewrite orb_true_r. reflexivity.
|
|
- rewrite (IHC (S k)). reflexivity.
|
|
- rewrite (IHC (S k)). reflexivity.
|
|
- rewrite IHC. rewrite orb_true_r. reflexivity.
|
|
Qed.
|
|
|
|
Lemma zfill_occurs0 : forall C body, zfill C 0 = body -> occurs0 body = true.
|
|
Proof. intros C body H. rewrite <- H. apply occurs_zfill. Qed.
|
|
|
|
Lemma R_Gc_disjoint : forall body, occurs0 body = false -> ~ (exists C, zfill C 0 = body).
|
|
Proof.
|
|
intros body Hf [C HC]. apply zfill_occurs0 in HC.
|
|
rewrite Hf in HC. discriminate HC.
|
|
Qed.
|
|
|
|
Print Assumptions occurs_zfill.
|
|
Print Assumptions zfill_occurs0.
|
|
Print Assumptions R_Gc_disjoint.
|
|
|
|
Lemma Star_red_sub_context : forall C t t', Star red_sub t t' -> Star red_sub (plug C t) (plug C t').
|
|
Proof.
|
|
intros C t t' H. induction H.
|
|
- apply star_refl.
|
|
- apply star_step with (u := plug C u).
|
|
+ apply red_sub_context. exact H.
|
|
+ exact IHStar.
|
|
Qed.
|
|
|
|
Lemma full_comp_aux_sub : forall n body u, occurs_count 0 body <= n ->
|
|
Plus red_sub (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. apply red_sub_gc. 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).
|
|
* apply red_sub_r. 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. apply red_sub_gc. exact E.
|
|
Qed.
|
|
|
|
Lemma plus_red_sub_full_comp : forall body u, Plus red_sub (ESub body u) (open_rec 0 u body).
|
|
Proof. intros. apply (full_comp_aux_sub (occurs_count 0 body) body u). lia. Qed.
|
|
|
|
Lemma star_red_sub_full_comp : forall body u, Star red_sub (ESub body u) (open_rec 0 u body).
|
|
Proof. intros. apply Plus_to_Star. apply plus_red_sub_full_comp. Qed.
|
|
|
|
Print Assumptions Star_red_sub_context.
|
|
Print Assumptions plus_red_sub_full_comp.
|
|
Print Assumptions star_red_sub_full_comp.
|
|
|
|
Fixpoint es_count (t : trm) : nat :=
|
|
match t with
|
|
| BVar _ | FVar _ => 0
|
|
| App a b => es_count a + es_count b
|
|
| Lam a => es_count a
|
|
| ESub a b => S (es_count a + es_count b)
|
|
end.
|
|
|
|
Inductive red_gc : trm -> trm -> Prop :=
|
|
| rgc_root : forall body u, occurs0 body = false -> red_gc (ESub body u) body
|
|
| rgc_ctx : forall C t t', red_gc t t' -> red_gc (plug C t) (plug C t').
|
|
|
|
Lemma es_count_plug_mono : forall C t t',
|
|
es_count t' < es_count t -> es_count (plug C t') < es_count (plug C t).
|
|
Proof.
|
|
induction C; intros a b H; simpl.
|
|
- exact H.
|
|
- pose proof (IHC a b H) as IH; lia.
|
|
- pose proof (IHC a b H) as IH; lia.
|
|
- pose proof (IHC a b H) as IH; lia.
|
|
- pose proof (IHC a b H) as IH; lia.
|
|
- pose proof (IHC a b H) as IH; lia.
|
|
Qed.
|
|
|
|
Lemma red_gc_measure : forall a b, red_gc a b -> es_count b < es_count a.
|
|
Proof.
|
|
intros a b H. induction H.
|
|
- simpl. lia.
|
|
- apply es_count_plug_mono. exact IHred_gc.
|
|
Qed.
|
|
|
|
Lemma red_gc_terminates : forall t, Acc (fun x y => red_gc y x) t.
|
|
Proof.
|
|
assert (H : forall n t, es_count t = n -> Acc (fun x y => red_gc y x) t).
|
|
{ intro n. induction n as [n IH] using lt_wf_ind.
|
|
intros t E. constructor. intros y Hy.
|
|
apply (IH (es_count y)).
|
|
- pose proof (red_gc_measure t y Hy). lia.
|
|
- reflexivity. }
|
|
intros t. apply (H (es_count t) t). reflexivity.
|
|
Qed.
|
|
|
|
Lemma red_gc_to_red_sub : forall a b, red_gc a b -> red_sub a b.
|
|
Proof.
|
|
intros a b H. induction H.
|
|
- apply red_sub_gc. exact H.
|
|
- apply red_sub_ctx. exact IHred_gc.
|
|
Qed.
|
|
|
|
Print Assumptions es_count_plug_mono.
|
|
Print Assumptions red_gc_measure.
|
|
Print Assumptions red_gc_terminates.
|
|
Print Assumptions red_gc_to_red_sub.
|