bi.v 8.27 KB
Newer Older
1
From iris.bi Require Export derived_connectives updates internal_eq plainly.
2
From iris.base_logic Require Export upred.
3
From iris Require Import options.
4 5
Import uPred_primitive.

6 7
(** BI instances for [uPred], and re-stating the remaining primitive laws in
terms of the BI interface. This file does *not* unseal. *)
8 9 10 11 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

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

Local Existing Instance entails_po.

Lemma uPred_bi_mixin (M : ucmraT) :
  BiMixin
    uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
    uPred_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: sep_ne.
  - exact: wand_ne.
  - exact: persistently_ne.
  - 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.
  - exact: sep_mono.
47
  - exact: True_sep_1.
48 49 50 51 52 53 54 55
  - exact: True_sep_2.
  - exact: sep_comm'.
  - exact: sep_assoc'.
  - exact: wand_intro_r.
  - exact: wand_elim_l'.
  - exact: persistently_mono.
  - exact: persistently_idemp_2.
  - (* emp ⊢ <pers> emp (ADMISSIBLE) *)
Ralf Jung's avatar
Ralf Jung committed
56
    trans (uPred_forall (M:=M) (λ _ : False, uPred_persistently uPred_emp)).
57 58 59 60 61 62 63 64 65 66 67 68 69
    + apply forall_intro=>[[]].
    + etrans; first exact: persistently_forall_2.
      apply persistently_mono. exact: pure_intro.
  - exact: @persistently_forall_2.
  - exact: @persistently_exist_1.
  - (* <pers> P ∗ Q ⊢ <pers> P (ADMISSIBLE) *)
    intros. etrans; first exact: sep_comm'.
    etrans; last exact: True_sep_2.
    apply sep_mono; last done.
    exact: pure_intro.
  - exact: persistently_and_sep_l_1.
Qed.

70 71 72 73
Lemma uPred_bi_later_mixin (M : ucmraT) :
  BiLaterMixin
    uPred_entails uPred_pure uPred_or uPred_impl
    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_persistently uPred_later.
74 75
Proof.
  split.
76
  - apply contractive_ne, later_contractive.
77 78 79 80 81 82 83 84 85 86 87 88
  - 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 : ucmraT) : bi :=
89
  {| bi_ofe_mixin := ofe_mixin_of (uPred M);
90 91
     bi_bi_mixin := uPred_bi_mixin M;
     bi_bi_later_mixin := uPred_bi_later_mixin M |}.
92

93
Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
94 95
Proof. apply later_contractive. Qed.

96 97 98 99 100 101 102 103 104 105 106 107 108 109 110
Lemma uPred_internal_eq_mixin M : BiInternalEqMixin (uPredI M) (@uPred_internal_eq M).
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 uPred_internal_eq M : BiInternalEq (uPredI M) :=
  {| bi_internal_eq_mixin := uPred_internal_eq_mixin M |}.

111
Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredI M) uPred_plainly.
112 113 114 115 116 117 118 119 120 121 122
Proof.
  split.
  - exact: plainly_ne.
  - exact: plainly_mono.
  - exact: plainly_elim_persistently.
  - exact: plainly_idemp_2.
  - exact: @plainly_forall_2.
  - exact: persistently_impl_plainly.
  - exact: plainly_impl_plainly.
  - (* P ⊢ ■ emp (ADMISSIBLE) *)
    intros P.
Ralf Jung's avatar
Ralf Jung committed
123
    trans (uPred_forall (M:=M) (λ _ : False , uPred_plainly uPred_emp)).
124 125 126 127 128 129 130 131 132 133 134
    + apply forall_intro=>[[]].
    + etrans; first exact: plainly_forall_2.
      apply plainly_mono. exact: pure_intro.
  - (* ■ P ∗ Q ⊢ ■ P (ADMISSIBLE) *)
    intros P Q. etrans; last exact: True_sep_2.
    etrans; first exact: sep_comm'.
    apply sep_mono; last done.
    exact: pure_intro.
  - exact: later_plainly_1.
  - exact: later_plainly_2.
Qed.
135
Global Instance uPred_plainly M : BiPlainly (uPredI M) :=
136 137
  {| bi_plainly_mixin := uPred_plainly_mixin M |}.

138 139 140
Global Instance uPred_prop_ext M : BiPropExt (uPredI M).
Proof. exact: prop_ext_2. Qed.

141 142 143 144 145 146 147 148 149
Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
Proof.
  split.
  - exact: bupd_ne.
  - exact: bupd_intro.
  - exact: bupd_mono.
  - exact: bupd_trans.
  - exact: bupd_frame_r.
Qed.
150
Global Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
151

152
Global Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredI M).
153 154 155 156
Proof. exact: bupd_plainly. Qed.

(** extra BI instances *)

Robbert Krebbers's avatar
Robbert Krebbers committed
157 158
Global Instance uPred_affine M : BiAffine (uPredI M) | 0.
Proof. intros P. exact: pure_intro. Qed.
159 160
(* Also add this to the global hint database, otherwise [eauto] won't work for
many lemmas that have [BiAffine] as a premise. *)
Tej Chajed's avatar
Tej Chajed committed
161
Hint Immediate uPred_affine : core.
162

163
Global Instance uPred_plainly_exist_1 M : BiPlainlyExist (uPredI M).
164
Proof. exact: @plainly_exist_1. Qed.
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179

(** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *)

Module uPred.

Section restate.
Context {M : ucmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.

(* Force implicit argument M *)
Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).

180 181 182
Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
Global Instance cmra_valid_ne {A : cmraT} : NonExpansive (@uPred_cmra_valid M A)
  := uPred_primitive.cmra_valid_ne.
183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214

(** Re-exporting primitive Own and valid lemmas *)
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_unit P : P  (uPred_ownM ε).
Proof. exact: uPred_primitive.ownM_unit. Qed.
Lemma later_ownM a :  uPred_ownM a   b, uPred_ownM b   (a  b).
Proof. exact: uPred_primitive.later_ownM. Qed.
Lemma bupd_ownM_updateP x (Φ : M  Prop) :
  x ~~>: Φ  uPred_ownM x  |==>  y, ⌜Φ y  uPred_ownM y.
Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.

Lemma ownM_valid (a : M) : uPred_ownM a   a.
Proof. exact: uPred_primitive.ownM_valid. Qed.
Lemma cmra_valid_intro {A : cmraT} P (a : A) :  a  P  ( a).
Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ {0} a   a  False.
Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) :  a    a.
Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
Lemma cmra_valid_weaken {A : cmraT} (a b : A) :  (a  b)   a.
Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
Lemma prod_validI {A B : cmraT} (x : A * B) :  x   x.1   x.2.
Proof. exact: uPred_primitive.prod_validI. Qed.
Lemma option_validI {A : cmraT} (mx : option A) :
   mx  match mx with Some x =>  x | None => True : uPred M end.
Proof. exact: uPred_primitive.option_validI. Qed.
Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) :  a  ⌜✓ a.
Proof. exact: uPred_primitive.discrete_valid. Qed.
215 216
Lemma discrete_fun_validI {A} {B : A  ucmraT} (g : discrete_fun B) :  g   i,  g i.
Proof. exact: uPred_primitive.discrete_fun_validI. Qed.
217 218

(** Consistency/soundness statement *)
219
Lemma pure_soundness φ : (@{uPredI M}  φ )  φ.
Ralf Jung's avatar
Ralf Jung committed
220
Proof. apply pure_soundness. Qed.
221

222
Lemma internal_eq_soundness {A : ofeT} (x y : A) : (@{uPredI M} x  y)  x  y.
223 224
Proof. apply internal_eq_soundness. Qed.

225
Lemma later_soundness P : (  P)   P.
Ralf Jung's avatar
Ralf Jung committed
226
Proof. apply later_soundness. Qed.
227
(** See [derived.v] for a similar soundness result for basic updates. *)
228 229
End restate.

230

231
(** New unseal tactic that also unfolds the BI layer.
232
    This is used by [base_logic.bupd_alt].
233 234
    TODO: Can we get rid of this? *)
Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
235
  unfold bi_emp; simpl;
236
  unfold uPred_emp, bupd, bi_bupd_bupd, bi_pure,
237 238 239 240
    bi_and, bi_or, bi_impl, bi_forall, bi_exist,
    bi_sep, bi_wand, bi_persistently, bi_later; simpl;
  unfold internal_eq, bi_internal_eq_internal_eq,
    plainly, bi_plainly_plainly; simpl;
241 242 243
  uPred_primitive.unseal.

End uPred.