Library iris.si_logic.bi

From iris.bi Require Export interface extensions.
From iris.si_logic Require Export siprop.
From iris.prelude Require Import options.
Import siProp_primitive.

BI instances for siProp, and re-stating the remaining primitive laws in terms of the BI interface. This file does *not* unseal.
We pick × and -* to coincide with ∧ and →, respectively. This seems to be the most reasonable choice to fit a "pure" higher-order logic into the proofmode's BI framework.
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 Existing Instance 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 ].
  -
    intros P Q R. repeat apply and_intro.
    + etrans; first apply and_elim_l. by apply and_elim_l.
    + etrans; first apply and_elim_l. by apply and_elim_r.
    + apply and_elim_r.
  -
    apply impl_intro_r.
  -
    apply impl_elim_l'.
Qed.

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 Instance siProp_pure_forall : BiPureForall siPropI.
Proof. exact: @pure_forall_2. Qed.

Global Instance siProp_later_contractive : BiLaterContractive siPropI.
Proof. exact: @later_contractive. Qed.

extra BI instances

Global Instance siProp_affine : BiAffine siPropI | 0.
Proof. intros P. exact: pure_intro. Qed.
Global Hint Immediate siProp_affine : core.

Global Instance siProp_persistent (P : siProp) : Persistent P.
Proof. done. Qed.

Re-state/export soundness lemmas
Module siProp.
Section restate.
The internal equality, internal validity, and soundness lemmas are lifted to any BI with equality in iris.bi.internal_eq, iris.bi.cmra and iris.bi.sbi. The versions specific for siProp should never be used by end-users and are therefore not restated here.
We restate the unsealing lemmas so that they also unfold the BI layer. The sealing lemmas are partially applied so that they also work under binders.
  Local Lemma siProp_emp_unseal : bi_emp = @siprop.siProp_pure_def True.
  Proof. by rewrite -siprop.siProp_pure_unseal. Qed.
  Local Lemma siProp_pure_unseal : bi_pure = @siprop.siProp_pure_def.
  Proof. by rewrite -siprop.siProp_pure_unseal. Qed.
  Local Lemma siProp_and_unseal : bi_and = @siprop.siProp_and_def.
  Proof. by rewrite -siprop.siProp_and_unseal. Qed.
  Local Lemma siProp_or_unseal : bi_or = @siprop.siProp_or_def.
  Proof. by rewrite -siprop.siProp_or_unseal. Qed.
  Local Lemma siProp_impl_unseal : bi_impl = @siprop.siProp_impl_def.
  Proof. by rewrite -siprop.siProp_impl_unseal. Qed.
  Local Lemma siProp_forall_unseal : @bi_forall _ = @siprop.siProp_forall_def.
  Proof. by rewrite -siprop.siProp_forall_unseal. Qed.
  Local Lemma siProp_exist_unseal : @bi_exist _ = @siprop.siProp_exist_def.
  Proof. by rewrite -siprop.siProp_exist_unseal. Qed.
  Local Lemma siProp_sep_unseal : bi_sep = @siprop.siProp_and_def.
  Proof. by rewrite -siprop.siProp_and_unseal. Qed.
  Local Lemma siProp_wand_unseal : bi_wand = @siprop.siProp_impl_def.
  Proof. by rewrite -siprop.siProp_impl_unseal. Qed.
  Local Lemma siProp_persistently_unseal : bi_persistently = @id siProp.
  Proof. done. Qed.
  Local Lemma siProp_later_unseal : bi_later = @siprop.siProp_later_def.
  Proof. by rewrite -siprop.siProp_later_unseal. Qed.
  Local Lemma siProp_internal_eq_unseal :
    @siProp_internal_eq = @siprop.siProp_internal_eq_def.
  Proof. apply siprop.siProp_internal_eq_unseal. Qed.
  Local Lemma siProp_cmra_valid_unseal :
    @siProp_cmra_valid = @siprop.siProp_cmra_valid_def.
  Proof. apply siprop.siProp_cmra_valid_unseal. Qed.

  Local Definition siProp_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).
End restate.

The final unseal tactic that also unfolds the BI layer.
Ltac unseal := rewrite !siProp_unseal /=.
End siProp.