Revert previous commits that eliminat Std/Classes.lean, only get rid of Reflexivity, Transitivity and Preorder

Reverts commits aa5e99e, 88bea9b and 96462af.

Author: alvinylt

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

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

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

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
 

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

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]

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

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

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
 

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