yiyunliu/pair-eta
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Four cases left for bool

Browse source
This commit is contained in:
Yiyun Liu 2025-01-12 22:45:06 -05:00
parent f68efaf938
commit 5bd998872a
1 changed files with 96 additions and 71 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

167
theories/fp_red.v
View file

@ -1151,6 +1151,22 @@ Module CRRed.
end. end.
Qed. Qed.
Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
R a b -> R (subst_Tm ρ a) (subst_Tm ρ b).
Proof.
move => h. move : m ρ.
elim : n a b /h => n /=;
lazymatch goal with
| [|- context[App (Abs _) _]] => move => * /=; apply AppAbs'; by asimpl
| [|- context[If (BVal _) _]] => hauto l:on use:IfBool
| [|- context[Proj _ (Pair _ _)]] => hauto l:on use:ProjPair
| [|- context[If (Abs _) _]] => move => * /=; apply IfAbs'; by asimpl
| _ => qauto ctrs:R
end.
Qed.
Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
End CRRed. End CRRed.
@ -1205,6 +1221,10 @@ Module CRReds.
induction h; hauto lq:on ctrs:rtc use:CRRed.renaming. induction h; hauto lq:on ctrs:rtc use:CRRed.renaming.
Qed. Qed.
Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
rtc CRRed.R a b -> rtc CRRed.R (subst_Tm ρ a) (subst_Tm ρ b).
Proof. induction 1; hauto lq:on ctrs:rtc use:CRRed.substing. Qed.
End CRReds. End CRReds.
@ -1963,11 +1983,10 @@ Proof.
- sauto lq: on. - sauto lq: on.
Qed. Qed.
Lemma Pair_EPar n (a b c : Tm n) : Lemma Pair_EPar n (a b c : Tm n) :
EPar.R (Pair a b) c -> EPar.R (Pair a b) c ->
(forall p, exists d, rtc RPar.R (Proj p c) d /\ EPar.R (if p is PL then a else b) d) /\ (forall p, exists d, rtc CRRed.R (Proj p c) d /\ EPar.R (if p is PL then a else b) d) /\
(exists d0 d1, rtc RPar.R (App (ren_Tm shift c) (VarTm var_zero)) (exists d0 d1, rtc CRRed.R (App (ren_Tm shift c) (VarTm var_zero))
(Pair (App (ren_Tm shift d0) (VarTm var_zero))(App (ren_Tm shift d1) (VarTm var_zero))) /\ (Pair (App (ren_Tm shift d0) (VarTm var_zero))(App (ren_Tm shift d1) (VarTm var_zero))) /\
EPar.R a d0 /\ EPar.R b d1). EPar.R a d0 /\ EPar.R b d1).
Proof. Proof.
@ -1981,44 +2000,44 @@ Proof.
exists (Abs (App (ren_Tm shift (if p is PL then d0 else d1)) (VarTm var_zero))). exists (Abs (App (ren_Tm shift (if p is PL then d0 else d1)) (VarTm var_zero))).
split. split.
* apply : relations.rtc_transitive. * apply : relations.rtc_transitive.
** apply RPars.ProjCong. apply RPars.AbsCong. eassumption. ** apply CRReds.ProjCong. apply CRReds.AbsCong. eassumption.
** apply : rtc_l. apply RPar.ProjAbs; eauto using RPar.refl. apply RPars.AbsCong. ** apply : rtc_l. apply CRRed.ProjAbs. apply CRReds.AbsCong.
apply : rtc_l. apply RPar.ProjPair; eauto using RPar.refl. apply : rtc_l. apply CRRed.ProjPair.
hauto l:on. hauto l:on.
* hauto lq:on use:EPar.AppEta'. * hauto lq:on use:EPar.AppEta'.
+ exists d0, d1. + exists d0, d1.
repeat split => //. repeat split => //.
apply : rtc_l. apply : RPar.AppAbs'; eauto using RPar.refl => //=. apply : rtc_l. apply : CRRed.AppAbs' => //=.
by asimpl; renamify. by asimpl; renamify.
- move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl). - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl).
split => [p|]. split => [p|].
+ move : iha => [/(_ p) [d [ih0 ih1]] _]. + move : iha => [/(_ p) [d [ih0 ih1]] _].
exists d. split=>//. exists d. split=>//.
apply : rtc_l. apply RPar.ProjPair; eauto using RPar.refl. apply : rtc_l. apply CRRed.ProjPair.
set q := (X in rtc RPar.R X d). set q := (X in rtc CRRed.R X d).
by have -> : q = Proj p a1 by hauto lq:on. by have -> : q = Proj p a1 by hauto lq:on.
+ move :iha => [iha _]. + move :iha => [iha _].
move : (iha PL) => [d0 [ih0 ih0']]. move : (iha PL) => [d0 [ih0 ih0']].
move : (iha PR) => [d1 [ih1 ih1']] {iha}. move : (iha PR) => [d1 [ih1 ih1']] {iha}.
exists d0, d1. exists d0, d1.
apply RPars.weakening in ih0, ih1. apply CRReds.renaming with (ξ := shift) in ih0, ih1.
repeat split => //=. repeat split => //=.
apply : rtc_l. apply RPar.AppPair; eauto using RPar.refl. apply : rtc_l. apply CRRed.AppPair.
apply RPars.PairCong; apply RPars.AppCong; eauto using rtc_refl. apply CRReds.PairCong; apply CRReds.AppCong; eauto using rtc_refl.
- move => n a0 a1 b0 b1 ha _ hb _ a b [*]. subst. - move => n a0 a1 b0 b1 ha _ hb _ a b [*]. subst.
split. split.
+ move => p. + move => p.
exists (if p is PL then a1 else b1). exists (if p is PL then a1 else b1).
split. split.
* apply rtc_once. apply : RPar.ProjPair'; eauto using RPar.refl. * apply rtc_once. apply : CRRed.ProjPair.
* hauto lq:on rew:off. * hauto lq:on rew:off.
+ exists a1, b1. + exists a1, b1.
split. apply rtc_once. apply RPar.AppPair; eauto using RPar.refl. split. apply rtc_once. apply CRRed.AppPair.
split => //. split => //.
Qed. Qed.
Lemma commutativity0 n (a b0 b1 : Tm n) : Lemma commutativity0 n (a b0 b1 : Tm n) :
EPar.R a b0 -> RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c. EPar.R a b0 -> CRRed.R a b1 -> exists c, rtc CRRed.R b0 c /\ EPar.R b1 c.
Proof. Proof.
move => h. move : b1. move => h. move : b1.
elim : n a b0 / h. elim : n a b0 / h.
@ -2027,85 +2046,91 @@ Proof.
move => [c [ih0 ih1]]. move => [c [ih0 ih1]].
exists (Abs (App (ren_Tm shift c) (VarTm var_zero))). exists (Abs (App (ren_Tm shift c) (VarTm var_zero))).
split. split.
+ hauto lq:on ctrs:rtc use:RPars.AbsCong, RPars.AppCong, RPars.renaming. + hauto lq:on ctrs:rtc use:CRReds.AbsCong, CRReds.AppCong, CRReds.renaming.
+ hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming. + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming.
- move => n a b0 hb0 ihb0 b1 /[dup] hb1 {}/ihb0. - move => n a b0 hb0 ihb0 b1 /[dup] hb1 {}/ihb0.
move => [c [ih0 ih1]]. move => [c [ih0 ih1]].
exists (Pair (Proj PL c) (Proj PR c)). split. exists (Pair (Proj PL c) (Proj PR c)). split.
+ apply RPars.PairCong; + apply CRReds.PairCong;
by apply RPars.ProjCong. by apply CRReds.ProjCong.
+ hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming. + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming.
- hauto l:on ctrs:rtc inv:RPar.R. - hauto l:on ctrs:rtc inv:CRRed.R.
- move => n a0 a1 h ih b1. - move => n a0 a1 h ih b1.
elim /RPar.inv => //= _. elim /CRRed.inv => //= _.
move => a2 a3 ? [*]. subst. move => a2 a3 ? [*]. subst.
hauto lq:on ctrs:rtc, RPar.R, EPar.R use:RPars.AbsCong. hauto lq:on ctrs:rtc, CRRed.R, EPar.R use:CRReds.AbsCong.
- move => n a0 a1 b0 b1 ha iha hb ihb b2. - move => n a0 a1 b0 b1 ha iha hb ihb b2.
elim /RPar.inv => //= _. elim /CRRed.inv => //= _.
+ move => a2 a3 b3 b4 h0 h1 [*]. subst. + move => a2 b3 [*]. subst. move {iha ihb}.
move /(_ _ ltac:(by eauto)) : ihb => [b [ihb0 ihb1]]. move /Abs_EPar : ha => [[d [ih1 ih2]] _].
have {}/iha : RPar.R (Abs a2) (Abs a3) by hauto lq:on ctrs:RPar.R. exists (subst_Tm (scons b1 VarTm) d).
move => [c [ih0 /Abs_EPar [[d [ih1 ih2]] _]]].
exists (subst_Tm (scons b VarTm) d).
split. split.
(* By substitution *) (* By substitution *)
* move /RPars.substing : ih2. * move /CRReds.substing : ih2.
move /(_ b). move /(_ _ (scons b1 VarTm)).
asimpl. asimpl.
eauto using relations.rtc_transitive, RPars.AppCong. eauto using relations.rtc_transitive, CRReds.AppCong.
(* By EPar morphing *) (* By EPar morphing *)
* by apply EPar.substing. * by apply EPar.substing.
+ move => a2 a3 b3 b4 c0 c1 h0 h1 h2 [*]. subst. + move => a2 b3 c [*]. subst. move {iha ihb}.
move /(_ _ ltac:(by eauto using RPar.PairCong)) : iha move /Pair_EPar : ha => [_ [d0 [d1 [ih0 [ih1 ih2]]]]].
=> [c [ihc0 ihc1]]. move /CRReds.substing : ih0. move /(_ _ (scons b1 VarTm)).
move /(_ _ ltac:(by eauto)) : ihb => [d [ihd0 ihd1]].
move /Pair_EPar : ihc1 => [_ [d0 [d1 [ih0 [ih1 ih2]]]]].
move /RPars.substing : ih0. move /(_ d).
asimpl => h. asimpl => h.
exists (Pair (App d0 d) (App d1 d)). exists (Pair (App d0 b1) (App d1 b1)).
split. split.
hauto lq:on use:relations.rtc_transitive, RPars.AppCong. hauto lq:on use:@relations.rtc_transitive, CRReds.AppCong.
apply EPar.PairCong; by apply EPar.AppCong. apply EPar.PairCong; by apply EPar.AppCong.
+ case : a0 ha iha => //=. + hauto lq:on ctrs:EPar.R, rtc use:CRReds.AppCong.
move => b ha hc b3 a0 [*]. subst. + move => a2 b3 b4 + [*]. subst.
admit. move /ihb => [b [h0 h1]].
+ hauto lq:on ctrs:EPar.R use:RPars.AppCong. exists (App a1 b).
- hauto lq:on ctrs:EPar.R inv:RPar.R use:RPars.PairCong. hauto q:on ctrs:EPar.R, rtc use:CRReds.AppCong.
- hauto lq:on ctrs:EPar.R, rtc inv:CRRed.R use:CRReds.PairCong.
- move => n p a b0 h0 ih0 b1. - move => n p a b0 h0 ih0 b1.
elim /RPar.inv => //= _. elim /CRRed.inv => //= _.
+ move => ? a0 a1 h [*]. subst. + move => ? a0 [*]. subst. move {ih0}.
move /(_ _ ltac:(by eauto using RPar.AbsCong)) : ih0 => [c [ih0 ih1]]. move /Abs_EPar : h0 => [_ [d [ih1 ih2]]].
move /Abs_EPar : ih1 => [_ [d [ih1 ih2]]].
exists (Abs (Proj p d)). exists (Abs (Proj p d)).
qauto l:on ctrs:EPar.R use:RPars.ProjCong, @relations.rtc_transitive. qauto l:on ctrs:EPar.R use:CRReds.ProjCong, @relations.rtc_transitive.
+ move => p0 a0 a1 b2 b3 h1 h2 [*]. subst. + move => p0 a0 b2 [*]. subst.
move /(_ _ ltac:(by eauto using RPar.PairCong)) : ih0 => [c [ih0 ih1]]. move /Pair_EPar : h0 => [/(_ p)[d [ihd ihd']] _].
move /Pair_EPar : ih1 => [/(_ p)[d [ihd ihd']] _].
exists d. split => //. exists d. split => //.
hauto lq:on use:RPars.ProjCong, relations.rtc_transitive. + hauto lq:on ctrs:EPar.R, rtc use:CRReds.ProjCong.
+ move => p0 b2 [*]. subst. - hauto lq:on inv:CRRed.R ctrs:EPar.R, rtc use:CRReds.BindCong.
admit. - hauto l:on ctrs:EPar.R inv:CRRed.R.
+ hauto lq:on ctrs:EPar.R use:RPars.ProjCong. - hauto l:on ctrs:EPar.R inv:CRRed.R.
- hauto lq:on inv:RPar.R ctrs:EPar.R, rtc use:RPars.BindCong. - hauto l:on ctrs:EPar.R inv:CRRed.R.
- hauto l:on ctrs:EPar.R inv:RPar.R. - hauto l:on ctrs:EPar.R inv:CRRed.R.
- hauto l:on ctrs:EPar.R inv:RPar.R.
- hauto l:on ctrs:EPar.R inv:RPar.R.
- hauto l:on ctrs:EPar.R inv:RPar.R.
- move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc u. - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc u.
elim /RPar.inv => //= _. elim /CRRed.inv => //= _.
+ move => a2 a3 b2 b3 c2 c3 ha2 hb2 hc2 [*]. subst. + move => a2 b2 c [*]{iha ihb ihc}. subst.
move /(_ _ ltac:(by eauto using RPar.AbsCong)) : iha => [c [ih0 ih1]]. move /Abs_EPar_If : ha => [d [h0 h1]].
move /Abs_EPar : ih1 => [[d [ih2 ih3]] _]. move /(_ b1 c1) : h1 => [e [h1 h2]].
have {}/ihb := hb2. move => [b4 [ihb0 ihb1]]. exists e. split => //.
have {}/ihc := hc2. move => [c4 [ihc0 ihc1]]. apply : OExp.merge; eauto.
exists (Abs (If d (ren_Tm shift b4) (ren_Tm shift c4))).
split. admit.
hauto lq:on ctrs:EPar.R use:EPar.renaming. hauto lq:on ctrs:EPar.R use:EPar.renaming.
+ admit. + move => a2 b2 c d [*]. subst.
+ admit. admit.
+ move => a2 b2 c [*]. subst.
admit.
+ (* Need the rule that if commutes with abs *) + (* Need the rule that if commutes with abs *)
admit. admit.
+ move => p a2 b2 c [*]. subst.
move {iha ihb ihc}.
admit.
+ move => a2 a3 b2 c h [*]. subst.
move /iha : h {iha} => [a [ha0 ha1]].
exists (If a b1 c1). split.
hauto lq:on ctrs:rtc use:CRReds.IfCong.
hauto lq:on ctrs:EPar.R.
+ move => a2 b2 b3 c + [*]. subst.
move /ihb => [b [? ?]].
exists (If a1 b c1).
hauto lq:on ctrs:rtc,EPar.R use:CRReds.IfCong.
+ move => a2 b2 c2 c3 + [*]. subst.
move /ihc => {ihc} [c [? ?]].
exists (If a1 b1 c).
hauto lq:on ctrs:rtc,EPar.R use:CRReds.IfCong.
Admitted. Admitted.
Lemma commutativity1 n (a b0 b1 : Tm n) : Lemma commutativity1 n (a b0 b1 : Tm n) :