Merge branch 'robbert/cmra_iso' into 'master'

Isomorphism and validy restriction constructions for cameras.

See merge request iris/iris!504

theories/algebra/auth.v

@@ -104,14 +104,12 @@ Instance auth_valid : Valid (auth A) := λ x,
       ✓ q ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ auth_frag_proj x ≼{n} a ∧ ✓{n} a)
   | None => ✓ auth_frag_proj x
   end.
-Global Arguments auth_valid !_ /.
 Instance auth_validN : ValidN (auth A) := λ n x,
   match auth_auth_proj x with
   | Some (q, ag) =>
       ✓{n} q ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ auth_frag_proj x ≼{n} a ∧ ✓{n} a
   | None => ✓{n} auth_frag_proj x
   end.
-Global Arguments auth_validN _ !_ /.
 Instance auth_pcore : PCore (auth A) := λ x,
   Some (Auth (core (auth_auth_proj x)) (core (auth_frag_proj x))).
 Instance auth_op : Op (auth A) := λ x y,
@@ -229,37 +227,26 @@ Proof. rewrite auth_both_frac_valid frac_valid'. naive_solver. Qed.
 
 Lemma auth_cmra_mixin : CmraMixin (auth A).
 Proof.
-  apply cmra_total_mixin.
-  - eauto.
-  - by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
-  - by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
-  - intros n [x a] [y b] [Hx Ha]; simpl in *. rewrite !auth_validN_eq.
-    destruct Hx as [x y Hx|]; first destruct Hx as [? Hx];
-      [destruct x,y|]; intros VI; ofe_subst; auto.
-  - intros [[[]|] ]; rewrite /= ?auth_valid_eq ?auth_validN_eq /=
-      ?cmra_valid_validN; naive_solver.
-  - intros n [[[]|] ]; rewrite !auth_validN_eq /=;
+  apply (iso_cmra_mixin_restrict (λ x : option (frac * agree A) * A, Auth x.1 x.2)
+    (λ x, (auth_auth_proj x, auth_frag_proj x))); try done.
+  - intros [x b]. by rewrite /= pair_pcore !cmra_pcore_core.
+  - intros n [[[q aa]|] b]; rewrite /= auth_validN_eq /=; last done.
+    intros (?&a&->&?&?). split; simpl; by eauto using cmra_validN_includedN.
+  - rewrite auth_validN_eq.
+    intros n [x1 b1] [x2 b2] [Hx ?]; simpl in *;
+      destruct Hx as [[q1 aa1] [q2 aa2] [??]|]; intros ?; by ofe_subst.
+  - rewrite auth_valid_eq auth_validN_eq.
+    intros [[[q aa]|] b]; rewrite /= cmra_valid_validN; naive_solver.
+  - rewrite auth_validN_eq. intros n [[[q aa]|] b];
       naive_solver eauto using dist_S, cmra_includedN_S, cmra_validN_S.
-  - by split; simpl; rewrite assoc.
-  - by split; simpl; rewrite comm.
-  - by split; simpl; rewrite ?cmra_core_l.
-  - by split; simpl; rewrite ?cmra_core_idemp.
-  - intros ??; rewrite! auth_included; intros [??].
-    by split; simpl; apply: cmra_core_mono. (* FIXME: FIXME(Coq #6294): needs new unification *)
   - assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
     { intros n a b1 b2 <-; apply cmra_includedN_l. }
-    intros n [[[q1 a1]|] b1] [[[q2 a2]|] b2]; rewrite auth_validN_eq /=;
-      try naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
-    intros [? [a [Eq [? Valid]]]].
-    assert (Eq': a1 ≡{n}≡ a2). { by apply agree_op_invN; rewrite Eq. }
+    rewrite auth_validN_eq. intros n [[[q1 a1]|] b1] [[[q2 a2]|] b2]; simpl;
+      [|naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN..].
+    intros [? [a [Ha12a [? Valid]]]].
+    assert (a1 ≡{n}≡ a2) as Ha12 by (apply agree_op_invN; by rewrite Ha12a).
     split; [naive_solver eauto using cmra_validN_op_l|].
-    exists a. rewrite -Eq -Eq' agree_idemp. naive_solver.
-  - intros n x y1 y2 ? [??]; simpl in *.
-    destruct (cmra_extend n (auth_auth_proj x) (auth_auth_proj y1)
-      (auth_auth_proj y2)) as (ea1&ea2&?&?&?); auto using auth_auth_proj_validN.
-    destruct (cmra_extend n (auth_frag_proj x) (auth_frag_proj y1) (auth_frag_proj y2))
-      as (b1&b2&?&?&?); auto using auth_frag_proj_validN.
-    by exists (Auth ea1 b1), (Auth ea2 b2).
+    exists a. rewrite -Ha12a -Ha12 agree_idemp. naive_solver.
 Qed.
 Canonical Structure authR := CmraT (auth A) auth_cmra_mixin.
 
@@ -390,11 +377,11 @@ Lemma auth_update_core_id q a b `{!CoreId b} :
   b ≼ a → ●{q} a ~~> ●{q} a ⋅ ◯ b.
 Proof.
   intros Ha%(core_id_extract _ _). apply cmra_total_update.
-  move=> n [[[q' ag]|] bf1] [Hq [a0 [Haa0 [Hbf1 Ha0]]]]; do 2 red; simpl in *.
-  + split; [done|]. exists a0. split_and!; [done| |done].
+  move=> n [[[q' ag]|] bf1] [Hq [a0 [Haa0 [Hbf1 Ha0]]]]; simpl in *.
+  + split; simpl; [done|]. exists a0. split_and!; [done| |done].
     assert (a ≡{n}≡ a0) as Haa0' by (apply to_agree_includedN; by exists ag).
     rewrite -Haa0' Ha Haa0' -assoc (comm _ b) assoc. by apply cmra_monoN_r.
-  + split; [done|]. exists a0. split_and!; [done| |done].
+  + split; simpl; [done|]. exists a0. split_and!; [done| |done].
     apply (inj to_agree) in Haa0.
     rewrite -Haa0 Ha Haa0 -assoc (comm _ b) assoc. by apply cmra_monoN_r.
 Qed.

theories/algebra/cmra.v

@@ -1668,3 +1668,86 @@ Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
   by apply discrete_funO_map_ne=>c; apply urFunctor_map_contractive.
 Qed.
+
+(** * Constructing a camera [B] through a bijection with [A] that
+is mostly an isomorphism but restricts validity. *)
+Lemma iso_cmra_mixin_restrict {A : cmraT} {B : Type}
+  `{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
+  (f : A → B) (g : B → A)
+  (* [g] is proper/non-expansive and injective w.r.t. setoid and OFE equality *)
+  (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)
+  (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
+  (* [g] is surjective (and [f] its inverse) *)
+  (gf : ∀ x, g (f x) ≡ x)
+  (* [g] commutes with [pcore] and [op] *)
+  (g_pcore : ∀ y, pcore (g y) ≡ g <$> pcore y)
+  (g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
+  (* The validity predicate on [B] restricts the one on [A] *)
+  (g_validN : ∀ n y, ✓{n} y → ✓{n} (g y))
+  (* The validity predicate on [B] satisfies the laws of validity *)
+  (valid_validN_ne : ∀ n, Proper (dist n ==> impl) (validN (A:=B) n))
+  (valid_rvalidN : ∀ y : B, ✓ y ↔ ∀ n, ✓{n} y)
+  (validN_S : ∀ n (y : B), ✓{S n} y → ✓{n} y)
+  (validN_op_l : ∀ n (y1 y2 : B), ✓{n} (y1 ⋅ y2) → ✓{n} y1) :
+  CmraMixin B.
+Proof.
+  split.
+  - intros y n z1 z2 Hz%g_dist. apply g_dist. by rewrite !g_op Hz.
+  - intros n y1 y2 cy Hy%g_dist Hy1.
+    assert (g <$> pcore y2 ≡{n}≡ Some (g cy))
+      as (cx&(cy'&->&->)%fmap_Some_1&?%g_dist)%dist_Some_inv_r'; [|by eauto].
+    by rewrite -g_pcore -Hy g_pcore Hy1.
+  - done.
+  - done.
+  - done.
+  - intros y1 y2 y3. apply g_equiv. by rewrite !g_op assoc.
+  - intros y1 y2. apply g_equiv. by rewrite !g_op comm.
+  - intros y cy Hy. apply g_equiv. rewrite g_op. apply cmra_pcore_l'.
+    by rewrite g_pcore Hy.
+  - intros y cy Hy.
+    assert (g <$> pcore cy ≡ Some (g cy)) as (cy'&->&?)%fmap_Some_equiv.
+    { rewrite -g_pcore.
+      apply cmra_pcore_idemp' with (g y). by rewrite g_pcore Hy. }
+    constructor. by apply g_equiv.
+  - intros y1 y2 cy [z Hy2] Hy1.
+    destruct (cmra_pcore_mono' (g y1) (g y2) (g cy)) as (cx&Hcgy2&[x Hcx]).
+    { exists (g z). rewrite -g_op. by apply g_equiv. }
+    { by rewrite g_pcore Hy1. }
+    assert (g <$> pcore y2 ≡ Some cx) as (cy'&->&?)%fmap_Some_equiv.
+    { by rewrite -g_pcore Hcgy2. }
+    exists cy'; split; [done|].
+    exists (f x). apply g_equiv. by rewrite g_op gf -Hcx.
+  - done.
+  - intros n y z1 z2 ?%g_validN ?.
+    destruct (cmra_extend n (g y) (g z1) (g z2)) as (x1&x2&Hgy&?&?).
+    { done. }
+    { rewrite -g_op. by apply g_dist. }
+    exists (f x1), (f x2). split_and!.
+    + apply g_equiv. by rewrite Hgy g_op !gf.
+    + apply g_dist. by rewrite gf.
+    + apply g_dist. by rewrite gf.
+Qed.
+
+(** * Constructing a camera through an isomorphism *)
+Lemma iso_cmra_mixin {A : cmraT} {B : Type}
+  `{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
+  (f : A → B) (g : B → A)
+  (* [g] is proper/non-expansive and injective w.r.t. setoid and OFE equality *)
+  (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)
+  (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
+  (* [g] is surjective (and [f] its inverse) *)
+  (gf : ∀ x, g (f x) ≡ x)
+  (* [g] commutes with [pcore], [op], [valid], and [validN] *)
+  (g_pcore : ∀ y, pcore (g y) ≡ g <$> pcore y)
+  (g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
+  (g_valid : ∀ y, ✓ (g y) ↔ ✓ y)
+  (g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y) :
+  CmraMixin B.
+Proof.
+  apply (iso_cmra_mixin_restrict f g); auto.
+  - by intros n y ?%g_validN.
+  - intros n y1 y2 Hy%g_dist Hy1. by rewrite -g_validN -Hy g_validN.
+  - intros y. rewrite -g_valid cmra_valid_validN. naive_solver.
+  - intros n y. rewrite -!g_validN. apply cmra_validN_S.
+  - intros n y1 y2. rewrite -!g_validN g_op. apply cmra_validN_op_l.
+Qed.

theories/algebra/ofe.v

@@ -1292,7 +1292,7 @@ Proof.
 Qed.
 
 (** * Constructing isomorphic OFEs *)
-Lemma iso_ofe_mixin {A : ofeT} `{Equiv B, Dist B} (g : B → A)
+Lemma iso_ofe_mixin {A : ofeT} {B : Type} `{!Equiv B, !Dist B} (g : B → A)
   (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)
   (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2) : OfeMixin B.
 Proof.