bi.v 5.68 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
From iris.bi Require Export bi.
From iris.si_logic Require Export siprop.
3
From iris Require Import options.
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5 6 7 8
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. *)

Robbert Krebbers's avatar
Robbert Krebbers committed
9 10 11
(** 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. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
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
    siProp_persistently.
Proof.
  split.
  - exact: entails_po.
  - exact: equiv_spec.
  - exact: pure_ne.
  - exact: and_ne.
  - exact: or_ne.
  - exact: impl_ne.
  - exact: forall_ne.
  - exact: exist_ne.
  - exact: and_ne.
  - exact: impl_ne.
  - solve_proper.
  - exact: pure_intro.
  - exact: pure_elim'.
  - exact: @pure_forall_2.
  - 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.
  - (* (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q' *)
    intros P P' Q Q' H1 H2. apply and_intro.
    + by etrans; first apply and_elim_l.
    + by etrans; first apply and_elim_r.
  - (* P ⊢ emp ∗ P *)
    intros P. apply and_intro; last done. by apply pure_intro.
  - (* emp ∗ P ⊢ P *)
    intros P. apply and_elim_r.
  - (* P ∗ Q ⊢ Q ∗ P *)
    intros P Q. apply and_intro. apply and_elim_r. apply and_elim_l.
  - (* (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R) *)
    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.
  - (* (P ∗ Q ⊢ R) → P ⊢ Q -∗ R *)
    apply impl_intro_r.
  - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
    apply impl_elim_l'.
  - (* (P ⊢ Q) → <pers> P ⊢ <pers> Q *)
    done.
  - (* <pers> P ⊢ <pers> <pers> P *)
    done.
  - (* emp ⊢ <pers> emp *)
    done.
  - (* (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a) *)
    done.
  - (* <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a) *)
    done.
  - (* <pers> P ∗ Q ⊢ <pers> P *)
    apply and_elim_l.
  - (* <pers> P ∧ Q ⊢ P ∗ Q *)
    done.
Qed.

88 89 90 91
Lemma siProp_bi_later_mixin :
  BiLaterMixin
    siProp_entails siProp_pure siProp_or siProp_impl
    (@siProp_forall) (@siProp_exist) siProp_sep siProp_persistently siProp_later.
Robbert Krebbers's avatar
Robbert Krebbers committed
92 93
Proof.
  split.
94
  - apply contractive_ne, later_contractive.
Robbert Krebbers's avatar
Robbert Krebbers committed
95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
  - exact: later_mono.
  - exact: later_intro.
  - exact: @later_forall_2.
  - exact: @later_exist_false.
  - (* ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q *)
    intros P Q.
    apply and_intro; apply later_mono. apply and_elim_l. apply and_elim_r.
  - (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
    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).
  - (* ▷ <pers> P ⊢ <pers> ▷ P *)
    done.
  - (* <pers> ▷ P ⊢ ▷ <pers> P *)
    done.
  - exact: later_false_em.
Qed.

Canonical Structure siPropI : bi :=
116
  {| bi_ofe_mixin := ofe_mixin_of siProp;
117
     bi_bi_mixin := siProp_bi_mixin; bi_bi_later_mixin := siProp_bi_later_mixin |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
118

119
Instance siProp_later_contractive : BiLaterContractive siPropI.
120 121
Proof. apply later_contractive. Qed.

122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
Lemma siProp_internal_eq_mixin : BiInternalEqMixin siPropI (@siProp_internal_eq).
Proof.
  split.
  - exact: internal_eq_ne.
  - exact: @internal_eq_refl.
  - exact: @internal_eq_rewrite.
  - exact: @fun_ext.
  - exact: @sig_eq.
  - exact: @discrete_eq_1.
  - exact: @later_eq_1.
  - exact: @later_eq_2.
Qed.
Global Instance siProp_internal_eq : BiInternalEq siPropI :=
  {| bi_internal_eq_mixin := siProp_internal_eq_mixin |}.

137
Lemma siProp_plainly_mixin : BiPlainlyMixin siPropI siProp_plainly.
Robbert Krebbers's avatar
Robbert Krebbers committed
138 139 140 141 142 143 144 145
Proof.
  split; try done.
  - solve_proper.
  - (* P ⊢ ■ emp *)
    intros P. by apply pure_intro.
  - (* ■ P ∗ Q ⊢ ■ P *)
    intros P Q. apply and_elim_l.
Qed.
146
Global Instance siProp_plainlyC : BiPlainly siPropI :=
Robbert Krebbers's avatar
Robbert Krebbers committed
147 148
  {| bi_plainly_mixin := siProp_plainly_mixin |}.

149 150 151
Global Instance siProp_prop_ext : BiPropExt siPropI.
Proof. exact: prop_ext_2. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
152 153 154 155 156 157 158 159 160 161 162 163 164
(** extra BI instances *)

Global Instance siProp_affine : BiAffine siPropI | 0.
Proof. intros P. exact: pure_intro. Qed.
(* Also add this to the global hint database, otherwise [eauto] won't work for
many lemmas that have [BiAffine] as a premise. *)
Hint Immediate siProp_affine : core.

Global Instance siProp_plain (P : siProp) : Plain P | 0.
Proof. done. Qed.
Global Instance siProp_persistent (P : siProp) : Persistent P.
Proof. done. Qed.

165
Global Instance siProp_plainly_exist_1 : BiPlainlyExist siPropI.
Robbert Krebbers's avatar
Robbert Krebbers committed
166 167 168 169 170 171
Proof. done. Qed.

(** Re-state/export soundness lemmas *)

Module siProp.
Section restate.
172
Lemma pure_soundness φ : (@{siPropI}  φ )  φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174
Proof. apply pure_soundness. Qed.

175
Lemma internal_eq_soundness {A : ofeT} (x y : A) : (@{siPropI} x  y)  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
176 177
Proof. apply internal_eq_soundness. Qed.

178
Lemma later_soundness (P : siProp) : (  P)   P.
Robbert Krebbers's avatar
Robbert Krebbers committed
179 180 181
Proof. apply later_soundness. Qed.
End restate.
End siProp.