(* iris/bi/algebra.v *)
From iris.algebra Require Import cmra view auth agree csum list excl gmap
From iris.algebra.lib Require Import excl_auth gmap_view dfrac_agree
From iris.bi Require Export sbi_unfold derived_laws
From iris.prelude Require Import options

Local SetDefault Proof Using "Type*".

Lemma ucmra_unit_validI{A : ucmra} : ⊢ ✓ (ε : A).
  Proof. sbi_unfold. apply ucmra_unit_validN. Qed.

Lemma cmra_validI_op_r{A : cmra} (x y : A) : ✓ (x ⋅ y) ⊢ ✓ y.
  Proof. sbi_unfold=> n. apply cmra_validN_op_r. Qed.

Lemma cmra_validI_op_l{A : cmra} (x y : A) : ✓ (x ⋅ y) ⊢ ✓ x.
  Proof. sbi_unfold=> n. apply cmra_validN_op_l. Qed.

Lemma cmra_later_opI`{!CmraTotal A} (x y1 y2 : A) :
    ▷ (✓ x ∧ x ≡ y1 ⋅ y2) ⊢ ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ ▷ (z1 ≡ y1) ∧ ▷ (z2 ≡ y2).
  Proof.
    sbi_unfold=> -[|n].
    - intros _. exists x, (core x). by rewrite cmra_core_r.
    - intros [??].
      destruct (cmra_extend n x y1 y2) as (z1 & z2 & ? & ? & ?); [done..|].
      exists z1, z2. auto using equiv_dist.
  Qed.

Lemma cmra_morphism_validI{A B : cmra} (f : A → B) `{!CmraMorphism f} x :
    ✓ x ⊢ ✓ (f x).
  Proof. sbi_unfold=> n. by apply cmra_morphism_validN. Qed.

Lemma prod_validI{A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
  Proof. by sbi_unfold. Qed.

Lemma prod_includedI{A B : cmra} (x y : A * B) :
    x ≼ y ⊣⊢ x.1 ≼ y.1 ∧ x.2 ≼ y.2.
  Proof. sbi_unfold=> n. apply prod_includedN. Qed.

Lemma option_validI{A : cmra} (mx : option A) :
    ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
  Proof. sbi_unfold=> n. by destruct mx. Qed.

Lemma option_includedI{A : cmra} (mx my : option A) :
    mx ≼ my ⊣⊢ match mx, my with
               | Some x, Some y => (x ≼ y) ∨ (x ≡ y)
               | None, _ => True
               | Some x, None => False
               end.
  Proof.
    sbi_unfold=> n. destruct mx, my; rewrite ?option_includedN; naive_solver.
  Qed.

Lemma option_included_totalI`{!CmraTotal A} (mx my : option A) :
    mx ≼ my ⊣⊢ match mx, my with
               | Some x, Some y => x ≼ y
               | None, _ => True
               | Some x, None => False
               end.
  Proof.
    sbi_unfold=> n; destruct mx, my;
      rewrite ?Some_includedN_total ?option_includedN; naive_solver.
  Qed.

Lemma Some_included_totalI`{!CmraTotal A} (x y : A) :
    Some x ≼ Some y ⊣⊢ x ≼ y.
  Proof. by rewrite option_included_totalI. Qed.

Lemma discrete_fun_validI{A} {B : A → ucmra} (g : discrete_fun B) :
    ✓ g ⊣⊢ ∀ i, ✓ g i.
  Proof. by sbi_unfold. Qed.

Lemma f_homom_includedI{A B : cmra} (x y : A) (f : A → B) `{!NonExpansive f} :

Lemma id_freeI_r{A : cmra} (x y : A) :
    IdFree x → ⊢@{PROP} ✓ x -∗ (x ⋅ y) ≡ x -∗ False.
  Proof. intros. sbi_unfold. eauto using id_freeN_r. Qed.

Lemma id_freeI_l{A : cmra} (x y : A) :
    IdFree x → ⊢ ✓ x -∗ (y ⋅ x) ≡ x -∗ False.
  Proof. intros. sbi_unfold. eauto using id_freeN_l. Qed.

Lemma gmap_equivIm1 m2 : m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
    Proof. by sbi_unfold. Qed.

Lemma gmap_union_equiv_eqIm m1 m2 :
      m ≡ m1 ∪ m2 ⊣⊢ ∃ m1' m2', ⌜ m = m1' ∪ m2' ⌝ ∧ m1' ≡ m1 ∧ m2' ≡ m2.
    Proof. sbi_unfold=> n. apply gmap_union_dist_eq. Qed.

Lemma gmap_validIm : ✓ m ⊣⊢ ∀ i, ✓ (m !! i).
    Proof. by sbi_unfold. Qed.

Lemma singleton_validIi x : ✓ ({[ i := x ]} : gmap K A) ⊣⊢ ✓ x.
    Proof. sbi_unfold=> n. apply singleton_validN. Qed.

Lemma list_equivIl1 l2 : l1 ≡ l2 ⊣⊢ ∀ i, l1 !! i ≡ l2 !! i.
    Proof. sbi_unfold. intros n. apply list_dist_lookup. Qed.

Lemma excl_equivIx y :
      x ≡ y ⊣⊢ match x, y with
                          | Excl a, Excl b => a ≡ b
                          | ExclInvalid, ExclInvalid => True
                          | _, _ => False
                          end.
    Proof.
      sbi_unfold; split; [by destruct 1|destruct x, y; by repeat constructor].
    Qed.

Lemma excl_validIx :
      ✓ x ⊣⊢ if x is ExclInvalid then False else True.
    Proof. by sbi_unfold. Qed.

Lemma excl_includedI(x y : excl A) :
      x ≼ y ⊣⊢ ⌜ y = ExclInvalid ⌝.
    Proof. sbi_unfold=> n; apply excl_includedN. Qed.

Lemma agree_equivIa b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b).
    Proof. sbi_unfold=> n. apply: inj_iff. Qed.

Lemma agree_op_invIx y : ✓ (x ⋅ y) ⊢ x ≡ y.
    Proof. sbi_unfold=> n. apply agree_op_invN. Qed.

Lemma to_agree_validIa : ⊢ ✓ to_agree a.
    Proof. by sbi_unfold. Qed.

Lemma to_agree_op_validIa b : ✓ (to_agree a ⋅ to_agree b) ⊣⊢ a ≡ b.
    Proof. sbi_unfold. apply to_agree_op_validN. Qed.

Lemma to_agree_uninjIx : ✓ x ⊢ ∃ a, to_agree a ≡ x.
    Proof. sbi_unfold=> n. exact: to_agree_uninjN. Qed.

Lemma agree_op_equiv_to_agreeIx y a :
      x ⋅ y ≡ to_agree a ⊢ x ≡ y ∧ y ≡ to_agree a.
    Proof.
      assert (x ⋅ y ≡ to_agree a ⊢ x ≡ y) as Hxy_equiv.
      { rewrite -(agree_op_invI x y) internal_eq_sym.
        apply: (internal_eq_rewrite' _ _ (λ o, ✓ o)%I); [solve_proper|done|].
        rewrite -(bi.absorbing_absorbingly (✓ _)).
        rewrite -to_agree_validI bi.absorbingly_emp_True. apply bi.True_intro. }
      apply bi.and_intro; first done.
      rewrite -{1}(idemp bi_and (_ ≡ _)%I) {1}Hxy_equiv. apply bi.impl_elim_l'.
      apply: (internal_eq_rewrite' _ _
        (λ y', x ⋅ y' ≡ to_agree a → y' ≡ to_agree a)%I); [solve_proper|done|].
      rewrite agree_idemp. apply bi.impl_refl.
    Qed.

Lemma agree_includedI(x y : agree A) : x ≼ y ⊣⊢ y ≡ x ⋅ y.
    Proof. sbi_unfold=> n. apply agree_includedN. Qed.

Lemma to_agree_includedIa b : to_agree a ≼ to_agree b ⊣⊢ a ≡ b.
    Proof. sbi_unfold=> n. apply: to_agree_includedN. Qed.

Lemma csum_equivI(x y : csum A B) :
      x ≡ y ⊣⊢ match x, y with
                          | Cinl a, Cinl a' => a ≡ a'
                          | Cinr b, Cinr b' => b ≡ b'
                          | CsumInvalid, CsumInvalid => True
                          | _, _ => False
                          end.
    Proof.
      sbi_unfold; split; [by destruct 1|destruct x, y; by repeat constructor].
    Qed.

Lemma csum_validI(x : csum A B) :
      ✓ x ⊣⊢ match x with
                        | Cinl a => ✓ a
                        | Cinr b => ✓ b
                        | CsumInvalid => False
                        end.
    Proof. by sbi_unfold. Qed.

Lemma csum_includedI(sx sy : csum A B) :
      sx ≼ sy ⊣⊢ match sx, sy with
                 | Cinl x, Cinl y => x ≼ y
                 | Cinr x, Cinr y => x ≼ y
                 | _, CsumInvalid => True
                 | _, _ => False
                 end.
    Proof.
      sbi_unfold=> n; destruct sx, sy; rewrite ?csum_includedN; naive_solver.
    Qed.

Lemma view_both_dfrac_validI_1(relI : siProp) dq a b :
      (∀ n, rel n a b → siProp_holds relI n) →
      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊢ ⌜✓dq⌝ ∧ <si_pure> relI.
    Proof.
      intros. sbi_unfold=> n. rewrite view_both_dfrac_validN. naive_solver.
    Qed.

Lemma view_both_dfrac_validI_2(relI : siProp) dq a b :
      (∀ n, siProp_holds relI n → rel n a b) →
      ⌜✓dq⌝ ∧ <si_pure> relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
    Proof.
      intros. sbi_unfold=> n. rewrite view_both_dfrac_validN. naive_solver.
    Qed.

Lemma view_both_dfrac_validI(relI : siProp) dq a b :
      (∀ n, rel n a b ↔ siProp_holds relI n) →
      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊣⊢ ⌜✓dq⌝ ∧ <si_pure> relI.
    Proof.
      intros. apply (anti_symm _);
        [apply view_both_dfrac_validI_1|apply view_both_dfrac_validI_2]; naive_solver.
    Qed.

Lemma view_both_validI_1(relI : siProp) a b :
      (∀ n, rel n a b → siProp_holds relI n) →
      ✓ (●V a ⋅ ◯V b : view rel) ⊢ <si_pure> relI.
    Proof. intros. by rewrite view_both_dfrac_validI_1 // bi.and_elim_r. Qed.

Lemma view_both_validI_2(relI : siProp) a b :
      (∀ n, siProp_holds relI n → rel n a b) →
      <si_pure> relI ⊢ ✓ (●V a ⋅ ◯V b : view rel).
    Proof.
      intros. rewrite -view_both_dfrac_validI_2 //.
      apply bi.and_intro; [|done]. by apply bi.pure_intro.
    Qed.

Lemma view_both_validI(relI : siProp) a b :
      (∀ n, rel n a b ↔ siProp_holds relI n) →
      ✓ (●V a ⋅ ◯V b : view rel) ⊣⊢ <si_pure> relI.
    Proof.
      intros. apply (anti_symm _);
        [apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
    Qed.

Lemma view_auth_dfrac_validI(relI : siProp) dq a :
      (∀ n, siProp_holds relI n ↔ rel n a ε) →
      ✓ (●V{dq} a : view rel) ⊣⊢ ⌜✓dq⌝ ∧ <si_pure> relI.
    Proof.
      intros. rewrite -(right_id ε op (●V{dq} a)). by apply view_both_dfrac_validI.
    Qed.

Lemma view_auth_validI(relI : siProp) a :
      (∀ n, siProp_holds relI n ↔ rel n a ε) →
      ✓ (●V a : view rel) ⊣⊢ <si_pure> relI.
    Proof. intros. rewrite -(right_id ε op (●V a)). by apply view_both_validI. Qed.

Lemma view_frag_validI(relI : siProp) b :
      (∀ n, siProp_holds relI n ↔ ∃ a, rel n a b) →
      ✓ (◯V b : view rel) ⊣⊢ <si_pure> relI.
    Proof. intros Hrel. sbi_unfold=> n. by rewrite Hrel. Qed.

Lemma auth_auth_dfrac_validIdq a : ✓ (●{dq} a) ⊣⊢ ⌜✓dq⌝ ∧ ✓ a.
    Proof. sbi_unfold=> n. apply auth_auth_dfrac_validN. Qed.

Lemma auth_auth_validIa : ✓ (● a) ⊣⊢ ✓ a.
    Proof. sbi_unfold=> n. apply auth_auth_validN. Qed.

Lemma auth_auth_dfrac_op_validIdq1 dq2 a1 a2 :
      ✓ (●{dq1} a1 ⋅ ●{dq2} a2) ⊣⊢ ✓ (dq1 ⋅ dq2) ∧ (a1 ≡ a2) ∧ ✓ a1.
    Proof. sbi_unfold=> n. apply auth_auth_dfrac_op_validN. Qed.

Lemma auth_frag_validIa : ✓ (◯ a) ⊣⊢ ✓ a.
    Proof. sbi_unfold=> n. apply auth_frag_validN. Qed.

Lemma auth_both_dfrac_validIdq a b :
      ✓ (●{dq} a ⋅ ◯ b) ⊣⊢ ⌜✓dq⌝ ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
    Proof.  sbi_unfold=> n. apply auth_both_dfrac_validN. Qed.

Lemma auth_both_validIa b :
      ✓ (● a ⋅ ◯ b) ⊣⊢ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
    Proof. sbi_unfold=> n. apply auth_both_validN. Qed.

Lemma excl_auth_agreeIa b : ✓ (●E a ⋅ ◯E b) ⊢ (a ≡ b).
    Proof. sbi_unfold=> n. apply excl_auth_agreeN. Qed.

Lemma dfrac_agree_validIdq a : ✓ (to_dfrac_agree dq a) ⊣⊢ ⌜✓ dq⌝.
    Proof. sbi_unfold=> n. rewrite /to_dfrac_agree pair_validN. naive_solver. Qed.

Lemma dfrac_agree_validI_2dq1 dq2 a b :
      ✓ (to_dfrac_agree dq1 a ⋅ to_dfrac_agree dq2 b) ⊣⊢ ⌜✓ (dq1 ⋅ dq2)⌝ ∧ (a ≡ b).
    Proof.
      rewrite prod_validI /= internal_cmra_valid_discrete to_agree_op_validI //.
    Qed.

Lemma frac_agree_validIq a : ✓ (to_frac_agree q a) ⊣⊢ ⌜(q ≤ 1)%Qp⌝.
    Proof.
      rewrite dfrac_agree_validI dfrac_valid_own //.
    Qed.

Lemma frac_agree_validI_2q1 q2 a b :
      ✓ (to_frac_agree q1 a ⋅ to_frac_agree q2 b) ⊣⊢ ⌜(q1 + q2 ≤ 1)%Qp⌝ ∧ (a ≡ b).
    Proof.
      rewrite dfrac_agree_validI_2 dfrac_valid_own //.
    Qed.

Lemma gmap_view_both_dfrac_validIdp m k dq v :
      ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ⊣⊢
      ∃ v' dq', ⌜✓ dp⌝ ∧ ⌜m !! k = Some v'⌝ ∧ ✓ (dq', v') ∧
                Some (dq, v) ≼ Some (dq', v').
    Proof. sbi_unfold=> n. apply: gmap_view_both_dfrac_validN. Qed.

Lemma gmap_view_both_validIm dp k v :
      ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k (DfracOwn 1) v) ⊣⊢
      ⌜ ✓ dp ⌝ ∧ ✓ v ∧ m !! k ≡ Some v.
    Proof. sbi_unfold=> n. apply gmap_view_both_validN. Qed.

Lemma gmap_view_both_validI_total`{!CmraTotal V} dp m k dq v :
      ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ⊢
      ∃ v', ⌜✓ dp ⌝ ∧ ⌜ ✓ dq⌝ ∧ ⌜m !! k = Some v'⌝ ∧ ✓ v' ∧ v ≼ v'.
    Proof. sbi_unfold=> n. apply: gmap_view_both_dfrac_validN_total. Qed.

Lemma gmap_view_frag_op_validIk dq1 dq2 v1 v2 :
      ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊣⊢
      ⌜✓ (dq1 ⋅ dq2)⌝ ∧ ✓ (v1 ⋅ v2).
    Proof. sbi_unfold=> n. apply gmap_view_frag_op_validN. Qed.