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

Prove structural properties of DJoin

Browse source
This commit is contained in:
Yiyun Liu 2025-02-03 14:55:31 -05:00
parent 3d42581bbe
commit 84cd0715c7
1 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
theories/fp_red.v
View file

@ -1846,4 +1846,19 @@ Qed.
(* "Declarative" Joinability *) (* "Declarative" Joinability *)
Module DJoin. Module DJoin.
Definition R {n} (a b : PTm n) := exists c, rtc RERed.R a c /\ rtc RERed.R b c. Definition R {n} (a b : PTm n) := exists c, rtc RERed.R a c /\ rtc RERed.R b c.
Lemma refl n (a : PTm n) : R a a.
Proof. sfirstorder use:@rtc_refl unfold:R. Qed.
Lemma symmetric n (a b : PTm n) : R a b -> R b a.
Proof. sfirstorder unfold:R. Qed.
Lemma transitive n (a b c : PTm n) : SN b -> R a b -> R b c -> R a c.
Proof.
rewrite /R.
move => + [ab [ha +]] [bc [+ hc]].
move : rered_confluence; repeat move/[apply].
move => [v [h0 h1]].
exists v. sfirstorder use:@relations.rtc_transitive.
Qed.
End DJoin. End DJoin.