(* iris/algebra/lib/frac_auth.v *)
From iris.algebra Require Export frac auth updates local_updates
From iris.algebra Require Import proofmode_classes
From iris.prelude Require Import options

Definition frac_authR{SI : sidx} (A : cmra) : cmra :=
  authR (optionUR (prodR fracR A)).

Definition frac_authUR{SI : sidx} (A : cmra) : ucmra :=
  authUR (optionUR (prodR fracR A)).

Definition frac_auth_auth{SI : sidx} {A : cmra} (x : A) : frac_authR A :=
  ● (Some (1%Qp,x)).

Definition frac_auth_frag{SI : sidx}
    {A : cmra} (q : frac) (x : A) : frac_authR A :=
  ◯ (Some (q,x)).

Global TypeclassesOpaque frac_auth_auth frac_auth_frag.

Global Instance: Params (@frac_auth_auth) 2 := {}.

Global Instance: Params (@frac_auth_frag) 3 := {}.

Global Instancefrac_auth_auth_ne : NonExpansive (@frac_auth_auth SI A).
  Proof. solve_proper. Qed.

Global Instancefrac_auth_auth_proper :
    Proper ((≡) ==> (≡)) (@frac_auth_auth SI A).
  Proof. solve_proper. Qed.

Global Instancefrac_auth_frag_ne q : NonExpansive (@frac_auth_frag SI A q).
  Proof. solve_proper. Qed.

Global Instancefrac_auth_frag_proper q :
    Proper ((≡) ==> (≡)) (@frac_auth_frag SI A q).
  Proof. solve_proper. Qed.

Global Instancefrac_auth_auth_discrete a : Discrete a → Discrete (●F a).
  Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.

Global Instancefrac_auth_frag_discrete q a : Discrete a → Discrete (◯F{q} a).
  Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed.

Lemma frac_auth_validNn a : ✓{n} a → ✓{n} (●F a ⋅ ◯F a).
  Proof. by rewrite auth_both_validN. Qed.

Lemma frac_auth_valida : ✓ a → ✓ (●F a ⋅ ◯F a).
  Proof. intros. by apply auth_both_valid_2. Qed.

Lemma frac_auth_agreeNn a b : ✓{n} (●F a ⋅ ◯F b) → a ≡{n}≡ b.
  Proof.
    rewrite auth_both_validN /= => -[Hincl Hvalid].
    by move: Hincl=> /Some_includedN_exclusive /(_ Hvalid ) [??].
  Qed.

Lemma frac_auth_agreea b : ✓ (●F a ⋅ ◯F b) → a ≡ b.
  Proof.
    intros. apply equiv_dist=> n. by apply frac_auth_agreeN, cmra_valid_validN.
  Qed.

Lemma frac_auth_agree_L`{!LeibnizEquiv A} a b : ✓ (●F a ⋅ ◯F b) → a = b.
  Proof. intros. by apply leibniz_equiv, frac_auth_agree. Qed.

Lemma frac_auth_includedNn q a b : ✓{n} (●F a ⋅ ◯F{q} b) → Some b ≼{n} Some a.
  Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.

Lemma frac_auth_included`{!CmraDiscrete A} q a b :
    ✓ (●F a ⋅ ◯F{q} b) → Some b ≼ Some a.
  Proof. by rewrite auth_both_valid_discrete /= => -[/Some_pair_included [_ ?] _]. Qed.

Lemma frac_auth_includedN_total`{!CmraTotal A} n q a b :
    ✓{n} (●F a ⋅ ◯F{q} b) → b ≼{n} a.
  Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.

Lemma frac_auth_included_total`{!CmraDiscrete A, !CmraTotal A} q a b :
    ✓ (●F a ⋅ ◯F{q} b) → b ≼ a.
  Proof. intros. by eapply Some_included_total, frac_auth_included. Qed.

Lemma frac_auth_auth_validNn a : ✓{n} (●F a) ↔ ✓{n} a.
  Proof.
    rewrite auth_auth_dfrac_validN Some_validN. split.
    - by intros [?[]].
    - intros. by split.
  Qed.

Lemma frac_auth_auth_valida : ✓ (●F a) ↔ ✓ a.
  Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed.

Lemma frac_auth_frag_validNn q a : ✓{n} (◯F{q} a) ↔ (q ≤ 1)%Qp ∧ ✓{n} a.
  Proof. by rewrite /frac_auth_frag auth_frag_validN. Qed.

Lemma frac_auth_frag_validq a : ✓ (◯F{q} a) ↔ (q ≤ 1)%Qp ∧ ✓ a.
  Proof. by rewrite /frac_auth_frag auth_frag_valid. Qed.

Lemma frac_auth_frag_opq1 q2 a1 a2 : ◯F{q1+q2} (a1 ⋅ a2) ≡ ◯F{q1} a1 ⋅ ◯F{q2} a2.
  Proof. done. Qed.

Lemma frac_auth_frag_op_validNn q1 q2 a b :
    ✓{n} (◯F{q1} a ⋅ ◯F{q2} b) ↔ (q1 + q2 ≤ 1)%Qp ∧ ✓{n} (a ⋅ b).
  Proof. by rewrite -frac_auth_frag_op frac_auth_frag_validN. Qed.

Lemma frac_auth_frag_op_validq1 q2 a b :
    ✓ (◯F{q1} a ⋅ ◯F{q2} b) ↔ (q1 + q2 ≤ 1)%Qp ∧ ✓ (a ⋅ b).
  Proof. by rewrite -frac_auth_frag_op frac_auth_frag_valid. Qed.

Global Instancefrac_auth_is_op (q q1 q2 : frac) (a a1 a2 : A) :
    IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2).
  Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.

Global Instancefrac_auth_is_op_core_id (q q1 q2 : frac) (a  : A) :
    CoreId a → IsOp q q1 q2 → IsOp' (◯F{q} a) (◯F{q1} a) (◯F{q2} a).
  Proof.
    rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
    by rewrite -frac_auth_frag_op -core_id_dup.
  Qed.

Lemma frac_auth_updateq a b a' b' :
    (a,b) ~l~> (a',b') → ●F a ⋅ ◯F{q} b ~~> ●F a' ⋅ ◯F{q} b'.
  Proof.
    intros. by apply auth_update, option_local_update, prod_local_update_2.
  Qed.

Lemma frac_auth_update_1a b a' : ✓ a' → ●F a ⋅ ◯F b ~~> ●F a' ⋅ ◯F a'.
  Proof.
    intros. by apply auth_update, option_local_update, exclusive_local_update.
  Qed.

Definition frac_authURF{SI : sidx} (F : rFunctor) : urFunctor :=
  authURF (optionURF (prodRF (constRF fracR) F)).

Global Instancefrac_authURF_contractive {SI : sidx} F :
  rFunctorContractive F → urFunctorContractive (frac_authURF F).
Proof. apply _. Qed.

Definition frac_authRF{SI : sidx} (F : rFunctor) : rFunctor :=
  authRF (optionURF (prodRF (constRF fracR) F)).

Global Instancefrac_authRF_contractive {SI : sidx} F :
  rFunctorContractive F → rFunctorContractive (frac_authRF F).
Proof. apply _. Qed.