(* iris/algebra/cmra.v *)
(* * Constructing a camera [B] through a mapping into [A]

The mapping may restrict the domain (i.e., we have an injection from [B] to [A],
not a bijection) and validity. These two restrictions work on opposite "ends" of
[A] according to [≼]: domain restriction must prove that when an element is in
the domain, so is its composition with other elements; validity restriction must
prove that if the composition of two elements is valid, then so are both of the
elements. The "domain" is the image of [g] in [A], or equivalently the part of
[A] where [f] returns [Some]. *)
Lemma inj_cmra_mixin_restrict_validity {SI : sidx} {A : cmra} {B : ofe}
  `{!PCore B, !Op B, !Valid B, !ValidN B}
  (f : A → option B) (g : B → A)
  (* [g] is proper/non-expansive and injective w.r.t. OFE equality *)
  (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
  (* [g] is surjective into the part of [A] where [is_Some ∘ f] holds
  (and [f] its inverse) *)
  (gf_dist : ∀ (x : A) (y : B) n, f x ≡{n}≡ Some y ↔ g y ≡{n}≡ x)
  (* [g] commutes with [pcore] (on the part where it is defined) and [op] *)
  (g_pcore_dist : ∀ (y cy : B) n,
    pcore y ≡{n}≡ Some cy ↔ pcore (g y) ≡{n}≡ Some (g cy))
  (g_op : ∀ (y1 y2 : B), g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
  (* [g] also commutes with [opM] when the right-hand side is produced by [f],
  and cancels the [f]. In particular this axiom implies that when taking an
  element in the domain ([g y]), its composition with *any* [x : A] is still in
  the domain, and [f] computes the preimage properly.
  Note that just requiring "the composition of two elements from the domain
  is in the domain" is insufficient for this lemma to hold. [g_op] already shows
  that this is the case, but the issue is that in [pcore_mono] we obtain a
  [g y1 ≼ g y2], and the existentially quantified "remainder" in the [≼] has no
  reason to be in the domain, so [g_op] is too weak to turn this into some
  relation between [y1] and [y2] in [B]. At the same time, [g_opM_f] does not
  impl [g_op] since we need [g_op] to prove that [⋅] in [B] respects [≡].
  Therefore both [g_op] and [g_opM_f] are required for this lemma to work. *)
  (g_opM_f : ∀ (x : A) (y : B), g (y ⋅? f x) ≡ g y ⋅ x)
  (* The validity predicate on [B] restricts the one on [A] *)
  (g_validN : ∀ n (y : B), ✓{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_le : ∀ n n' (y : B), ✓{n} y → n' ≤ n → ✓{n'} y)
  (validN_op_l : ∀ n (y1 y2 : B), ✓{n} (y1 ⋅ y2) → ✓{n} y1) :
  CmraMixin B.
Proof.
  (* Some general derived facts that will be useful later. *)
  assert (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2).
  { intros ??. rewrite !equiv_dist. naive_solver. }
  assert (g_pcore : ∀ (y cy : B),
    pcore y ≡ Some cy ↔ pcore (g y) ≡ Some (g cy)).
  { intros. rewrite !equiv_dist. naive_solver. }
  assert (gf : ∀ x y, f x ≡ Some y ↔ g y ≡ x).
  { intros. rewrite !equiv_dist. naive_solver. }
  assert (fg : ∀ y, f (g y) ≡ Some y).
  { intros. apply gf. done. }
  assert (g_ne : NonExpansive g).
  { intros n ???. apply g_dist. done. }
  (* Some of the CMRA properties are useful in proving the others. *)
  assert (b_pcore_l' : ∀ y cy : B, pcore y ≡ Some cy → cy ⋅ y ≡ y).
  { intros y cy Hy. apply g_equiv. rewrite g_op. apply cmra_pcore_l'.
    apply g_pcore. done. }
  assert (b_pcore_idemp : ∀ y cy : B, pcore y ≡ Some cy → pcore cy ≡ Some cy).
  { intros y cy Hy. eapply g_pcore, cmra_pcore_idemp', g_pcore. done. }
  (* Now prove all the mixin laws. *)
  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].
    assert (Hgcy : pcore (g y1) ≡ Some (g cy)).
    { apply g_pcore. rewrite Hy1. done. }
    rewrite equiv_dist in Hgcy. specialize (Hgcy n).
    rewrite Hy in Hgcy. apply g_pcore_dist in Hgcy. rewrite Hgcy. done.
  - 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 Hcy. apply b_pcore_l'. by rewrite Hcy.
  - intros y cy Hcy. eapply b_pcore_idemp. by rewrite -Hcy.
  - 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. }
    { apply g_pcore. rewrite Hy1 //. }
    apply (reflexive_eq (R:=equiv)) in Hcgy2.
    rewrite -g_opM_f in Hcx. rewrite Hcx in Hcgy2.
    apply g_pcore in Hcgy2.
    apply Some_equiv_eq in Hcgy2 as [cy' [-> Hcy']].
    eexists. split; first done.
    destruct (f x) as [y|].
    + exists y. done.
    + exists cy. apply (reflexive_eq (R:=equiv)), b_pcore_idemp, b_pcore_l' in Hy1.
      rewrite Hy1 //.
  - done.
  - intros n y z1 z2 ?%g_validN ?.
    destruct (cmra_extend n (g y) (g z1) (g z2)) as (x1&x2&Hgy&Hx1&Hx2).
    { done. }
    { rewrite -g_op. by apply g_dist. }
    symmetry in Hx1, Hx2.
    apply gf_dist in Hx1, Hx2.
    destruct (f x1) as [y1|] eqn:Hy1; last first.
    { exfalso. inversion Hx1. }
    destruct (f x2) as [y2|] eqn:Hy2; last first.
    { exfalso. inversion Hx2. }
    exists y1, y2. split_and!.
    + apply g_equiv. rewrite Hgy g_op.
      f_equiv; symmetry; apply gf; rewrite ?Hy1 ?Hy2 //.
    + apply g_dist. apply (inj Some) in Hx1. rewrite Hx1 //.
    + apply g_dist. apply (inj Some) in Hx2. rewrite Hx2 //.
Qed.