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

Finish full commutativity

Browse source
This commit is contained in:
Yiyun Liu 2024-12-22 15:44:48 -05:00
parent 4599c1d65d
commit 6daef9c807
1 changed files with 20 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
theories/fp_red.v
View file

@ -417,7 +417,7 @@ Proof.
split => //. split => //.
Qed. Qed.
Lemma commutativity 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 -> 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.
@ -483,6 +483,25 @@ Proof.
+ hauto lq:on ctrs:EPar.R use:RPars.ProjCong. + hauto lq:on ctrs:EPar.R use:RPars.ProjCong.
Qed. Qed.
Lemma commutativity1 n (a b0 b1 : Tm n) :
EPar.R a b0 -> rtc RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c.
Proof.
move => + h. move : b0.
elim : a b1 / h.
- sfirstorder.
- qauto l:on use:relations.rtc_transitive, commutativity0.
Qed.
Lemma commutativity n (a b0 b1 : Tm n) :
rtc EPar.R a b0 -> rtc RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ rtc EPar.R b1 c.
move => h. move : b1. elim : a b0 /h.
- sfirstorder.
- move => a0 a1 a2 + ha1 ih b1 +.
move : commutativity1; repeat move/[apply].
hauto q:on ctrs:rtc.
Qed.
Lemma EPar_Par n (a b : Tm n) : EPar.R a b -> Par.R a b. Lemma EPar_Par n (a b : Tm n) : EPar.R a b -> Par.R a b.
Proof. induction 1; hauto lq:on ctrs:Par.R. Qed. Proof. induction 1; hauto lq:on ctrs:Par.R. Qed.