(* iris/base_logic/bi.v *)
From iris.bi Require Export derived_connectives extensions
From iris.bi Require Export sbi updates internal_eq plainly cmra
From iris.si_logic Require Export bi
From iris.bi Require Import derived_laws derived_laws_later
From iris.base_logic Require Export upred
From iris.prelude Require Import options

Local ExistingInstance entails_po.

Definition uPred_pure{M} (φ : Prop) : uPred M := uPred_si_pure ⌜ φ ⌝.

Definition uPred_emp{M} : uPred M := uPred_pure True.

Local Lemmapure_ne {M} n : Proper (iff ==> dist n) (@uPred_pure M).
Proof. intros φ1 φ2 Hφ. apply si_pure_ne. by rewrite Hφ. Qed.

Local Lemmapure_intro {M} (φ : Prop) (P : uPred M) :
  φ → uPred_entails P (uPred_pure φ).
Proof.
  intros. trans (uPred_si_pure (∀ x : False, True) : uPred M).
  - etrans; last apply si_pure_forall_2. by apply forall_intro.
  - by apply si_pure_mono, bi.pure_intro.
Qed.

Local Lemmapure_elim' {M} (φ : Prop) (P : uPred M) :
  (φ → uPred_entails (uPred_pure True) P) →
  uPred_entails (uPred_pure φ) P.
Proof.
  intros HφP. etrans; last apply persistently_elim.
  etrans; last apply si_pure_si_emp_valid.
  apply si_pure_mono. apply bi.pure_elim'=> ?.
  rewrite -(si_emp_valid_si_pure True). by apply si_emp_valid_mono, HφP.
Qed.

Lemma uPred_bi_mixin(M : ucmra) :
  BiMixin
    uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand.
Proof.
  split.
  - exact: entails_po.
  - exact: equiv_entails.
  - exact: pure_ne.
  - exact: and_ne.
  - exact: or_ne.
  - exact: impl_ne.
  - exact: forall_ne.
  - exact: exist_ne.
  - exact: sep_ne.
  - exact: wand_ne.
  - exact: pure_intro.
  - exact: pure_elim'.
  - exact: and_elim_l.
  - exact: and_elim_r.
  - exact: and_intro.
  - exact: or_intro_l.
  - exact: or_intro_r.
  - exact: or_elim.
  - exact: impl_intro_r.
  - exact: impl_elim_l'.
  - exact: @forall_intro.
  - exact: @forall_elim.
  - exact: @exist_intro.
  - exact: @exist_elim.
  - exact: sep_mono.
  - exact: True_sep_1.
  - exact: True_sep_2.
  - exact: sep_comm'.
  - exact: sep_assoc'.
  - exact: wand_intro_r.
  - exact: wand_elim_l'.
Qed.

Lemma uPred_bi_persistently_mixin(M : ucmra) :
  BiPersistentlyMixin
    uPred_entails uPred_emp uPred_and
    (@uPred_exist M) uPred_sep uPred_persistently.
Proof.
  split.
  - exact: persistently_ne.
  - exact: persistently_mono.
  - exact: persistently_idemp_2.
  -
    trans (uPred_forall (M:=M) (λ _ : False, uPred_persistently uPred_emp)).
    + apply forall_intro=>-[].
    + etrans; first exact: persistently_forall_2.
      by apply persistently_mono, pure_intro.
  -
    intros P Q.
    trans (uPred_forall (M:=M) (λ b : bool, uPred_persistently (if b then P else Q))).
    + apply forall_intro=>[[]].
      * apply and_elim_l.
      * apply and_elim_r.
    + etrans; first exact: persistently_forall_2.
      apply persistently_mono. apply and_intro.
      * etrans; first apply (forall_elim true). done.
      * etrans; first apply (forall_elim false). done.
  - exact: @persistently_exist_1.
  -
    intros. etrans; first exact: sep_comm'.
    etrans; last exact: True_sep_2.
    apply sep_mono; last done. by apply pure_intro.
  - exact: persistently_and_sep_l_1.
Qed.

Lemma uPred_bi_later_mixin(M : ucmra) :
  BiLaterMixin
    uPred_entails uPred_pure uPred_or uPred_impl
    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_persistently uPred_later.
Proof.
  split.
  - apply contractive_ne, later_contractive.
  - exact: later_mono.
  - exact: later_intro.
  - exact: @later_forall_2.
  - exact: @later_exist_false.
  - exact: later_sep_1.
  - exact: later_sep_2.
  - exact: later_persistently_1.
  - exact: later_persistently_2.
  - exact: later_false_em.
Qed.
Canonical Structure uPredI (M : ucmra) : bi :=
  {| bi_ofe_mixin := ofe_mixin_of (uPred M);
     bi_bi_mixin := uPred_bi_mixin M;
     bi_bi_later_mixin := uPred_bi_later_mixin M;
     bi_bi_persistently_mixin := uPred_bi_persistently_mixin M |}.

Lemma uPred_sbi_mixinM : SbiMixin (uPredI M) uPred_si_pure uPred_si_emp_valid.
Proof.
  split.
  - exact: si_pure_ne.
  - exact: si_emp_valid_ne.
  - exact: si_pure_mono.
  - exact: si_emp_valid_mono.
  - exact: si_emp_valid_si_pure.
  - exact: si_pure_si_emp_valid.
  - exact: si_pure_impl_2.
  - exact: @si_pure_forall_2.
  - exact: si_pure_later.
  -
    intros Pi. apply True_sep_2.
  - exact: @si_emp_valid_later_1.
  -
    intros P. apply si_emp_valid_mono, and_intro; [|done].
    apply bi.True_intro.
Qed.

Lemma uPred_sbi_prop_ext_mixinM : SbiPropExtMixin (uPredI M) uPred_si_emp_valid.
Proof. apply sbi_prop_ext_mixin. apply prop_ext_2. Qed.

Global InstanceuPred_sbi M : Sbi (uPredI M) :=
  {| sbi_sbi_mixin := uPred_sbi_mixin M;
     sbi_sbi_prop_ext_mixin := uPred_sbi_prop_ext_mixin M |}.

Lemma uPred_bupd_mixinM : BiBUpdMixin (uPredI M) uPred_bupd.
Proof.
  split.
  - exact: bupd_ne.
  - exact: bupd_intro.
  - exact: bupd_mono.
  - exact: bupd_trans.
  - exact: bupd_frame_r.
Qed.

Global InstanceuPred_bi_bupd M : BiBUpd (uPredI M) :=
  {| bi_bupd_mixin := uPred_bupd_mixin M |}.

Global InstanceuPred_affine M : BiAffine (uPredI M) | 0.
Proof. intros P. exact: bi.pure_intro. Qed.

Global HintImmediate uPred_affine : core.

Global InstanceuPred_persistently_forall M : BiPersistentlyForall (uPredI M).
Proof. exact: @persistently_forall_2. Qed.

Global InstanceuPred_pure_forall M : BiPureForall (uPredI M).
Proof.
  intros A φ. etrans; [apply si_pure_forall_2|].
  apply si_pure_mono, pure_forall_2.
Qed.

Global InstanceuPred_later_contractive {M} : BiLaterContractive (uPredI M).
Proof. exact: @later_contractive. Qed.

Global InstanceuPred_sbi_emp_valid_exist {M} : SbiEmpValidExist (uPredI M).
Proof. exact: @si_emp_valid_exist_1. Qed.

Global InstanceuPred_persistently_impl_si_pure M :
  BiPersistentlyImplSiPure (uPredI M).
Proof. exact: persistently_impl_si_pure. Qed.

Global InstanceuPred_bi_bupd_sbi M : BiBUpdSbi (uPredI M).
Proof. exact: bupd_si_pure. Qed.

Global InstanceownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.

Lemma ownM_valid(a : M) : uPred_ownM a ⊢ ✓ a.
  Proof. exact: uPred_primitive.ownM_valid. Qed.

Lemma ownM_op(a1 a2 : M) :
    uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
  Proof. exact: uPred_primitive.ownM_op. Qed.

Lemma persistently_ownM_core(a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
  Proof. exact: uPred_primitive.persistently_ownM_core. Qed.

Lemma ownM_unitP : P ⊢ uPred_ownM ε.
  Proof. exact: uPred_primitive.ownM_unit. Qed.

Lemma later_ownMa : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
  Proof. exact: uPred_primitive.later_ownM. Qed.

Lemma bupd_ownM_updatePx (Φ : M → Prop) :
    x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
  Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.

Lemma ownM_forall{A} (f : A → M) :
    (∀ a, uPred_ownM (f a)) ⊢ ∃ z, uPred_ownM z ∧ (∀ a, f a ≼ z).
  Proof. exact: uPred_primitive.ownM_forall. Qed.

Local LemmauPred_emp_unseal :
    bi_emp = @upred.uPred_si_pure_def M (siprop.siProp_pure_def True).
  Proof. by rewrite -upred.uPred_si_pure_unseal -siprop.siProp_pure_unseal. Qed.

Local LemmauPred_pure_unseal :
    bi_pure = λ φ, @upred.uPred_si_pure_def M (siprop.siProp_pure_def φ).
  Proof. by rewrite -upred.uPred_si_pure_unseal -siprop.siProp_pure_unseal. Qed.

Local LemmauPred_si_pure_unseal : si_pure = @upred.uPred_si_pure_def M.
  Proof. by rewrite -upred.uPred_si_pure_unseal. Qed.

Local LemmauPred_si_emp_valid_unseal :
    si_emp_valid = @upred.uPred_si_emp_valid_def M.
  Proof. by rewrite -upred.uPred_si_emp_valid_unseal. Qed.

Local LemmauPred_and_unseal : bi_and = @upred.uPred_and_def M.
  Proof. by rewrite -upred.uPred_and_unseal. Qed.

Local LemmauPred_or_unseal : bi_or = @upred.uPred_or_def M.
  Proof. by rewrite -upred.uPred_or_unseal. Qed.

Local LemmauPred_impl_unseal : bi_impl = @upred.uPred_impl_def M.
  Proof. by rewrite -upred.uPred_impl_unseal. Qed.

Local LemmauPred_forall_unseal : @bi_forall _ = @upred.uPred_forall_def M.
  Proof. by rewrite -upred.uPred_forall_unseal. Qed.

Local LemmauPred_exist_unseal : @bi_exist _ = @upred.uPred_exist_def M.
  Proof. by rewrite -upred.uPred_exist_unseal. Qed.

Local LemmauPred_sep_unseal : bi_sep = @upred.uPred_sep_def M.
  Proof. by rewrite -upred.uPred_sep_unseal. Qed.

Local LemmauPred_wand_unseal : bi_wand = @upred.uPred_wand_def M.
  Proof. by rewrite -upred.uPred_wand_unseal. Qed.

Local LemmauPred_persistently_unseal :
    bi_persistently = @upred.uPred_persistently_def M.
  Proof. by rewrite -upred.uPred_persistently_unseal. Qed.

Local LemmauPred_later_unseal : bi_later = @upred.uPred_later_def M.
  Proof. by rewrite -upred.uPred_later_unseal. Qed.

Local LemmauPred_bupd_unseal : bupd = @upred.uPred_bupd_def M.
  Proof. by rewrite -upred.uPred_bupd_unseal. Qed.

Local DefinitionuPred_unseal :=
    (uPred_emp_unseal, uPred_pure_unseal,
    uPred_si_pure_unseal, uPred_si_emp_valid_unseal,
    uPred_and_unseal, uPred_or_unseal,
    uPred_impl_unseal, uPred_forall_unseal, uPred_exist_unseal,
    uPred_sep_unseal, uPred_wand_unseal,
    uPred_persistently_unseal, uPred_later_unseal,
    upred.uPred_ownM_unseal, @uPred_bupd_unseal).

Ltac unseal:= rewrite !uPred_unseal /=.