(* iris/si_logic/bi.v *)
From iris.bi Require Export interface extensions
From iris.si_logic Require Export siprop
From iris.prelude Require Import options

Definition siProp_emp: siProp := siProp_pure True.

Definition siProp_sep: siProp → siProp → siProp := siProp_and.

Definition siProp_wand: siProp → siProp → siProp := siProp_impl.

Definition siProp_persistently(P : siProp) : siProp := P.

Definition siProp_plainly(P : siProp) : siProp := P.

Local ExistingInstance entails_po.

Lemma siProp_bi_mixin:
  BiMixin
    siProp_entails siProp_emp siProp_pure siProp_and siProp_or siProp_impl
    (@siProp_forall) (@siProp_exist) siProp_sep siProp_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: and_ne.
  - exact: impl_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.
  -
    intros P P' Q Q' H1 H2. apply and_intro.
    + by etrans; first apply and_elim_l.
    + by etrans; first apply and_elim_r.
  -
    intros P. apply and_intro; last done. by apply pure_intro.
  -
    intros P. apply and_elim_r.
  -
    intros P Q. apply and_intro; [ apply and_elim_r | apply and_elim_l ].

Lemma siProp_bi_persistently_mixin:
  BiPersistentlyMixin
    siProp_entails siProp_emp siProp_and
    (@siProp_exist) siProp_sep siProp_persistently.
Proof.
  split.
  - solve_proper.
  -
    done.
  -
    done.
  -
    done.
  -
    done.
  -
    done.
  -
    apply and_elim_l.
  -
    done.
Qed.

Lemma siProp_bi_later_mixin:
  BiLaterMixin
    siProp_entails siProp_pure siProp_or siProp_impl
    (@siProp_forall) (@siProp_exist) siProp_sep siProp_persistently siProp_later.
Proof.
  split.
  - apply contractive_ne, later_contractive.
  - exact: later_mono.
  - exact: later_intro.
  - exact: @later_forall_2.
  - exact: @later_exist_false.
  -
    intros P Q.
    apply and_intro; apply later_mono.
    + apply and_elim_l.
    + apply and_elim_r.
  -
    intros P Q.
    trans (siProp_forall (λ b : bool, siProp_later (if b then P else Q))).
    { apply forall_intro=> -[].
      - apply and_elim_l.
      - apply and_elim_r. }
    etrans; [apply later_forall_2|apply later_mono].
    apply and_intro.
    + refine (forall_elim true).
    + refine (forall_elim false).
  -
    done.
  -
    done.
  - exact: later_false_em.
Qed.
Canonical Structure siPropI : bi :=
  {| bi_ofe_mixin := ofe_mixin_of siProp;
     bi_bi_mixin := siProp_bi_mixin;
     bi_bi_persistently_mixin := siProp_bi_persistently_mixin;
     bi_bi_later_mixin := siProp_bi_later_mixin |}.

Global InstancesiProp_pure_forall : BiPureForall siPropI.
Proof. exact: @pure_forall_2. Qed.

Global InstancesiProp_later_contractive : BiLaterContractive siPropI.
Proof. exact: @later_contractive. Qed.

Global InstancesiProp_affine : BiAffine siPropI | 0.
Proof. intros P. exact: pure_intro. Qed.

Global HintImmediate siProp_affine : core.

Global InstancesiProp_persistent (P : siProp) : Persistent P.
Proof. done. Qed.

Local LemmasiProp_emp_unseal : bi_emp = @siprop.siProp_pure_def True.
  Proof. by rewrite -siprop.siProp_pure_unseal. Qed.

Local LemmasiProp_pure_unseal : bi_pure = @siprop.siProp_pure_def.
  Proof. by rewrite -siprop.siProp_pure_unseal. Qed.

Local LemmasiProp_and_unseal : bi_and = @siprop.siProp_and_def.
  Proof. by rewrite -siprop.siProp_and_unseal. Qed.

Local LemmasiProp_or_unseal : bi_or = @siprop.siProp_or_def.
  Proof. by rewrite -siprop.siProp_or_unseal. Qed.

Local LemmasiProp_impl_unseal : bi_impl = @siprop.siProp_impl_def.
  Proof. by rewrite -siprop.siProp_impl_unseal. Qed.

Local LemmasiProp_forall_unseal : @bi_forall _ = @siprop.siProp_forall_def.
  Proof. by rewrite -siprop.siProp_forall_unseal. Qed.

Local LemmasiProp_exist_unseal : @bi_exist _ = @siprop.siProp_exist_def.
  Proof. by rewrite -siprop.siProp_exist_unseal. Qed.

Local LemmasiProp_sep_unseal : bi_sep = @siprop.siProp_and_def.
  Proof. by rewrite -siprop.siProp_and_unseal. Qed.

Local LemmasiProp_wand_unseal : bi_wand = @siprop.siProp_impl_def.
  Proof. by rewrite -siprop.siProp_impl_unseal. Qed.

Local LemmasiProp_persistently_unseal : bi_persistently = @id siProp.
  Proof. done. Qed.

Local LemmasiProp_later_unseal : bi_later = @siprop.siProp_later_def.
  Proof. by rewrite -siprop.siProp_later_unseal. Qed.

Local LemmasiProp_internal_eq_unseal :
    @siProp_internal_eq = @siprop.siProp_internal_eq_def.
  Proof. apply siprop.siProp_internal_eq_unseal. Qed.

Local LemmasiProp_cmra_valid_unseal :
    @siProp_cmra_valid = @siprop.siProp_cmra_valid_def.
  Proof. apply siprop.siProp_cmra_valid_unseal. Qed.

Local DefinitionsiProp_unseal :=
    (siProp_emp_unseal, siProp_pure_unseal, siProp_and_unseal, siProp_or_unseal,
    siProp_impl_unseal, siProp_forall_unseal, siProp_exist_unseal,
    siProp_sep_unseal, siProp_wand_unseal,
    siProp_persistently_unseal, siProp_later_unseal,
    siProp_internal_eq_unseal, siProp_cmra_valid_unseal).

Ltac unseal:= rewrite !siProp_unseal /=.