Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0

modures/auth.v

@@ -6,12 +6,14 @@ Add Printing Constructor auth.
 Arguments Auth {_} _ _.
 Arguments authoritative {_} _.
 Arguments own {_} _.
-Notation "◯ x" := (Auth ExclUnit x) (at level 20).
-Notation "● x" := (Auth (Excl x) ∅) (at level 20).
+Notation "◯ a" := (Auth ExclUnit a) (at level 20).
+Notation "● a" := (Auth (Excl a) ∅) (at level 20).
 
 (* COFE *)
 Section cofe.
 Context {A : cofeT}.
+Implicit Types a b : A.
+Implicit Types x y : auth A.
 
 Instance auth_equiv : Equiv (auth A) := λ x y,
   authoritative x ≡ authoritative y ∧ own x ≡ own y.
@@ -20,10 +22,16 @@ Instance auth_dist : Dist (auth A) := λ n x y,
 
 Global Instance Auth_ne : Proper (dist n ==> dist n ==> dist n) (@Auth A).
 Proof. by split. Qed.
+Global Instance Auth_proper : Proper ((≡) ==> (≡) ==> (≡)) (@Auth A).
+Proof. by split. Qed.
 Global Instance authoritative_ne: Proper (dist n ==> dist n) (@authoritative A).
 Proof. by destruct 1. Qed.
+Global Instance authoritative_proper : Proper ((≡) ==> (≡)) (@authoritative A).
+Proof. by destruct 1. Qed.
 Global Instance own_ne : Proper (dist n ==> dist n) (@own A).
 Proof. by destruct 1. Qed.
+Global Instance own_proper : Proper ((≡) ==> (≡)) (@own A).
+Proof. by destruct 1. Qed.
 
 Instance auth_compl : Compl (auth A) := λ c,
   Auth (compl (chain_map authoritative c)) (compl (chain_map own c)).
@@ -36,14 +44,14 @@ Proof.
     + by intros ?; split.
     + by intros ?? [??]; split; symmetry.
     + intros ??? [??] [??]; split; etransitivity; eauto.
-  * by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
+  * by intros ? [??] [??] [??]; split; apply dist_S.
   * by split.
   * intros c n; split. apply (conv_compl (chain_map authoritative c) n).
     apply (conv_compl (chain_map own c) n).
 Qed.
 Canonical Structure authC := CofeT auth_cofe_mixin.
-Instance Auth_timeless (x : excl A) (y : A) :
-  Timeless x → Timeless y → Timeless (Auth x y).
+Instance Auth_timeless (ea : excl A) (b : A) :
+  Timeless ea → Timeless b → Timeless (Auth ea b).
 Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed.
 Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A).
 Proof. by intros ? [??] [??] [??]; f_equal'; apply leibniz_equiv. Qed.
@@ -54,6 +62,8 @@ Arguments authC : clear implicits.
 (* CMRA *)
 Section cmra.
 Context {A : cmraT}.
+Implicit Types a b : A.
+Implicit Types x y : auth A.
 
 Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
 Instance auth_validN : ValidN (auth A) := λ n x,
@@ -114,22 +124,46 @@ Definition auth_cmra_extend_mixin : CMRAExtendMixin (auth A).
 Proof.
   intros n x y1 y2 ? [??]; simpl in *.
   destruct (cmra_extend_op n (authoritative x) (authoritative y1)
-    (authoritative y2)) as (z1&?&?&?); auto using authoritative_validN.
+    (authoritative y2)) as (ea&?&?&?); auto using authoritative_validN.
   destruct (cmra_extend_op n (own x) (own y1) (own y2))
-    as (z2&?&?&?); auto using own_validN.
-  by exists (Auth (z1.1) (z2.1), Auth (z1.2) (z2.2)).
+    as (b&?&?&?); auto using own_validN.
+  by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
 Qed.
 Canonical Structure authRA : cmraT :=
   CMRAT auth_cofe_mixin auth_cmra_mixin auth_cmra_extend_mixin.
-Instance auth_cmra_identity `{Empty A} : CMRAIdentity A → CMRAIdentity authRA.
+
+(** The notations ◯ and ● only work for CMRAs with an empty element. So, in
+what follows, we assume we have an empty element. *)
+Context `{Empty A, !CMRAIdentity A}.
+
+Global Instance auth_cmra_identity : CMRAIdentity authRA.
 Proof.
   split; simpl.
   * by apply (@cmra_empty_valid A _).
   * by intros x; constructor; rewrite /= left_id.
   * apply Auth_timeless; apply _.
 Qed.
-Lemma auth_frag_op (a b : A) : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
+Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
 Proof. done. Qed.
+
+Lemma auth_update a a' b b' :
+  (∀ n af, ✓{n} a → a ={n}= a' ⋅ af → b ={n}= b' ⋅ af ∧ ✓{n} b) →
+  ● a ⋅ ◯ a' ⇝ ● b ⋅ ◯ b'.
+Proof.
+  move=> Hab [[] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
+  destruct (Hab (S n) (bf1 ⋅ bf2)) as [Ha' ?]; auto.
+  { by rewrite Ha left_id associative. }
+  split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done].
+Qed.
+Lemma auth_update_op_l a a' b :
+  ✓ (b ⋅ a) → ● a ⋅ ◯ a' ⇝ ● (b ⋅ a) ⋅ ◯ (b ⋅ a').
+Proof.
+  intros; apply auth_update.
+  by intros n af ? Ha; split; [by rewrite Ha associative|].
+Qed.
+Lemma auth_update_op_r a a' b :
+  ✓ (a ⋅ b) → ● a ⋅ ◯ a' ⇝ ● (a ⋅ b) ⋅ ◯ (a' ⋅ b).
+Proof. rewrite -!(commutative _ b); apply auth_update_op_l. Qed.
 End cmra.
 
 Arguments authRA : clear implicits.

modures/cmra.v

@@ -143,12 +143,12 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
 (** * Frame preserving updates *)
 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,
   ✓{S n} (x ⋅ z) → ∃ y, P y ∧ ✓{S n} (y ⋅ z).
-Instance: Params (@cmra_updateP) 3.
+Instance: Params (@cmra_updateP) 1.
 Infix "⇝:" := cmra_updateP (at level 70).
 Definition cmra_update {A : cmraT} (x y : A) := ∀ z n,
   ✓{S n} (x ⋅ z) → ✓{S n} (y ⋅ z).
 Infix "⇝" := cmra_update (at level 70).
-Instance: Params (@cmra_update) 3.
+Instance: Params (@cmra_update) 1.
 
 (** * Properties **)
 Section cmra.
@@ -193,6 +193,17 @@ Proof.
   intros x x' Hx y y' Hy.
   by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
 Qed.
+Global Instance cmra_update_proper :
+  Proper ((≡) ==> (≡) ==> iff) (@cmra_update A).
+Proof.
+  intros x1 x2 Hx y1 y2 Hy; split=>? z n; [rewrite -Hx -Hy|rewrite Hx Hy]; auto.
+Qed.
+Global Instance cmra_updateP_proper :
+  Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
+Proof.
+  intros x1 x2 Hx P1 P2 HP; split=>Hup z n;
+    [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto.
+Qed.
 
 (** ** Validity *)
 Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.

modures/excl.v

@@ -27,6 +27,14 @@ Inductive excl_dist `{Dist A} : Dist (excl A) :=
   | ExclUnit_dist n : ExclUnit ={n}= ExclUnit
   | ExclBot_dist n : ExclBot ={n}= ExclBot.
 Existing Instance excl_dist.
+Global Instance Excl_ne : Proper (dist n ==> dist n) (@Excl A).
+Proof. by constructor. Qed.
+Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A).
+Proof. by constructor. Qed.
+Global Instance Excl_inj : Injective (≡) (≡) (@Excl A).
+Proof. by inversion_clear 1. Qed.
+Global Instance Excl_dist_inj n : Injective (dist n) (dist n) (@Excl A).
+Proof. by inversion_clear 1. Qed.
 Program Definition excl_chain
     (c : chain (excl A)) (x : A) (H : maybe Excl (c 1) = Some x) : chain A :=
   {| chain_car n := match c n return _ with Excl y => y | _ => x end |}.
@@ -66,10 +74,6 @@ Proof.
 Qed.
 Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
 
-Global Instance Excl_inj : Injective (≡) (≡) (@Excl A).
-Proof. by inversion_clear 1. Qed.
-Global Instance Excl_dist_inj n : Injective (dist n) (dist n) (@Excl A).
-Proof. by inversion_clear 1. Qed.
 Global Instance Excl_timeless (x : A) : Timeless x → Timeless (Excl x).
 Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
 Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).