Skip to content

feat: saved propositions #503

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
markusdemedeiros wants to merge 5 commits into
base: master
Choose a base branch
from
+420 −3
Open

feat: saved propositions #503

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
9b75e8a
first draft
markusdemedeiros Jul 7, 2026
322e9cd
pass
markusdemedeiros Jul 8, 2026
1fae385
chore: cleanup
markusdemedeiros Jul 8, 2026
b1a45f6
Merge branch 'master' into savedprop
markusdemedeiros Jul 8, 2026
6d4f0b3
remove aliases to notation
markusdemedeiros Jul 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 10 additions & 3 deletions Iris/Iris/Algebra/Lib/DFracAgree.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ Authors: Markus de Medeiros
-/
module

import Iris.Algebra.DFrac
import Iris.Algebra.Agree
public import Iris.Algebra.DFrac
public import Iris.Algebra.Agree
meta import Iris.Std.RocqPorting

/-!
Expand All @@ -16,6 +16,8 @@ The product of the discardable fraction camera and the agree camera, bundled wit
convenience definitions and lemmas.
-/

@[expose] public section

namespace Iris

open OFE CMRA DFrac
Expand All @@ -32,6 +34,11 @@ variable {A : Type _} [OFE A]

instance instLeibniz [Leibniz A] : Leibniz (DFracAgreeR A) := inferInstance

instance dfrac_agree_mk_discard_coreId {A : Type _} [OFE A] (a : A) :
CoreId (DFracAgree.mk .discard a) := by
show CoreId (DFrac.discard, toAgree a)
infer_instance

@[rocq_alias to_dfrac_agree_ne]
instance mk_ne {d : DFrac} : NonExpansive (mk d : A → DFracAgreeR A) where
ne _ _ _ h := ⟨.rfl, NonExpansive.ne (f := toAgree) h⟩
Expand Down Expand Up @@ -183,7 +190,7 @@ end Frac
/-! ## Functors -/

@[rocq_alias dfrac_agreeRF]
abbrev DFracAgreeRF (T : COFE.OFunctorPre) [RFunctor T] : COFE.OFunctorPre :=
abbrev DFracAgreeRF (T : COFE.OFunctorPre) [COFE.OFunctor T] : COFE.OFunctorPre :=
ProdOF (constOF DFrac) (AgreeRF T)

end DFracAgree
Expand Down
5 changes: 5 additions & 0 deletions Iris/Iris/Algebra/OFE.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1260,6 +1260,11 @@ instance oFunctor_discreteFunOF {C} (F : C → OFunctorPre) [∀ c, OFunctor (F
map_id _ _ := OFunctor.map_id ..
map_comp _ _ _ _ _ _ := OFunctor.map_comp ..

@[rocq_alias discrete_funOF_contractive]
instance oFunctor_discreteFunOF_contractive {C} (F : C → OFunctorPre)
[∀ c, OFunctorContractive (F c)] : OFunctorContractive (DiscreteFunOF F) where
map_contractive.1 h _ _ := OFunctorContractive.map_contractive.distLater_dist h _

end DiscreteFunOF

section Option
Expand Down
22 changes: 22 additions & 0 deletions Iris/Iris/BI/Algebra.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -363,4 +363,26 @@ theorem auth_both_validI (a b : A) :
· exact exists_elim fun c n ⟨hi, hvn⟩ => ⟨DFrac.valid_own_one, ⟨⟨c, hi⟩, hvn⟩⟩

end auth

section dfrac_agree
variable [Sbi PROP] {A : Type _} [OFE A]

open BI

@[rocq_alias dfrac_agree_validI]
theorem dfrac_agree_validI (dq : DFrac) (x : A) :
internalCmraValid (DFracAgree.mk dq x) ⊣⊢@{PROP} ⌜✓ dq⌝ := by
refine (prod_validI (DFracAgree.mk dq x)).trans ⟨?_, ?_⟩
· exact and_elim_l.trans internalCmraValid_discrete.mp
· exact and_intro internalCmraValid_discrete.mpr
(sep_elim_emp_valid_left (toAgree_validI x) sep_elim_left)

@[rocq_alias dfrac_agree_validI_2]
theorem dfrac_agree_validI_2 (dq1 dq2 : DFrac) (x y : A) :
internalCmraValid (DFracAgree.mk dq1 x • DFracAgree.mk dq2 y) ⊣⊢@{PROP}
⌜✓ (dq1 • dq2)⌝ ∧ internalEq x y :=
(prod_validI _).trans (and_congr internalCmraValid_discrete (toAgree_op_validI x y))

end dfrac_agree

end Iris
Loading