(* iris/algebra/dfrac.v *)
From stdpp Require Import countable
From iris.algebra Require Export cmra
From iris.algebra Require Import proofmode_classes updates frac
From iris.prelude Require Import options

Inductive dfrac:=
  | DfracOwn : Qp → dfrac
  | DfracDiscarded : dfrac
  | DfracBoth : Qp → dfrac.

Global Instancedfrac_inhabited : Inhabited dfrac := populate DfracDiscarded.

Global Instancedfrac_eq_dec : EqDecision dfrac.
  Proof. solve_decision. Defined.

Global Instancedfrac_countable : Countable dfrac.
  Proof.
    set (enc dq := match dq with
      | DfracOwn q => inl q
      | DfracDiscarded => inr (inl ())
      | DfracBoth q => inr (inr q)
      end).
    set (dec y := Some match y with
      | inl q => DfracOwn q
      | inr (inl ()) => DfracDiscarded
      | inr (inr q) => DfracBoth q
      end).
    refine (inj_countable enc dec _). by intros [].
  Qed.

Global InstanceDfracOwn_inj : Inj (=) (=) DfracOwn.
  Proof. by injection 1. Qed.

Global InstanceDfracBoth_inj : Inj (=) (=) DfracBoth.
  Proof. by injection 1. Qed.

Local Instancedfrac_valid_instance : Valid dfrac := λ dq,
    match dq with
    | DfracOwn q => q ≤ 1
    | DfracDiscarded => True
    | DfracBoth q => q < 1
    end%Qp.

Local Instancedfrac_pcore_instance : PCore dfrac := λ dq,
    match dq with
    | DfracOwn q => None
    | DfracDiscarded => Some DfracDiscarded
    | DfracBoth q => Some DfracDiscarded
    end.

Local Instancedfrac_op_instance : Op dfrac := λ dq dp,
    match dq, dp with
    | DfracOwn q, DfracOwn q' => DfracOwn (q + q')
    | DfracOwn q, DfracDiscarded => DfracBoth q
    | DfracOwn q, DfracBoth q' => DfracBoth (q + q')
    | DfracDiscarded, DfracOwn q' => DfracBoth q'
    | DfracDiscarded, DfracDiscarded => DfracDiscarded
    | DfracDiscarded, DfracBoth q' => DfracBoth q'
    | DfracBoth q, DfracOwn q' => DfracBoth (q + q')
    | DfracBoth q, DfracDiscarded => DfracBoth q
    | DfracBoth q, DfracBoth q' => DfracBoth (q + q')
    end.

Lemma dfrac_validdq :
    ✓ dq ↔ match dq with
           | DfracOwn q => q ≤ 1
           | DfracDiscarded => True
           | DfracBoth q => q < 1
           end%Qp.
  Proof. done. Qed.

Lemma dfrac_op_ownq p : DfracOwn p ⋅ DfracOwn q = DfracOwn (p + q).
  Proof. done. Qed.

Lemma dfrac_op_discarded:
    DfracDiscarded ⋅ DfracDiscarded = DfracDiscarded.
  Proof. done. Qed.

Lemma dfrac_own_includedq p : DfracOwn q ≼ DfracOwn p ↔ (q < p)%Qp.
  Proof.
    rewrite Qp.lt_sum. split.
    - rewrite /included /op /dfrac_op_instance. intros [[o| |?] [= ->]]. by exists o.
    - intros [o ->]. exists (DfracOwn o). by rewrite dfrac_op_own.
  Qed.

Lemma dfrac_discarded_included:
    DfracDiscarded ≼ DfracDiscarded.
  Proof. exists DfracDiscarded. done. Qed.

Definition dfrac_ra_mixin: RAMixin dfrac.
  Proof.
    split; try apply _.
    - intros [?| |?] ? dq <-; intros [= <-]; eexists _; done.
    - intros [?| |?] [?| |?] [?| |?];
        rewrite /op /dfrac_op_instance 1?assoc_L 1?assoc_L; done.
    - intros [?| |?] [?| |?];
        rewrite /op /dfrac_op_instance 1?(comm_L Qp.add); done.
    - intros [?| |?] dq; rewrite /pcore /dfrac_pcore_instance; intros [= <-];
        rewrite /op /dfrac_op_instance; done.
    - intros [?| |?] ? [= <-]; done.
    - intros [?| |?] [?| |?] ? [[?| |?] [=]] [= <-]; eexists _; split; try done;
        apply dfrac_discarded_included.
    - intros [q| |q] [q'| |q']; rewrite /op /dfrac_op_instance /valid /dfrac_valid_instance //.
      + intros. trans (q + q')%Qp; [|done]. apply Qp.le_add_l.
      + apply Qp.lt_le_incl.
      + intros. trans (q + q')%Qp; [|by apply Qp.lt_le_incl]. apply Qp.le_add_l.
      + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
      + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
  Qed.
  Canonical Structure dfracR := discreteR dfrac dfrac_ra_mixin.

Global Instancedfrac_cmra_discrete : CmraDiscrete dfracR.
  Proof. apply discrete_cmra_discrete. Qed.

Global Instancedfrac_full_exclusive : Exclusive (DfracOwn 1).
  Proof.
    intros [q| |q];
      rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid //=.
    - apply Qp.not_add_le_l.
    - move=> /Qp.lt_le_incl. apply Qp.not_add_le_l.
  Qed.

Global Instancedfrac_cancelable q : Cancelable (DfracOwn q).
  Proof.
    apply: discrete_cancelable.
    intros [q1| |q1][q2| |q2] _ [=]; simplify_eq/=; try done.
    - by destruct (Qp.add_id_free q q2).
    - by destruct (Qp.add_id_free q q1).
  Qed.

Global Instancedfrac_own_id_free q : IdFree (DfracOwn q).
  Proof. intros [q'| |q'] _ [=]. by apply (Qp.add_id_free q q'). Qed.

Global Instancedfrac_discarded_core_id : CoreId DfracDiscarded.
  Proof. by constructor. Qed.

Lemma dfrac_valid_ownp : ✓ DfracOwn p ↔ (p ≤ 1)%Qp.
  Proof. done. Qed.

Lemma dfrac_valid_own_1: ✓ DfracOwn 1.
  Proof. done. Qed.

Lemma dfrac_valid_own_rdq q : ✓ (dq ⋅ DfracOwn q) → (q < 1)%Qp.
  Proof.
    destruct dq as [q'| |q']; [|done|].
    - apply Qp.lt_le_trans, Qp.lt_add_r.
    - intro Hlt. etrans; last apply Hlt. apply Qp.lt_add_r.
  Qed.

Lemma dfrac_valid_own_ldq q : ✓ (DfracOwn q ⋅ dq) → (q < 1)%Qp.
  Proof using SI. rewrite comm. apply dfrac_valid_own_r. Qed.

Lemma dfrac_valid_discarded: ✓ DfracDiscarded.
  Proof. done. Qed.

Lemma dfrac_valid_own_discardedq :
    ✓ (DfracOwn q ⋅ DfracDiscarded) ↔ (q < 1)%Qp.
  Proof. done. Qed.

Global Instancedfrac_is_op q q1 q2 :
    IsOp q q1 q2 →
    IsOp' (DfracOwn q) (DfracOwn q1) (DfracOwn q2).
  Proof. rewrite /IsOp' /IsOp dfrac_op_own=>-> //. Qed.

Lemma dfrac_discard_updatedq : dq ~~> DfracDiscarded.
  Proof.
    intros n [[q'| |q']|]; rewrite -!cmra_discrete_valid_iff //=.
    - apply dfrac_valid_own_r.
    - apply cmra_valid_op_r.
  Qed.

Lemma dfrac_undiscard_update: DfracDiscarded ~~>: λ k, ∃ q, k = DfracOwn q.
  Proof.
    apply cmra_discrete_updateP. intros [[q'| |q']|].
    - intros [qd Hqd]%Qp.lt_sum. exists (DfracOwn (qd/2)%Qp).
      split; first by eexists. apply dfrac_valid_own.
      rewrite Hqd Qp.add_comm -Qp.add_le_mono_l.
      by apply Qp.div_le.
    - intros _. exists (DfracOwn (1/2)); split; first by eexists.
      by apply dfrac_valid_own_discarded.
    - intros [qd Hqd]%Qp.lt_sum. exists (DfracOwn (qd/2)%Qp).
      split; first by eexists. rewrite /= /op /valid /cmra_op /cmra_valid /=.
      rewrite Hqd Qp.add_comm -Qp.add_lt_mono_l.
      by apply Qp.div_lt.
    - intros _. exists (DfracOwn 1); split; first by eexists.
      by apply dfrac_valid_own.
  Qed.