iris_unstable/algebra/monotone.v

@@ -39,28 +39,16 @@ Section ofe.
   Local Definition below (a : A) (x : mra R) := ∃ b, b ∈ x ∧ R a b.
 
   Local Lemma below_app a x y : below a (x ++ y) ↔ below a x ∨ below a y.
-  Proof.
-    split.
-    - intros (b & [|]%elem_of_app & ?); [left|right]; exists b; eauto.
-    - intros [(b & ? & ?)|(b & ? & ?)]; exists b; rewrite elem_of_app; eauto.
-  Qed.
+  Proof. set_solver. Qed.
 
   Local Lemma below_principal a b : below a (principal R b) ↔ R a b.
-  Proof.
-    split.
-    - intros (c & ->%elem_of_list_singleton & ?); done.
-    - intros Hab; exists b; split; first apply elem_of_list_singleton; done.
-  Qed.
+  Proof. set_solver. Qed.
 
   Local Instance mra_equiv : Equiv (mra R) :=
     λ x y, ∀ a, below a x ↔ below a y.
 
   Local Instance mra_equiv_equiv : Equivalence mra_equiv.
-  Proof.
-    split; [by firstorder|by firstorder|].
-    intros ??? Heq1 Heq2 ?; split; intros ?;
-      [apply Heq2; apply Heq1|apply Heq1; apply Heq2]; done.
-  Qed.
+  Proof. unfold mra_equiv; split; intros ?; naive_solver. Qed.
 
   Canonical Structure mraO := discreteO (mra R).
 End ofe.
@@ -83,12 +71,12 @@ Section cmra.
     apply discrete_cmra_mixin; first apply _.
     apply ra_total_mixin.
     - eauto.
-    - intros ??? Heq a; specialize (Heq a); rewrite !below_app; firstorder.
+    - intros ??? Heq a; by rewrite !below_app (Heq a).
     - intros ?; done.
     - done.
-    - intros ????; rewrite !below_app; firstorder.
-    - intros ???; rewrite !below_app; firstorder.
-    - rewrite /core /pcore /=; intros ??; rewrite below_app; firstorder.
+    - intros ????; rewrite !below_app; by intuition.
+    - intros ???; rewrite !below_app; by intuition.
+    - rewrite /core /pcore /=; intros ??; rewrite below_app; by intuition.
     - done.
     - intros ? ? [? ?]; eexists _; done.
     - done.
@@ -119,53 +107,41 @@ Section cmra.
     intros [z ->]; rewrite assoc mra_idemp; done.
   Qed.
 
-  Lemma principal_R_opN_base `{!Transitive R} n x y :
-    (∀ b, b ∈ y → ∃ c, c ∈ x ∧ R b c) → y ⋅ x ≡{n}≡ x.
+  Lemma principal_R_op_base `{!Transitive R} x y :
+    (∀ b, b ∈ y → ∃ c, c ∈ x ∧ R b c) → y ⋅ x ≡ x.
   Proof.
-    intros HR; split; rewrite /op /mra_op below_app; [|by firstorder].
+    intros HR. split; rewrite /op /mra_op below_app; [|by intuition].
     intros [(c & (d & Hd1 & Hd2)%HR & Hc2)|]; [|done].
     exists d; split; [|transitivity c]; done.
   Qed.
 
-  Lemma principal_R_opN `{!Transitive R} n a b :
-    R a b → principal R a ⋅ principal R b ≡{n}≡ principal R b.
-  Proof.
-    intros; apply principal_R_opN_base; intros c; rewrite /principal.
-    setoid_rewrite elem_of_list_singleton => ->; eauto.
-  Qed.
-
   Lemma principal_R_op `{!Transitive R} a b :
     R a b → principal R a ⋅ principal R b ≡ principal R b.
-  Proof. by intros ? ?; apply (principal_R_opN 0). Qed.
-
-  Lemma principal_op_RN n a b x :
-    R a a → principal R a ⋅ x ≡{n}≡ principal R b → R a b.
   Proof.
-    intros Ha HR.
-    destruct (HR a) as [[z [HR1%elem_of_list_singleton HR2]] _];
-      last by subst; eauto.
-    rewrite /op /mra_op /principal below_app below_principal; auto.
+    intros; apply principal_R_op_base; intros c; rewrite /principal.
+    set_solver.
   Qed.
 
   Lemma principal_op_R' a b x :
     R a a → principal R a ⋅ x ≡ principal R b → R a b.
-  Proof. intros ? ?; eapply (principal_op_RN 0); eauto. Qed.
+  Proof. move=> Ha /(_ a) HR. set_solver. Qed.
 
   Lemma principal_op_R `{!Reflexive R} a b x :
     principal R a ⋅ x ≡ principal R b → R a b.
-  Proof. intros; eapply principal_op_R'; eauto. Qed.
+  Proof. by apply principal_op_R'. Qed.
 
-  Lemma principal_includedN `{!PreOrder R} n a b :
-    principal R a ≼{n} principal R b ↔ R a b.
+  Lemma principal_included `{!PreOrder R} a b :
+    principal R a ≼ principal R b ↔ R a b.
   Proof.
     split.
-    - intros [z Hz]; eapply principal_op_RN; first done. by rewrite Hz.
-    - intros ?; exists (principal R b); rewrite principal_R_opN; eauto.
+    - move=> [z Hz]. by eapply principal_op_R.
+    - intros ?; exists (principal R b). by rewrite principal_R_op.
   Qed.
 
-  Lemma principal_included `{!PreOrder R} a b :
-    principal R a ≼ principal R b ↔ R a b.
-  Proof. apply (principal_includedN 0). Qed.
+  (* Useful? *)
+  Lemma principal_includedN `{!PreOrder R} n a b :
+    principal R a ≼{n} principal R b ↔ R a b.
+  Proof. by rewrite -principal_included -cmra_discrete_included_iff. Qed.
 
   Lemma mra_local_update_grow `{!Transitive R} a x b:
     R a b →
@@ -175,15 +151,8 @@ Section cmra.
     apply local_update_unital_discrete.
     intros z _ Habz.
     split; first done.
-    intros w; split.
-    - intros (y & ->%elem_of_list_singleton & Hy2).
-      exists b; split; first constructor; done.
-    - intros (y & [->|Hy1]%elem_of_cons & Hy2).
-      + exists b; split; first constructor; done.
-      + exists b; split; first constructor.
-        specialize (Habz w) as [_ [c [->%elem_of_list_singleton Hc2]]].
-        { exists y; split; first (by apply elem_of_app; right); eauto. }
-        etrans; eauto.
+    intros w. specialize (Habz w).
+    set_solver.
   Qed.
 
   Lemma mra_local_update_get_frag `{!PreOrder R} a b:
@@ -202,45 +171,58 @@ End cmra.
 Global Arguments mraR {_} _.
 Global Arguments mraUR {_} _.
 
+(**
+If [R] is a partial order, relative to a setoid [S] on the carrier [A],
+then [principal R] is proper and injective.
 
-(* Might be useful if the type of elements is an OFE. *)
-Section mra_over_ofe.
-  Context {A : ofe} {R : relation A}.
+The following theory generalizes over an arbitrary setoid [S] and necessary properties,
+but is overly general, so we encapsulate the instances in an opt-in module.
+*)
+Module mra_over_rel.
+Section mra_over_rel.
+  Context {A : Type} {R : relation A}.
   Implicit Types a b : A.
   Implicit Types x y : mra R.
+  Implicit Type (S : relation A).
 
-  Global Instance principal_ne
-         `{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
-    NonExpansive (principal R).
-  Proof. intros n a1 a2 Ha; split; rewrite !below_principal !Ha; done. Qed.
-
-  Global Instance principal_proper
-         `{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
-    Proper ((≡) ==> (≡)) (principal R) := ne_proper _.
+  #[export] Instance principal_rel_proper S
+         `{!Proper (S ==> S ==> iff) R} `{!Reflexive S} :
+    Proper (S ==> (≡)) (principal R).
+  Proof. intros a1 a2 Ha; split; rewrite ->!below_principal, !Ha; done. Qed.
 
   Lemma principal_inj_related a b :
     principal R a ≡ principal R b → R a a → R a b.
-  Proof.
-    intros Hab ?.
-    destruct (Hab a) as [[? [?%elem_of_list_singleton ?]] _];
-      last by subst; auto.
-    exists a; rewrite /principal elem_of_list_singleton; done.
-  Qed.
+  Proof. move=> /(_ a). set_solver. Qed.
 
-  Lemma principal_inj_general a b :
+  Lemma principal_inj_general S a b :
     principal R a ≡ principal R b →
-    R a a → R b b → (R a b → R b a → a ≡ b) → a ≡ b.
+    R a a → R b b → (R a b → R b a → S a b) → S a b.
   Proof. intros ??? Has; apply Has; apply principal_inj_related; auto. Qed.
 
-  Global Instance principal_inj_instance `{!Reflexive R} `{!AntiSymm (≡) R} :
-    Inj (≡) (≡) (principal R).
-  Proof. intros ???; apply principal_inj_general; auto. Qed.
+  #[export] Instance principal_inj {S} `{!Reflexive R} `{!AntiSymm S R} :
+    Inj S (≡) (principal R).
+  Proof. intros ???. apply principal_inj_general => //. apply: anti_symm. Qed.
+End mra_over_rel.
+End mra_over_rel.
 
-  Global Instance principal_injN `{!Reflexive R} {Has : AntiSymm (≡) R} n :
-    Inj (dist n) (dist n) (principal R).
-  Proof.
-    intros x y Hxy%discrete_iff; last apply _.
-    eapply equiv_dist; revert Hxy; apply inj; apply _.
-  Qed.
+(* Specialize [mra_over_rel] to equality. Only [principal_inj] seems generally useful. *)
+Global Instance principal_inj `{R : relation A} `{!Reflexive R} `{!AntiSymm (=) R} :
+  Inj (=) (≡) (principal R) := mra_over_rel.principal_inj.
+
+(* Might be useful if the type of elements is an OFE. *)
+Section mra_over_ofe.
+  Context {A : ofe} {R : relation A}.
+  Implicit Types a b : A.
+  Implicit Types x y : mra R.
+
+  Import mra_over_rel.
+
+  Global Instance principal_proper
+         `{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
+    Proper ((≡) ==> (≡)) (principal R) := ne_proper _.
 
+  (* TODO: Useful? Clients should rather call equiv_dist. *)
+  Lemma principal_injN `{!Reflexive R} {Has : AntiSymm (≡) R} n :
+    Inj (dist n) (≡) (principal R).
+  Proof. intros x y Hxy%(inj _). by apply equiv_dist. Qed.
 End mra_over_ofe.

tests/monotone.v

+Require Import iris.unstable.algebra.monotone.
+
+Section test_mra_over_eq.
+  Context {A : Type} {R : relation A}.
+  Context `{!Reflexive R} {Has : AntiSymm (=) R}.
+
+  Implicit Types a b : A.
+  Implicit Types x y : mra R.
+
+  Lemma test1 a b : principal R a ≡ principal R b → a = b.
+  Proof.
+    by intros ?%(inj _).
+  Qed.
+
+End test_mra_over_eq.
+
+Section test_mra_over_ofe.
+  Context {A : ofe} {R : relation A}.
+  Implicit Types a b : A.
+  Implicit Types x y : mra R.
+
+  Import mra_over_rel.
+  Context `{!Reflexive R} {Has : AntiSymm (≡) R}.
+  Lemma test a b : principal R a ≡ principal R b → a ≡ b.
+  Proof.
+    by intros ?%(inj _).
+  Qed.
+
+  Lemma principal_ne
+         `{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
+    NonExpansive (principal R).
+  Proof. apply _. Abort.
+
+  Lemma principal_inj_instance :
+    Inj (≡) (≡) (principal R).
+  Proof. apply _. Abort.
+
+  (* Also questionable. *)
+  Instance principal_injN' n :
+    Inj (dist n) (dist n) (principal R).
+  Proof. apply principal_injN. Abort.
+End test_mra_over_ofe.