refactor: remove duplicate type classes in Iris/Std/Classes.lean and reuse definitions from core libraries

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) :

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 : Preorder Entails
+  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,12 +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 :=
-  Transitive.trans h1 h2
+  BI.entails_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 := BI.entails_refl
 
 theorem BIBase.Entails.of_eq [BI PROP] {P Q : PROP} (h : P = Q) : P ⊢ Q := h ▸ .rfl
 

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 => refl
+  | false, false => by rfl
   | false, true  => sep_mono_right intuitionisticallyIf_elim
   | true,  false => sep_mono_left intuitionisticallyIf_elim
   | true,  true  => intuitionisticallyIf_sep_mpr

Iris/Iris/BI/SIProp.lean

@@ -153,15 +153,16 @@ 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 _ h := h
-  trans h₁ h₂ n h := h₂ n (h₁ n h)
+instance siPropPreorder : Std.IsPreorder SiProp where
+  le_refl _ _ := id
+  le_trans _ _ _ h₁ h₂ n h := h₂ n (h₁ n h)
 
 /-! ## BI instance -/
 
 @[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⟩

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

Iris/Iris/Instances/Classical/Instance.lean

@@ -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 heapPropPreorder : 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 σ
@@ -47,9 +45,10 @@ instance : Std.Preorder (Entails (PROP := 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 ▸ ⟨refl, refl⟩,
+    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₂ σ⟩)
   ⟩
 

Iris/Iris/Instances/UPred/Instance.lean

@@ -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) :
@@ -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.refl
-  persistently_and_2 := Std.refl
+  persistently_emp_2 := uPred_entails_preorder.le_refl emp
+  persistently_and_2 {P Q} := uPred_entails_preorder.le_refl iprop(<pers> P ∧ <pers> Q)
   persistently_sExists_1 _ _ := fun ⟨p, HΨ, H⟩ => by
     refine ⟨iprop(<pers> p), ⟨p, ?_⟩, H⟩
     ext; exact and_iff_right HΨ

Iris/Iris/ProofMode/Instances.lean

@@ -862,7 +862,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)

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 ∗ <pers> out) := and_intro refl <| sep_mono_right pf3
+    _ ⊢ (e2 ∗ □?p1 out1 ∗ □?p2 out2) ∧ (e2 ∗ <pers> out) := and_intro .rfl <| sep_mono_right pf3
     _ ⊢ (e2 ∗ □?p1 out1 ∗ □?p2 out2) ∧ <pers> 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}
     _ ⊢ <pers> newOutGives           := persistently_absorb_right
   calc
     _ ⊢ e ∗ □ outGives                                          := pf1
-    _ ⊢ (e ∗ □ outGives) ∧ <pers> outGives ∧ <pers> newOutGives := and_intro refl <| and_intro pf4 pf5
+    _ ⊢ (e ∗ □ outGives) ∧ <pers> outGives ∧ <pers> newOutGives := and_intro .rfl <| and_intro pf4 pf5
     _ ⊢ (e ∗ □ outGives) ∧ <pers> (outGives ∧ newOutGives)      := and_mono_right <| persistently_and.mpr
     _ ⊢ (e ∗ □ outGives) ∧ <pers> outGivesCombined              := and_mono_right <| persistently_mono instGivesCombined.make_and.mp
     _ ⊢ (e ∗ □ outGives) ∗ □ outGivesCombined                   := persistently_and_intuitionistically_sep_right.mp

Iris/Iris/Std/Classes.lean

@@ -19,20 +19,6 @@ 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
-
-
 /-- 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

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
 
@@ -159,9 +158,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
 

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,15 +128,15 @@ 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
     return none
 
   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
@@ -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

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