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

Minor

Browse source
This commit is contained in:
Yiyun Liu 2024-12-21 00:05:42 -05:00
parent ec19e91a47
commit 7e4b0f3e81
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
theories/fp_red.v
View file

@ -311,7 +311,6 @@ Proof.
apply rtc_once. apply : RPar.Proj2Abs; eauto using RPar.refl. apply rtc_once. apply : RPar.Proj2Abs; eauto using RPar.refl.
Qed. Qed.
Lemma commutativity n (a b0 b1 : Tm n) : Lemma commutativity 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 -> RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c.
Proof. Proof.
@ -322,23 +321,26 @@ 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.
+ sfirstorder use:RPars_AbsCong, RPars_AppCong, RPars_renaming. + sfirstorder use:RPars.AbsCong, RPars.AppCong, RPars.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 (Proj1 c) (Proj2 c)). split. exists (Pair (Proj1 c) (Proj2 c)). split.
+ apply RPars_PairCong; admit. + apply RPars.PairCong.
by apply RPars.Proj1Cong.
by apply RPars.Proj2Cong.
+ 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:RPar.R.
- move => n a0 a1 h ih b1. - move => n a0 a1 h ih b1.
elim /RPar.inv => //= _. elim /RPar.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, RPar.R, EPar.R use:RPars.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 /RPar.inv => //= _.
+ move => a2 a3 b3 b4 h0 h1 [*]. subst. + move => a2 a3 b3 b4 h0 h1 [*]. subst.
have {}/iha : RPar.R (Abs a2) (Abs a3) by hauto lq:on ctrs:RPar.R. have {}/iha : RPar.R (Abs a2) (Abs a3) by hauto lq:on ctrs:RPar.R.
move => [c [ih0 ih1]]. move => [c [ih0 /Abs_EPar [ih1 ih2]]].
elim /EPar.inv : ha => //= _. elim /EPar.inv : ha => //= _.
* move => a0 a4 h *. subst. * move => a0 a4 h *. subst.