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

Add more cases

Browse source
This commit is contained in:
Yiyun Liu 2024-12-17 00:41:32 -05:00
parent 45bc061b4d
commit a285b44a46
1 changed files with 16 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
theories/fp_red.v
View file

@ -231,7 +231,17 @@ Proof.
- eauto using RPar.renaming, rtc_l. - eauto using RPar.renaming, rtc_l.
Qed. Qed.
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. Lemma RPars_Abs_inv n (a : Tm (S n)) b :
rtc RPar.R (Abs a) b -> exists a', b = Abs a' /\ rtc RPar.R a a'.
Proof.
move E : (Abs a) => b0 h. move : a E.
elim : b0 b / h.
- hauto lq:on ctrs:rtc.
- hauto lq:on ctrs:rtc inv:RPar.R, rtc.
Qed.
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.
Proof. Proof.
move => h. move : b1. move => h. move : b1.
elim : n a b0 / h. elim : n a b0 / h.
@ -247,8 +257,11 @@ Proof.
exists (Pair c c). split. exists (Pair c c). split.
+ by apply RPars_PairCong. + by apply RPars_PairCong.
+ hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming. + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming.
- admit. (* hauto lq:on ctrs:RPar.R, EPar.R inv:RPar.R. *) - hauto l:on ctrs:rtc inv:RPar.R.
- admit. (* hauto lq:on ctrs:RPar.R, EPar.R inv:RPar.R. *) - move => n a0 a1 h ih b1.
elim /RPar.inv => //= _.
move => a2 a3 ? [*]. subst.
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.