embedding.v 14.5 KB
Newer Older
1
From iris.bi Require Import interface derived_laws_later big_op.
2
From iris.bi Require Import plainly updates internal_eq.
3
From iris.algebra Require Import monoid.
4 5 6 7
From iris Require Import options.

(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
Set Default Proof Using "Type*".
8

9 10 11
Class Embed (A B : Type) := embed : A  B.
Arguments embed {_ _ _} _%I : simpl never.
Notation "⎡ P ⎤" := (embed P) : bi_scope.
12
Instance: Params (@embed) 3 := {}.
13
Typeclasses Opaque embed.
14

15 16 17
Hint Mode Embed ! - : typeclass_instances.
Hint Mode Embed - ! : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
18
(* Mixins allow us to create instances easily without having to use Program *)
19
Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
20 21
  bi_embed_mixin_ne : NonExpansive (embed (A:=PROP1) (B:=PROP2));
  bi_embed_mixin_mono : Proper (() ==> ()) (embed (A:=PROP1) (B:=PROP2));
Robbert Krebbers's avatar
Robbert Krebbers committed
22
  bi_embed_mixin_emp_valid_inj (P : PROP1) :
23
    (@{PROP2} P)   P;
24 25 26 27 28
  (** The following axiom expresses that the embedding is injective in the OFE
  sense. Instead of this axiom being expressed in terms of [siProp] or
  externally (i.e., as [Inj (dist n) (dist n) embed]), it is expressed using the
  internal equality of _any other_ BI [PROP']. This is more general, as we do
  not have any machinary to embed [siProp] into a BI with internal equality. *)
29 30
  bi_embed_mixin_interal_inj `{BiInternalEq PROP'} (P Q : PROP1) :
    P  Q @{PROP'} (P  Q);
31 32 33 34 35 36 37 38 39 40 41 42 43
  bi_embed_mixin_emp_2 : emp @{PROP2} emp;
  bi_embed_mixin_impl_2 (P Q : PROP1) :
    (P  Q) @{PROP2} P  Q;
  bi_embed_mixin_forall_2 A (Φ : A  PROP1) :
    ( x, ⎡Φ x) @{PROP2}  x, Φ x;
  bi_embed_mixin_exist_1 A (Φ : A  PROP1) :
     x, Φ x @{PROP2}  x, ⎡Φ x;
  bi_embed_mixin_sep (P Q : PROP1) :
    P  Q @{PROP2} P  Q;
  bi_embed_mixin_wand_2 (P Q : PROP1) :
    (P - Q) @{PROP2} P - Q;
  bi_embed_mixin_persistently (P : PROP1) :
    <pers> P @{PROP2} <pers> P
44 45 46 47 48 49
}.

Class BiEmbed (PROP1 PROP2 : bi) := {
  bi_embed_embed :> Embed PROP1 PROP2;
  bi_embed_mixin : BiEmbedMixin PROP1 PROP2 bi_embed_embed;
}.
50 51
Hint Mode BiEmbed ! - : typeclass_instances.
Hint Mode BiEmbed - ! : typeclass_instances.
52
Arguments bi_embed_embed : simpl never.
53

54 55
Class BiEmbedEmp (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} :=
  embed_emp_1 :  emp : PROP1   emp.
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57 58
Hint Mode BiEmbedEmp ! - - : typeclass_instances.
Hint Mode BiEmbedEmp - ! - : typeclass_instances.

59 60 61 62 63 64 65 66 67 68
Class BiEmbedLater (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} :=
  embed_later P : ⎡▷ P @{PROP2}  P.
Hint Mode BiEmbedLater ! - - : typeclass_instances.
Hint Mode BiEmbedLater - ! - : typeclass_instances.

Class BiEmbedInternalEq (PROP1 PROP2 : bi)
    `{!BiEmbed PROP1 PROP2, !BiInternalEq PROP1, !BiInternalEq PROP2} :=
  embed_internal_eq_1 (A : ofeT) (x y : A) : x  y @{PROP2} x  y.
Hint Mode BiEmbedInternalEq ! - - - - : typeclass_instances.
Hint Mode BiEmbedInternalEq - ! - - - : typeclass_instances.
69

70
Class BiEmbedBUpd (PROP1 PROP2 : bi)
71 72
    `{!BiEmbed PROP1 PROP2, !BiBUpd PROP1, !BiBUpd PROP2} :=
  embed_bupd P : |==> P @{PROP2} |==> P.
73 74 75
Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances.
Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances.

76
Class BiEmbedFUpd (PROP1 PROP2 : bi)
77 78
    `{!BiEmbed PROP1 PROP2, !BiFUpd PROP1, !BiFUpd PROP2} :=
  embed_fupd E1 E2 P : |={E1,E2}=> P @{PROP2} |={E1,E2}=> P.
79 80 81
Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.

82
Class BiEmbedPlainly (PROP1 PROP2 : bi)
83 84
    `{!BiEmbed PROP1 PROP2, !BiPlainly PROP1, !BiPlainly PROP2} :=
  embed_plainly (P : PROP1) : ⎡■ P @{PROP2}  P.
85 86 87
Hint Mode BiEmbedPlainly - ! - - - : typeclass_instances.
Hint Mode BiEmbedPlainly ! - - - - : typeclass_instances.

88 89 90 91 92 93 94 95 96 97
Section embed_laws.
  Context `{BiEmbed PROP1 PROP2}.
  Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
  Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
  Implicit Types P : PROP1.

  Global Instance embed_ne : NonExpansive embed.
  Proof. eapply bi_embed_mixin_ne, bi_embed_mixin. Qed.
  Global Instance embed_mono : Proper (() ==> ()) embed.
  Proof. eapply bi_embed_mixin_mono, bi_embed_mixin. Qed.
Gregory Malecha's avatar
Gregory Malecha committed
98
  Lemma embed_emp_valid_inj P : (@{PROP2} P)   P.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
  Proof. eapply bi_embed_mixin_emp_valid_inj, bi_embed_mixin. Qed.
100 101 102
  Lemma embed_interal_inj `{!BiInternalEq PROP'} (P Q : PROP1) :
    P  Q @{PROP'} (P  Q).
  Proof. eapply bi_embed_mixin_interal_inj, bi_embed_mixin. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
103 104
  Lemma embed_emp_2 : emp  emp.
  Proof. eapply bi_embed_mixin_emp_2, bi_embed_mixin. Qed.
105 106 107 108 109 110 111 112 113 114
  Lemma embed_impl_2 P Q : (P  Q)  P  Q.
  Proof. eapply bi_embed_mixin_impl_2, bi_embed_mixin. Qed.
  Lemma embed_forall_2 A (Φ : A  PROP1) : ( x, ⎡Φ x)   x, Φ x.
  Proof. eapply bi_embed_mixin_forall_2, bi_embed_mixin. Qed.
  Lemma embed_exist_1 A (Φ : A  PROP1) :  x, Φ x   x, ⎡Φ x.
  Proof. eapply bi_embed_mixin_exist_1, bi_embed_mixin. Qed.
  Lemma embed_sep P Q : P  Q  P  Q.
  Proof. eapply bi_embed_mixin_sep, bi_embed_mixin. Qed.
  Lemma embed_wand_2 P Q : (P - Q)  P - Q.
  Proof. eapply bi_embed_mixin_wand_2, bi_embed_mixin. Qed.
115
  Lemma embed_persistently P : <pers> P  <pers> P.
116 117
  Proof. eapply bi_embed_mixin_persistently, bi_embed_mixin. Qed.
End embed_laws.
118

119 120 121 122
Section embed.
  Context `{BiEmbed PROP1 PROP2}.
  Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
  Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
123
  Implicit Types P Q R : PROP1.
124

125
  Global Instance embed_proper : Proper (() ==> ()) embed.
126
  Proof. apply (ne_proper _). Qed.
127
  Global Instance embed_flip_mono : Proper (flip () ==> flip ()) embed.
128
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130 131 132 133 134
  Global Instance embed_entails_inj : Inj () () embed.
  Proof.
    move=> P Q /bi.entails_wand. rewrite embed_wand_2.
    by move=> /embed_emp_valid_inj /bi.wand_entails.
  Qed.

135
  Global Instance embed_inj : Inj () () embed.
136
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
    intros P Q EQ. apply bi.equiv_spec, conj; apply (inj embed); rewrite EQ //.
138 139
  Qed.

Gregory Malecha's avatar
Gregory Malecha committed
140
  Lemma embed_emp_valid (P : PROP1) : ( P)  ( P).
141
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
142 143 144
    rewrite /bi_emp_valid. split=> HP.
    - by apply embed_emp_valid_inj.
    - by rewrite embed_emp_2 HP.
145 146
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
147 148 149
  Lemma embed_emp `{!BiEmbedEmp PROP1 PROP2} :  emp   emp.
  Proof. apply (anti_symm _); eauto using embed_emp_1, embed_emp_2. Qed.

150
  Lemma embed_forall A (Φ : A  PROP1) :  x, Φ x   x, ⎡Φ x.
151
  Proof.
152
    apply bi.equiv_spec; split; [|apply embed_forall_2].
153 154
    apply bi.forall_intro=>?. by rewrite bi.forall_elim.
  Qed.
155
  Lemma embed_exist A (Φ : A  PROP1) :  x, Φ x   x, ⎡Φ x.
156
  Proof.
157
    apply bi.equiv_spec; split; [apply embed_exist_1|].
158 159
    apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
  Qed.
160 161 162 163 164
  Lemma embed_and P Q : P  Q  P  Q.
  Proof. rewrite !bi.and_alt embed_forall. by f_equiv=>-[]. Qed.
  Lemma embed_or P Q : P  Q  P  Q.
  Proof. rewrite !bi.or_alt embed_exist. by f_equiv=>-[]. Qed.
  Lemma embed_impl P Q : P  Q  (P  Q).
165
  Proof.
166 167
    apply bi.equiv_spec; split; [|apply embed_impl_2].
    apply bi.impl_intro_l. by rewrite -embed_and bi.impl_elim_r.
168
  Qed.
169
  Lemma embed_wand P Q : P - Q  (P - Q).
170
  Proof.
171 172
    apply bi.equiv_spec; split; [|apply embed_wand_2].
    apply bi.wand_intro_l. by rewrite -embed_sep bi.wand_elim_r.
173
  Qed.
174
  Lemma embed_pure φ : ⎡⌜φ⌝⎤  ⌜φ⌝.
175
  Proof.
176
    rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) embed_exist.
177
    do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|].
178
    rewrite -(_ : (emp  emp : PROP1)  True) ?embed_impl;
179 180 181
      last apply bi.True_intro.
    apply bi.impl_intro_l. by rewrite right_id.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
182

183 184 185 186
  Lemma embed_iff P Q : P  Q  (P  Q).
  Proof. by rewrite embed_and !embed_impl. Qed.
  Lemma embed_wand_iff P Q : P - Q  (P - Q).
  Proof. by rewrite embed_and !embed_wand. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
187 188 189 190
  Lemma embed_affinely_2 P : <affine> P  <affine> P.
  Proof. by rewrite embed_and -embed_emp_2. Qed.
  Lemma embed_affinely `{!BiEmbedEmp PROP1 PROP2} P : <affine> P  <affine> P.
  Proof. by rewrite /bi_intuitionistically embed_and embed_emp. Qed.
191
  Lemma embed_absorbingly P : <absorb> P  <absorb> P.
192
  Proof. by rewrite embed_sep embed_pure. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
193 194 195 196 197
  Lemma embed_intuitionistically_2 P :  P  ⎡□ P.
  Proof. by rewrite /bi_intuitionistically -embed_affinely_2 embed_persistently. Qed.
  Lemma embed_intuitionistically `{!BiEmbedEmp PROP1 PROP2} P : ⎡□ P   P.
  Proof. by rewrite /bi_intuitionistically embed_affinely embed_persistently. Qed.

198
  Lemma embed_persistently_if P b : <pers>?b P  <pers>?b P.
199
  Proof. destruct b; simpl; auto using embed_persistently. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
200 201 202 203
  Lemma embed_affinely_if_2 P b : <affine>?b P  <affine>?b P.
  Proof. destruct b; simpl; auto using embed_affinely_2. Qed.
  Lemma embed_affinely_if `{!BiEmbedEmp PROP1 PROP2} P b :
    <affine>?b P  <affine>?b P.
204
  Proof. destruct b; simpl; auto using embed_affinely. Qed.
205 206
  Lemma embed_absorbingly_if b P : <absorb>?b P  <absorb>?b P.
  Proof. destruct b; simpl; auto using embed_absorbingly. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
207 208 209 210
  Lemma embed_intuitionistically_if_2 P b : ?b P  ⎡□?b P.
  Proof. destruct b; simpl; auto using embed_intuitionistically_2. Qed.
  Lemma embed_intuitionistically_if `{!BiEmbedEmp PROP1 PROP2} P b :
    ⎡□?b P  ?b P.
211
  Proof. destruct b; simpl; auto using embed_intuitionistically. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
212

213 214
  Global Instance embed_persistent P : Persistent P  Persistent P.
  Proof. intros ?. by rewrite /Persistent -embed_persistently -persistent. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
  Global Instance embed_affine `{!BiEmbedEmp PROP1 PROP2} P : Affine P  Affine P.
216 217 218 219 220 221
  Proof. intros ?. by rewrite /Affine (affine P) embed_emp. Qed.
  Global Instance embed_absorbing P : Absorbing P  Absorbing P.
  Proof. intros ?. by rewrite /Absorbing -embed_absorbingly absorbing. Qed.

  Global Instance embed_and_homomorphism :
    MonoidHomomorphism bi_and bi_and () embed.
222 223
  Proof.
    by split; [split|]; try apply _;
224
      [setoid_rewrite embed_and|rewrite embed_pure].
225
  Qed.
226 227
  Global Instance embed_or_homomorphism :
    MonoidHomomorphism bi_or bi_or () embed.
228 229
  Proof.
    by split; [split|]; try apply _;
230
      [setoid_rewrite embed_or|rewrite embed_pure].
231
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
232 233 234

  Global Instance embed_sep_entails_homomorphism :
    MonoidHomomorphism bi_sep bi_sep (flip ()) embed.
235
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
236 237
    split; [split|]; simpl; try apply _;
      [by setoid_rewrite embed_sep|by rewrite embed_emp_2].
238
  Qed.
239

Robbert Krebbers's avatar
Robbert Krebbers committed
240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275
  Lemma embed_big_sepL_2 {A} (Φ : nat  A  PROP1) l :
    ([ list] kx  l, ⎡Φ k x)  [ list] kx  l, Φ k x.
  Proof. apply (big_opL_commute (R:=flip ()) _). Qed.
  Lemma embed_big_sepM_2 `{Countable K} {A} (Φ : K  A  PROP1) (m : gmap K A) :
    ([ map] kx  m, ⎡Φ k x)  [ map] kx  m, Φ k x.
  Proof. apply (big_opM_commute (R:=flip ()) _). Qed.
  Lemma embed_big_sepS_2 `{Countable A} (Φ : A  PROP1) (X : gset A) :
    ([ set] y  X, ⎡Φ y)  [ set] y  X, Φ y.
  Proof. apply (big_opS_commute (R:=flip ()) _). Qed.
  Lemma embed_big_sepMS_2 `{Countable A} (Φ : A  PROP1) (X : gmultiset A) :
    ([ mset] y  X, ⎡Φ y)  [ mset] y  X, Φ y.
  Proof. apply (big_opMS_commute (R:=flip ()) _). Qed.

  Section big_ops_emp.
    Context `{!BiEmbedEmp PROP1 PROP2}.

    Global Instance embed_sep_homomorphism :
      MonoidHomomorphism bi_sep bi_sep () embed.
    Proof.
      by split; [split|]; try apply _;
        [setoid_rewrite embed_sep|rewrite embed_emp].
    Qed.

    Lemma embed_big_sepL {A} (Φ : nat  A  PROP1) l :
      [ list] kx  l, Φ k x  [ list] kx  l, ⎡Φ k x.
    Proof. apply (big_opL_commute _). Qed.
    Lemma embed_big_sepM `{Countable K} {A} (Φ : K  A  PROP1) (m : gmap K A) :
      [ map] kx  m, Φ k x  [ map] kx  m, ⎡Φ k x.
    Proof. apply (big_opM_commute _). Qed.
    Lemma embed_big_sepS `{Countable A} (Φ : A  PROP1) (X : gset A) :
      [ set] y  X, Φ y  [ set] y  X, ⎡Φ y.
    Proof. apply (big_opS_commute _). Qed.
    Lemma embed_big_sepMS `{Countable A} (Φ : A  PROP1) (X : gmultiset A) :
      [ mset] y  X, Φ y  [ mset] y  X, ⎡Φ y.
    Proof. apply (big_opMS_commute _). Qed.
  End big_ops_emp.
276

277 278
  Section later.
    Context `{!BiEmbedLater PROP1 PROP2}.
279

280 281 282 283
    Lemma embed_laterN n P : ⎡▷^n P  ^n P.
    Proof. induction n=>//=. rewrite embed_later. by f_equiv. Qed.
    Lemma embed_except_0 P : ⎡◇ P   P.
    Proof. by rewrite embed_or embed_later embed_pure. Qed.
284

285 286 287 288 289 290 291 292
    Global Instance embed_timeless P : Timeless P  Timeless P.
    Proof.
      intros ?. by rewrite /Timeless -embed_except_0 -embed_later timeless.
    Qed.
  End later.

  Section internal_eq.
    Context `{!BiInternalEq PROP1, !BiInternalEq PROP2, !BiEmbedInternalEq PROP1 PROP2}.
Robbert Krebbers's avatar
Robbert Krebbers committed
293

294 295 296 297 298 299 300 301
    Lemma embed_internal_eq (A : ofeT) (x y : A) : x  y @{PROP2} x  y.
    Proof.
      apply bi.equiv_spec; split; [apply embed_internal_eq_1|].
      etrans; [apply (internal_eq_rewrite x y (λ y, x  y%I)); solve_proper|].
      rewrite -(internal_eq_refl True%I) embed_pure.
      eapply bi.impl_elim; [done|]. apply bi.True_intro.
    Qed.
  End internal_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
302

303 304
  Section plainly.
    Context `{!BiPlainly PROP1, !BiPlainly PROP2, !BiEmbedPlainly PROP1 PROP2}.
Robbert Krebbers's avatar
Robbert Krebbers committed
305

306 307 308 309 310 311 312
    Lemma embed_plainly_if p P : ⎡■?p P  ?p P.
    Proof. destruct p; simpl; auto using embed_plainly. Qed.

    Lemma embed_plain (P : PROP1) : Plain P  Plain (PROP:=PROP2) P.
    Proof. intros ?. by rewrite /Plain {1}(plain P) embed_plainly. Qed.
  End plainly.
End embed.
Robbert Krebbers's avatar
Robbert Krebbers committed
313 314 315

(* Not defined using an ordinary [Instance] because the default
[class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
316
search for the other premises fail. See the proof of [monPred_objectively_plain]
Robbert Krebbers's avatar
Robbert Krebbers committed
317
for an example where it would fail with a regular [Instance].*)
318
Hint Extern 4 (Plain _) => notypeclasses refine (embed_plain _ _) : typeclass_instances.