Generalize monoid/big-op homomorphisms to ordered monoids.

theories/algebra/auth.v

@@ -207,8 +207,9 @@ Proof. done. Qed.
 Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
 Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
 
-Global Instance auth_frag_sep_homomorphism : MonoidHomomorphism op op (Auth None).
-Proof. done. Qed.
+Global Instance auth_frag_sep_homomorphism :
+  MonoidHomomorphism op op (≡) (Auth None).
+Proof. by split; [split; try apply _|]. Qed.
 
 Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
 Proof. by rewrite /op /auth_op /= left_id. Qed.

theories/algebra/big_op.v

 From iris.algebra Require Export monoid.
-From stdpp Require Import functions gmap gmultiset.
+From stdpp Require Export functions gmap gmultiset.
 Set Default Proof Using "Type*".
 Local Existing Instances monoid_ne monoid_assoc monoid_comm
   monoid_left_id monoid_right_id monoid_proper
+  monoid_homomorphism_rel_po monoid_homomorphism_rel_proper
+  monoid_homomorphism_op_proper
   monoid_homomorphism_ne weak_monoid_homomorphism_proper.
 
 (** We define the following big operators with binders build in:
@@ -399,35 +401,36 @@ Section homomorphisms.
   Context `{Monoid M1 o1, Monoid M2 o2}.
   Infix "`o1`" := o1 (at level 50, left associativity).
   Infix "`o2`" := o2 (at level 50, left associativity).
+  Instance foo {A} (R : relation A) : RewriteRelation R.
 
-  Lemma big_opL_commute {A} (h : M1 → M2) `{!MonoidHomomorphism o1 o2 h}
+  Lemma big_opL_commute {A} (h : M1 → M2) `{!MonoidHomomorphism o1 o2 R h}
       (f : nat → A → M1) l :
-    h ([^o1 list] k↦x ∈ l, f k x) ≡ ([^o2 list] k↦x ∈ l, h (f k x)).
+    R (h ([^o1 list] k↦x ∈ l, f k x)) ([^o2 list] k↦x ∈ l, h (f k x)).
   Proof.
     revert f. induction l as [|x l IH]=> f /=.
-    - by rewrite monoid_homomorphism_unit.
-    - by rewrite monoid_homomorphism -IH.
+    - apply monoid_homomorphism_unit.
+    - by rewrite monoid_homomorphism IH.
   Qed.
-  Lemma big_opL_commute1 {A} (h : M1 → M2) `{!WeakMonoidHomomorphism o1 o2 h}
+  Lemma big_opL_commute1 {A} (h : M1 → M2) `{!WeakMonoidHomomorphism o1 o2 R h}
       (f : nat → A → M1) l :
-    l ≠ [] → h ([^o1 list] k↦x ∈ l, f k x) ≡ ([^o2 list] k↦x ∈ l, h (f k x)).
+    l ≠ [] → R (h ([^o1 list] k↦x ∈ l, f k x)) ([^o2 list] k↦x ∈ l, h (f k x)).
   Proof.
     intros ?. revert f. induction l as [|x [|x' l'] IH]=> f //.
     - by rewrite !big_opL_singleton.
-    - by rewrite !(big_opL_cons _ x) monoid_homomorphism -IH.
+    - by rewrite !(big_opL_cons _ x) monoid_homomorphism IH.
   Qed.
 
   Lemma big_opM_commute `{Countable K} {A} (h : M1 → M2)
-      `{!MonoidHomomorphism o1 o2 h} (f : K → A → M1) m :
-    h ([^o1 map] k↦x ∈ m, f k x) ≡ ([^o2 map] k↦x ∈ m, h (f k x)).
+      `{!MonoidHomomorphism o1 o2 R h} (f : K → A → M1) m :
+    R (h ([^o1 map] k↦x ∈ m, f k x)) ([^o2 map] k↦x ∈ m, h (f k x)).
   Proof.
     intros. induction m as [|i x m ? IH] using map_ind.
     - by rewrite !big_opM_empty monoid_homomorphism_unit.
     - by rewrite !big_opM_insert // monoid_homomorphism -IH.
   Qed.
   Lemma big_opM_commute1 `{Countable K} {A} (h : M1 → M2)
-      `{!WeakMonoidHomomorphism o1 o2 h} (f : K → A → M1) m :
-    m ≠ ∅ → h ([^o1 map] k↦x ∈ m, f k x) ≡ ([^o2 map] k↦x ∈ m, h (f k x)).
+      `{!WeakMonoidHomomorphism o1 o2 R h} (f : K → A → M1) m :
+    m ≠ ∅ → R (h ([^o1 map] k↦x ∈ m, f k x)) ([^o2 map] k↦x ∈ m, h (f k x)).
   Proof.
     intros. induction m as [|i x m ? IH] using map_ind; [done|].
     destruct (decide (m = ∅)) as [->|].
@@ -436,16 +439,16 @@ Section homomorphisms.
   Qed.
 
   Lemma big_opS_commute `{Countable A} (h : M1 → M2)
-      `{!MonoidHomomorphism o1 o2 h} (f : A → M1) X :
-    h ([^o1 set] x ∈ X, f x) ≡ ([^o2 set] x ∈ X, h (f x)).
+      `{!MonoidHomomorphism o1 o2 R h} (f : A → M1) X :
+    R (h ([^o1 set] x ∈ X, f x)) ([^o2 set] x ∈ X, h (f x)).
   Proof.
     intros. induction X as [|x X ? IH] using collection_ind_L.
     - by rewrite !big_opS_empty monoid_homomorphism_unit.
     - by rewrite !big_opS_insert // monoid_homomorphism -IH.
   Qed.
   Lemma big_opS_commute1 `{Countable A} (h : M1 → M2)
-      `{!WeakMonoidHomomorphism o1 o2 h} (f : A → M1) X :
-    X ≠ ∅ → h ([^o1 set] x ∈ X, f x) ≡ ([^o2 set] x ∈ X, h (f x)).
+      `{!WeakMonoidHomomorphism o1 o2 R h} (f : A → M1) X :
+    X ≠ ∅ → R (h ([^o1 set] x ∈ X, f x)) ([^o2 set] x ∈ X, h (f x)).
   Proof.
     intros. induction X as [|x X ? IH] using collection_ind_L; [done|].
     destruct (decide (X = ∅)) as [->|].
@@ -454,16 +457,16 @@ Section homomorphisms.
   Qed.
 
   Lemma big_opMS_commute `{Countable A} (h : M1 → M2)
-      `{!MonoidHomomorphism o1 o2 h} (f : A → M1) X :
-    h ([^o1 mset] x ∈ X, f x) ≡ ([^o2 mset] x ∈ X, h (f x)).
+      `{!MonoidHomomorphism o1 o2 R h} (f : A → M1) X :
+    R (h ([^o1 mset] x ∈ X, f x)) ([^o2 mset] x ∈ X, h (f x)).
   Proof.
     intros. induction X as [|x X IH] using gmultiset_ind.
     - by rewrite !big_opMS_empty monoid_homomorphism_unit.
     - by rewrite !big_opMS_union !big_opMS_singleton monoid_homomorphism -IH.
   Qed.
   Lemma big_opMS_commute1 `{Countable A} (h : M1 → M2)
-      `{!WeakMonoidHomomorphism o1 o2 h} (f : A → M1) X :
-    X ≠ ∅ → h ([^o1 mset] x ∈ X, f x) ≡ ([^o2 mset] x ∈ X, h (f x)).
+      `{!WeakMonoidHomomorphism o1 o2 R h} (f : A → M1) X :
+    X ≠ ∅ → R (h ([^o1 mset] x ∈ X, f x)) ([^o2 mset] x ∈ X, h (f x)).
   Proof.
     intros. induction X as [|x X IH] using gmultiset_ind; [done|].
     destruct (decide (X = ∅)) as [->|].
@@ -474,38 +477,38 @@ Section homomorphisms.
   Context `{!LeibnizEquiv M2}.
 
   Lemma big_opL_commute_L {A} (h : M1 → M2)
-      `{!MonoidHomomorphism o1 o2 h} (f : nat → A → M1) l :
+      `{!MonoidHomomorphism o1 o2 (≡) h} (f : nat → A → M1) l :
     h ([^o1 list] k↦x ∈ l, f k x) = ([^o2 list] k↦x ∈ l, h (f k x)).
   Proof. unfold_leibniz. by apply big_opL_commute. Qed.
   Lemma big_opL_commute1_L {A} (h : M1 → M2)
-      `{!WeakMonoidHomomorphism o1 o2 h} (f : nat → A → M1) l :
+      `{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : nat → A → M1) l :
     l ≠ [] → h ([^o1 list] k↦x ∈ l, f k x) = ([^o2 list] k↦x ∈ l, h (f k x)).
   Proof. unfold_leibniz. by apply big_opL_commute1. Qed.
 
   Lemma big_opM_commute_L `{Countable K} {A} (h : M1 → M2)
-      `{!MonoidHomomorphism o1 o2 h} (f : K → A → M1) m :
+      `{!MonoidHomomorphism o1 o2 (≡) h} (f : K → A → M1) m :
     h ([^o1 map] k↦x ∈ m, f k x) = ([^o2 map] k↦x ∈ m, h (f k x)).
   Proof. unfold_leibniz. by apply big_opM_commute. Qed.
   Lemma big_opM_commute1_L `{Countable K} {A} (h : M1 → M2)
-      `{!WeakMonoidHomomorphism o1 o2 h} (f : K → A → M1) m :
+      `{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : K → A → M1) m :
     m ≠ ∅ → h ([^o1 map] k↦x ∈ m, f k x) = ([^o2 map] k↦x ∈ m, h (f k x)).
   Proof. unfold_leibniz. by apply big_opM_commute1. Qed.
 
   Lemma big_opS_commute_L `{Countable A} (h : M1 → M2)
-      `{!MonoidHomomorphism o1 o2 h} (f : A → M1) X :
+      `{!MonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
     h ([^o1 set] x ∈ X, f x) = ([^o2 set] x ∈ X, h (f x)).
   Proof. unfold_leibniz. by apply big_opS_commute. Qed.
   Lemma big_opS_commute1_L `{ Countable A} (h : M1 → M2)
-      `{!WeakMonoidHomomorphism o1 o2 h} (f : A → M1) X :
+      `{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
     X ≠ ∅ → h ([^o1 set] x ∈ X, f x) = ([^o2 set] x ∈ X, h (f x)).
   Proof. intros. rewrite <-leibniz_equiv_iff. by apply big_opS_commute1. Qed.
 
   Lemma big_opMS_commute_L `{Countable A} (h : M1 → M2)
-      `{!MonoidHomomorphism o1 o2 h} (f : A → M1) X :
+      `{!MonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
     h ([^o1 mset] x ∈ X, f x) = ([^o2 mset] x ∈ X, h (f x)).
   Proof. unfold_leibniz. by apply big_opMS_commute. Qed.
   Lemma big_opMS_commute1_L `{Countable A} (h : M1 → M2)
-      `{!WeakMonoidHomomorphism o1 o2 h} (f : A → M1) X :
+      `{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
     X ≠ ∅ → h ([^o1 mset] x ∈ X, f x) = ([^o2 mset] x ∈ X, h (f x)).
   Proof. intros. rewrite <-leibniz_equiv_iff. by apply big_opMS_commute1. Qed.
 End homomorphisms.

theories/algebra/gmap.v

@@ -201,8 +201,8 @@ Implicit Types i : K.
 Implicit Types x y : A.
 
 Global Instance lookup_op_homomorphism :
-  MonoidHomomorphism op op (lookup i : gmap K A → option A).
-Proof. split; [split|]. apply _. intros m1 m2; by rewrite lookup_op. done. Qed.
+  MonoidHomomorphism op op (≡) (lookup i : gmap K A → option A).
+Proof. split; [split|]; try apply _. intros m1 m2; by rewrite lookup_op. done. Qed.
 
 Lemma lookup_opM m1 mm2 i : (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (!! i)).
 Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.

theories/algebra/monoid.v

@@ -33,18 +33,23 @@ Proof. intros x. etrans; [apply monoid_comm|apply monoid_left_id]. Qed.
 commuting with each other. We also consider a [WeakMonoidHomomorphism] which
 does not necesarrily commute with unit; an example is the [own] connective: we
 only have `True ==∗ own γ ∅`, not `True ↔ own γ ∅`. *)
-Class WeakMonoidHomomorphism {M1 M2 : ofeT} (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2)
-    `{Monoid M1 o1, Monoid M2 o2} (f : M1 → M2) := {
+Class WeakMonoidHomomorphism {M1 M2 : ofeT}
+    (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{Monoid M1 o1, Monoid M2 o2}
+    (R : relation M2) (f : M1 → M2) := {
+  monoid_homomorphism_rel_po : PreOrder R;
+  monoid_homomorphism_rel_proper : Proper ((≡) ==> (≡) ==> iff) R;
+  monoid_homomorphism_op_proper : Proper (R ==> R ==> R) o2;
   monoid_homomorphism_ne : NonExpansive f;
-  monoid_homomorphism x y : f (o1 x y) ≡ o2 (f x) (f y)
+  monoid_homomorphism x y : R (f (o1 x y)) (o2 (f x) (f y))
 }.
 
-Class MonoidHomomorphism {M1 M2 : ofeT} (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2)
-    `{Monoid M1 o1, Monoid M2 o2} (f : M1 → M2) := {
-  monoid_homomorphism_weak :> WeakMonoidHomomorphism o1 o2 f;
-  monoid_homomorphism_unit : f monoid_unit ≡ monoid_unit
+Class MonoidHomomorphism {M1 M2 : ofeT}
+    (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{Monoid M1 o1, Monoid M2 o2}
+    (R : relation M2) (f : M1 → M2) := {
+  monoid_homomorphism_weak :> WeakMonoidHomomorphism o1 o2 R f;
+  monoid_homomorphism_unit : R (f monoid_unit) monoid_unit
 }.
 
 Lemma weak_monoid_homomorphism_proper
-  `{WeakMonoidHomomorphism M1 M2 o1 o2 f} : Proper ((≡) ==> (≡)) f.
+  `{WeakMonoidHomomorphism M1 M2 o1 o2 R f} : Proper ((≡) ==> (≡)) f.
 Proof. apply ne_proper, monoid_homomorphism_ne. Qed.

theories/base_logic/derived.v

@@ -937,54 +937,54 @@ Global Instance uPred_sep_monoid : Monoid (@uPred_sep M) :=
   {| monoid_unit := True%I |}.
 
 Global Instance uPred_always_and_homomorphism :
-  MonoidHomomorphism uPred_and uPred_and (@uPred_always M).
-Proof. split; [split|]. apply _. apply always_and. apply always_pure. Qed.
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always M).
+Proof. split; [split; try apply _|]. apply always_and. apply always_pure. Qed.
 Global Instance uPred_always_if_and_homomorphism b :
-  MonoidHomomorphism uPred_and uPred_and (@uPred_always_if M b).
-Proof. split; [split|]. apply _. apply always_if_and. apply always_if_pure. Qed.
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always_if M b).
+Proof. split; [split; try apply _|]. apply always_if_and. apply always_if_pure. Qed.
 Global Instance uPred_later_monoid_and_homomorphism :
-  MonoidHomomorphism uPred_and uPred_and (@uPred_later M).
-Proof. split; [split|]. apply _. apply later_and. apply later_True. Qed.
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_later M).
+Proof. split; [split; try apply _|]. apply later_and. apply later_True. Qed.
 Global Instance uPred_laterN_and_homomorphism n :
-  MonoidHomomorphism uPred_and uPred_and (@uPred_laterN M n).
-Proof. split; [split|]. apply _. apply laterN_and. apply laterN_True. Qed.
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_laterN M n).
+Proof. split; [split; try apply _|]. apply laterN_and. apply laterN_True. Qed.
 Global Instance uPred_except_0_and_homomorphism :
-  MonoidHomomorphism uPred_and uPred_and (@uPred_except_0 M).
-Proof. split; [split|]. apply _. apply except_0_and. apply except_0_True. Qed.
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_except_0 M).
+Proof. split; [split; try apply _|]. apply except_0_and. apply except_0_True. Qed.
 
 Global Instance uPred_always_or_homomorphism :
-  MonoidHomomorphism uPred_or uPred_or (@uPred_always M).
-Proof. split; [split|]. apply _. apply always_or. apply always_pure. Qed.
+  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always M).
+Proof. split; [split; try apply _|]. apply always_or. apply always_pure. Qed.
 Global Instance uPred_always_if_or_homomorphism b :
-  MonoidHomomorphism uPred_or uPred_or (@uPred_always_if M b).
-Proof. split; [split|]. apply _. apply always_if_or. apply always_if_pure. Qed.
+  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always_if M b).
+Proof. split; [split; try apply _|]. apply always_if_or. apply always_if_pure. Qed.
 Global Instance uPred_later_monoid_or_homomorphism :
-  WeakMonoidHomomorphism uPred_or uPred_or (@uPred_later M).
-Proof. split. apply _. apply later_or. Qed.
+  WeakMonoidHomomorphism uPred_or uPred_or (≡) (@uPred_later M).
+Proof. split; try apply _. apply later_or. Qed.
 Global Instance uPred_laterN_or_homomorphism n :
-  WeakMonoidHomomorphism uPred_or uPred_or (@uPred_laterN M n).
-Proof. split. apply _. apply laterN_or. Qed.
+  WeakMonoidHomomorphism uPred_or uPred_or (≡) (@uPred_laterN M n).
+Proof. split; try apply _. apply laterN_or. Qed.
 Global Instance uPred_except_0_or_homomorphism :
-  WeakMonoidHomomorphism uPred_or uPred_or (@uPred_except_0 M).
-Proof. split. apply _. apply except_0_or. Qed. 
+  WeakMonoidHomomorphism uPred_or uPred_or (≡) (@uPred_except_0 M).
+Proof. split; try apply _. apply except_0_or. Qed. 
 
 Global Instance uPred_always_sep_homomorphism :
-  MonoidHomomorphism uPred_sep uPred_sep (@uPred_always M).
-Proof. split; [split|]. apply _. apply always_sep. apply always_pure. Qed.
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always M).
+Proof. split; [split; try apply _|]. apply always_sep. apply always_pure. Qed.
 Global Instance uPred_always_if_sep_homomorphism b :
-  MonoidHomomorphism uPred_sep uPred_sep (@uPred_always_if M b).
-Proof. split; [split|]. apply _. apply always_if_sep. apply always_if_pure. Qed.
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always_if M b).
+Proof. split; [split; try apply _|]. apply always_if_sep. apply always_if_pure. Qed.
 Global Instance uPred_later_monoid_sep_homomorphism :
-  MonoidHomomorphism uPred_sep uPred_sep (@uPred_later M).
-Proof. split; [split|]. apply _. apply later_sep. apply later_True. Qed.
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_later M).
+Proof. split; [split; try apply _|]. apply later_sep. apply later_True. Qed.
 Global Instance uPred_laterN_sep_homomorphism n :
-  MonoidHomomorphism uPred_sep uPred_sep (@uPred_laterN M n).
-Proof. split; [split|]. apply _. apply laterN_sep. apply laterN_True. Qed.
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_laterN M n).
+Proof. split; [split; try apply _|]. apply laterN_sep. apply laterN_True. Qed.
 Global Instance uPred_except_0_sep_homomorphism :
-  MonoidHomomorphism uPred_sep uPred_sep (@uPred_except_0 M).
-Proof. split; [split|]. apply _. apply except_0_sep. apply except_0_True. Qed.
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_except_0 M).
+Proof. split; [split; try apply _|]. apply except_0_sep. apply except_0_True. Qed.
 Global Instance uPred_ownM_sep_homomorphism :
-  MonoidHomomorphism op uPred_sep (@uPred_ownM M).
-Proof. split; [split|]. apply _. apply ownM_op. apply ownM_empty'. Qed.
+  MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
+Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_empty'. Qed.
 End derived.
 End uPred.

theories/base_logic/lib/auth.v

@@ -95,8 +95,8 @@ Section auth.
   Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.
   Global Instance auth_own_sep_homomorphism γ :
-    WeakMonoidHomomorphism op uPred_sep (auth_own γ).
-  Proof. split. apply _. apply auth_own_op. Qed.
+    WeakMonoidHomomorphism op uPred_sep (≡) (auth_own γ).
+  Proof. split; try apply _. apply auth_own_op. Qed.
 
   Global Instance own_mono' γ : Proper (flip (≼) ==> (⊢)) (auth_own γ).
   Proof. intros a1 a2. apply auth_own_mono. Qed.

theories/base_logic/lib/own.v

@@ -178,8 +178,8 @@ Qed.
 
 (** Big op class instances *)
 Instance own_cmra_sep_homomorphism `{inG Σ (A:ucmraT)} :
-  WeakMonoidHomomorphism op uPred_sep (own γ).
-Proof. split. apply _. apply own_op. Qed.
+  WeakMonoidHomomorphism op uPred_sep (≡) (own γ).
+Proof. split; try apply _. apply own_op. Qed.
 
 (** Proofmode class instances *)
 Section proofmode_classes.