From e14416646ada0ce9033c8aae7efe8014b414bf05 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 15 Jul 2026 10:34:33 +0200 Subject: [PATCH 01/11] Deprecate `Reflexive` and `Transitive` in `Std/Classes.lean` --- Iris/Iris/BI/Algebra.lean | 2 +- Iris/Iris/BI/BI.lean | 6 ++-- Iris/Iris/BI/DerivedLaws.lean | 2 +- Iris/Iris/BI/MonPred.lean | 36 ++++++++++----------- Iris/Iris/BI/SIProp.lean | 2 +- Iris/Iris/Instances/Classical/Instance.lean | 2 +- Iris/Iris/Instances/UPred/Instance.lean | 6 ++-- Iris/Iris/ProofMode/Instances.lean | 2 +- Iris/Iris/ProofMode/Tactics/Combine.lean | 4 +-- Iris/Iris/Std/Classes.lean | 13 +------- Iris/Iris/Std/PartialMap.lean | 7 ++-- Iris/Iris/Std/Rewrite.lean | 2 +- 12 files changed, 37 insertions(+), 47 deletions(-) diff --git a/Iris/Iris/BI/Algebra.lean b/Iris/Iris/BI/Algebra.lean index 32fb70df9..b456c13ab 100644 --- a/Iris/Iris/BI/Algebra.lean +++ b/Iris/Iris/BI/Algebra.lean @@ -270,7 +270,7 @@ theorem agree_includedI (x y : Agree A) : · refine siPure_mono (exists_elim (fun c => ?_)) exact (fun n Heq => (includedN.mp ⟨c, Heq⟩).trans op_commN) · refine siPure_mono (exists_intro_trans y ?_) - exact entails_preorder.refl + rfl @[rocq_alias to_agree_includedI] theorem toAgree_includedI (a b : A) : diff --git a/Iris/Iris/BI/BI.lean b/Iris/Iris/BI/BI.lean index 7b83c8ddc..cce3d4146 100644 --- a/Iris/Iris/BI/BI.lean +++ b/Iris/Iris/BI/BI.lean @@ -82,12 +82,12 @@ class BI (PROP : Type _) extends COFE PROP, BI.BIBase PROP where namespace BI -attribute [instance] BI.entails_preorder +attribute [reducible,instance] BI.entails_preorder theorem BIBase.Entails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q) (h2 : Q ⊢ R) : P ⊢ R := - Transitive.trans h1 h2 + Trans.trans h1 h2 -@[simp] theorem BIBase.Entails.rfl [BI PROP] {P : PROP} : P ⊢ P := refl +@[simp,refl] theorem BIBase.Entails.rfl [BI PROP] {P : PROP} : P ⊢ P := Std.Refl.refl P theorem BIBase.Entails.of_eq [BI PROP] {P Q : PROP} (h : P = Q) : P ⊢ Q := h ▸ .rfl diff --git a/Iris/Iris/BI/DerivedLaws.lean b/Iris/Iris/BI/DerivedLaws.lean index 2e71ef58c..cbd16c00a 100644 --- a/Iris/Iris/BI/DerivedLaws.lean +++ b/Iris/Iris/BI/DerivedLaws.lean @@ -2026,7 +2026,7 @@ theorem intuitionisticallyIf_sep {p : Bool} [BI PROP] [BIPositive PROP] {P Q : P theorem intuitionisticallyIf_sep_conj {p1 p2 : Bool} [BI PROP] {P Q : PROP} : (□?p1 P ∗ □?p2 Q) ⊢ □?(p1 && p2) (P ∗ Q) := match p1, p2 with - | false, false => refl + | false, false => by rfl | false, true => sep_mono_right intuitionisticallyIf_elim | true, false => sep_mono_left intuitionisticallyIf_elim | true, true => intuitionisticallyIf_sep_mpr diff --git a/Iris/Iris/BI/MonPred.lean b/Iris/Iris/BI/MonPred.lean index 67e825cdb..ab70217b1 100644 --- a/Iris/Iris/BI/MonPred.lean +++ b/Iris/Iris/BI/MonPred.lean @@ -219,7 +219,7 @@ def imp (P Q : MonPred I PROP) : MonPred I PROP where monPred_at := MonPred.upclosed (fun i => iprop(P.monPred_at i → Q.monPred_at i)) monPred_mono h := forall_intro fun k => (forall_elim k).trans - (imp_mono_left (pure_mono fun hjk => Transitive.trans h hjk)) + (imp_mono_left (pure_mono fun hjk => Trans.trans h hjk)) #rocq_ignore monPred_defs.monPred_impl_def "Rocq unsealed definition body; use MonPred.imp." #rocq_ignore monPred_defs.monPred_impl_aux "Rocq sealing auxiliary definition." @@ -279,7 +279,7 @@ def wand (P Q : MonPred I PROP) : MonPred I PROP where monPred_at := MonPred.upclosed (fun i => iprop(P.monPred_at i -∗ Q.monPred_at i)) monPred_mono h := forall_intro fun k => (forall_elim k).trans - (imp_mono_left (pure_mono fun hjk => Transitive.trans h hjk)) + (imp_mono_left (pure_mono fun hjk => Trans.trans h hjk)) #rocq_ignore monPred_defs.monPred_wand_def "Rocq unsealed definition body; use MonPred.wand." #rocq_ignore monPred_defs.monPred_wand_aux "Rocq sealing auxiliary definition." @@ -310,7 +310,7 @@ def later (P : MonPred I PROP) : MonPred I PROP where @[rocq_alias monPred_defs.monPred_in] def monPred_in (j : I.car) : MonPred I PROP where monPred_at i := iprop(⌜I.rel j i⌝) - monPred_mono h := pure_mono fun hji => Transitive.trans hji h + monPred_mono h := pure_mono fun hji => Trans.trans hji h #rocq_ignore monPred_defs.monPred_in_def "Rocq unsealed definition body; use MonPred.monPred_in." #rocq_ignore monPred_defs.monPred_in_aux "Rocq sealing auxiliary definition." @@ -393,7 +393,7 @@ mixins, packaged into `monPredI : bi`). -/ @[rocq_alias monPredI] instance : BI (MonPred I PROP) where entails_preorder := - { refl := entails_at.mpr fun _ => BIBase.Entails.rfl + { refl _ := entails_at.mpr fun _ => BIBase.Entails.rfl trans := fun h h' => entails_at.mpr fun i => (entails_at.mp h i).trans (entails_at.mp h' i) } equiv_iff := fun {P Q} => ⟨fun h => ⟨entails_at.mpr fun i => (equiv_iff.mp (equiv_at.mp h i)).mp, @@ -435,7 +435,7 @@ instance : BI (MonPred I PROP) where (P.monPred_mono hij).trans <| imp_intro (entails_at.mp h j) imp_elim {P Q R} h := entails_at.mpr fun i => imp_elim <| (entails_at.mp h i).trans <| - (forall_elim i).trans <| pure_imp_elim (Reflexive.refl : I.rel i i) + (forall_elim i).trans <| pure_imp_elim (Std.Refl.refl i : I.rel i i) sForall_intro h := entails_at.mpr fun i => MonPred.sForall_at_intro i fun q hΨ => entails_at.mp (h q hΨ) i sForall_elim h := entails_at.mpr fun i => MonPred.sForall_at_elim i h @@ -453,7 +453,7 @@ instance : BI (MonPred I PROP) where exact (sep_mono_right (P.monPred_mono hij)).trans (sep_symm.trans (entails_at.mp h j)) wand_elim {P Q R} h := entails_at.mpr fun i => (sep_mono_left ((entails_at.mp h i).trans - ((forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i))))).trans wand_elim_left + ((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i))))).trans wand_elim_left persistently_mono h := entails_at.mpr fun i => persistently_mono (entails_at.mp h i) persistently_idem_2 := entails_at.mpr fun i => persistently_idem_2 persistently_emp_2 := entails_at.mpr fun i => persistently_emp_2 @@ -477,7 +477,7 @@ instance : BI (MonPred I PROP) where refine (MonPred.sForall_at_elim (q := MonPred.imp (MonPred.pure (Φ r)) (MonPred.later r)) i ⟨r, rfl⟩).trans ?_ refine (forall_elim i).trans ?_ - exact (pure_imp_elim (Reflexive.refl : I.rel i i)).trans (pure_imp_elim hΦ) + exact (pure_imp_elim (Std.Refl.refl i : I.rel i i)).trans (pure_imp_elim hΦ) later_sExists_false := fun {Φ} => entails_at.mpr fun i => by refine later_sExists_false.trans (or_mono BIBase.Entails.rfl ?_) refine exists_elim fun p => pure_elim_left fun ⟨q, hΦ, hq⟩ => ?_ @@ -518,14 +518,14 @@ instance : BiEmbed PROP (MonPred I PROP) where emp_valid_inj _ h := entails_at.mp h (Inhabited.default : I.car) emp_2 := entails_at.mpr fun _ => .rfl impl_2 _ _ := entails_at.mpr fun i => - (forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i)) + (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i)) forall_2 := fun _Ψ {_} h => entails_at.mpr fun i => sForall_intro fun P hΨ => entails_at.mp (h P hΨ) i exist_1 := fun _Ψ {_} h => entails_at.mpr fun i => sExists_elim fun P hΨ => entails_at.mp (h P hΨ) i sep _ _ := BIBase.BiEntails.of_eq rfl wand_2 _ _ := entails_at.mpr fun i => - (forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i)) + (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i)) persistently _ := BIBase.BiEntails.of_eq rfl #rocq_ignore monPred_embedding_mixin "Rocq mixin record; subsumed by the BiEmbed instance." @@ -627,7 +627,7 @@ instance [BIFUpdate PROP] : BIFUpdate (MonPred I PROP) where trans := entails_at.mpr fun _ => BIFUpdate.trans mask_frame_right_strong h := entails_at.mpr fun i => (BIFUpdate.mono - (((forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i))) : _ ⊢@{PROP} _)).trans + (((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i))) : _ ⊢@{PROP} _)).trans (BIFUpdate.mask_frame_right_strong h) frame_right := entails_at.mpr fun _ => fupd_frame_right @@ -849,12 +849,12 @@ instance monPred_affine (P : MonPred I PROP) [∀ i, Affine (P.monPred_at i)] : @[rocq_alias monPred_impl_force] theorem monPred_impl_force (i : I.car) (P Q : MonPred I PROP) : (iprop(P → Q) : MonPred I PROP).monPred_at i ⊢ iprop(P.monPred_at i → Q.monPred_at i) := - (forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i)) + (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i)) @[rocq_alias monPred_wand_force] theorem monPred_wand_force (i : I.car) (P Q : MonPred I PROP) : (iprop(P -∗ Q) : MonPred I PROP).monPred_at i ⊢ iprop(P.monPred_at i -∗ Q.monPred_at i) := - (forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i)) + (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i)) /-! ### The `monPred_in` assertion -/ @@ -862,7 +862,7 @@ theorem monPred_wand_force (i : I.car) (P Q : MonPred I PROP) : theorem monPred_in_intro (P : MonPred I PROP) : P ⊢ iprop(∃ i, MonPred.monPred_in i ∧ ⎡P.monPred_at i⎤) := entails_at.mpr fun j => - (and_intro (pure_intro (Reflexive.refl : I.rel j j)) .rfl).trans <| + (and_intro (pure_intro (Std.Refl.refl j : I.rel j j)) .rfl).trans <| (exists_intro (Ψ := fun i => (iprop(MonPred.monPred_in i ∧ ⎡P.monPred_at i⎤) : MonPred I PROP).monPred_at j) j).trans (monPred_at_exist j fun i => iprop(MonPred.monPred_in i ∧ ⎡P.monPred_at i⎤)).mpr @@ -873,12 +873,12 @@ theorem monPred_in_elim (P : MonPred I PROP) (i : I.car) : entails_at.mpr fun j => pure_elim (I.rel i j) .rfl fun hij => forall_intro fun _k => imp_intro_swap <| pure_elim_left fun hjk => - imp_intro <| and_elim_r.trans (P.monPred_mono (Transitive.trans hij hjk)) + imp_intro <| and_elim_r.trans (P.monPred_mono (Trans.trans hij hjk)) @[rocq_alias monPred_in_mono] theorem monPred_in_mono {i j : I.car} (h : I.rel j i) : (MonPred.monPred_in i : MonPred I PROP) ⊢ MonPred.monPred_in j := - entails_at.mpr fun _ => pure_mono fun hik => Transitive.trans h hik + entails_at.mpr fun _ => pure_mono fun hik => Trans.trans h hik #rocq_ignore monPred_in_proper "Use monPred_in_mono." @@ -944,7 +944,7 @@ instance impl_objective (P Q : MonPred I PROP) [Objective P] [Objective Q] : Objective (iprop(P → Q)) where objective_at i _j := forall_intro fun k => imp_intro <| and_elim_l.trans <| - (((forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i))) : _ ⊢@{PROP} _).trans <| + (((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i))) : _ ⊢@{PROP} _).trans <| imp_mono (Objective.objective_at k i) (Objective.objective_at i k) @[rocq_alias wand_objective] @@ -952,7 +952,7 @@ instance wand_objective (P Q : MonPred I PROP) [Objective P] [Objective Q] : Objective (iprop(P -∗ Q)) where objective_at i _j := forall_intro fun k => imp_intro <| and_elim_l.trans <| - (((forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i))) : _ ⊢@{PROP} _).trans <| + (((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i))) : _ ⊢@{PROP} _).trans <| wand_mono (Objective.objective_at k i) (Objective.objective_at i k) @[rocq_alias forall_objective] @@ -1449,7 +1449,7 @@ instance instSbiMonPred : Sbi (MonPred I PROP) where monPred_impl_force i (iprop(⌜Ψi q⌝)) (SiPure.siPure q : MonPred I PROP) persistently_imp_siPure {P Q} := entails_at.mpr fun i => by refine (forall_elim i).trans ?_ - refine (pure_imp_elim (Reflexive.refl : I.rel i i)).trans ?_ + refine (pure_imp_elim (Std.Refl.refl i : I.rel i i)).trans ?_ refine persistently_imp_siPure.trans (persistently_mono ?_) refine forall_intro fun j => imp_intro <| pure_elim_right fun (hij : I.rel i j) => ?_ exact imp_mono_right (Q.monPred_mono hij) diff --git a/Iris/Iris/BI/SIProp.lean b/Iris/Iris/BI/SIProp.lean index 219bc52fb..779175924 100644 --- a/Iris/Iris/BI/SIProp.lean +++ b/Iris/Iris/BI/SIProp.lean @@ -154,7 +154,7 @@ instance : BIBase SiProp where #rocq_ignore siProp_persistently "Included in BIBase instance." instance : Std.Preorder (BIBase.Entails (PROP := SiProp)) where - refl _ h := h + refl _ _ := id trans h₁ h₂ n h := h₂ n (h₁ n h) /-! ## BI instance -/ diff --git a/Iris/Iris/Instances/Classical/Instance.lean b/Iris/Iris/Instances/Classical/Instance.lean index df8272d39..340187d4f 100644 --- a/Iris/Iris/Instances/Classical/Instance.lean +++ b/Iris/Iris/Instances/Classical/Instance.lean @@ -49,7 +49,7 @@ instance : COFE (HeapProp Val) := COFE.ofDiscrete _ instance : BI (HeapProp Val) where entails_preorder := by infer_instance equiv_iff {P Q} := ⟨ - fun h => h.to_eq ▸ ⟨refl, refl⟩, + fun h => h.to_eq ▸ ⟨Std.Refl.refl P, Std.Refl.refl P⟩, fun ⟨h₁, h₂⟩ => OFE.Equiv.of_eq (funext fun σ => propext ⟨h₁ σ, h₂ σ⟩) ⟩ diff --git a/Iris/Iris/Instances/UPred/Instance.lean b/Iris/Iris/Instances/UPred/Instance.lean index 3e63dc321..fa683255f 100644 --- a/Iris/Iris/Instances/UPred/Instance.lean +++ b/Iris/Iris/Instances/UPred/Instance.lean @@ -267,7 +267,7 @@ instance : BIBase (UPred M) where @[rocq_alias uPred_primitive.entails_po] instance uPred_entails_preorder : Std.Preorder (Entails (PROP := UPred M)) where - refl _ _ H := H + refl _ _ _ H := H trans H1 H2 _ _ Hv := H2 _ _ <| H1 _ _ Hv @[rocq_alias uPred_primitive.entails_lim] @@ -386,8 +386,8 @@ instance : BI (UPred M) where refine P.mono H ?_ .refl refine (incN_iff_right ?_).mpr (incN_refl _) exact (core_idem x.val).dist - persistently_emp_2 := Std.refl - persistently_and_2 := Std.refl + persistently_emp_2 := Std.Refl.refl emp + persistently_and_2 {P Q} := Std.Refl.refl iprop( P ∧ Q) persistently_sExists_1 _ _ := fun ⟨p, HΨ, H⟩ => by refine ⟨iprop( p), ⟨p, ?_⟩, H⟩ ext; exact and_iff_right HΨ diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean index 8ebc6aa25..58b286133 100644 --- a/Iris/Iris/ProofMode/Instances.lean +++ b/Iris/Iris/ProofMode/Instances.lean @@ -860,7 +860,7 @@ instance elimModal_absorbingly_here [BI PROP] p (P Q : PROP) [Absorbing Q] : @[rocq_alias maybe_combine_sep_as_default] instance (priority := default - 20) combineSepAs_default [BI PROP] (P Q : PROP) : CombineSepAs P Q iprop(P ∗ Q) where - combine_sep_as := refl + combine_sep_as := by rfl @[rocq_alias maybe_combine_sep_as_affinely] instance combineSepAs_affinely [BI PROP] (Q1 Q2 P : PROP) diff --git a/Iris/Iris/ProofMode/Tactics/Combine.lean b/Iris/Iris/ProofMode/Tactics/Combine.lean index 1b5cca40b..132b1d05c 100644 --- a/Iris/Iris/ProofMode/Tactics/Combine.lean +++ b/Iris/Iris/ProofMode/Tactics/Combine.lean @@ -47,7 +47,7 @@ theorem combine_gives_step [BI PROP] {p1 p2 : Bool} {e e1 e2 out1 out2 out : PRO _ ⊢ (e2 ∗ □?p2 out2) ∗ □?p1 out1 := sep_mono_left pf2.mp _ ⊢ e2 ∗ □?p2 out2 ∗ □?p1 out1 := sep_assoc.mp _ ⊢ e2 ∗ □?p1 out1 ∗ □?p2 out2 := sep_mono_right sep_comm.mp - _ ⊢ (e2 ∗ □?p1 out1 ∗ □?p2 out2) ∧ (e2 ∗ out) := and_intro refl <| sep_mono_right pf3 + _ ⊢ (e2 ∗ □?p1 out1 ∗ □?p2 out2) ∧ (e2 ∗ out) := and_intro .rfl <| sep_mono_right pf3 _ ⊢ (e2 ∗ □?p1 out1 ∗ □?p2 out2) ∧ out := and_mono_right sep_elim_right _ ⊢ (e2 ∗ □?p1 out1 ∗ □?p2 out2) ∗ □ out := persistently_and_intuitionistically_sep_right.mp _ ⊢ (e2 ∗ □?p2 out2 ∗ □?p1 out1) ∗ □ out := sep_mono_left <| sep_mono_right sep_comm.mp @@ -77,7 +77,7 @@ theorem combine_gives_step_conj [BI PROP] {p1 p2 : Bool} _ ⊢ newOutGives := persistently_absorb_right calc _ ⊢ e ∗ □ outGives := pf1 - _ ⊢ (e ∗ □ outGives) ∧ outGives ∧ newOutGives := and_intro refl <| and_intro pf4 pf5 + _ ⊢ (e ∗ □ outGives) ∧ outGives ∧ newOutGives := and_intro .rfl <| and_intro pf4 pf5 _ ⊢ (e ∗ □ outGives) ∧ (outGives ∧ newOutGives) := and_mono_right <| persistently_and.mpr _ ⊢ (e ∗ □ outGives) ∧ outGivesCombined := and_mono_right <| persistently_mono instGivesCombined.make_and.mp _ ⊢ (e ∗ □ outGives) ∗ □ outGivesCombined := persistently_and_intuitionistically_sep_right.mp diff --git a/Iris/Iris/Std/Classes.lean b/Iris/Iris/Std/Classes.lean index 3b147de3c..d286b97ff 100644 --- a/Iris/Iris/Std/Classes.lean +++ b/Iris/Iris/Std/Classes.lean @@ -19,19 +19,8 @@ export Top (top) notation "⊤" => top -/-- Require that a relation `R` on `a` is reflexive. -/ -class Reflexive (R : Relation α) where - refl {x : α} : R x x -export Reflexive (refl) - -/-- Require that a relation `R` on `α` is transitive. -/ -class Transitive (R : Relation α) where - trans {x y z : α} : R x y → R y z → R x z -export Transitive (trans) - /-- Require that a relation `R` on `α` is a preorder, i.e. that it is reflexive and transitive. -/ -class Preorder (R : Relation α) extends Reflexive R, Transitive R - +class Preorder (R : Relation α) extends Std.Refl R, Trans R R R /-- Require that a binary function `f` on `α` is idempotent in a relation `R` on `α`. -/ class Idempotent (R : Relation α) (f : α → α → α) where diff --git a/Iris/Iris/Std/PartialMap.lean b/Iris/Iris/Std/PartialMap.lean index 221a25664..8f8ef2359 100644 --- a/Iris/Iris/Std/PartialMap.lean +++ b/Iris/Iris/Std/PartialMap.lean @@ -8,7 +8,6 @@ module import Batteries.Data.List.Perm import Iris.Std.FromMathlib public import Iris.Std.GenSets -public import Iris.Std.GenSets /-! ## Partial Maps @@ -158,9 +157,11 @@ instance : SDiff (M V) := ⟨difference⟩ /-- Two PartialMaps are pointwise equivalent. -/ @[simp] def equiv (m1 m2 : M V) : Prop := ∀ k, get? m1 k = get? m2 k -theorem equiv.refl : ∀ {a : M V}, equiv a a := by simp only [equiv, implies_true] +@[simp,refl] +theorem equiv.refl : ∀ a : M V, equiv a a := by simp only [equiv, implies_true] -instance instEquivRefl : Reflexive (@equiv K V M _) := ⟨equiv.refl⟩ +instance instEquivRefl : Std.Refl (@equiv K V M _) where + refl := equiv.refl theorem equiv.trans : ∀ {a b c : M V}, equiv a b → equiv b c → equiv a c := by simp_all diff --git a/Iris/Iris/Std/Rewrite.lean b/Iris/Iris/Std/Rewrite.lean index 25d2794a2..992930a03 100644 --- a/Iris/Iris/Std/Rewrite.lean +++ b/Iris/Iris/Std/Rewrite.lean @@ -135,7 +135,7 @@ where applyReflexivity (goal : MVarId) : TacticM Unit := do try - discard <| apply' goal ``refl + discard <| apply' goal ``Std.Refl.refl catch _ => pure () go (goal : MVarId) (rule : TSyntax `term) : TacticM Bool := do From 69302f391dddaa465ba643e1067e0651535bc8e1 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 15 Jul 2026 11:44:46 +0200 Subject: [PATCH 02/11] Replace the custom `Preorder` type class with `Std.Preorder` --- Iris/Iris/BI/BI.lean | 13 ++-- Iris/Iris/BI/BIBase.lean | 6 +- Iris/Iris/BI/DerivedLaws.lean | 2 +- Iris/Iris/BI/MonPred.lean | 83 +++++++++++---------- Iris/Iris/BI/SIProp.lean | 8 +- Iris/Iris/Instances/Classical/Instance.lean | 12 ++- Iris/Iris/Instances/UPred/Instance.lean | 12 +-- Iris/Iris/Std/Classes.lean | 3 - 8 files changed, 71 insertions(+), 68 deletions(-) diff --git a/Iris/Iris/BI/BI.lean b/Iris/Iris/BI/BI.lean index cce3d4146..cab742eb0 100644 --- a/Iris/Iris/BI/BI.lean +++ b/Iris/Iris/BI/BI.lean @@ -22,7 +22,7 @@ theorem liftRel_eq : liftRel (@Eq α) A B ↔ A = B := by /-- Require that a separation logic with carrier type `PROP` fulfills all necessary axioms. -/ class BI (PROP : Type _) extends COFE PROP, BI.BIBase PROP where - entails_preorder : Preorder Entails + entails_preorder : Std.IsPreorder PROP equiv_iff {P Q : PROP} : (P ≡ Q) ↔ P ⊣⊢ Q := by simp and_ne : OFE.NonExpansive₂ and @@ -82,12 +82,15 @@ class BI (PROP : Type _) extends COFE PROP, BI.BIBase PROP where namespace BI -attribute [reducible,instance] BI.entails_preorder +attribute [instance] BI.entails_preorder -theorem BIBase.Entails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q) (h2 : Q ⊢ R) : P ⊢ R := - Trans.trans h1 h2 +theorem BIBase.Entails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q) (h2 : Q ⊢ R) : P ⊢ R := by + dsimp [BIBase.Entails] at * + exact Trans.trans h1 h2 -@[simp,refl] theorem BIBase.Entails.rfl [BI PROP] {P : PROP} : P ⊢ P := Std.Refl.refl P +@[simp,refl] theorem BIBase.Entails.rfl [BI PROP] {P : PROP} : P ⊢ P := by + dsimp [BIBase.Entails] at * + exact Std.Refl.refl P theorem BIBase.Entails.of_eq [BI PROP] {P Q : PROP} (h : P = Q) : P ⊢ Q := h ▸ .rfl diff --git a/Iris/Iris/BI/BIBase.lean b/Iris/Iris/BI/BIBase.lean index 48f9f37db..b8e53f085 100644 --- a/Iris/Iris/BI/BIBase.lean +++ b/Iris/Iris/BI/BIBase.lean @@ -21,8 +21,8 @@ open Lean /-- Require the definitions of the separation logic connectives and units on a carrier type `PROP`. -/ -class BIBase (PROP : Type u) where - Entails : PROP → PROP → Prop +class BIBase (PROP : Type u) extends LE PROP where + -- Entails : LE PROP -- PROP → PROP → Prop emp : PROP pure : Prop → PROP and : PROP → PROP → PROP @@ -35,6 +35,8 @@ class BIBase (PROP : Type u) where persistently : PROP → PROP later : PROP → PROP +def BIBase.Entails [LE PROP] (P Q : PROP) : Prop := P ≤ Q + namespace BIBase def «forall» [BIBase PROP] {α : Sort _} (P : α → PROP) : PROP := sForall fun p => ∃ a, P a = p diff --git a/Iris/Iris/BI/DerivedLaws.lean b/Iris/Iris/BI/DerivedLaws.lean index cbd16c00a..52a4d1eb9 100644 --- a/Iris/Iris/BI/DerivedLaws.lean +++ b/Iris/Iris/BI/DerivedLaws.lean @@ -2026,7 +2026,7 @@ theorem intuitionisticallyIf_sep {p : Bool} [BI PROP] [BIPositive PROP] {P Q : P theorem intuitionisticallyIf_sep_conj {p1 p2 : Bool} [BI PROP] {P Q : PROP} : (□?p1 P ∗ □?p2 Q) ⊢ □?(p1 && p2) (P ∗ Q) := match p1, p2 with - | false, false => by rfl + | false, false => Std.IsPreorder.le_refl _ | false, true => sep_mono_right intuitionisticallyIf_elim | true, false => sep_mono_left intuitionisticallyIf_elim | true, true => intuitionisticallyIf_sep_mpr diff --git a/Iris/Iris/BI/MonPred.lean b/Iris/Iris/BI/MonPred.lean index ab70217b1..bd11db4af 100644 --- a/Iris/Iris/BI/MonPred.lean +++ b/Iris/Iris/BI/MonPred.lean @@ -43,8 +43,11 @@ predicates are functions out of a `BiIndex` that are monotone w.r.t. this order. structure BiIndex where car : Type _ [inhabited : Inhabited car] - rel : car → car → Prop - [preorder : Std.Preorder rel] + -- rel : car → car → Prop + + rel : LE car + + [preorder : Std.IsPreorder car] attribute [instance] BiIndex.inhabited BiIndex.preorder @@ -56,7 +59,7 @@ scoped infix:40 " ⊑ᵢ " => BiIndex.rel _ /-- A `BiIndex` with a bottom element `bot`: every index is above `bot`. -/ @[rocq_alias BiIndexBottom] class BiIndexBottom (I : BiIndex) (bot : I.car) : Prop where - bot_le : ∀ i : I.car, I.rel bot i + bot_le : ∀ i : I.car, I.rel.le bot i /-- A monotone predicate over `BiIndex` `I` valued in the base BI `PROP`: a function `monPred_at : I → PROP` monotone w.r.t. the index order. -/ @@ -65,7 +68,7 @@ structure MonPred (I : BiIndex) (PROP : Type _) [BIBase PROP] where /-- The underlying index-indexed family (Rocq `monPred_at`). -/ monPred_at : I.car → PROP /-- Monotonicity in the index (Rocq `monPred_mono`: `Proper ((⊑) ==> (⊢))`). -/ - monPred_mono : ∀ {i j : I.car}, I.rel i j → (monPred_at i ⊢ monPred_at j) + monPred_mono : ∀ {i j : I.car}, I.rel.le i j → (monPred_at i ⊢ monPred_at j) namespace MonPred @@ -85,7 +88,7 @@ theorem ext {P Q : MonPred I PROP} (h : ∀ i, P.monPred_at i = Q.monPred_at i) so the result is monotone. -/ @[rocq_alias monPred_defs.monPred_upclosed] def upclosed [BI PROP] (Φ : I.car → PROP) : I.car → PROP := - fun i => iprop(∀ j, ⌜I.rel i j⌝ → Φ j) + fun i => iprop(∀ j, ⌜I.rel.le i j⌝ → Φ j) end MonPred @@ -118,7 +121,7 @@ namespace MonPred `monPred_sig`. -/ @[rocq_alias monPred_sig] def toSig : - MonPred I PROP -n> { f : I.car → PROP // ∀ {i j : I.car}, I.rel i j → (f i ⊢ f j) } where + MonPred I PROP -n> { f : I.car → PROP // ∀ {i j : I.car}, I.rel.le i j → (f i ⊢ f j) } where f P := ⟨P.monPred_at, fun h => P.monPred_mono h⟩ ne.1 _ _ _ h := h @@ -126,7 +129,7 @@ def toSig : Rocq `sig_monPred`. -/ @[rocq_alias sig_monPred] def ofSig : - { f : I.car → PROP // ∀ {i j : I.car}, I.rel i j → (f i ⊢ f j) } -n> MonPred I PROP where + { f : I.car → PROP // ∀ {i j : I.car}, I.rel.le i j → (f i ⊢ f j) } -n> MonPred I PROP where f P := ⟨P.val, P.property⟩ ne.1 _ _ _ h := h @@ -134,7 +137,7 @@ def ofSig : theorem ofSig_ne : OFE.NonExpansive (ofSig (I := I) (PROP := PROP)) := ofSig.ne @[rocq_alias sig_monPred_proper] -theorem ofSig_proper {P Q : { f : I.car → PROP // ∀ {i j : I.car}, I.rel i j → (f i ⊢ f j) }} +theorem ofSig_proper {P Q : { f : I.car → PROP // ∀ {i j : I.car}, I.rel.le i j → (f i ⊢ f j) }} (h : P ≡ Q) : ofSig P ≡ ofSig Q := ofSig.ne.eqv h @[rocq_alias monPred_sig_ne] @@ -147,7 +150,7 @@ theorem toSig_proper {P Q : MonPred I PROP} (h : P ≡ Q) : toSig P ≡ toSig Q theorem ofSig_toSig (P : MonPred I PROP) : ofSig (toSig P) = P := rfl @[rocq_alias monPred_sig_monPred] -theorem toSig_ofSig (P : { f : I.car → PROP // ∀ {i j : I.car}, I.rel i j → (f i ⊢ f j) }) : +theorem toSig_ofSig (P : { f : I.car → PROP // ∀ {i j : I.car}, I.rel.le i j → (f i ⊢ f j) }) : toSig (ofSig P) = P := rfl end MonPred @@ -309,7 +312,7 @@ def later (P : MonPred I PROP) : MonPred I PROP where @[rocq_alias monPred_defs.monPred_in] def monPred_in (j : I.car) : MonPred I PROP where - monPred_at i := iprop(⌜I.rel j i⌝) + monPred_at i := iprop(⌜I.rel.le j i⌝) monPred_mono h := pure_mono fun hji => Trans.trans hji h #rocq_ignore monPred_defs.monPred_in_def "Rocq unsealed definition body; use MonPred.monPred_in." @@ -358,7 +361,7 @@ section Instances variable {I : BiIndex} {PROP : Type _} [BI PROP] instance : BIBase (MonPred I PROP) where - Entails := MonPred.Entails + le := MonPred.Entails emp := MonPred.emp pure := MonPred.pure and := MonPred.and @@ -393,8 +396,8 @@ mixins, packaged into `monPredI : bi`). -/ @[rocq_alias monPredI] instance : BI (MonPred I PROP) where entails_preorder := - { refl _ := entails_at.mpr fun _ => BIBase.Entails.rfl - trans := fun h h' => entails_at.mpr fun i => (entails_at.mp h i).trans (entails_at.mp h' i) } + { le_refl _ := entails_at.mpr fun _ => BIBase.Entails.rfl + le_trans := fun _ _ _ h h' => entails_at.mpr fun i => (entails_at.mp h i).trans (entails_at.mp h' i) } equiv_iff := fun {P Q} => ⟨fun h => ⟨entails_at.mpr fun i => (equiv_iff.mp (equiv_at.mp h i)).mp, entails_at.mpr fun i => (equiv_iff.mp (equiv_at.mp h i)).mpr⟩, @@ -431,11 +434,11 @@ instance : BI (MonPred I PROP) where or_intro_r := entails_at.mpr fun i => or_intro_r or_elim h h' := entails_at.mpr fun i => or_elim (entails_at.mp h i) (entails_at.mp h' i) imp_intro {P Q R} h := entails_at.mpr fun i => - forall_intro fun j => imp_intro <| pure_elim_right fun (hij : I.rel i j) => + forall_intro fun j => imp_intro <| pure_elim_right fun (hij : I.rel.le i j) => (P.monPred_mono hij).trans <| imp_intro (entails_at.mp h j) imp_elim {P Q R} h := entails_at.mpr fun i => imp_elim <| (entails_at.mp h i).trans <| - (forall_elim i).trans <| pure_imp_elim (Std.Refl.refl i : I.rel i i) + (forall_elim i).trans <| pure_imp_elim (Std.Refl.refl i : I.rel.le i i) sForall_intro h := entails_at.mpr fun i => MonPred.sForall_at_intro i fun q hΨ => entails_at.mp (h q hΨ) i sForall_elim h := entails_at.mpr fun i => MonPred.sForall_at_elim i h @@ -448,12 +451,12 @@ instance : BI (MonPred I PROP) where sep_assoc_l := entails_at.mpr fun i => sep_assoc_l wand_intro {P Q R} h := entails_at.mpr fun i => by refine forall_intro fun j => imp_intro ?_ - refine pure_elim_right fun (hij : I.rel i j) => ?_ + refine pure_elim_right fun (hij : I.rel.le i j) => ?_ refine wand_intro (sep_symm.trans ?_) exact (sep_mono_right (P.monPred_mono hij)).trans (sep_symm.trans (entails_at.mp h j)) wand_elim {P Q R} h := entails_at.mpr fun i => (sep_mono_left ((entails_at.mp h i).trans - ((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i))))).trans wand_elim_left + ((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i))))).trans wand_elim_left persistently_mono h := entails_at.mpr fun i => persistently_mono (entails_at.mp h i) persistently_idem_2 := entails_at.mpr fun i => persistently_idem_2 persistently_emp_2 := entails_at.mpr fun i => persistently_emp_2 @@ -477,7 +480,7 @@ instance : BI (MonPred I PROP) where refine (MonPred.sForall_at_elim (q := MonPred.imp (MonPred.pure (Φ r)) (MonPred.later r)) i ⟨r, rfl⟩).trans ?_ refine (forall_elim i).trans ?_ - exact (pure_imp_elim (Std.Refl.refl i : I.rel i i)).trans (pure_imp_elim hΦ) + exact (pure_imp_elim (Std.Refl.refl i : I.rel.le i i)).trans (pure_imp_elim hΦ) later_sExists_false := fun {Φ} => entails_at.mpr fun i => by refine later_sExists_false.trans (or_mono BIBase.Entails.rfl ?_) refine exists_elim fun p => pure_elim_left fun ⟨q, hΦ, hq⟩ => ?_ @@ -491,7 +494,7 @@ instance : BI (MonPred I PROP) where later_false_em {P} := entails_at.mpr fun i => by refine later_false_em.trans (or_mono_right ?_) refine forall_intro fun j => imp_intro ?_ - refine pure_elim_right fun (hij : I.rel i j) => ?_ + refine pure_elim_right fun (hij : I.rel.le i j) => ?_ exact imp_mono BIBase.Entails.rfl (P.monPred_mono hij) #rocq_ignore monPred_unseal "Rocq unsealing command." @@ -518,14 +521,14 @@ instance : BiEmbed PROP (MonPred I PROP) where emp_valid_inj _ h := entails_at.mp h (Inhabited.default : I.car) emp_2 := entails_at.mpr fun _ => .rfl impl_2 _ _ := entails_at.mpr fun i => - (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i)) + (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i)) forall_2 := fun _Ψ {_} h => entails_at.mpr fun i => sForall_intro fun P hΨ => entails_at.mp (h P hΨ) i exist_1 := fun _Ψ {_} h => entails_at.mpr fun i => sExists_elim fun P hΨ => entails_at.mp (h P hΨ) i sep _ _ := BIBase.BiEntails.of_eq rfl wand_2 _ _ := entails_at.mpr fun i => - (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i)) + (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i)) persistently _ := BIBase.BiEntails.of_eq rfl #rocq_ignore monPred_embedding_mixin "Rocq mixin record; subsumed by the BiEmbed instance." @@ -627,7 +630,7 @@ instance [BIFUpdate PROP] : BIFUpdate (MonPred I PROP) where trans := entails_at.mpr fun _ => BIFUpdate.trans mask_frame_right_strong h := entails_at.mpr fun i => (BIFUpdate.mono - (((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i))) : _ ⊢@{PROP} _)).trans + (((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i))) : _ ⊢@{PROP} _)).trans (BIFUpdate.mask_frame_right_strong h) frame_right := entails_at.mpr fun _ => fupd_frame_right @@ -676,7 +679,7 @@ theorem monPred_at_or (i : I.car) (P Q : MonPred I PROP) : @[rocq_alias monPred_at_impl] theorem monPred_at_impl (i : I.car) (P Q : MonPred I PROP) : (iprop(P → Q)).monPred_at i ⊣⊢ - iprop(∀ j, ⌜I.rel i j⌝ → (P.monPred_at j → Q.monPred_at j)) := + iprop(∀ j, ⌜I.rel.le i j⌝ → (P.monPred_at j → Q.monPred_at j)) := BIBase.BiEntails.of_eq rfl @[rocq_alias monPred_at_forall] @@ -700,7 +703,7 @@ theorem monPred_at_sep (i : I.car) (P Q : MonPred I PROP) : @[rocq_alias monPred_at_wand] theorem monPred_at_wand (i : I.car) (P Q : MonPred I PROP) : (iprop(P -∗ Q)).monPred_at i ⊣⊢ - iprop(∀ j, ⌜I.rel i j⌝ → (P.monPred_at j -∗ Q.monPred_at j)) := + iprop(∀ j, ⌜I.rel.le i j⌝ → (P.monPred_at j -∗ Q.monPred_at j)) := BIBase.BiEntails.of_eq rfl @[rocq_alias monPred_at_persistently] @@ -715,7 +718,7 @@ theorem monPred_at_later (i : I.car) (P : MonPred I PROP) : @[rocq_alias monPred_at_in] theorem monPred_at_in (i j : I.car) : - (MonPred.monPred_in j : MonPred I PROP).monPred_at i ⊣⊢ iprop(⌜I.rel j i⌝) := + (MonPred.monPred_in j : MonPred I PROP).monPred_at i ⊣⊢ iprop(⌜I.rel.le j i⌝) := BIBase.BiEntails.of_eq rfl @[rocq_alias monPred_at_embed] @@ -795,12 +798,12 @@ theorem monPred_at_emp_valid (P : MonPred I PROP) : (⊢ P) ↔ ∀ i, ⊢ P.mon entails_at @[rocq_alias monPred_at_mono] -theorem monPred_at_mono {P Q : MonPred I PROP} {i j : I.car} (h : P ⊢ Q) (hij : I.rel i j) : +theorem monPred_at_mono {P Q : MonPred I PROP} {i j : I.car} (h : P ⊢ Q) (hij : I.rel.le i j) : P.monPred_at i ⊢ Q.monPred_at j := (entails_at.mp h i).trans (Q.monPred_mono hij) @[rocq_alias monPred_at_flip_mono] -theorem monPred_at_flip_mono {P Q : MonPred I PROP} {i j : I.car} (h : Q ⊢ P) (hij : I.rel j i) : +theorem monPred_at_flip_mono {P Q : MonPred I PROP} {i j : I.car} (h : Q ⊢ P) (hij : I.rel.le j i) : Q.monPred_at j ⊢ P.monPred_at i := monPred_at_mono h hij @@ -849,12 +852,12 @@ instance monPred_affine (P : MonPred I PROP) [∀ i, Affine (P.monPred_at i)] : @[rocq_alias monPred_impl_force] theorem monPred_impl_force (i : I.car) (P Q : MonPred I PROP) : (iprop(P → Q) : MonPred I PROP).monPred_at i ⊢ iprop(P.monPred_at i → Q.monPred_at i) := - (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i)) + (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i)) @[rocq_alias monPred_wand_force] theorem monPred_wand_force (i : I.car) (P Q : MonPred I PROP) : (iprop(P -∗ Q) : MonPred I PROP).monPred_at i ⊢ iprop(P.monPred_at i -∗ Q.monPred_at i) := - (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i)) + (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i)) /-! ### The `monPred_in` assertion -/ @@ -862,7 +865,7 @@ theorem monPred_wand_force (i : I.car) (P Q : MonPred I PROP) : theorem monPred_in_intro (P : MonPred I PROP) : P ⊢ iprop(∃ i, MonPred.monPred_in i ∧ ⎡P.monPred_at i⎤) := entails_at.mpr fun j => - (and_intro (pure_intro (Std.Refl.refl j : I.rel j j)) .rfl).trans <| + (and_intro (pure_intro (Std.Refl.refl j : I.rel.le j j)) .rfl).trans <| (exists_intro (Ψ := fun i => (iprop(MonPred.monPred_in i ∧ ⎡P.monPred_at i⎤) : MonPred I PROP).monPred_at j) j).trans (monPred_at_exist j fun i => iprop(MonPred.monPred_in i ∧ ⎡P.monPred_at i⎤)).mpr @@ -871,36 +874,36 @@ theorem monPred_in_intro (P : MonPred I PROP) : theorem monPred_in_elim (P : MonPred I PROP) (i : I.car) : (MonPred.monPred_in i : MonPred I PROP) ⊢ iprop(⎡P.monPred_at i⎤ → P) := entails_at.mpr fun j => - pure_elim (I.rel i j) .rfl fun hij => + pure_elim (I.rel.le i j) .rfl fun hij => forall_intro fun _k => imp_intro_swap <| pure_elim_left fun hjk => imp_intro <| and_elim_r.trans (P.monPred_mono (Trans.trans hij hjk)) @[rocq_alias monPred_in_mono] -theorem monPred_in_mono {i j : I.car} (h : I.rel j i) : +theorem monPred_in_mono {i j : I.car} (h : I.rel.le j i) : (MonPred.monPred_in i : MonPred I PROP) ⊢ MonPred.monPred_in j := entails_at.mpr fun _ => pure_mono fun hik => Trans.trans h hik #rocq_ignore monPred_in_proper "Use monPred_in_mono." @[rocq_alias monPred_in_flip_mono] -theorem monPred_in_flip_mono {i j : I.car} (h : I.rel i j) : +theorem monPred_in_flip_mono {i j : I.car} (h : I.rel.le i j) : (MonPred.monPred_in j : MonPred I PROP) ⊢ MonPred.monPred_in i := monPred_in_mono h @[rocq_alias monPred_in_persistent] instance monPred_in_persistent (i : I.car) : Persistent (MonPred.monPred_in i : MonPred I PROP) where - persistent := entails_at.mpr fun j => (pure_persistent (I.rel i j)).persistent + persistent := entails_at.mpr fun j => (pure_persistent (I.rel.le i j)).persistent @[rocq_alias monPred_in_absorbing] instance monPred_in_absorbing (i : I.car) : Absorbing (MonPred.monPred_in i : MonPred I PROP) where - absorbing := entails_at.mpr fun j => (pure_absorbing (I.rel i j)).absorbing + absorbing := entails_at.mpr fun j => (pure_absorbing (I.rel.le i j)).absorbing @[rocq_alias monPred_in_timeless] instance monPred_in_timeless (i : I.car) : Timeless (MonPred.monPred_in i : MonPred I PROP) where - timeless := entails_at.mpr fun j => (pure_timeless (I.rel i j)).timeless + timeless := entails_at.mpr fun j => (pure_timeless (I.rel.le i j)).timeless /-! ### Objective predicates -/ @@ -944,7 +947,7 @@ instance impl_objective (P Q : MonPred I PROP) [Objective P] [Objective Q] : Objective (iprop(P → Q)) where objective_at i _j := forall_intro fun k => imp_intro <| and_elim_l.trans <| - (((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i))) : _ ⊢@{PROP} _).trans <| + (((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i))) : _ ⊢@{PROP} _).trans <| imp_mono (Objective.objective_at k i) (Objective.objective_at i k) @[rocq_alias wand_objective] @@ -952,7 +955,7 @@ instance wand_objective (P Q : MonPred I PROP) [Objective P] [Objective Q] : Objective (iprop(P -∗ Q)) where objective_at i _j := forall_intro fun k => imp_intro <| and_elim_l.trans <| - (((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel i i))) : _ ⊢@{PROP} _).trans <| + (((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i))) : _ ⊢@{PROP} _).trans <| wand_mono (Objective.objective_at k i) (Objective.objective_at i k) @[rocq_alias forall_objective] @@ -1449,9 +1452,9 @@ instance instSbiMonPred : Sbi (MonPred I PROP) where monPred_impl_force i (iprop(⌜Ψi q⌝)) (SiPure.siPure q : MonPred I PROP) persistently_imp_siPure {P Q} := entails_at.mpr fun i => by refine (forall_elim i).trans ?_ - refine (pure_imp_elim (Std.Refl.refl i : I.rel i i)).trans ?_ + refine (pure_imp_elim (Std.Refl.refl i : I.rel.le i i)).trans ?_ refine persistently_imp_siPure.trans (persistently_mono ?_) - refine forall_intro fun j => imp_intro <| pure_elim_right fun (hij : I.rel i j) => ?_ + refine forall_intro fun j => imp_intro <| pure_elim_right fun (hij : I.rel.le i j) => ?_ exact imp_mono_right (Q.monPred_mono hij) siPure_later {Pi} := ⟨entails_at.mpr fun _ => siPure_later.mp, entails_at.mpr fun _ => siPure_later.mpr⟩ diff --git a/Iris/Iris/BI/SIProp.lean b/Iris/Iris/BI/SIProp.lean index 779175924..e1a738587 100644 --- a/Iris/Iris/BI/SIProp.lean +++ b/Iris/Iris/BI/SIProp.lean @@ -135,7 +135,7 @@ instance : IsCOFE SiProp where #rocq_ignore siProp_compl "Included in IsCOFE instance." instance : BIBase SiProp where - Entails := SiProp.entails + le := SiProp.entails emp := SiProp.pure True pure := SiProp.pure and := SiProp.and @@ -153,9 +153,9 @@ instance : BIBase SiProp where #rocq_ignore siProp_wand "Included in BIBase instance." #rocq_ignore siProp_persistently "Included in BIBase instance." -instance : Std.Preorder (BIBase.Entails (PROP := SiProp)) where - refl _ _ := id - trans h₁ h₂ n h := h₂ n (h₁ n h) +instance : Std.IsPreorder SiProp where + le_refl _ _ := id + le_trans _ _ _ h₁ h₂ n h := h₂ n (h₁ n h) /-! ## BI instance -/ diff --git a/Iris/Iris/Instances/Classical/Instance.lean b/Iris/Iris/Instances/Classical/Instance.lean index 340187d4f..d0116b816 100644 --- a/Iris/Iris/Instances/Classical/Instance.lean +++ b/Iris/Iris/Instances/Classical/Instance.lean @@ -19,7 +19,7 @@ open Iris.BI Iris.Instances.Data Std abbrev HeapProp (Val : Type _) := State Val → Prop instance : BIBase (HeapProp Val) where - Entails P Q := ∀ σ, P σ → Q σ + le P Q := ∀ σ, P σ → Q σ emp σ := σ = ∅ pure φ _ := φ and P Q σ := P σ ∧ Q σ @@ -32,13 +32,11 @@ instance : BIBase (HeapProp Val) where persistently P _ := P ∅ later P σ := P σ -instance : Std.Preorder (Entails (PROP := HeapProp Val)) where - refl := by - simp only [BI.Entails] +instance : Std.IsPreorder (HeapProp Val) where + le_refl := by intro _ _ h exact h - trans := by - simp only [BI.Entails] + le_trans := by intro _ _ _ h_xy h_yz σ h_x apply h_yz σ apply h_xy σ @@ -49,7 +47,7 @@ instance : COFE (HeapProp Val) := COFE.ofDiscrete _ instance : BI (HeapProp Val) where entails_preorder := by infer_instance equiv_iff {P Q} := ⟨ - fun h => h.to_eq ▸ ⟨Std.Refl.refl P, Std.Refl.refl P⟩, + fun h => h.to_eq ▸ ⟨Std.IsPreorder.le_refl P, Std.IsPreorder.le_refl P⟩, fun ⟨h₁, h₂⟩ => OFE.Equiv.of_eq (funext fun σ => propext ⟨h₁ σ, h₂ σ⟩) ⟩ diff --git a/Iris/Iris/Instances/UPred/Instance.lean b/Iris/Iris/Instances/UPred/Instance.lean index fa683255f..1be517149 100644 --- a/Iris/Iris/Instances/UPred/Instance.lean +++ b/Iris/Iris/Instances/UPred/Instance.lean @@ -233,7 +233,7 @@ instance bupd_ne : OFE.NonExpansive (bupd : UPred M → UPred M) where exact OFE.Dist.le Hx (Nat.le_trans Hk Hm) instance : BIBase (UPred M) where - Entails := UPred.Entails + le := UPred.Entails emp := UPred.emp pure := UPred.pure and := UPred.and @@ -266,9 +266,9 @@ instance : BIBase (UPred M) where #rocq_ignore uPred_primitive.uPred_unseal "No `Ltac unseal` rewrite is needed; nothing is sealed." @[rocq_alias uPred_primitive.entails_po] -instance uPred_entails_preorder : Std.Preorder (Entails (PROP := UPred M)) where - refl _ _ _ H := H - trans H1 H2 _ _ Hv := H2 _ _ <| H1 _ _ Hv +instance uPred_entails_preorder : Std.IsPreorder (UPred M) where + le_refl _ _ _ H := H + le_trans _ _ _ H1 H2 _ _ Hv := H2 _ _ <| H1 _ _ Hv @[rocq_alias uPred_primitive.entails_lim] theorem uPred_entails_lim {cP cQ : Chain (UPred M)} (H : ∀ n, cP n ⊢ cQ n) : @@ -386,8 +386,8 @@ instance : BI (UPred M) where refine P.mono H ?_ .refl refine (incN_iff_right ?_).mpr (incN_refl _) exact (core_idem x.val).dist - persistently_emp_2 := Std.Refl.refl emp - persistently_and_2 {P Q} := Std.Refl.refl iprop( P ∧ Q) + persistently_emp_2 := Std.IsPreorder.le_refl emp + persistently_and_2 {P Q} := Std.IsPreorder.le_refl iprop( P ∧ Q) persistently_sExists_1 _ _ := fun ⟨p, HΨ, H⟩ => by refine ⟨iprop( p), ⟨p, ?_⟩, H⟩ ext; exact and_iff_right HΨ diff --git a/Iris/Iris/Std/Classes.lean b/Iris/Iris/Std/Classes.lean index d286b97ff..acec5521b 100644 --- a/Iris/Iris/Std/Classes.lean +++ b/Iris/Iris/Std/Classes.lean @@ -19,9 +19,6 @@ export Top (top) notation "⊤" => top -/-- Require that a relation `R` on `α` is a preorder, i.e. that it is reflexive and transitive. -/ -class Preorder (R : Relation α) extends Std.Refl R, Trans R R R - /-- Require that a binary function `f` on `α` is idempotent in a relation `R` on `α`. -/ class Idempotent (R : Relation α) (f : α → α → α) where idem {x : α} : R (f x x) x From af17f95e6a6ad2e5b1812a564e03520b50e6066d Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 15 Jul 2026 13:09:28 +0200 Subject: [PATCH 03/11] Instead of having `BI` extending `LE`, prove `LE` instance separately --- Iris/Iris/BI/BI.lean | 20 ++++++++++++-------- Iris/Iris/BI/BIBase.lean | 6 ++---- Iris/Iris/BI/DerivedLaws.lean | 5 +++-- Iris/Iris/BI/MonPred.lean | 7 +++---- Iris/Iris/BI/SIProp.lean | 7 ++++--- Iris/Iris/Instances/Classical/Instance.lean | 7 ++++--- Iris/Iris/Instances/UPred/Instance.lean | 9 +++++---- 7 files changed, 33 insertions(+), 28 deletions(-) diff --git a/Iris/Iris/BI/BI.lean b/Iris/Iris/BI/BI.lean index cab742eb0..3582c54dc 100644 --- a/Iris/Iris/BI/BI.lean +++ b/Iris/Iris/BI/BI.lean @@ -22,7 +22,9 @@ theorem liftRel_eq : liftRel (@Eq α) A B ↔ A = B := by /-- Require that a separation logic with carrier type `PROP` fulfills all necessary axioms. -/ class BI (PROP : Type _) extends COFE PROP, BI.BIBase PROP where - entails_preorder : Std.IsPreorder PROP + entails_refl {P : PROP} : P ⊢ P + entails_trans {P Q R : PROP} : (P ⊢ Q) → (Q ⊢ R) → P ⊢ R + equiv_iff {P Q : PROP} : (P ≡ Q) ↔ P ⊣⊢ Q := by simp and_ne : OFE.NonExpansive₂ and @@ -82,15 +84,17 @@ class BI (PROP : Type _) extends COFE PROP, BI.BIBase PROP where namespace BI -attribute [instance] BI.entails_preorder +instance [BIBase PROP] : LE PROP where + le := BIBase.Entails + +instance BI.entails_preorder [BI PROP] : Std.IsPreorder PROP where + le_refl _ := BI.entails_refl + le_trans _ _ _ := BI.entails_trans -theorem BIBase.Entails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q) (h2 : Q ⊢ R) : P ⊢ R := by - dsimp [BIBase.Entails] at * - exact Trans.trans h1 h2 +theorem BIBase.Entails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q) (h2 : Q ⊢ R) : P ⊢ R := + BI.entails_trans h1 h2 -@[simp,refl] theorem BIBase.Entails.rfl [BI PROP] {P : PROP} : P ⊢ P := by - dsimp [BIBase.Entails] at * - exact Std.Refl.refl P +@[simp,refl] theorem BIBase.Entails.rfl [BI PROP] {P : PROP} : P ⊢ P := BI.entails_refl theorem BIBase.Entails.of_eq [BI PROP] {P Q : PROP} (h : P = Q) : P ⊢ Q := h ▸ .rfl diff --git a/Iris/Iris/BI/BIBase.lean b/Iris/Iris/BI/BIBase.lean index b8e53f085..48f9f37db 100644 --- a/Iris/Iris/BI/BIBase.lean +++ b/Iris/Iris/BI/BIBase.lean @@ -21,8 +21,8 @@ open Lean /-- Require the definitions of the separation logic connectives and units on a carrier type `PROP`. -/ -class BIBase (PROP : Type u) extends LE PROP where - -- Entails : LE PROP -- PROP → PROP → Prop +class BIBase (PROP : Type u) where + Entails : PROP → PROP → Prop emp : PROP pure : Prop → PROP and : PROP → PROP → PROP @@ -35,8 +35,6 @@ class BIBase (PROP : Type u) extends LE PROP where persistently : PROP → PROP later : PROP → PROP -def BIBase.Entails [LE PROP] (P Q : PROP) : Prop := P ≤ Q - namespace BIBase def «forall» [BIBase PROP] {α : Sort _} (P : α → PROP) : PROP := sForall fun p => ∃ a, P a = p diff --git a/Iris/Iris/BI/DerivedLaws.lean b/Iris/Iris/BI/DerivedLaws.lean index 52a4d1eb9..447aaf4c2 100644 --- a/Iris/Iris/BI/DerivedLaws.lean +++ b/Iris/Iris/BI/DerivedLaws.lean @@ -21,7 +21,8 @@ open Iris.Std BI /-! # Entails -/ -instance entails_trans [BI PROP] : Trans (α := PROP) Entails Entails Entails where +/- Necessary for `calc`-style proofs. -/ +instance entails_trans' [BI PROP] : Trans (α := PROP) Entails Entails Entails where trans h1 h2 := h1.trans h2 instance entails_antisymm [BI PROP] : Antisymmetric (α := PROP) BiEntails Entails where antisymm h1 h2 := ⟨h1, h2⟩ @@ -2026,7 +2027,7 @@ theorem intuitionisticallyIf_sep {p : Bool} [BI PROP] [BIPositive PROP] {P Q : P theorem intuitionisticallyIf_sep_conj {p1 p2 : Bool} [BI PROP] {P Q : PROP} : (□?p1 P ∗ □?p2 Q) ⊢ □?(p1 && p2) (P ∗ Q) := match p1, p2 with - | false, false => Std.IsPreorder.le_refl _ + | false, false => by rfl | false, true => sep_mono_right intuitionisticallyIf_elim | true, false => sep_mono_left intuitionisticallyIf_elim | true, true => intuitionisticallyIf_sep_mpr diff --git a/Iris/Iris/BI/MonPred.lean b/Iris/Iris/BI/MonPred.lean index bd11db4af..c5b3482c4 100644 --- a/Iris/Iris/BI/MonPred.lean +++ b/Iris/Iris/BI/MonPred.lean @@ -361,7 +361,7 @@ section Instances variable {I : BiIndex} {PROP : Type _} [BI PROP] instance : BIBase (MonPred I PROP) where - le := MonPred.Entails + Entails := MonPred.Entails emp := MonPred.emp pure := MonPred.pure and := MonPred.and @@ -395,9 +395,8 @@ theorem dist_at {n : Nat} {P Q : MonPred I PROP} : mixins, packaged into `monPredI : bi`). -/ @[rocq_alias monPredI] instance : BI (MonPred I PROP) where - entails_preorder := - { le_refl _ := entails_at.mpr fun _ => BIBase.Entails.rfl - le_trans := fun _ _ _ h h' => entails_at.mpr fun i => (entails_at.mp h i).trans (entails_at.mp h' i) } + entails_refl := entails_at.mpr fun _ => BIBase.Entails.rfl + entails_trans := fun h h' => entails_at.mpr fun i => (entails_at.mp h i).trans (entails_at.mp h' i) equiv_iff := fun {P Q} => ⟨fun h => ⟨entails_at.mpr fun i => (equiv_iff.mp (equiv_at.mp h i)).mp, entails_at.mpr fun i => (equiv_iff.mp (equiv_at.mp h i)).mpr⟩, diff --git a/Iris/Iris/BI/SIProp.lean b/Iris/Iris/BI/SIProp.lean index e1a738587..9b7e5b7fe 100644 --- a/Iris/Iris/BI/SIProp.lean +++ b/Iris/Iris/BI/SIProp.lean @@ -135,7 +135,7 @@ instance : IsCOFE SiProp where #rocq_ignore siProp_compl "Included in IsCOFE instance." instance : BIBase SiProp where - le := SiProp.entails + Entails := SiProp.entails emp := SiProp.pure True pure := SiProp.pure and := SiProp.and @@ -153,7 +153,7 @@ instance : BIBase SiProp where #rocq_ignore siProp_wand "Included in BIBase instance." #rocq_ignore siProp_persistently "Included in BIBase instance." -instance : Std.IsPreorder SiProp where +instance siPropPreorder : Std.IsPreorder SiProp where le_refl _ _ := id le_trans _ _ _ h₁ h₂ n h := h₂ n (h₁ n h) @@ -161,7 +161,8 @@ instance : Std.IsPreorder SiProp where @[rocq_alias siPropI] instance instBI : BI SiProp where - entails_preorder := inferInstance + entails_refl := siPropPreorder.le_refl _ + entails_trans := siPropPreorder.le_trans _ _ _ equiv_iff.mp heq := ⟨fun n hP => (heq n .refl).mp hP, fun n hQ => (heq n .refl).mpr hQ⟩ equiv_iff.mpr H _ _ _ := ⟨H.1 _, H.2 _⟩ and_ne.ne _ _ _ h₁ _ _ h₂ m h := ⟨.imp (h₁ h).mp (h₂ h).mp, .imp (h₁ h).mpr (h₂ h).mpr⟩ diff --git a/Iris/Iris/Instances/Classical/Instance.lean b/Iris/Iris/Instances/Classical/Instance.lean index d0116b816..2e56b78f8 100644 --- a/Iris/Iris/Instances/Classical/Instance.lean +++ b/Iris/Iris/Instances/Classical/Instance.lean @@ -19,7 +19,7 @@ open Iris.BI Iris.Instances.Data Std abbrev HeapProp (Val : Type _) := State Val → Prop instance : BIBase (HeapProp Val) where - le P Q := ∀ σ, P σ → Q σ + Entails P Q := ∀ σ, P σ → Q σ emp σ := σ = ∅ pure φ _ := φ and P Q σ := P σ ∧ Q σ @@ -32,7 +32,7 @@ instance : BIBase (HeapProp Val) where persistently P _ := P ∅ later P σ := P σ -instance : Std.IsPreorder (HeapProp Val) where +instance heapPropPreorder : Std.IsPreorder (HeapProp Val) where le_refl := by intro _ _ h exact h @@ -45,7 +45,8 @@ instance : Std.IsPreorder (HeapProp Val) where instance : COFE (HeapProp Val) := COFE.ofDiscrete _ instance : BI (HeapProp Val) where - entails_preorder := by infer_instance + entails_refl := heapPropPreorder.le_refl _ + entails_trans := heapPropPreorder.le_trans _ _ _ equiv_iff {P Q} := ⟨ fun h => h.to_eq ▸ ⟨Std.IsPreorder.le_refl P, Std.IsPreorder.le_refl P⟩, fun ⟨h₁, h₂⟩ => OFE.Equiv.of_eq (funext fun σ => propext ⟨h₁ σ, h₂ σ⟩) diff --git a/Iris/Iris/Instances/UPred/Instance.lean b/Iris/Iris/Instances/UPred/Instance.lean index 1be517149..53aa99cc7 100644 --- a/Iris/Iris/Instances/UPred/Instance.lean +++ b/Iris/Iris/Instances/UPred/Instance.lean @@ -233,7 +233,7 @@ instance bupd_ne : OFE.NonExpansive (bupd : UPred M → UPred M) where exact OFE.Dist.le Hx (Nat.le_trans Hk Hm) instance : BIBase (UPred M) where - le := UPred.Entails + Entails := UPred.Entails emp := UPred.emp pure := UPred.pure and := UPred.and @@ -280,7 +280,8 @@ theorem uPred_entails_lim {cP cQ : Chain (UPred M)} (H : ∀ n, cP n ⊢ cQ n) : @[rocq_alias uPredI] instance : BI (UPred M) where - entails_preorder := inferInstance + entails_refl := uPred_entails_preorder.le_refl _ + entails_trans := uPred_entails_preorder.le_trans _ _ _ equiv_iff {_ _} := by constructor <;> intro HE · exact ⟨fun n ⟨x, Hv⟩ H => (HE n n x .refl Hv).mp H, @@ -386,8 +387,8 @@ instance : BI (UPred M) where refine P.mono H ?_ .refl refine (incN_iff_right ?_).mpr (incN_refl _) exact (core_idem x.val).dist - persistently_emp_2 := Std.IsPreorder.le_refl emp - persistently_and_2 {P Q} := Std.IsPreorder.le_refl iprop( P ∧ Q) + persistently_emp_2 := uPred_entails_preorder.le_refl emp + persistently_and_2 {P Q} := uPred_entails_preorder.le_refl iprop( P ∧ Q) persistently_sExists_1 _ _ := fun ⟨p, HΨ, H⟩ => by refine ⟨iprop( p), ⟨p, ?_⟩, H⟩ ext; exact and_iff_right HΨ From 96462afd66946e7dd408632bb3b66c81517ffada Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 15 Jul 2026 13:35:42 +0200 Subject: [PATCH 04/11] Eliminate `Std/Classes.lean` --- Iris/Iris/BI/BIBase.lean | 1 - Iris/Iris/BI/DerivedLaws.lean | 53 ++++++----------------- Iris/Iris/BI/DerivedLawsLater.lean | 1 - Iris/Iris/BI/Instances.lean | 1 - Iris/Iris/Std.lean | 1 - Iris/Iris/Std/Classes.lean | 67 ------------------------------ Iris/Iris/Std/CoPset.lean | 6 +-- Iris/Iris/Std/GenMultiSets.lean | 1 - Iris/Iris/Std/GenSets.lean | 14 +++---- Iris/Iris/Std/List.lean | 1 - Iris/Iris/Std/Positives.lean | 1 - Iris/Iris/Std/Rewrite.lean | 1 - 12 files changed, 23 insertions(+), 125 deletions(-) delete mode 100644 Iris/Iris/Std/Classes.lean diff --git a/Iris/Iris/BI/BIBase.lean b/Iris/Iris/BI/BIBase.lean index 48f9f37db..c15dc31f2 100644 --- a/Iris/Iris/BI/BIBase.lean +++ b/Iris/Iris/BI/BIBase.lean @@ -6,7 +6,6 @@ Authors: Lars König, Mario Carneiro module public meta import Iris.BI.Notation -public import Iris.Std.Classes public meta import Iris.Std.DelabRule public meta import Iris.Std.Rewrite public import Iris.Std.BigOp diff --git a/Iris/Iris/BI/DerivedLaws.lean b/Iris/Iris/BI/DerivedLaws.lean index 447aaf4c2..f108acc91 100644 --- a/Iris/Iris/BI/DerivedLaws.lean +++ b/Iris/Iris/BI/DerivedLaws.lean @@ -9,7 +9,6 @@ public import Iris.BI.Classes public import Iris.BI.Extensions public import Iris.BI.BI public import Iris.Std.Nat -public import Iris.Std.Classes public import Iris.Std.Rewrite public import Iris.Std.TC import Iris.Std.RocqPorting @@ -24,8 +23,7 @@ open Iris.Std BI /- Necessary for `calc`-style proofs. -/ instance entails_trans' [BI PROP] : Trans (α := PROP) Entails Entails Entails where trans h1 h2 := h1.trans h2 -instance entails_antisymm [BI PROP] : Antisymmetric (α := PROP) BiEntails Entails where - antisymm h1 h2 := ⟨h1, h2⟩ + #rocq_ignore bi.entails_proper "Derivable from _ne with NonExpansive.eqv." instance equiv_trans [BI PROP] : Trans (α := PROP) BiEntails BiEntails BiEntails where @@ -209,13 +207,11 @@ theorem exists_mono [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ⊢ Ψ a) : theorem exists_congr [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ⊣⊢ Ψ a) : (∃ a, Φ a) ⊣⊢ ∃ a, Ψ a := ⟨exists_mono fun a => (h a).1, exists_mono fun a => (h a).2⟩ -theorem and_self [BI PROP] {P : PROP} : P ∧ P ⊣⊢ P := ⟨and_elim_l, and_intro .rfl .rfl⟩ @[rocq_alias bi.and_idem] -instance [BI PROP] : Idempotent (α := PROP) BiEntails and := ⟨and_self⟩ +theorem and_self [BI PROP] {P : PROP} : P ∧ P ⊣⊢ P := ⟨and_elim_l, and_intro .rfl .rfl⟩ -theorem or_self [BI PROP] {P : PROP} : P ∨ P ⊣⊢ P := ⟨or_elim .rfl .rfl, or_intro_l⟩ @[rocq_alias bi.or_idem] -instance [BI PROP] : Idempotent (α := PROP) BiEntails or := ⟨or_self⟩ +theorem or_self [BI PROP] {P : PROP} : P ∨ P ⊣⊢ P := ⟨or_elim .rfl .rfl, or_intro_l⟩ #rocq_ignore bi.and_mono' "Use and_mono" #rocq_ignore bi.and_flip_mono' "Use and_mono" @@ -230,61 +226,48 @@ instance [BI PROP] : Idempotent (α := PROP) BiEntails or := ⟨or_self⟩ @[rocq_alias bi.and_comm] theorem and_comm [BI PROP] {P Q : PROP} : P ∧ Q ⊣⊢ Q ∧ P := ⟨and_symm, and_symm⟩ -instance [BI PROP] : Commutative (α := PROP) BiEntails and := ⟨and_comm⟩ @[rocq_alias bi.or_comm] theorem or_comm [BI PROP] {P Q : PROP} : P ∨ Q ⊣⊢ Q ∨ P := ⟨or_symm, or_symm⟩ -instance [BI PROP] : Commutative (α := PROP) BiEntails or := ⟨or_comm⟩ @[rocq_alias bi.True_and] theorem true_and [BI PROP] {P : PROP} : True ∧ P ⊣⊢ P := ⟨and_elim_r, and_intro (pure_intro trivial) .rfl⟩ -instance [BI PROP] : LeftId (· ⊣⊢@{PROP} ·) iprop(True) and := ⟨true_and⟩ @[rocq_alias bi.and_True] theorem and_true [BI PROP] {P : PROP} : P ∧ True ⊣⊢ P := and_comm.trans true_and -instance [BI PROP] : RightId (· ⊣⊢@{PROP} ·) iprop(True) and := ⟨and_true⟩ @[rocq_alias bi.False_and] theorem false_and [BI PROP] {P : PROP} : False ∧ P ⊣⊢ False := ⟨and_elim_l, false_elim⟩ -instance [BI PROP] : LeftAbsorb (· ⊣⊢@{PROP} ·) iprop(False) and := ⟨false_and⟩ @[rocq_alias bi.and_False] theorem and_false [BI PROP] {P : PROP} : P ∧ False ⊣⊢ False := and_comm.trans false_and -instance [BI PROP] : RightAbsorb (· ⊣⊢@{PROP} ·) iprop(False) and := ⟨and_false⟩ @[rocq_alias bi.True_or] theorem true_or [BI PROP] {P : PROP} : True ∨ P ⊣⊢ True := ⟨true_intro, or_intro_l⟩ -instance [BI PROP] : LeftAbsorb (· ⊣⊢@{PROP} ·) iprop(True) or := ⟨true_or⟩ @[rocq_alias bi.or_True] theorem or_true [BI PROP] {P : PROP} : P ∨ True ⊣⊢ True := or_comm.trans true_or -instance [BI PROP] : RightAbsorb (· ⊣⊢@{PROP} ·) iprop(True) or := ⟨or_true⟩ @[rocq_alias bi.False_or] theorem false_or [BI PROP] {P : PROP} : False ∨ P ⊣⊢ P := ⟨or_elim false_elim .rfl, or_intro_r⟩ -instance [BI PROP] : LeftId (α := PROP) BiEntails iprop(False) or := ⟨false_or⟩ @[rocq_alias bi.or_False] theorem or_false [BI PROP] {P : PROP} : P ∨ False ⊣⊢ P := or_comm.trans false_or -instance [BI PROP] : RightId (α := PROP) BiEntails iprop(False) or := ⟨or_false⟩ @[rocq_alias bi.and_assoc] theorem and_assoc [BI PROP] {P Q R : PROP} : (P ∧ Q) ∧ R ⊣⊢ P ∧ Q ∧ R := ⟨and_intro (and_elim_left_trans and_elim_l) (and_mono_left and_elim_r), and_intro (and_mono_right and_elim_l) (and_elim_right_trans and_elim_r)⟩ -instance [BI PROP] : Associative (α := PROP) BiEntails and := ⟨and_assoc⟩ @[rocq_alias bi.or_assoc] theorem or_assoc [BI PROP] {P Q R : PROP} : (P ∨ Q) ∨ R ⊣⊢ P ∨ Q ∨ R := ⟨or_elim (or_mono_right or_intro_l) (or_intro_right_trans or_intro_r), or_elim (or_intro_left_trans or_intro_l) (or_mono_left or_intro_r)⟩ -instance [BI PROP] : Associative (α := PROP) BiEntails or := ⟨or_assoc⟩ @[rocq_alias bi.True_impl] theorem true_imp [BI PROP] {P : PROP} : (True → P) ⊣⊢ P := ⟨and_true.2.trans imp_elim_left, imp_intro and_elim_l⟩ -instance [BI PROP] : LeftId (· ⊣⊢@{PROP} ·) iprop(True) imp := ⟨true_imp⟩ @[rocq_alias bi.impl_refl] theorem imp_self [BI PROP] {P Q : PROP} : Q ⊢ P → P := imp_intro and_elim_r @@ -390,7 +373,7 @@ instance bi_and_monoid [BI PROP] : LawfulBigOp and (iprop(True) : PROP) BiEntail trans h1 h2 := h1.trans h2 comm := and_comm assoc := and_assoc - left_id := left_id + left_id := true_and congr_l := and_congr_left /-! # BI -/ @@ -435,13 +418,11 @@ theorem wand_congr_right [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : (P -∗ Q @[rocq_alias bi.sep_comm] theorem sep_comm [BI PROP] {P Q : PROP} : P ∗ Q ⊣⊢ Q ∗ P := ⟨sep_symm, sep_symm⟩ -instance [BI PROP] : Commutative (α := PROP) BiEntails sep := ⟨sep_comm⟩ @[rocq_alias bi.sep_assoc] theorem sep_assoc [BI PROP] {P Q R : PROP} : (P ∗ Q) ∗ R ⊣⊢ P ∗ Q ∗ R := ⟨sep_assoc_l, (sep_comm.trans <| sep_congr_left sep_comm).1.trans <| sep_assoc_l.trans (sep_comm.trans <| sep_congr_right sep_comm).2⟩ -instance [BI PROP] : Associative (α := PROP) BiEntails sep := ⟨sep_assoc⟩ theorem sep_left_comm [BI PROP] {P Q R : PROP} : P ∗ Q ∗ R ⊣⊢ Q ∗ P ∗ R := sep_assoc.symm.trans <| (sep_congr_left sep_comm).trans sep_assoc @@ -452,12 +433,10 @@ theorem sep_right_comm [BI PROP] {P Q R : PROP} : (P ∗ Q) ∗ R ⊣⊢ (P ∗ theorem sep_sep_sep_comm [BI PROP] {P Q R S : PROP} : (P ∗ Q) ∗ (R ∗ S) ⊣⊢ (P ∗ R) ∗ (Q ∗ S) := sep_assoc.trans <| (sep_congr_right sep_left_comm).trans sep_assoc.symm -@[rocq_alias bi.emp_sep] -instance [BI PROP] : LeftId (α := PROP) BiEntails emp sep := ⟨emp_sep⟩ +#rocq_ignore bi.emp_sep "The type class LeftId in Lean is not general enough" -theorem sep_emp [BI PROP] {P : PROP} : P ∗ emp ⊣⊢ P := sep_comm.trans emp_sep @[rocq_alias bi.sep_emp] -instance [BI PROP] : RightId (α := PROP) BiEntails emp sep := ⟨sep_emp⟩ +theorem sep_emp [BI PROP] {P : PROP} : P ∗ emp ⊣⊢ P := sep_comm.trans emp_sep @[rocq_alias bi.bi_sep_monoid] instance bi_sep_monoid [BI PROP] : LawfulBigOp sep (emp : PROP) BiEntails where @@ -466,7 +445,7 @@ instance bi_sep_monoid [BI PROP] : LawfulBigOp sep (emp : PROP) BiEntails where trans h1 h2 := h1.trans h2 comm := sep_comm assoc := sep_assoc - left_id := left_id + left_id := emp_sep congr_l := sep_congr_left @[rocq_alias bi.True_sep_2] @@ -487,16 +466,12 @@ theorem wand_elim_swap [BI PROP] {P Q R : PROP} (h : Q ⊢ P -∗ R) : P ∗ Q @[rocq_alias bi.wand_elim_l] theorem wand_elim_left [BI PROP] {P Q : PROP} : (P -∗ Q) ∗ P ⊢ Q := wand_elim .rfl +@[rocq_alias bi.False_sep] theorem false_sep [BI PROP] {P : PROP} : False ∗ P ⊣⊢ False := ⟨(sep_mono_left (P' := iprop(P -∗ False)) false_elim).trans wand_elim_left, false_elim⟩ -@[rocq_alias bi.False_sep] -instance [BI PROP] : LeftAbsorb (· ⊣⊢@{PROP} ·) iprop(False) sep where - left_absorb := false_sep -theorem sep_false [BI PROP] {P : PROP} : P ∗ False ⊣⊢ False := sep_comm.trans false_sep @[rocq_alias bi.sep_False] -instance [BI PROP] : RightAbsorb (· ⊣⊢@{PROP} ·) iprop(False) sep where - right_absorb := sep_false +theorem sep_false [BI PROP] {P : PROP} : P ∗ False ⊣⊢ False := sep_comm.trans false_sep @[rocq_alias bi.wand_elim_r] theorem wand_elim_right [BI PROP] {P Q : PROP} : P ∗ (P -∗ Q) ⊢ Q := wand_elim_swap .rfl @@ -1027,13 +1002,13 @@ theorem affinely_intro [BI PROP] {P Q : PROP} [Affine P] (h : P ⊢ Q) : P ⊢ < @[rocq_alias bi.emp_and] theorem emp_and [BI PROP] {P : PROP} [Affine P] : emp ∧ P ⊣⊢ P := ⟨and_elim_r, and_intro affine .rfl⟩ -@[rocq_alias bi.emp_and'] -instance emp_and_biaffine [BI PROP] [BIAffine PROP] : LeftId (α := PROP) BiEntails emp and := ⟨emp_and⟩ + +#rocq_ignore bi.emp_and' "The type class LeftId in Lean is not general enough" @[rocq_alias bi.and_emp] theorem and_emp [BI PROP] {P : PROP} [Affine P] : P ∧ emp ⊣⊢ P := and_comm.trans emp_and -@[rocq_alias bi.and_emp'] -instance and_emp_biaffine [BI PROP] [BIAffine PROP] : RightId (α := PROP) BiEntails emp and := ⟨and_emp⟩ + +#rocq_ignore bi.and_emp' "The type class RightId in Lean is not general enough" @[rocq_alias bi.emp_or] theorem emp_or [BI PROP] {P : PROP} [Affine P] : emp ∨ P ⊣⊢ emp := ⟨or_elim .rfl affine, or_intro_l⟩ @@ -1058,14 +1033,12 @@ instance [BI PROP] [BIAffine PROP] (P : PROP) : Absorbing P where @[rocq_alias bi.True_sep] theorem true_sep [BI PROP] {P : PROP} [Absorbing P] : True ∗ P ⊣⊢ P := ⟨absorbing, true_sep_mpr⟩ -instance [BI PROP] [BIAffine PROP] : LeftId (α := PROP) BiEntails iprop(True) sep := ⟨true_sep⟩ @[rocq_alias bi.True_sep'] theorem true_sep_flip [BI PROP] {P : PROP} [Absorbing P] : P ⊣⊢ True ∗ P := true_sep.symm @[rocq_alias bi.sep_True] theorem sep_true [BI PROP] {P : PROP} [Absorbing P] : P ∗ True ⊣⊢ P := sep_comm.trans true_sep -instance [BI PROP] [BIAffine PROP] : RightId (α := PROP) BiEntails iprop(True) sep := ⟨sep_true⟩ @[rocq_alias bi.sep_True'] theorem sep_true_flip [BI PROP] {P : PROP} [Absorbing P] : P ⊣⊢ P ∗ True := diff --git a/Iris/Iris/BI/DerivedLawsLater.lean b/Iris/Iris/BI/DerivedLawsLater.lean index 3bc9ff86f..6e963755f 100644 --- a/Iris/Iris/BI/DerivedLawsLater.lean +++ b/Iris/Iris/BI/DerivedLawsLater.lean @@ -10,7 +10,6 @@ public import Iris.BI.Extensions public import Iris.BI.BI public import Iris.BI.DerivedLaws public import Iris.BI.BigOp.BigOp -public import Iris.Std.Classes public import Iris.Std.Rewrite public import Iris.Std.TC public import Iris.Std.RocqPorting diff --git a/Iris/Iris/BI/Instances.lean b/Iris/Iris/BI/Instances.lean index b9e330ed0..c057a3b86 100644 --- a/Iris/Iris/BI/Instances.lean +++ b/Iris/Iris/BI/Instances.lean @@ -9,7 +9,6 @@ public import Iris.BI.Classes public import Iris.BI.DerivedLaws public import Iris.BI.Extensions public import Iris.BI.BI -public import Iris.Std.Classes @[expose] public section diff --git a/Iris/Iris/Std.lean b/Iris/Iris/Std.lean index 6539947bf..6c57ffdca 100644 --- a/Iris/Iris/Std.lean +++ b/Iris/Iris/Std.lean @@ -1,6 +1,5 @@ module -public import Iris.Std.Classes public import Iris.Std.Expr public import Iris.Std.HeapInstances public import Iris.Std.Infinite diff --git a/Iris/Iris/Std/Classes.lean b/Iris/Iris/Std/Classes.lean deleted file mode 100644 index acec5521b..000000000 --- a/Iris/Iris/Std/Classes.lean +++ /dev/null @@ -1,67 +0,0 @@ -/- -Copyright (c) 2022 Lars König. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Lars König --/ -module - -@[expose] public section - -namespace Iris.Std - -/-- Represents a binary relation with two arguments of the same type `α`. -/ -abbrev Relation (α : Type _) := α → α → Prop - -/-- Require that a type `α` has a distinguished top element. -/ -class Top (α : Type u) where - top : α -export Top (top) - -notation "⊤" => top - -/-- Require that a binary function `f` on `α` is idempotent in a relation `R` on `α`. -/ -class Idempotent (R : Relation α) (f : α → α → α) where - idem {x : α} : R (f x x) x -export Idempotent (idem) - -/-- Require that a binary function `f` from `β` to `α` is commutative in a relation `R` on `α`. -/ -class Commutative (R : Relation α) (f : β → β → α) where - comm {x y : β} : R (f x y) (f y x) -export Commutative (comm) - -/-- Require that an element `i` of `α` is the left unit of a binary function `f` on `α` in a -relation `R` on `α`. -/ -class LeftId (R : Relation α) (i : α) (f : α → α → α) where - left_id {x : α} : R (f i x) x -export LeftId (left_id) - -/-- Require that an element `i` of `α` is the right unit of a binary function `f` on `α` in a -relation `R` on `α`. -/ -class RightId (R : Relation α) (i : α) (f : α → α → α) where - right_id {x : α} : R (f x i) x -export RightId (right_id) - -class LeftAbsorb (R : Relation α) (i : α) (f : α → α → α) where - left_absorb {x : α} : R (f i x) i -export LeftAbsorb (left_absorb) - -class RightAbsorb (R : Relation α) (i : α) (f : α → α → α) where - right_absorb {x : α} : R (f x i) i -export RightAbsorb (right_absorb) - -/-- Require that a binary function `f` on `α` is associative in a relation `R` on `α`. -/ -class Associative (R : Relation α) (f : α → α → α) where - assoc {x y z : α} : R (f (f x y) z) (f x (f y z)) -export Associative (assoc) - -/-- Require that a relation `S` on `α` is antisymmetrical with `R` as its equivalence relation. -/ -class Antisymmetric (R : Relation α) (S : outParam <| Relation α) where - antisymm {x y : α} : (left : S x y) → (right : S y x) → R x y -export Antisymmetric (antisymm) - -class Disjoint (α : Type u) where - disjoint : α -> α -> Prop -export Disjoint (disjoint) -infix:50 " ## " => Disjoint.disjoint - -end Iris.Std diff --git a/Iris/Iris/Std/CoPset.lean b/Iris/Iris/Std/CoPset.lean index c860d2776..06cfbae43 100644 --- a/Iris/Iris/Std/CoPset.lean +++ b/Iris/Iris/Std/CoPset.lean @@ -6,7 +6,6 @@ Authors: Remy Seassau, Markus de Medeiros, Sergei Stepanenko module public import Iris.Std.Positives -public import Iris.Std.Classes public import Iris.Std.GenSets import Iris.Std.List @@ -220,8 +219,6 @@ instance : EmptyCollection CoPset where emptyCollection := CoPset.empty def full : CoPset := ⟨CoPsetRaw.leaf true, rfl⟩ -instance : Iris.Std.Top CoPset where top := CoPset.full - @[simp] def singleton (p : Pos) : CoPset := ⟨CoPsetRaw.Singleton p, coPsetSingleton_wf p⟩ instance : Singleton Pos CoPset where @@ -255,6 +252,9 @@ theorem mem_empty {p : Pos} : p ∉ (∅ : CoPset) := by theorem mem_full {p : Pos} : p ∈ full := by simp only [Membership.mem, full, CoPsetRaw.ElemOf] +/-- `CoPset.full` is the top element in the type `CoPset`. -/ +notation "⊤" => CoPset.full + @[simp] theorem subseteq_top {X : CoPset} : X ⊆ ⊤ := λ _ _ => mem_full diff --git a/Iris/Iris/Std/GenMultiSets.lean b/Iris/Iris/Std/GenMultiSets.lean index 2751a727a..beb8330dd 100644 --- a/Iris/Iris/Std/GenMultiSets.lean +++ b/Iris/Iris/Std/GenMultiSets.lean @@ -5,7 +5,6 @@ Authors: Haokun Li -/ module -public import Iris.Std.Classes public import Iris.Std.GenSets public import Batteries.Data.List.Perm diff --git a/Iris/Iris/Std/GenSets.lean b/Iris/Iris/Std/GenSets.lean index 3c40aa10b..8285d1d0e 100644 --- a/Iris/Iris/Std/GenSets.lean +++ b/Iris/Iris/Std/GenSets.lean @@ -5,7 +5,6 @@ Authors: Zongyuan Liu, Sergei Stepanenko -/ module -public import Iris.Std.Classes public import Iris.Std.Infinite import Batteries.Data.List.Perm import Iris.Std.List @@ -68,9 +67,10 @@ instance : HasSubset S := ⟨fun S₁ S₂ => ∀ x, x ∈ S₁ → x ∈ S₂ is in `S₂` but they are not equal. -/ instance : HasSSubset S := ⟨fun S₁ S₂ => S₁ ≠ S₂ ∧ ∀ x, x ∈ S₁ → x ∈ S₂⟩ +def Disjoint (S₁ S₂ : S) : Prop := ∀ x, ¬(x ∈ S₁ ∧ x ∈ S₂) + /-- Two sets are disjoint if they share no common elements. -/ -instance : Disjoint S where - disjoint S₁ S₂ := ∀ x, ¬(x ∈ S₁ ∧ x ∈ S₂) +infix:50 " ## " => Disjoint class FiniteSet (S : Type _) (A : outParam (Type _)) extends LawfulSet S A where toList : S → List A @@ -371,13 +371,13 @@ instance : Trans (fun x y : S => x ⊆ y) (·⊆ ·) (·⊆ ·) where /-- Disjoint sets have empty intersection and vice versa. -/ theorem disjoint_intersection {X Y : S} : X ## Y ↔ X ∩ Y = ∅ := by - simp only [Disjoint.disjoint] + simp only [Disjoint] exact ⟨fun H => by ext x; rw [mem_inter]; simp [H, mem_empty], fun H x => by rw [<-mem_inter, H]; exact mem_empty⟩ /-- Disjointness is symmetric. -/ theorem disjoint_comm {s₁ s₂ : S} : s₁ ## s₂ ↔ s₂ ## s₁ := by - simp only [Disjoint.disjoint] + simp only [Disjoint] exact ⟨fun h x ⟨hx1, hx2⟩ => h x ⟨hx2, hx1⟩, fun h x ⟨hx1, hx2⟩ => h x ⟨hx2, hx1⟩⟩ @[symm] @@ -393,7 +393,7 @@ theorem disjoint_empty_right {s : S} : s ## ∅ := by /-- Singleton disjointness. -/ theorem disjoint_singleton_left {s : S} {x : A} : {x} ## s ↔ x ∉ s := by - simp only [Disjoint.disjoint] + simp only [Disjoint] constructor · intro h hx; exact h x ⟨(mem_singleton.mpr rfl), hx⟩ · intro h y ⟨hy1, hy2⟩; rw [mem_singleton] at hy1; subst hy1; exact h hy2 @@ -414,7 +414,7 @@ theorem disjoint_subset_right {s₁ s₂ t : S} : s₁ ⊆ s₂ → t ## s₂ /-- Union is disjoint iff both parts are disjoint. -/ theorem disjoint_union_left {s₁ s₂ t : S} : (s₁ ∪ s₂) ## t ↔ s₁ ## t ∧ s₂ ## t := by - simp only [Disjoint.disjoint] + simp only [Disjoint] constructor · intro h; constructor · exact fun x ⟨hx1, hx2⟩ => h x ⟨(mem_union.mpr (.inl hx1)), hx2⟩ diff --git a/Iris/Iris/Std/List.lean b/Iris/Iris/Std/List.lean index 2cf681e76..18507b28d 100644 --- a/Iris/Iris/Std/List.lean +++ b/Iris/Iris/Std/List.lean @@ -6,7 +6,6 @@ Authors: Zongyuan Liu module public import Iris.Std.FromMathlib -public import Iris.Std.Classes import Batteries.Data.List.Basic import Batteries.Data.List.Perm diff --git a/Iris/Iris/Std/Positives.lean b/Iris/Iris/Std/Positives.lean index 842c6d78e..0f712d4ad 100644 --- a/Iris/Iris/Std/Positives.lean +++ b/Iris/Iris/Std/Positives.lean @@ -5,7 +5,6 @@ Authors: Remy Seassau, Markus de Medeiros, Sergei Stepanenko -/ module -public import Iris.Std.Classes public import Iris.Std.Infinite @[expose] public section diff --git a/Iris/Iris/Std/Rewrite.lean b/Iris/Iris/Std/Rewrite.lean index 992930a03..a2aefa961 100644 --- a/Iris/Iris/Std/Rewrite.lean +++ b/Iris/Iris/Std/Rewrite.lean @@ -5,7 +5,6 @@ Authors: Lars König -/ module -public import Iris.Std.Classes public meta import Iris.Std.Tactic public meta import Lean.Elab.Tactic From 88bea9b8481add73b64b716a6f67b8ae82a1f433 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 15 Jul 2026 15:02:35 +0200 Subject: [PATCH 05/11] Bug fix: `Std/Namespaces.lean` --- Iris/Iris/Std/GenSets.lean | 17 +++++++++++------ Iris/Iris/Std/Namespaces.lean | 4 +++- 2 files changed, 14 insertions(+), 7 deletions(-) diff --git a/Iris/Iris/Std/GenSets.lean b/Iris/Iris/Std/GenSets.lean index 8285d1d0e..bd6be74d8 100644 --- a/Iris/Iris/Std/GenSets.lean +++ b/Iris/Iris/Std/GenSets.lean @@ -67,10 +67,15 @@ instance : HasSubset S := ⟨fun S₁ S₂ => ∀ x, x ∈ S₁ → x ∈ S₂ is in `S₂` but they are not equal. -/ instance : HasSSubset S := ⟨fun S₁ S₂ => S₁ ≠ S₂ ∧ ∀ x, x ∈ S₁ → x ∈ S₂⟩ -def Disjoint (S₁ S₂ : S) : Prop := ∀ x, ¬(x ∈ S₁ ∧ x ∈ S₂) +class Disjoint (α : Type u) where + disjoint : α → α → Prop +export Disjoint (disjoint) /-- Two sets are disjoint if they share no common elements. -/ -infix:50 " ## " => Disjoint +infix:50 " ## " => Disjoint.disjoint + +instance instDisjoint : Disjoint S where + disjoint S₁ S₂ := ∀ x, ¬(x ∈ S₁ ∧ x ∈ S₂) class FiniteSet (S : Type _) (A : outParam (Type _)) extends LawfulSet S A where toList : S → List A @@ -371,13 +376,13 @@ instance : Trans (fun x y : S => x ⊆ y) (·⊆ ·) (·⊆ ·) where /-- Disjoint sets have empty intersection and vice versa. -/ theorem disjoint_intersection {X Y : S} : X ## Y ↔ X ∩ Y = ∅ := by - simp only [Disjoint] + simp only [Disjoint.disjoint] exact ⟨fun H => by ext x; rw [mem_inter]; simp [H, mem_empty], fun H x => by rw [<-mem_inter, H]; exact mem_empty⟩ /-- Disjointness is symmetric. -/ theorem disjoint_comm {s₁ s₂ : S} : s₁ ## s₂ ↔ s₂ ## s₁ := by - simp only [Disjoint] + simp only [Disjoint.disjoint] exact ⟨fun h x ⟨hx1, hx2⟩ => h x ⟨hx2, hx1⟩, fun h x ⟨hx1, hx2⟩ => h x ⟨hx2, hx1⟩⟩ @[symm] @@ -393,7 +398,7 @@ theorem disjoint_empty_right {s : S} : s ## ∅ := by /-- Singleton disjointness. -/ theorem disjoint_singleton_left {s : S} {x : A} : {x} ## s ↔ x ∉ s := by - simp only [Disjoint] + simp only [Disjoint.disjoint] constructor · intro h hx; exact h x ⟨(mem_singleton.mpr rfl), hx⟩ · intro h y ⟨hy1, hy2⟩; rw [mem_singleton] at hy1; subst hy1; exact h hy2 @@ -414,7 +419,7 @@ theorem disjoint_subset_right {s₁ s₂ t : S} : s₁ ⊆ s₂ → t ## s₂ /-- Union is disjoint iff both parts are disjoint. -/ theorem disjoint_union_left {s₁ s₂ t : S} : (s₁ ∪ s₂) ## t ↔ s₁ ## t ∧ s₂ ## t := by - simp only [Disjoint] + simp only [Disjoint.disjoint] constructor · intro h; constructor · exact fun x ⟨hx1, hx2⟩ => h x ⟨(mem_union.mpr (.inl hx1)), hx2⟩ diff --git a/Iris/Iris/Std/Namespaces.lean b/Iris/Iris/Std/Namespaces.lean index 5bfc047e5..7e6120a34 100644 --- a/Iris/Iris/Std/Namespaces.lean +++ b/Iris/Iris/Std/Namespaces.lean @@ -12,6 +12,8 @@ meta import Iris.Std.RocqPorting @[expose] public section +open Iris Std + abbrev Namespace := List Pos instance : DecidableEq Namespace := by infer_instance @@ -37,7 +39,7 @@ instance : Coe Lean.Name Namespace where coe := ofName infix:80 ".@" => ndot -instance ndisjoint : Iris.Std.Disjoint Namespace where +instance ndisjoint : Disjoint Namespace where disjoint N1 N2 := nclose N1 ## nclose N2 theorem nclose_root : ↑nroot = CoPset.full := by rfl From aa5e99e5879e5cc10b7c40ca73f09c5a4be31352 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 15 Jul 2026 15:11:48 +0200 Subject: [PATCH 06/11] Bug fix: `Examples/ClosedProofs.lean` and `HeapLang/PrimitiveLaws.lean` --- Iris/Iris/Examples/ClosedProofs.lean | 2 +- Iris/Iris/HeapLang/PrimitiveLaws.lean | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/Examples/ClosedProofs.lean b/Iris/Iris/Examples/ClosedProofs.lean index 08fc68aaa..cda32cad9 100644 --- a/Iris/Iris/Examples/ClosedProofs.lean +++ b/Iris/Iris/Examples/ClosedProofs.lean @@ -63,7 +63,7 @@ example : True := by icases inv_alloc nroot ⊤ iprop(True) $$ [] with >#Hinv · itrivial imod inv_acc $$ Hinv with ⟨HP, Hcl⟩ - · rw [nclose_root]; exact subset_refl + · rw [nclose_root] imod Hcl $$ HP with HP iapply fupd_mask_intro empty_subset iintro Hcl diff --git a/Iris/Iris/HeapLang/PrimitiveLaws.lean b/Iris/Iris/HeapLang/PrimitiveLaws.lean index 9e1a724c3..31ee62e24 100644 --- a/Iris/Iris/HeapLang/PrimitiveLaws.lean +++ b/Iris/Iris/HeapLang/PrimitiveLaws.lean @@ -561,7 +561,8 @@ theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × · iapply HWPe; iexact Hp ihave HWPe := (show iprop(WP e @ s; E {{ v_e, ∃ pvs', proph p pvs' ∗ ∀ pvs'', ⌜pvs' = (v_e, w) :: pvs''⌝ -∗ proph p pvs'' -∗ Φ v_e }}) ⊢ _ - by rw [wp_unfold.to_eq]; simp only [wp.pre, hne]; exact .rfl) $$ HWPe + by rw [wp_unfold.to_eq]) $$ HWPe + simp only [wp.pre, hne] cases obs using List.reverseRec with | nil => ihave Hσ_e : iprop(stateInterp σ₁ ns ([] ++ obs') nt) $$ [Hheap Hpmap] From 65273e69de26165128ec1a82d86c1e8c77d9e3df Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 23 Jul 2026 18:16:31 +0200 Subject: [PATCH 07/11] Revert previous commits that eliminat `Std/Classes.lean`, only get rid of `Reflexivity`, `Transitivity` and `Preorder` Reverts commits aa5e99e, 88bea9b and 96462af. --- Iris/Iris/BI/BIBase.lean | 1 + Iris/Iris/BI/DerivedLaws.lean | 53 +++++++++++++++------ Iris/Iris/BI/DerivedLawsLater.lean | 1 + Iris/Iris/BI/Instances.lean | 1 + Iris/Iris/Examples/ClosedProofs.lean | 2 +- Iris/Iris/HeapLang/PrimitiveLaws.lean | 3 +- Iris/Iris/Std.lean | 1 + Iris/Iris/Std/Classes.lean | 67 +++++++++++++++++++++++++++ Iris/Iris/Std/CoPset.lean | 6 +-- Iris/Iris/Std/GenMultiSets.lean | 1 + Iris/Iris/Std/GenSets.lean | 9 +--- Iris/Iris/Std/List.lean | 1 + Iris/Iris/Std/Namespaces.lean | 4 +- Iris/Iris/Std/Positives.lean | 1 + Iris/Iris/Std/Rewrite.lean | 1 + 15 files changed, 123 insertions(+), 29 deletions(-) create mode 100644 Iris/Iris/Std/Classes.lean diff --git a/Iris/Iris/BI/BIBase.lean b/Iris/Iris/BI/BIBase.lean index c15dc31f2..48f9f37db 100644 --- a/Iris/Iris/BI/BIBase.lean +++ b/Iris/Iris/BI/BIBase.lean @@ -6,6 +6,7 @@ Authors: Lars König, Mario Carneiro module public meta import Iris.BI.Notation +public import Iris.Std.Classes public meta import Iris.Std.DelabRule public meta import Iris.Std.Rewrite public import Iris.Std.BigOp diff --git a/Iris/Iris/BI/DerivedLaws.lean b/Iris/Iris/BI/DerivedLaws.lean index f108acc91..447aaf4c2 100644 --- a/Iris/Iris/BI/DerivedLaws.lean +++ b/Iris/Iris/BI/DerivedLaws.lean @@ -9,6 +9,7 @@ public import Iris.BI.Classes public import Iris.BI.Extensions public import Iris.BI.BI public import Iris.Std.Nat +public import Iris.Std.Classes public import Iris.Std.Rewrite public import Iris.Std.TC import Iris.Std.RocqPorting @@ -23,7 +24,8 @@ open Iris.Std BI /- Necessary for `calc`-style proofs. -/ instance entails_trans' [BI PROP] : Trans (α := PROP) Entails Entails Entails where trans h1 h2 := h1.trans h2 - +instance entails_antisymm [BI PROP] : Antisymmetric (α := PROP) BiEntails Entails where + antisymm h1 h2 := ⟨h1, h2⟩ #rocq_ignore bi.entails_proper "Derivable from _ne with NonExpansive.eqv." instance equiv_trans [BI PROP] : Trans (α := PROP) BiEntails BiEntails BiEntails where @@ -207,11 +209,13 @@ theorem exists_mono [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ⊢ Ψ a) : theorem exists_congr [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ⊣⊢ Ψ a) : (∃ a, Φ a) ⊣⊢ ∃ a, Ψ a := ⟨exists_mono fun a => (h a).1, exists_mono fun a => (h a).2⟩ -@[rocq_alias bi.and_idem] theorem and_self [BI PROP] {P : PROP} : P ∧ P ⊣⊢ P := ⟨and_elim_l, and_intro .rfl .rfl⟩ +@[rocq_alias bi.and_idem] +instance [BI PROP] : Idempotent (α := PROP) BiEntails and := ⟨and_self⟩ -@[rocq_alias bi.or_idem] theorem or_self [BI PROP] {P : PROP} : P ∨ P ⊣⊢ P := ⟨or_elim .rfl .rfl, or_intro_l⟩ +@[rocq_alias bi.or_idem] +instance [BI PROP] : Idempotent (α := PROP) BiEntails or := ⟨or_self⟩ #rocq_ignore bi.and_mono' "Use and_mono" #rocq_ignore bi.and_flip_mono' "Use and_mono" @@ -226,48 +230,61 @@ theorem or_self [BI PROP] {P : PROP} : P ∨ P ⊣⊢ P := ⟨or_elim .rfl .rfl, @[rocq_alias bi.and_comm] theorem and_comm [BI PROP] {P Q : PROP} : P ∧ Q ⊣⊢ Q ∧ P := ⟨and_symm, and_symm⟩ +instance [BI PROP] : Commutative (α := PROP) BiEntails and := ⟨and_comm⟩ @[rocq_alias bi.or_comm] theorem or_comm [BI PROP] {P Q : PROP} : P ∨ Q ⊣⊢ Q ∨ P := ⟨or_symm, or_symm⟩ +instance [BI PROP] : Commutative (α := PROP) BiEntails or := ⟨or_comm⟩ @[rocq_alias bi.True_and] theorem true_and [BI PROP] {P : PROP} : True ∧ P ⊣⊢ P := ⟨and_elim_r, and_intro (pure_intro trivial) .rfl⟩ +instance [BI PROP] : LeftId (· ⊣⊢@{PROP} ·) iprop(True) and := ⟨true_and⟩ @[rocq_alias bi.and_True] theorem and_true [BI PROP] {P : PROP} : P ∧ True ⊣⊢ P := and_comm.trans true_and +instance [BI PROP] : RightId (· ⊣⊢@{PROP} ·) iprop(True) and := ⟨and_true⟩ @[rocq_alias bi.False_and] theorem false_and [BI PROP] {P : PROP} : False ∧ P ⊣⊢ False := ⟨and_elim_l, false_elim⟩ +instance [BI PROP] : LeftAbsorb (· ⊣⊢@{PROP} ·) iprop(False) and := ⟨false_and⟩ @[rocq_alias bi.and_False] theorem and_false [BI PROP] {P : PROP} : P ∧ False ⊣⊢ False := and_comm.trans false_and +instance [BI PROP] : RightAbsorb (· ⊣⊢@{PROP} ·) iprop(False) and := ⟨and_false⟩ @[rocq_alias bi.True_or] theorem true_or [BI PROP] {P : PROP} : True ∨ P ⊣⊢ True := ⟨true_intro, or_intro_l⟩ +instance [BI PROP] : LeftAbsorb (· ⊣⊢@{PROP} ·) iprop(True) or := ⟨true_or⟩ @[rocq_alias bi.or_True] theorem or_true [BI PROP] {P : PROP} : P ∨ True ⊣⊢ True := or_comm.trans true_or +instance [BI PROP] : RightAbsorb (· ⊣⊢@{PROP} ·) iprop(True) or := ⟨or_true⟩ @[rocq_alias bi.False_or] theorem false_or [BI PROP] {P : PROP} : False ∨ P ⊣⊢ P := ⟨or_elim false_elim .rfl, or_intro_r⟩ +instance [BI PROP] : LeftId (α := PROP) BiEntails iprop(False) or := ⟨false_or⟩ @[rocq_alias bi.or_False] theorem or_false [BI PROP] {P : PROP} : P ∨ False ⊣⊢ P := or_comm.trans false_or +instance [BI PROP] : RightId (α := PROP) BiEntails iprop(False) or := ⟨or_false⟩ @[rocq_alias bi.and_assoc] theorem and_assoc [BI PROP] {P Q R : PROP} : (P ∧ Q) ∧ R ⊣⊢ P ∧ Q ∧ R := ⟨and_intro (and_elim_left_trans and_elim_l) (and_mono_left and_elim_r), and_intro (and_mono_right and_elim_l) (and_elim_right_trans and_elim_r)⟩ +instance [BI PROP] : Associative (α := PROP) BiEntails and := ⟨and_assoc⟩ @[rocq_alias bi.or_assoc] theorem or_assoc [BI PROP] {P Q R : PROP} : (P ∨ Q) ∨ R ⊣⊢ P ∨ Q ∨ R := ⟨or_elim (or_mono_right or_intro_l) (or_intro_right_trans or_intro_r), or_elim (or_intro_left_trans or_intro_l) (or_mono_left or_intro_r)⟩ +instance [BI PROP] : Associative (α := PROP) BiEntails or := ⟨or_assoc⟩ @[rocq_alias bi.True_impl] theorem true_imp [BI PROP] {P : PROP} : (True → P) ⊣⊢ P := ⟨and_true.2.trans imp_elim_left, imp_intro and_elim_l⟩ +instance [BI PROP] : LeftId (· ⊣⊢@{PROP} ·) iprop(True) imp := ⟨true_imp⟩ @[rocq_alias bi.impl_refl] theorem imp_self [BI PROP] {P Q : PROP} : Q ⊢ P → P := imp_intro and_elim_r @@ -373,7 +390,7 @@ instance bi_and_monoid [BI PROP] : LawfulBigOp and (iprop(True) : PROP) BiEntail trans h1 h2 := h1.trans h2 comm := and_comm assoc := and_assoc - left_id := true_and + left_id := left_id congr_l := and_congr_left /-! # BI -/ @@ -418,11 +435,13 @@ theorem wand_congr_right [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : (P -∗ Q @[rocq_alias bi.sep_comm] theorem sep_comm [BI PROP] {P Q : PROP} : P ∗ Q ⊣⊢ Q ∗ P := ⟨sep_symm, sep_symm⟩ +instance [BI PROP] : Commutative (α := PROP) BiEntails sep := ⟨sep_comm⟩ @[rocq_alias bi.sep_assoc] theorem sep_assoc [BI PROP] {P Q R : PROP} : (P ∗ Q) ∗ R ⊣⊢ P ∗ Q ∗ R := ⟨sep_assoc_l, (sep_comm.trans <| sep_congr_left sep_comm).1.trans <| sep_assoc_l.trans (sep_comm.trans <| sep_congr_right sep_comm).2⟩ +instance [BI PROP] : Associative (α := PROP) BiEntails sep := ⟨sep_assoc⟩ theorem sep_left_comm [BI PROP] {P Q R : PROP} : P ∗ Q ∗ R ⊣⊢ Q ∗ P ∗ R := sep_assoc.symm.trans <| (sep_congr_left sep_comm).trans sep_assoc @@ -433,10 +452,12 @@ theorem sep_right_comm [BI PROP] {P Q R : PROP} : (P ∗ Q) ∗ R ⊣⊢ (P ∗ theorem sep_sep_sep_comm [BI PROP] {P Q R S : PROP} : (P ∗ Q) ∗ (R ∗ S) ⊣⊢ (P ∗ R) ∗ (Q ∗ S) := sep_assoc.trans <| (sep_congr_right sep_left_comm).trans sep_assoc.symm -#rocq_ignore bi.emp_sep "The type class LeftId in Lean is not general enough" +@[rocq_alias bi.emp_sep] +instance [BI PROP] : LeftId (α := PROP) BiEntails emp sep := ⟨emp_sep⟩ -@[rocq_alias bi.sep_emp] theorem sep_emp [BI PROP] {P : PROP} : P ∗ emp ⊣⊢ P := sep_comm.trans emp_sep +@[rocq_alias bi.sep_emp] +instance [BI PROP] : RightId (α := PROP) BiEntails emp sep := ⟨sep_emp⟩ @[rocq_alias bi.bi_sep_monoid] instance bi_sep_monoid [BI PROP] : LawfulBigOp sep (emp : PROP) BiEntails where @@ -445,7 +466,7 @@ instance bi_sep_monoid [BI PROP] : LawfulBigOp sep (emp : PROP) BiEntails where trans h1 h2 := h1.trans h2 comm := sep_comm assoc := sep_assoc - left_id := emp_sep + left_id := left_id congr_l := sep_congr_left @[rocq_alias bi.True_sep_2] @@ -466,12 +487,16 @@ theorem wand_elim_swap [BI PROP] {P Q R : PROP} (h : Q ⊢ P -∗ R) : P ∗ Q @[rocq_alias bi.wand_elim_l] theorem wand_elim_left [BI PROP] {P Q : PROP} : (P -∗ Q) ∗ P ⊢ Q := wand_elim .rfl -@[rocq_alias bi.False_sep] theorem false_sep [BI PROP] {P : PROP} : False ∗ P ⊣⊢ False := ⟨(sep_mono_left (P' := iprop(P -∗ False)) false_elim).trans wand_elim_left, false_elim⟩ +@[rocq_alias bi.False_sep] +instance [BI PROP] : LeftAbsorb (· ⊣⊢@{PROP} ·) iprop(False) sep where + left_absorb := false_sep -@[rocq_alias bi.sep_False] theorem sep_false [BI PROP] {P : PROP} : P ∗ False ⊣⊢ False := sep_comm.trans false_sep +@[rocq_alias bi.sep_False] +instance [BI PROP] : RightAbsorb (· ⊣⊢@{PROP} ·) iprop(False) sep where + right_absorb := sep_false @[rocq_alias bi.wand_elim_r] theorem wand_elim_right [BI PROP] {P Q : PROP} : P ∗ (P -∗ Q) ⊢ Q := wand_elim_swap .rfl @@ -1002,13 +1027,13 @@ theorem affinely_intro [BI PROP] {P Q : PROP} [Affine P] (h : P ⊢ Q) : P ⊢ < @[rocq_alias bi.emp_and] theorem emp_and [BI PROP] {P : PROP} [Affine P] : emp ∧ P ⊣⊢ P := ⟨and_elim_r, and_intro affine .rfl⟩ - -#rocq_ignore bi.emp_and' "The type class LeftId in Lean is not general enough" +@[rocq_alias bi.emp_and'] +instance emp_and_biaffine [BI PROP] [BIAffine PROP] : LeftId (α := PROP) BiEntails emp and := ⟨emp_and⟩ @[rocq_alias bi.and_emp] theorem and_emp [BI PROP] {P : PROP} [Affine P] : P ∧ emp ⊣⊢ P := and_comm.trans emp_and - -#rocq_ignore bi.and_emp' "The type class RightId in Lean is not general enough" +@[rocq_alias bi.and_emp'] +instance and_emp_biaffine [BI PROP] [BIAffine PROP] : RightId (α := PROP) BiEntails emp and := ⟨and_emp⟩ @[rocq_alias bi.emp_or] theorem emp_or [BI PROP] {P : PROP} [Affine P] : emp ∨ P ⊣⊢ emp := ⟨or_elim .rfl affine, or_intro_l⟩ @@ -1033,12 +1058,14 @@ instance [BI PROP] [BIAffine PROP] (P : PROP) : Absorbing P where @[rocq_alias bi.True_sep] theorem true_sep [BI PROP] {P : PROP} [Absorbing P] : True ∗ P ⊣⊢ P := ⟨absorbing, true_sep_mpr⟩ +instance [BI PROP] [BIAffine PROP] : LeftId (α := PROP) BiEntails iprop(True) sep := ⟨true_sep⟩ @[rocq_alias bi.True_sep'] theorem true_sep_flip [BI PROP] {P : PROP} [Absorbing P] : P ⊣⊢ True ∗ P := true_sep.symm @[rocq_alias bi.sep_True] theorem sep_true [BI PROP] {P : PROP} [Absorbing P] : P ∗ True ⊣⊢ P := sep_comm.trans true_sep +instance [BI PROP] [BIAffine PROP] : RightId (α := PROP) BiEntails iprop(True) sep := ⟨sep_true⟩ @[rocq_alias bi.sep_True'] theorem sep_true_flip [BI PROP] {P : PROP} [Absorbing P] : P ⊣⊢ P ∗ True := diff --git a/Iris/Iris/BI/DerivedLawsLater.lean b/Iris/Iris/BI/DerivedLawsLater.lean index 6e963755f..3bc9ff86f 100644 --- a/Iris/Iris/BI/DerivedLawsLater.lean +++ b/Iris/Iris/BI/DerivedLawsLater.lean @@ -10,6 +10,7 @@ public import Iris.BI.Extensions public import Iris.BI.BI public import Iris.BI.DerivedLaws public import Iris.BI.BigOp.BigOp +public import Iris.Std.Classes public import Iris.Std.Rewrite public import Iris.Std.TC public import Iris.Std.RocqPorting diff --git a/Iris/Iris/BI/Instances.lean b/Iris/Iris/BI/Instances.lean index c057a3b86..b9e330ed0 100644 --- a/Iris/Iris/BI/Instances.lean +++ b/Iris/Iris/BI/Instances.lean @@ -9,6 +9,7 @@ public import Iris.BI.Classes public import Iris.BI.DerivedLaws public import Iris.BI.Extensions public import Iris.BI.BI +public import Iris.Std.Classes @[expose] public section diff --git a/Iris/Iris/Examples/ClosedProofs.lean b/Iris/Iris/Examples/ClosedProofs.lean index cda32cad9..08fc68aaa 100644 --- a/Iris/Iris/Examples/ClosedProofs.lean +++ b/Iris/Iris/Examples/ClosedProofs.lean @@ -63,7 +63,7 @@ example : True := by icases inv_alloc nroot ⊤ iprop(True) $$ [] with >#Hinv · itrivial imod inv_acc $$ Hinv with ⟨HP, Hcl⟩ - · rw [nclose_root] + · rw [nclose_root]; exact subset_refl imod Hcl $$ HP with HP iapply fupd_mask_intro empty_subset iintro Hcl diff --git a/Iris/Iris/HeapLang/PrimitiveLaws.lean b/Iris/Iris/HeapLang/PrimitiveLaws.lean index 31ee62e24..9e1a724c3 100644 --- a/Iris/Iris/HeapLang/PrimitiveLaws.lean +++ b/Iris/Iris/HeapLang/PrimitiveLaws.lean @@ -561,8 +561,7 @@ theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × · iapply HWPe; iexact Hp ihave HWPe := (show iprop(WP e @ s; E {{ v_e, ∃ pvs', proph p pvs' ∗ ∀ pvs'', ⌜pvs' = (v_e, w) :: pvs''⌝ -∗ proph p pvs'' -∗ Φ v_e }}) ⊢ _ - by rw [wp_unfold.to_eq]) $$ HWPe - simp only [wp.pre, hne] + by rw [wp_unfold.to_eq]; simp only [wp.pre, hne]; exact .rfl) $$ HWPe cases obs using List.reverseRec with | nil => ihave Hσ_e : iprop(stateInterp σ₁ ns ([] ++ obs') nt) $$ [Hheap Hpmap] diff --git a/Iris/Iris/Std.lean b/Iris/Iris/Std.lean index 6c57ffdca..6539947bf 100644 --- a/Iris/Iris/Std.lean +++ b/Iris/Iris/Std.lean @@ -1,5 +1,6 @@ module +public import Iris.Std.Classes public import Iris.Std.Expr public import Iris.Std.HeapInstances public import Iris.Std.Infinite diff --git a/Iris/Iris/Std/Classes.lean b/Iris/Iris/Std/Classes.lean new file mode 100644 index 000000000..acec5521b --- /dev/null +++ b/Iris/Iris/Std/Classes.lean @@ -0,0 +1,67 @@ +/- +Copyright (c) 2022 Lars König. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lars König +-/ +module + +@[expose] public section + +namespace Iris.Std + +/-- Represents a binary relation with two arguments of the same type `α`. -/ +abbrev Relation (α : Type _) := α → α → Prop + +/-- Require that a type `α` has a distinguished top element. -/ +class Top (α : Type u) where + top : α +export Top (top) + +notation "⊤" => top + +/-- Require that a binary function `f` on `α` is idempotent in a relation `R` on `α`. -/ +class Idempotent (R : Relation α) (f : α → α → α) where + idem {x : α} : R (f x x) x +export Idempotent (idem) + +/-- Require that a binary function `f` from `β` to `α` is commutative in a relation `R` on `α`. -/ +class Commutative (R : Relation α) (f : β → β → α) where + comm {x y : β} : R (f x y) (f y x) +export Commutative (comm) + +/-- Require that an element `i` of `α` is the left unit of a binary function `f` on `α` in a +relation `R` on `α`. -/ +class LeftId (R : Relation α) (i : α) (f : α → α → α) where + left_id {x : α} : R (f i x) x +export LeftId (left_id) + +/-- Require that an element `i` of `α` is the right unit of a binary function `f` on `α` in a +relation `R` on `α`. -/ +class RightId (R : Relation α) (i : α) (f : α → α → α) where + right_id {x : α} : R (f x i) x +export RightId (right_id) + +class LeftAbsorb (R : Relation α) (i : α) (f : α → α → α) where + left_absorb {x : α} : R (f i x) i +export LeftAbsorb (left_absorb) + +class RightAbsorb (R : Relation α) (i : α) (f : α → α → α) where + right_absorb {x : α} : R (f x i) i +export RightAbsorb (right_absorb) + +/-- Require that a binary function `f` on `α` is associative in a relation `R` on `α`. -/ +class Associative (R : Relation α) (f : α → α → α) where + assoc {x y z : α} : R (f (f x y) z) (f x (f y z)) +export Associative (assoc) + +/-- Require that a relation `S` on `α` is antisymmetrical with `R` as its equivalence relation. -/ +class Antisymmetric (R : Relation α) (S : outParam <| Relation α) where + antisymm {x y : α} : (left : S x y) → (right : S y x) → R x y +export Antisymmetric (antisymm) + +class Disjoint (α : Type u) where + disjoint : α -> α -> Prop +export Disjoint (disjoint) +infix:50 " ## " => Disjoint.disjoint + +end Iris.Std diff --git a/Iris/Iris/Std/CoPset.lean b/Iris/Iris/Std/CoPset.lean index 06cfbae43..c860d2776 100644 --- a/Iris/Iris/Std/CoPset.lean +++ b/Iris/Iris/Std/CoPset.lean @@ -6,6 +6,7 @@ Authors: Remy Seassau, Markus de Medeiros, Sergei Stepanenko module public import Iris.Std.Positives +public import Iris.Std.Classes public import Iris.Std.GenSets import Iris.Std.List @@ -219,6 +220,8 @@ instance : EmptyCollection CoPset where emptyCollection := CoPset.empty def full : CoPset := ⟨CoPsetRaw.leaf true, rfl⟩ +instance : Iris.Std.Top CoPset where top := CoPset.full + @[simp] def singleton (p : Pos) : CoPset := ⟨CoPsetRaw.Singleton p, coPsetSingleton_wf p⟩ instance : Singleton Pos CoPset where @@ -252,9 +255,6 @@ theorem mem_empty {p : Pos} : p ∉ (∅ : CoPset) := by theorem mem_full {p : Pos} : p ∈ full := by simp only [Membership.mem, full, CoPsetRaw.ElemOf] -/-- `CoPset.full` is the top element in the type `CoPset`. -/ -notation "⊤" => CoPset.full - @[simp] theorem subseteq_top {X : CoPset} : X ⊆ ⊤ := λ _ _ => mem_full diff --git a/Iris/Iris/Std/GenMultiSets.lean b/Iris/Iris/Std/GenMultiSets.lean index beb8330dd..2751a727a 100644 --- a/Iris/Iris/Std/GenMultiSets.lean +++ b/Iris/Iris/Std/GenMultiSets.lean @@ -5,6 +5,7 @@ Authors: Haokun Li -/ module +public import Iris.Std.Classes public import Iris.Std.GenSets public import Batteries.Data.List.Perm diff --git a/Iris/Iris/Std/GenSets.lean b/Iris/Iris/Std/GenSets.lean index bd6be74d8..3c40aa10b 100644 --- a/Iris/Iris/Std/GenSets.lean +++ b/Iris/Iris/Std/GenSets.lean @@ -5,6 +5,7 @@ Authors: Zongyuan Liu, Sergei Stepanenko -/ module +public import Iris.Std.Classes public import Iris.Std.Infinite import Batteries.Data.List.Perm import Iris.Std.List @@ -67,14 +68,8 @@ instance : HasSubset S := ⟨fun S₁ S₂ => ∀ x, x ∈ S₁ → x ∈ S₂ is in `S₂` but they are not equal. -/ instance : HasSSubset S := ⟨fun S₁ S₂ => S₁ ≠ S₂ ∧ ∀ x, x ∈ S₁ → x ∈ S₂⟩ -class Disjoint (α : Type u) where - disjoint : α → α → Prop -export Disjoint (disjoint) - /-- Two sets are disjoint if they share no common elements. -/ -infix:50 " ## " => Disjoint.disjoint - -instance instDisjoint : Disjoint S where +instance : Disjoint S where disjoint S₁ S₂ := ∀ x, ¬(x ∈ S₁ ∧ x ∈ S₂) class FiniteSet (S : Type _) (A : outParam (Type _)) extends LawfulSet S A where diff --git a/Iris/Iris/Std/List.lean b/Iris/Iris/Std/List.lean index 18507b28d..2cf681e76 100644 --- a/Iris/Iris/Std/List.lean +++ b/Iris/Iris/Std/List.lean @@ -6,6 +6,7 @@ Authors: Zongyuan Liu module public import Iris.Std.FromMathlib +public import Iris.Std.Classes import Batteries.Data.List.Basic import Batteries.Data.List.Perm diff --git a/Iris/Iris/Std/Namespaces.lean b/Iris/Iris/Std/Namespaces.lean index 7e6120a34..5bfc047e5 100644 --- a/Iris/Iris/Std/Namespaces.lean +++ b/Iris/Iris/Std/Namespaces.lean @@ -12,8 +12,6 @@ meta import Iris.Std.RocqPorting @[expose] public section -open Iris Std - abbrev Namespace := List Pos instance : DecidableEq Namespace := by infer_instance @@ -39,7 +37,7 @@ instance : Coe Lean.Name Namespace where coe := ofName infix:80 ".@" => ndot -instance ndisjoint : Disjoint Namespace where +instance ndisjoint : Iris.Std.Disjoint Namespace where disjoint N1 N2 := nclose N1 ## nclose N2 theorem nclose_root : ↑nroot = CoPset.full := by rfl diff --git a/Iris/Iris/Std/Positives.lean b/Iris/Iris/Std/Positives.lean index 0f712d4ad..842c6d78e 100644 --- a/Iris/Iris/Std/Positives.lean +++ b/Iris/Iris/Std/Positives.lean @@ -5,6 +5,7 @@ Authors: Remy Seassau, Markus de Medeiros, Sergei Stepanenko -/ module +public import Iris.Std.Classes public import Iris.Std.Infinite @[expose] public section diff --git a/Iris/Iris/Std/Rewrite.lean b/Iris/Iris/Std/Rewrite.lean index a2aefa961..992930a03 100644 --- a/Iris/Iris/Std/Rewrite.lean +++ b/Iris/Iris/Std/Rewrite.lean @@ -5,6 +5,7 @@ Authors: Lars König -/ module +public import Iris.Std.Classes public meta import Iris.Std.Tactic public meta import Lean.Elab.Tactic From 2963dad31fbe7c677acadf90ef824d49e7751e31 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 23 Jul 2026 19:20:36 +0200 Subject: [PATCH 08/11] Bug fix: `Trans` too general --- Iris/Iris/Std/Classes.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Iris/Iris/Std/Classes.lean b/Iris/Iris/Std/Classes.lean index acec5521b..3296649f7 100644 --- a/Iris/Iris/Std/Classes.lean +++ b/Iris/Iris/Std/Classes.lean @@ -19,6 +19,8 @@ export Top (top) notation "⊤" => top +def trans [Trans R R R] : R a b → R b c → R a c := Trans.trans + /-- Require that a binary function `f` on `α` is idempotent in a relation `R` on `α`. -/ class Idempotent (R : Relation α) (f : α → α → α) where idem {x : α} : R (f x x) x From 8b948322a8e24a0e503435777a3481242b589746 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 24 Jul 2026 09:53:19 +0200 Subject: [PATCH 09/11] Bug fix --- Iris/Iris/HeapLang/PrimitiveLaws.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Iris/Iris/HeapLang/PrimitiveLaws.lean b/Iris/Iris/HeapLang/PrimitiveLaws.lean index b696b2d27..f94174b15 100644 --- a/Iris/Iris/HeapLang/PrimitiveLaws.lean +++ b/Iris/Iris/HeapLang/PrimitiveLaws.lean @@ -559,11 +559,12 @@ theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × · iapply HWPe; iexact Hp ihave HWPe := (show iprop(WP e @ s; E {{ v_e, ∃ pvs', proph p pvs' ∗ ∀ pvs'', ⌜pvs' = (v_e, w) :: pvs''⌝ -∗ proph p pvs'' -∗ Φ v_e }}) ⊢ _ - by rw [wp_unfold.to_eq]; simp only [wp.pre, hne]; exact .rfl) $$ HWPe + by rw [wp_unfold.to_eq]) $$ HWPe cases obs using List.reverseRec with | nil => ihave Hσ_e : iprop(stateInterp σ₁ ns ([] ++ obs') nt) $$ [Hheap Hpmap] · iapply (stateInterp_split σ₁ ns ([] ++ obs') nt).mpr; iframe Hheap; iexact Hpmap + simp only [wp.pre, hne] imod HWPe $$ %_ %_ %_ %_ %_ Hσ_e with ⟨%Hred_e, _⟩ imodintro isplitr @@ -578,6 +579,7 @@ theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × ihave Hσ_e : iprop(stateInterp σ₁ ns (init ++ (lastObs :: obs')) nt) $$ [Hheap Hpmap] · iapply (stateInterp_split σ₁ ns (init ++ (lastObs :: obs')) nt).mpr iframe Hheap; rw [← hassoc]; iexact Hpmap + simp only [wp.pre, hne] imod HWPe $$ %_ %_ %_ %_ %_ Hσ_e with ⟨%Hred_e, HWPe⟩ imodintro isplitr From a95d97dd76fcf5568c52500c58be6b15a0365879 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 24 Jul 2026 13:38:49 +0200 Subject: [PATCH 10/11] Remove unnecessary spaces and comments --- Iris/Iris/BI/MonPred.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Iris/Iris/BI/MonPred.lean b/Iris/Iris/BI/MonPred.lean index eb21829ff..74e5a33d9 100644 --- a/Iris/Iris/BI/MonPred.lean +++ b/Iris/Iris/BI/MonPred.lean @@ -43,10 +43,7 @@ predicates are functions out of a `BiIndex` that are monotone w.r.t. this order. structure BiIndex where car : Type _ [inhabited : Inhabited car] - -- rel : car → car → Prop - rel : LE car - [preorder : Std.IsPreorder car] attribute [instance] BiIndex.inhabited BiIndex.preorder From 57563f631539d792b732294b3f422474d8a8484a Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 24 Jul 2026 15:48:56 +0200 Subject: [PATCH 11/11] Eliminate the redundant `trans` theorem --- Iris/Iris/Std/Classes.lean | 2 -- Iris/Iris/Std/Rewrite.lean | 9 +++++---- Iris/Iris/Std/Tactic.lean | 12 ++++++------ 3 files changed, 11 insertions(+), 12 deletions(-) diff --git a/Iris/Iris/Std/Classes.lean b/Iris/Iris/Std/Classes.lean index 3296649f7..acec5521b 100644 --- a/Iris/Iris/Std/Classes.lean +++ b/Iris/Iris/Std/Classes.lean @@ -19,8 +19,6 @@ export Top (top) notation "⊤" => top -def trans [Trans R R R] : R a b → R b c → R a c := Trans.trans - /-- Require that a binary function `f` on `α` is idempotent in a relation `R` on `α`. -/ class Idempotent (R : Relation α) (f : α → α → α) where idem {x : α} : R (f x x) x diff --git a/Iris/Iris/Std/Rewrite.lean b/Iris/Iris/Std/Rewrite.lean index 992930a03..4af1b3378 100644 --- a/Iris/Iris/Std/Rewrite.lean +++ b/Iris/Iris/Std/Rewrite.lean @@ -118,7 +118,8 @@ private partial def rewriteTMR where applyTransitivity (goal : MVarId) : TacticM <| Option <| MVarId × MVarId := do try - let some <| goalL :: goalR :: [] ← apply' goal ``trans + let some <| goalL :: goalR :: [] ← apply' goal (← `((Trans.trans : + ∀ {α} {r} [Trans r r r] {a b c : α}, r a b → r b c → r a c))) | return none return some (goalL, goalR) catch _ => @@ -127,7 +128,7 @@ where applyMonotonicity (goal : MVarId) : TacticM <| Option <| List MVarId := do for rule in (← getMonotonicityRules) do try - if let some goals ← apply' goal rule then + if let some goals ← apply' goal (mkCIdent rule) then return ← goals.mapM normalizeGoal catch _ => continue @@ -135,7 +136,7 @@ where applyReflexivity (goal : MVarId) : TacticM Unit := do try - discard <| apply' goal ``Std.Refl.refl + discard <| apply' goal (← `(Std.Refl.refl)) catch _ => pure () go (goal : MVarId) (rule : TSyntax `term) : TacticM Bool := do @@ -194,7 +195,7 @@ elab "rw' " "[" rules:rwRule',*,? "]" : tactic => do withoutRecover <| evalTactic (← `(tactic| try first | rfl - | exact refl + | exact Std.Refl.refl _ )) end Iris.Std diff --git a/Iris/Iris/Std/Tactic.lean b/Iris/Iris/Std/Tactic.lean index b2da2bac0..4eed9fd64 100644 --- a/Iris/Iris/Std/Tactic.lean +++ b/Iris/Iris/Std/Tactic.lean @@ -13,13 +13,13 @@ public meta section namespace Iris.Std open Lean Lean.Elab.Tactic Lean.Meta -/-- Apply the theorem with the name `name` to the goal `goal`. The flag `recover` is set to `false` +/-- +Apply the theorem expressed by `term` to the goal `goal`. The flag `recover` is set to `false` and the transparency mode is set to `reducible`. Only non-dependent arguments of the applied -theorem are turned into goals. -/ -def apply' (goal : MVarId) (name : Name) : TacticM <| Option <| List MVarId := do - unless (← getEnv).contains name do return none - let value ← mkConstWithFreshMVarLevels name -- reference, not body; needs only the type - +theorem are turned into goals. +-/ +def apply' (goal : MVarId) (term : Term) : TacticM <| Option <| List MVarId := do + let value ← goal.withContext <| elabTermForApply term let goals ← withoutRecover <| withReducible <| goal.apply value { newGoals := .nonDependentOnly } setGoals <| goals ++ (← getUnsolvedGoals) return goals