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

Add stub for par compile

Browse source
This commit is contained in:
Yiyun Liu 2025-01-20 16:49:47 -05:00
parent 9c9ce52b63
commit 7850314935
2 changed files with 16 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
theories/compile.v
View file

@ -66,6 +66,18 @@ Module Join.
Lemma UnivInj n i j : R (Univ i : Tm n) (Univ j) -> i = j. Lemma UnivInj n i j : R (Univ i : Tm n) (Univ j) -> i = j.
Proof. hauto l:on use:join_univ_inj. Qed. Proof. hauto l:on use:join_univ_inj. Qed.
Lemma transitive n (a b c : Tm n) :
R a b -> R b c -> R a c.
Proof. hauto l:on use:join_transitive unfold:R. Qed.
Lemma symmetric n (a b : Tm n) :
R a b -> R b a.
Proof. hauto l:on use:join_symmetric. Qed.
Lemma reflexive n (a : Tm n) :
R a a.
Proof. hauto l:on use:join_refl. Qed.
End Join. End Join.
Module Equiv. Module Equiv.
@ -135,3 +147,6 @@ Module EquivJoin.
- hauto l:on. - hauto l:on.
Qed. Qed.
End EquivJoin. End EquivJoin.
Module CompilePar.
End CompilePar.

2
theories/logrel.v
View file

@ -344,7 +344,7 @@ Proof.
sfirstorder. sfirstorder.
Qed. Qed.
#[export]Hint Resolve join_univ_ne_contra join_bind_ne_contra join_univ_pi_contra join_symmetric join_transitive : join. #[export]Hint Resolve join_univ_ne_contra join_bind_ne_contra join_univ_pi_contra Join.symmetric Join.transitive : join.
Lemma InterpExt_Join n i I (A B : Tm n) PA PB : Lemma InterpExt_Join n i I (A B : Tm n) PA PB :
⟦ A ⟧ i ;; I ↘ PA -> ⟦ A ⟧ i ;; I ↘ PA ->