Prove most of the confluence results for eta reduction
This commit is contained in:
parent
e75d7745fe
commit
34a0c2856e
2 changed files with 137 additions and 5 deletions
|
|
@ -766,6 +766,8 @@ Module ERed.
|
||||||
R B0 B1 ->
|
R B0 B1 ->
|
||||||
R (TBind p A B0) (TBind p A B1).
|
R (TBind p A B0) (TBind p A B1).
|
||||||
|
|
||||||
|
Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
|
||||||
|
|
||||||
Lemma AppEta' n a (u : Tm n) :
|
Lemma AppEta' n a (u : Tm n) :
|
||||||
u = (Abs (App (ren_Tm shift a) (VarTm var_zero))) ->
|
u = (Abs (App (ren_Tm shift a) (VarTm var_zero))) ->
|
||||||
R a u.
|
R a u.
|
||||||
|
|
@ -1764,15 +1766,13 @@ Qed.
|
||||||
Lemma prov_pair n (u : Tm n) a : prov u a <-> prov u (Pair (Proj PL a) (Proj PR a)).
|
Lemma prov_pair n (u : Tm n) a : prov u a <-> prov u (Pair (Proj PL a) (Proj PR a)).
|
||||||
Proof. hauto lq:on inv:prov ctrs:prov. Qed.
|
Proof. hauto lq:on inv:prov ctrs:prov. Qed.
|
||||||
|
|
||||||
Derive Dependent Inversion inv with (forall n (a b : Tm n), ERed.R a b) Sort Prop.
|
|
||||||
|
|
||||||
Lemma prov_ered n (u : Tm n) a b : prov u a -> ERed.R a b -> prov u b.
|
Lemma prov_ered n (u : Tm n) a b : prov u a -> ERed.R a b -> prov u b.
|
||||||
Proof.
|
Proof.
|
||||||
move => h.
|
move => h.
|
||||||
move : b.
|
move : b.
|
||||||
elim : u a / h.
|
elim : u a / h.
|
||||||
- move => p A A0 B B0 hA hB b.
|
- move => p A A0 B B0 hA hB b.
|
||||||
elim /inv => // _.
|
elim /ERed.inv => // _.
|
||||||
+ move => a0 *. subst.
|
+ move => a0 *. subst.
|
||||||
rewrite -prov_lam.
|
rewrite -prov_lam.
|
||||||
by constructor.
|
by constructor.
|
||||||
|
|
@ -1782,7 +1782,7 @@ Proof.
|
||||||
+ qauto l:on ctrs:prov use:@rtc_r, ERed_EPar, EPar_Par.
|
+ qauto l:on ctrs:prov use:@rtc_r, ERed_EPar, EPar_Par.
|
||||||
+ qauto l:on ctrs:prov use:@rtc_r, ERed_EPar, EPar_Par.
|
+ qauto l:on ctrs:prov use:@rtc_r, ERed_EPar, EPar_Par.
|
||||||
- move => h a ha iha b.
|
- move => h a ha iha b.
|
||||||
elim /inv => // _.
|
elim /ERed.inv => // _.
|
||||||
+ move => a0 *. subst.
|
+ move => a0 *. subst.
|
||||||
rewrite -prov_lam.
|
rewrite -prov_lam.
|
||||||
by constructor.
|
by constructor.
|
||||||
|
|
@ -1792,7 +1792,7 @@ Proof.
|
||||||
+ hauto lq:on ctrs:prov use:ERed.substing.
|
+ hauto lq:on ctrs:prov use:ERed.substing.
|
||||||
- hauto lq:on inv:ERed.R, prov ctrs:prov.
|
- hauto lq:on inv:ERed.R, prov ctrs:prov.
|
||||||
- move => h a b ha iha hb ihb b0.
|
- move => h a b ha iha hb ihb b0.
|
||||||
elim /inv => //_.
|
elim /ERed.inv => //_.
|
||||||
+ move => a0 *. subst.
|
+ move => a0 *. subst.
|
||||||
rewrite -prov_lam.
|
rewrite -prov_lam.
|
||||||
by constructor.
|
by constructor.
|
||||||
|
|
|
||||||
|
|
@ -869,3 +869,135 @@ Proof.
|
||||||
eauto using InterpUnivN_back_preservation_star.
|
eauto using InterpUnivN_back_preservation_star.
|
||||||
+ hauto lq:on use:@relations.rtc_r, InterpUniv_back_clos_star.
|
+ hauto lq:on use:@relations.rtc_r, InterpUniv_back_clos_star.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
Lemma ne_nf_preservation n (a b : Tm n) : ERed.R b a -> (ne a -> ne b) /\ (nf a -> nf b).
|
||||||
|
Proof.
|
||||||
|
move => h. elim : n b a /h => //=.
|
||||||
|
- move => n a.
|
||||||
|
split => //=.
|
||||||
|
hauto lqb:on use:ne_nf_ren db:nfne.
|
||||||
|
- hauto lqb:on db:nfne.
|
||||||
|
- hauto lqb:on db:nfne.
|
||||||
|
- hauto lqb:on db:nfne.
|
||||||
|
- hauto lqb:on db:nfne.
|
||||||
|
- hauto lqb:on db:nfne.
|
||||||
|
- hauto lqb:on db:nfne.
|
||||||
|
- hauto lqb:on db:nfne.
|
||||||
|
- hauto lqb:on db:nfne.
|
||||||
|
- hauto lqb:on db:nfne.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Fixpoint size_tm {n} (a : Tm n) :=
|
||||||
|
match a with
|
||||||
|
| VarTm _ => 1
|
||||||
|
| TBind _ A B => 1 + Nat.add (size_tm A) (size_tm B)
|
||||||
|
| Abs a => 1 + size_tm a
|
||||||
|
| App a b => 1 + Nat.add (size_tm a) (size_tm b)
|
||||||
|
| Proj p a => 1 + size_tm a
|
||||||
|
| Pair a b => 1 + Nat.add (size_tm a) (size_tm b)
|
||||||
|
| Bot => 1
|
||||||
|
| Univ _ => 1
|
||||||
|
end.
|
||||||
|
|
||||||
|
Lemma size_tm_ren n m (ξ : fin n -> fin m) a : size_tm (ren_Tm ξ a) = size_tm a.
|
||||||
|
Proof.
|
||||||
|
move : m ξ. elim : n / a => //=; scongruence.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
#[export]Hint Rewrite size_tm_ren : size_tm.
|
||||||
|
|
||||||
|
Lemma size_η_lt n (a b : Tm n) :
|
||||||
|
ERed.R b a ->
|
||||||
|
size_tm b < size_tm a.
|
||||||
|
Proof.
|
||||||
|
move => h. elim : b a / h => //=; hauto l:on rew:db:size_tm.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma ered_local_confluence n (a b c : Tm n) :
|
||||||
|
ERed.R b a ->
|
||||||
|
ERed.R c a ->
|
||||||
|
exists d, rtc ERed.R d b /\ rtc ERed.R d c.
|
||||||
|
Proof.
|
||||||
|
move => h. move : c.
|
||||||
|
elim : n b a / h => n.
|
||||||
|
- move => a c.
|
||||||
|
elim /ERed.inv => //= _.
|
||||||
|
+ move => ? ? [*]. subst.
|
||||||
|
have : subst_Tm (scons Bot VarTm) (ren_Tm shift c) = (subst_Tm (scons Bot VarTm) (ren_Tm shift a))
|
||||||
|
by congruence.
|
||||||
|
asimpl => ?. subst.
|
||||||
|
eauto using rtc_refl.
|
||||||
|
+ move => a0 a1 ha ? [*]. subst.
|
||||||
|
elim /ERed.inv : ha => //= _.
|
||||||
|
* move => a1 a2 b0 ha ? [*]. subst.
|
||||||
|
have [a2 [h0 h1]] : exists a2, ERed.R a2 a /\ a1 = ren_Tm shift a2 by admit. subst.
|
||||||
|
eexists. split; cycle 1.
|
||||||
|
apply : relations.rtc_r; cycle 1.
|
||||||
|
apply ERed.AppEta.
|
||||||
|
apply rtc_refl.
|
||||||
|
eauto using relations.rtc_once.
|
||||||
|
* hauto q:on ctrs:rtc, ERed.R inv:ERed.R.
|
||||||
|
- move => a c ha.
|
||||||
|
elim /ERed.inv : ha => //= _.
|
||||||
|
+ hauto l:on.
|
||||||
|
+ move => a0 a1 b0 ha ? [*]. subst.
|
||||||
|
elim /ERed.inv : ha => //= _.
|
||||||
|
move => p a1 a2 ha ? [*]. subst.
|
||||||
|
exists a1. split. by apply relations.rtc_once.
|
||||||
|
apply : rtc_l. apply ERed.PairEta.
|
||||||
|
apply : rtc_l. apply ERed.PairCong1. eauto using ERed.ProjCong.
|
||||||
|
apply rtc_refl.
|
||||||
|
+ move => a0 b0 b1 ha ? [*]. subst.
|
||||||
|
elim /ERed.inv : ha => //= _ p a0 a1 h ? [*]. subst.
|
||||||
|
exists a0. split; first by apply relations.rtc_once.
|
||||||
|
apply : rtc_l; first by apply ERed.PairEta.
|
||||||
|
apply relations.rtc_once.
|
||||||
|
hauto lq:on ctrs:ERed.R.
|
||||||
|
- move => a0 a1 ha iha c.
|
||||||
|
elim /ERed.inv => //= _.
|
||||||
|
+ move => a2 ? [*]. subst.
|
||||||
|
elim /ERed.inv : ha => //=_.
|
||||||
|
* move => a1 a2 b0 ha ? [*] {iha}. subst.
|
||||||
|
have [a0 [h0 h1]] : exists a0, ERed.R a0 c /\ a1 = ren_Tm shift a0 by admit. subst.
|
||||||
|
exists a0. split; last by apply relations.rtc_once.
|
||||||
|
apply relations.rtc_once. apply ERed.AppEta.
|
||||||
|
* hauto q:on inv:ERed.R.
|
||||||
|
+ hauto l:on use:EReds.AbsCong.
|
||||||
|
- move => a0 a1 b ha iha c.
|
||||||
|
elim /ERed.inv => //= _.
|
||||||
|
+ hauto lq:on ctrs:rtc use:EReds.AppCong.
|
||||||
|
+ hauto lq:on use:@relations.rtc_once ctrs:ERed.R.
|
||||||
|
- move => a b0 b1 hb ihb c.
|
||||||
|
elim /ERed.inv => //=_.
|
||||||
|
+ move => a0 a1 a2 ha ? [*]. subst.
|
||||||
|
move {ihb}. exists (App a0 b0).
|
||||||
|
hauto lq:on use:@relations.rtc_once ctrs:ERed.R.
|
||||||
|
+ hauto lq:on ctrs:rtc use:EReds.AppCong.
|
||||||
|
- move => a0 a1 b ha iha c.
|
||||||
|
elim /ERed.inv => //= _.
|
||||||
|
+ move => ? ?[*]. subst.
|
||||||
|
elim /ERed.inv : ha => //= _ p a1 a2 h ? [*]. subst.
|
||||||
|
exists a1. split; last by apply relations.rtc_once.
|
||||||
|
apply : rtc_l. apply ERed.PairEta.
|
||||||
|
apply relations.rtc_once. hauto lq:on ctrs:ERed.R.
|
||||||
|
+ hauto lq:on ctrs:rtc use:EReds.PairCong.
|
||||||
|
+ hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
|
||||||
|
- move => a b0 b1 hb hc c. elim /ERed.inv => //= _.
|
||||||
|
+ move => ? ? [*]. subst.
|
||||||
|
elim /ERed.inv : hb => //= _ p a0 a1 ha ? [*]. subst.
|
||||||
|
move {hc}.
|
||||||
|
exists a0. split; last by apply relations.rtc_once.
|
||||||
|
apply : rtc_l; first by apply ERed.PairEta.
|
||||||
|
hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
|
||||||
|
+ hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
|
||||||
|
+ hauto lq:on ctrs:rtc use:EReds.PairCong.
|
||||||
|
- qauto l:on inv:ERed.R use:EReds.ProjCong.
|
||||||
|
- move => p A0 A1 B hA ihA.
|
||||||
|
move => c. elim/ERed.inv => //=.
|
||||||
|
+ hauto lq:on ctrs:rtc use:EReds.BindCong.
|
||||||
|
+ hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
|
||||||
|
- move => p A B0 B1 hB ihB c.
|
||||||
|
elim /ERed.inv => //=.
|
||||||
|
+ hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
|
||||||
|
+ hauto lq:on ctrs:rtc use:EReds.BindCong.
|
||||||
|
Admitted.
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue