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

Add missing lemma
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful
Details

Browse source
This commit is contained in:
Yiyun Liu 2025-07-10 18:12:37 -04:00
parent 3209c26e03
commit 9992b04e2d
1 changed files with 14 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

18
theories/algorithmic.v
View file

@ -1820,13 +1820,23 @@ Proof.
hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
apply /Sub.FromJoin /DJoin.FromRRed0. by apply HRed.ToRRed.
Qed.
Lemma coqleq_complete_unty Γ (A B : PTm) i :
Γ ⊢ A ∈ PUniv i ->
Γ ⊢ B ∈ PUniv i ->
Sub.R A B ->
A ≪ B.
Proof.
move => h *.
have : salgo_dom_r A B by
hauto lq:on use:fundamental_theorem, logrel.SemWt_SN, sn_algo_dom, algo_dom_salgo_dom.
hauto lq:on use:coqleq_complete'.
Qed.
Lemma coqleq_complete Γ (a b : PTm) :
Γ ⊢ a ≲ b -> a ≪ b.
Proof.
move => h.
have : salgo_dom_r a b /\ Sub.R a b by
hauto lq:on use:fundamental_theorem, logrel.SemLEq_SemWt, logrel.SemWt_SN, sn_algo_dom, algo_dom_salgo_dom.
hauto lq:on use:regularity, coqleq_complete'.
hauto use:coqleq_complete_unty, regularity, logrel.SemLEq_SemWt, fundamental_theorem.
Qed.
Lemma coqleq_sound : forall Γ (a b : PTm) i j,