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

Add confluence proof for EPar and RPar

Browse source
This commit is contained in:
Yiyun Liu 2024-12-24 00:52:06 -05:00
parent 0407bc7bb9
commit 90b24b259b
1 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
theories/fp_red.v
View file

@ -690,3 +690,26 @@ Lemma RPar_diamond n (c a1 b1 : Tm n) :
RPar.R c b1 -> RPar.R c b1 ->
exists d2, RPar.R a1 d2 /\ RPar.R b1 d2. exists d2, RPar.R a1 d2 /\ RPar.R b1 d2.
Proof. hauto l:on use:RPar_triangle. Qed. Proof. hauto l:on use:RPar_triangle. Qed.
Lemma RPar_confluent n (c a1 b1 : Tm n) :
rtc RPar.R c a1 ->
rtc RPar.R c b1 ->
exists d2, rtc RPar.R a1 d2 /\ rtc RPar.R b1 d2.
Proof.
sfirstorder use:relations.diamond_confluent, RPar_diamond.
Qed.
Lemma EPar_confluent n (c a1 b1 : Tm n) :
rtc EPar.R c a1 ->
rtc EPar.R c b1 ->
exists d2, rtc EPar.R a1 d2 /\ rtc EPar.R b1 d2.
Proof.
sfirstorder use:relations.diamond_confluent, EPar_diamond.
Qed.
Lemma Par_confluent n (c a1 b1 : Tm n) :
rtc Par.R c a1 ->
rtc Par.R c b1 ->
exists d2, rtc Par.R a1 d2 /\ rtc Par.R b1 d2.
Proof.
Admitted.