(* iris/bi/sbi.v *)
From iris.si_logic Require Export bi
From iris.bi Require Import derived_laws derived_laws_later
From iris.prelude Require Import options

Local SetPrimitive Projections.

Class SiPure(PROP : Type) : Type := si_pure : siProp → PROP.

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

Global HintMode SiPure ! : typeclass_instances.

Global Argumentssi_pure {_}%_type_scope {_} _%_bi_scope.

Global TypeclassesOpaque si_pure.

Class SiEmpValid(PROP : Type) : Type := si_emp_valid : PROP → siProp.

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

Global HintMode SiEmpValid ! : typeclass_instances.

Global TypeclassesOpaque si_emp_valid.

Global Argumentssi_emp_valid {_}%_type_scope {_} _%_bi_scope.

Record SbiMixin(PROP : bi) `(!SiPure PROP, SiEmpValid PROP) := {

Record SbiPropExtMixin(PROP : bi) `(!SiEmpValid PROP) := {
  sbi_mixin_prop_ext_si_emp_valid_2 (P Q : PROP) :
    <si_emp_valid> (P ∗-∗ Q) ⊢@{siPropI} siProp_internal_eq P Q;
}.

Class Sbi(PROP : bi) := {
  #[global] sbi_si_pure :: SiPure PROP;
  #[global] sbi_si_emp_valid :: SiEmpValid PROP;
  sbi_sbi_mixin : SbiMixin PROP sbi_si_pure sbi_si_emp_valid;
  sbi_sbi_prop_ext_mixin : SbiPropExtMixin PROP sbi_si_emp_valid;
}.

Global HintMode Sbi ! : typeclass_instances.

Global Argumentssbi_si_pure : simpl never.

Global Argumentssbi_si_emp_valid : simpl never.

Class SbiEmpValidExistPROP `{!Sbi PROP} :=
  si_emp_valid_exist_1 : ∀ {A} (Φ : A → PROP),
    <si_emp_valid> (∃ x, Φ x) ⊢@{siPropI} ∃ x, <si_emp_valid> Φ x.

Global ArgumentsSbiEmpValidExist _ {_}.

Global Argumentssi_emp_valid_exist_1 _ {_ _} _.

Global HintMode SbiEmpValidExist ! - : typeclass_instances.

Class BiPersistentlyImplSiPurePROP `{!Sbi PROP} :=
  persistently_impl_si_pure Pi (Q : PROP) :
    (<si_pure> Pi → <pers> Q) ⊢ <pers> (<si_pure> Pi → Q).

Global ArgumentsBiPersistentlyImplSiPure _ {_}.

Global Argumentspersistently_impl_si_pure _ {_ _} _.

Global HintMode BiPersistentlyImplSiPure ! - : typeclass_instances.

Lemma siprop_sbi_mixin: SbiMixin siProp id id.
Proof.
  split; rewrite /si_pure /si_emp_valid; try (done || apply _).
  intros P. by rewrite bi.affine_affinely.
Qed.

Lemma siprop_sbi_prop_ext_mixin: SbiPropExtMixin siProp id.
Proof. split; intros P Q. apply siProp_primitive.prop_ext_2. Qed.

Global Instancesiprop_sbi : Sbi siPropI :=
  {| sbi_sbi_mixin := siprop_sbi_mixin;
     sbi_sbi_prop_ext_mixin := siprop_sbi_prop_ext_mixin |}.

Global Instancesiprop_sbi_emp_valid_exist : SbiEmpValidExist siPropI.
Proof. done. Qed.

Global Instancesiprop_bi_persistently_impl_si_pure :
  BiPersistentlyImplSiPure siPropI.
Proof. done. Qed.

Global Instancesi_pure_ne : NonExpansive (si_pure (PROP:=PROP)).
  Proof. eapply sbi_mixin_si_pure_ne, sbi_sbi_mixin. Qed.

Global Instancesi_emp_valid_ne : NonExpansive (si_emp_valid (PROP:=PROP)).
  Proof. eapply sbi_mixin_si_emp_valid_ne, sbi_sbi_mixin. Qed.

Lemma si_pure_monoPi Qi :
    (Pi ⊢@{siPropI} Qi) → <si_pure> Pi ⊢@{PROP} <si_pure> Qi.
  Proof. eapply sbi_mixin_si_pure_mono, sbi_sbi_mixin. Qed.

Lemma si_emp_valid_monoP Q :
    (P ⊢@{PROP} Q) → <si_emp_valid> P ⊢@{siPropI} <si_emp_valid> Q.
  Proof. eapply sbi_mixin_si_emp_valid_mono, sbi_sbi_mixin. Qed.

Lemma si_emp_valid_si_purePi :
    <si_emp_valid> <si_pure>@{PROP} Pi ⊣⊢@{siPropI} Pi.
  Proof. eapply sbi_mixin_si_emp_valid_si_pure, sbi_sbi_mixin. Qed.

Lemma si_pure_si_emp_valid(P : PROP) :
    <si_pure> <si_emp_valid> P ⊢ <pers> P.
  Proof. eapply sbi_mixin_si_pure_si_emp_valid, sbi_sbi_mixin. Qed.

Lemma si_pure_impl_2Pi Qi :
    (<si_pure> Pi → <si_pure> Qi) ⊢@{PROP} <si_pure> (Pi → Qi).
  Proof. eapply sbi_mixin_si_pure_impl_2, sbi_sbi_mixin. Qed.

Lemma si_pure_forall_2{A} (Φi : A → siProp) :
   (∀ x, <si_pure> Φi x) ⊢@{PROP} <si_pure> (∀ x, Φi x).
  Proof. eapply sbi_mixin_si_pure_forall_2, sbi_sbi_mixin. Qed.

Lemma si_pure_laterPi :
    <si_pure> ▷ Pi ⊣⊢@{PROP} ▷ <si_pure> Pi.
  Proof. eapply sbi_mixin_si_pure_later, sbi_sbi_mixin. Qed.

Global Instancesi_pure_absorbing Pi :
    Absorbing (PROP:=PROP) (<si_pure> Pi).
  Proof. eapply sbi_mixin_si_pure_absorbing, sbi_sbi_mixin. Qed.

Lemma si_emp_valid_affinely_2(P : PROP) :
    <si_emp_valid> P ⊢@{siPropI} <si_emp_valid> <affine> P.
  Proof. eapply sbi_mixin_si_emp_valid_affinely_2, sbi_sbi_mixin. Qed.

Lemma si_emp_valid_later_1(P : PROP) :
    <si_emp_valid> ▷ P ⊢@{siPropI} ▷ <si_emp_valid> P.
  Proof. eapply sbi_mixin_si_emp_valid_later_1, sbi_sbi_mixin. Qed.

Global Instancesi_pure_proper : Proper ((⊣⊢) ==> (⊣⊢)) (si_pure (PROP:=PROP)).
  Proof. apply (ne_proper _). Qed.

Global Instancesi_emp_valid_proper :
    Proper ((⊣⊢) ==> (⊣⊢)) (si_emp_valid (PROP:=PROP)).
  Proof. apply (ne_proper _). Qed.

Global Instancesi_pure_mono' : Proper ((⊢) ==> (⊢)) (si_pure (PROP:=PROP)).
  Proof. intros Pi Qi. apply si_pure_mono. Qed.

Global Instancesi_pure_flip_mono' :
    Proper (flip (⊢) ==> flip (⊢)) (si_pure (PROP:=PROP)).
  Proof. solve_proper. Qed.

Global Instancesi_emp_valid_mono' :
    Proper ((⊢) ==> (⊢)) (si_emp_valid (PROP:=PROP)).
  Proof. intros P Q. apply si_emp_valid_mono. Qed.

Global Instancesi_emp_valid_flip_mono' :
    Proper (flip (⊢) ==> flip (⊢)) (si_emp_valid (PROP:=PROP)).
  Proof. solve_proper. Qed.

Global Instancesi_pure_persistent Pi : Persistent (PROP:=PROP) (<si_pure> Pi).
  Proof.
    rewrite /Persistent.
    by rewrite -{1}(si_emp_valid_si_pure (PROP:=PROP) Pi) si_pure_si_emp_valid.
  Qed.

Lemma si_pure_forall{A} (Φi : A → siProp) :
    <si_pure> (∀ x, Φi x) ⊣⊢@{PROP} ∀ x, <si_pure> Φi x.
  Proof.
    apply (anti_symm _); [|apply si_pure_forall_2].
    apply bi.forall_intro=> x. by rewrite (bi.forall_elim x).
  Qed.

Lemma si_pure_exist{A} (Φi : A → siProp) :
    <si_pure> (∃ x, Φi x) ⊣⊢@{PROP} ∃ x, <si_pure> Φi x.
  Proof.
    apply (anti_symm _).
    - rewrite -(bi.persistent_persistently (∃ x, <si_pure> _)).
      rewrite -si_pure_si_emp_valid. f_equiv. apply bi.exist_elim=> x.
      by rewrite -(bi.exist_intro x) si_emp_valid_si_pure.
    - apply bi.exist_elim=> x. by rewrite -(bi.exist_intro x).
  Qed.

Lemma si_pure_andPi Qi :
    <si_pure> (Pi ∧ Qi) ⊣⊢@{PROP} <si_pure> Pi ∧ <si_pure> Qi.
  Proof. rewrite !bi.and_alt si_pure_forall. by f_equiv=> -[]. Qed.

Lemma si_pure_and_sepPi Qi :
    <si_pure> (Pi ∧ Qi) ⊣⊢@{PROP} <si_pure> Pi ∗ <si_pure> Qi.
  Proof.
    rewrite si_pure_and.
    apply (anti_symm _); [apply (bi.persistent_and_sep_1 _ _)|].
    apply bi.and_intro; [apply (bi.sep_elim_l _ _)|apply (bi.sep_elim_r _ _)].
  Qed.

Lemma si_pure_orPi Qi :
    <si_pure> (Pi ∨ Qi) ⊣⊢@{PROP} <si_pure> Pi ∨ <si_pure> Qi.
  Proof. rewrite !bi.or_alt si_pure_exist. by f_equiv=> -[]. Qed.

Lemma si_pure_pureφ : <si_pure> ⌜ φ ⌝ ⊣⊢@{PROP} ⌜ φ ⌝.
  Proof.
    rewrite bi.pure_alt si_pure_exist (bi.pure_alt φ). f_equiv=> _.
    apply (anti_symm _); [apply bi.True_intro|].
    trans (∀ _ : Empty_set, <si_pure>@{PROP} True)%I; [by apply bi.forall_intro|].
    rewrite -si_pure_forall. f_equiv. apply bi.True_intro.
  Qed.

Lemma si_pure_implPi Qi :
    <si_pure> (Pi → Qi) ⊣⊢@{PROP} (<si_pure> Pi → <si_pure> Qi).
  Proof.
    apply (anti_symm _); [|apply si_pure_impl_2].
    apply bi.impl_intro_l. by rewrite -si_pure_and bi.impl_elim_r.
  Qed.

Lemma si_pure_impl_wandPi Qi :
    <si_pure> (Pi → Qi) ⊣⊢@{PROP} (<si_pure> Pi -∗ <si_pure> Qi).
  Proof.
    apply (anti_symm _).
    - apply bi.wand_intro_l. by rewrite -si_pure_and_sep bi.impl_elim_r.
    - rewrite si_pure_impl. apply bi.impl_intro_l.
      by rewrite bi.persistent_and_affinely_sep_l bi.affinely_elim bi.wand_elim_r.
  Qed.

Lemma si_pure_iffPi Qi :
    <si_pure> (Pi ↔ Qi) ⊣⊢@{PROP} (<si_pure> Pi ↔ <si_pure> Qi).
  Proof. by rewrite /bi_iff si_pure_and -!si_pure_impl. Qed.

Lemma si_pure_impl_iff_wandPi Qi :
    <si_pure> (Pi ↔ Qi) ⊣⊢@{PROP} (<si_pure> Pi ∗-∗ <si_pure> Qi).
  Proof. by rewrite /bi_wand_iff si_pure_and -!si_pure_impl_wand. Qed.

Lemma si_pure_laterNn Pi :
    <si_pure> ▷^n Pi ⊣⊢@{PROP} ▷^n <si_pure> Pi.
  Proof.
    induction n as [|n IH]; simpl; [done|].
    by rewrite si_pure_later IH.
  Qed.

Lemma si_pure_except_0Pi : <si_pure> ◇ Pi ⊣⊢@{PROP} ◇ <si_pure> Pi.
  Proof. by rewrite /bi_except_0 si_pure_or si_pure_later si_pure_pure. Qed.

Lemma absorbingly_si_purePi : <absorb> <si_pure> Pi ⊣⊢@{PROP} <si_pure> Pi.
  Proof. by rewrite bi.absorbing_absorbingly. Qed.

Lemma persistently_si_purePi : <pers> <si_pure> Pi ⊣⊢@{PROP} <si_pure> Pi.
  Proof. by rewrite bi.persistent_persistently. Qed.

Global Instancesi_pure_timeless Pi :
    Timeless Pi → Timeless (PROP:=PROP) (<si_pure> Pi).
  Proof.
    rewrite /Timeless=> HP. by rewrite -si_pure_later -si_pure_except_0 HP.
  Qed.

Lemma si_pure_si_emp_valid_elimP `{!Absorbing P} :
    <si_pure> <si_emp_valid> P ⊢ P.
  Proof. rewrite si_pure_si_emp_valid. by apply bi.persistently_elim. Qed.

Lemma affinely_si_pure_si_emp_validP :
    <affine> <si_pure> <si_emp_valid> P ⊢ P.
  Proof. rewrite si_pure_si_emp_valid. apply bi.intuitionistically_elim. Qed.

Lemma si_emp_valid_affinelyP :
    <si_emp_valid> <affine> P ⊣⊢@{siPropI} <si_emp_valid> P.
  Proof.
    apply (anti_symm _);
      [by rewrite bi.affinely_elim|apply si_emp_valid_affinely_2].
  Qed.

Lemma si_emp_valid_persistentlyP :
    <si_emp_valid> <pers> P ⊣⊢@{siPropI} <si_emp_valid> P.
  Proof.
    apply (anti_symm _).
    - by rewrite -si_emp_valid_affinely -{2}(bi.intuitionistically_elim P).
    - rewrite -(si_emp_valid_si_pure (PROP:=PROP) (si_emp_valid P)).
      by rewrite si_pure_si_emp_valid.
  Qed.

Lemma si_emp_valid_intuitionisticallyP :
    <si_emp_valid> □ P ⊣⊢@{siPropI} <si_emp_valid> P.
  Proof.
    by rewrite /bi_intuitionistically si_emp_valid_affinely si_emp_valid_persistently.
  Qed.

Lemma si_emp_valid_pureφ : <si_emp_valid> (⌜ φ ⌝ : PROP) ⊣⊢@{siPropI} ⌜ φ ⌝.
  Proof.
    by rewrite -(si_emp_valid_si_pure (PROP:=PROP) ⌜ φ ⌝) si_pure_pure.
  Qed.

Lemma si_emp_valid_emp: <si_emp_valid> (emp : PROP) ⊣⊢@{siPropI} True.
  Proof.
    rewrite -bi.affinely_emp -bi.affinely_True_emp.
    by rewrite !si_emp_valid_affinely si_emp_valid_pure.
  Qed.

Lemma si_emp_valid_forall{A} (Φ : A → PROP) :
    <si_emp_valid> (∀ x, Φ x) ⊣⊢@{siPropI} ∀ x, <si_emp_valid> (Φ x).
  Proof.
    apply (anti_symm _).
    - apply bi.forall_intro=> x. by rewrite (bi.forall_elim x).
    - rewrite -(si_emp_valid_si_pure (PROP:=PROP) (∀ x : A, _)).
      rewrite si_pure_forall -si_emp_valid_affinely bi.affinely_forall.
      by setoid_rewrite affinely_si_pure_si_emp_valid.
  Qed.

Lemma si_emp_valid_exist_2{A} (Φ : A → PROP) :
    (∃ x, <si_emp_valid> Φ x) ⊢@{siPropI} <si_emp_valid> (∃ x, Φ x).
  Proof. apply bi.exist_elim=> x. by rewrite -(bi.exist_intro x). Qed.

Lemma si_emp_valid_exist`{!SbiEmpValidExist PROP} {A} (Φ : A → PROP) :
    <si_emp_valid> (∃ x, Φ x) ⊣⊢@{siPropI} ∃ x, <si_emp_valid> Φ x.
  Proof.
    apply (anti_symm _); [apply: si_emp_valid_exist_1|apply si_emp_valid_exist_2].
  Qed.

Lemma si_emp_valid_andP Q :
    <si_emp_valid> (P ∧ Q) ⊣⊢@{siPropI} <si_emp_valid> P ∧ <si_emp_valid> Q.
  Proof. rewrite !bi.and_alt si_emp_valid_forall. by f_equiv=> -[]. Qed.

Lemma si_emp_valid_or_2P Q :
    <si_emp_valid> P ∨ <si_emp_valid> Q ⊢@{siPropI} <si_emp_valid> (P ∨ Q).
  Proof. rewrite !bi.or_alt -si_emp_valid_exist_2. by f_equiv=> -[]. Qed.

Lemma si_emp_valid_or`{!SbiEmpValidExist PROP} P Q :
    <si_emp_valid> (P ∨ Q) ⊣⊢@{siPropI} <si_emp_valid> P ∨ <si_emp_valid> Q.
  Proof. rewrite !bi.or_alt si_emp_valid_exist. by f_equiv=> -[]. Qed.

Lemma si_emp_valid_impl_si_purePi Q :
    (Pi → <si_emp_valid> Q) ⊢@{siPropI} <si_emp_valid> (<si_pure> Pi → Q).
  Proof.
    rewrite -(si_emp_valid_si_pure (PROP:=PROP) (_ → _)) -si_emp_valid_affinely.
    f_equiv. apply bi.impl_intro_l. rewrite bi.affinely_and_r.
    by rewrite -si_pure_and bi.impl_elim_r affinely_si_pure_si_emp_valid.
  Qed.

Lemma si_emp_valid_sep`{!BiPositive PROP} P Q :
    <si_emp_valid> (P ∗ Q) ⊣⊢@{siPropI} <si_emp_valid> P ∧ <si_emp_valid> Q.
  Proof.
    rewrite -si_emp_valid_intuitionistically bi.intuitionistically_sep.
    rewrite -bi.and_sep_intuitionistically si_emp_valid_and.
    by rewrite !si_emp_valid_intuitionistically.
  Qed.

Lemma si_emp_valid_wand_si_purePi Q :
    (Pi → <si_emp_valid> Q) ⊢@{siPropI} <si_emp_valid> (<affine> <si_pure> Pi -∗ Q).
  Proof.
    by rewrite -bi.persistent_impl_wand_affinely -si_emp_valid_impl_si_pure.
  Qed.

Lemma si_emp_valid_laterP :
    <si_emp_valid> ▷ P ⊣⊢@{siPropI} ▷ <si_emp_valid> P.
  Proof.
    apply (anti_symm _); [apply si_emp_valid_later_1|].
    rewrite -(si_emp_valid_si_pure (PROP:=PROP) (▷ _)). rewrite si_pure_later.
    rewrite si_pure_si_emp_valid.
    by rewrite bi.later_persistently si_emp_valid_persistently.
  Qed.

Lemma si_emp_valid_laterNn P :
    <si_emp_valid> ▷^n P ⊣⊢@{siPropI} ▷^n <si_emp_valid> P.
  Proof.
    induction n as [|n IH]; simpl; [done|].
    by rewrite si_emp_valid_later IH.
  Qed.

Lemma si_emp_valid_except_0P :
    <si_emp_valid> ◇ P ⊣⊢@{siPropI} ◇ <si_emp_valid> P.
  Proof.
    apply (anti_symm _).
    - trans (▷ <si_emp_valid> P ∧ <si_emp_valid> ◇ P)%I.
      { apply bi.and_intro, reflexivity.
        by rewrite -si_emp_valid_later bi.except_0_into_later. }
      rewrite bi.later_false_em bi.and_or_r. apply bi.or_elim.
      { rewrite bi.and_elim_l. apply bi.or_intro_l. }
      apply bi.or_intro_r'. rewrite si_emp_valid_impl_si_pure -si_emp_valid_and.
      f_equiv. rewrite si_pure_later si_pure_pure.
      by rewrite bi.and_or_l bi.impl_elim_l bi.and_elim_r idemp.
    - rewrite /bi_except_0 -si_emp_valid_or_2.
      by rewrite si_emp_valid_later si_emp_valid_pure.
  Qed.

Global Instancesi_emp_valid_timeless P :
    Timeless P → Timeless (<si_emp_valid> P).
  Proof.
    rewrite /Timeless=> HP.
    by rewrite -si_emp_valid_later -si_emp_valid_except_0 HP.
  Qed.

Lemma si_emp_valid_emp_validP : (⊢@{siPropI} <si_emp_valid> P) ↔ ⊢ P.
  Proof.
    rewrite /bi_emp_valid. split; intros HP.
    - rewrite -bi.affinely_True_emp -si_pure_pure.
      by rewrite bi.True_emp HP affinely_si_pure_si_emp_valid.
    - by rewrite -bi.True_emp -si_emp_valid_emp HP.
  Qed.

Lemma si_pure_emp_validPi : (⊢@{PROP} <si_pure> Pi) ↔ ⊢@{siPropI} Pi.
  Proof. by rewrite -si_emp_valid_emp_valid si_emp_valid_si_pure. Qed.

Lemma si_pure_entailsPi Qi :
    (<si_pure> Pi ⊢@{PROP} <si_pure> Qi) ↔ (Pi ⊢@{siPropI} Qi).
  Proof.
    split; [|by intros ->].
    intros HPQ. rewrite -(si_emp_valid_si_pure (PROP:=PROP) Pi) HPQ.
    by rewrite si_emp_valid_si_pure.
  Qed.

Global Instancesi_pure_inj : Inj (⊣⊢) (⊣⊢) (si_pure (PROP:=PROP)).
  Proof.
    intros Pi Qi HPQ.
    apply (anti_symm _); apply si_pure_entails; by rewrite HPQ.
  Qed.

Lemma pure_soundnessφ : (⊢@{PROP} ⌜ φ ⌝) → φ.
  Proof.
    rewrite -si_pure_pure si_pure_emp_valid.
    apply siProp_primitive.pure_soundness.
  Qed.

Lemma later_soundnessP : (⊢ ▷ P) → ⊢ P.
  Proof.
    rewrite -!si_emp_valid_emp_valid si_emp_valid_later.
    apply siProp_primitive.later_soundness.
  Qed.

Lemma laterN_soundnessP n : (⊢ ▷^n P) → ⊢ P.
  Proof.
    induction n as [|n IH]; intros ?; simpl; [done|].
    by apply IH, later_soundness.
  Qed.