embedding.v 14.7 KB
Newer Older
1
From iris.bi Require Import interface derived_laws_sbi big_op plainly updates.
2
From iris.algebra Require Import monoid.
3

4 5 6
Class Embed (A B : Type) := embed : A  B.
Arguments embed {_ _ _} _%I : simpl never.
Notation "⎡ P ⎤" := (embed P) : bi_scope.
7
Instance: Params (@embed) 3 := {}.
8
Typeclasses Opaque embed.
9

10 11 12
Hint Mode Embed ! - : typeclass_instances.
Hint Mode Embed - ! : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
13
(* Mixins allow us to create instances easily without having to use Program *)
14
Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
15 16
  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
17 18
  bi_embed_mixin_emp_valid_inj (P : PROP1) :
    bi_emp_valid (PROP:=PROP2) P  bi_emp_valid P;
19 20 21 22 23 24 25 26 27 28 29 30 31
  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
32 33 34 35 36 37
}.

Class BiEmbed (PROP1 PROP2 : bi) := {
  bi_embed_embed :> Embed PROP1 PROP2;
  bi_embed_mixin : BiEmbedMixin PROP1 PROP2 bi_embed_embed;
}.
38 39
Hint Mode BiEmbed ! - : typeclass_instances.
Hint Mode BiEmbed - ! : typeclass_instances.
40
Arguments bi_embed_embed : simpl never.
41

Robbert Krebbers's avatar
Robbert Krebbers committed
42 43 44 45 46 47
Class BiEmbedEmp (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2} := {
  embed_emp_1 :  emp : PROP1   emp;
}.
Hint Mode BiEmbedEmp ! - - : typeclass_instances.
Hint Mode BiEmbedEmp - ! - : typeclass_instances.

48 49
Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
  embed_internal_eq_1 (A : ofeT) (x y : A) : x  y  x  y;
Robbert Krebbers's avatar
Robbert Krebbers committed
50
  embed_later P : ⎡▷ P   P;
51
  embed_interal_inj (PROP' : sbi) (P Q : PROP1) : P  Q @{PROP'} (P  Q);
52
}.
53 54
Hint Mode SbiEmbed ! - - : typeclass_instances.
Hint Mode SbiEmbed - ! - : typeclass_instances.
55

56 57
Class BiEmbedBUpd (PROP1 PROP2 : bi)
      `{BiEmbed PROP1 PROP2, BiBUpd PROP1, BiBUpd PROP2} := {
58
  embed_bupd  P : |==> P @{PROP2} |==> P
59 60 61 62 63 64
}.
Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances.
Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances.

Class BiEmbedFUpd (PROP1 PROP2 : sbi)
      `{BiEmbed PROP1 PROP2, BiFUpd PROP1, BiFUpd PROP2} := {
65
  embed_fupd E1 E2 P : |={E1,E2}=> P @{PROP2} |={E1,E2}=> P
66 67 68 69
}.
Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.

70 71 72 73 74 75 76
Class BiEmbedPlainly (PROP1 PROP2 : sbi)
      `{BiEmbed PROP1 PROP2, BiPlainly PROP1, BiPlainly PROP2} := {
  embed_plainly_2 (P : PROP1) :  P  (⎡■ P : PROP2)
}.
Hint Mode BiEmbedPlainly - ! - - - : typeclass_instances.
Hint Mode BiEmbedPlainly ! - - - - : typeclass_instances.

77 78 79 80 81 82 83 84 85 86
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88 89 90
  Lemma embed_emp_valid_inj P : (P : PROP2)%I  P.
  Proof. eapply bi_embed_mixin_emp_valid_inj, bi_embed_mixin. Qed.
  Lemma embed_emp_2 : emp  emp.
  Proof. eapply bi_embed_mixin_emp_2, bi_embed_mixin. Qed.
91 92 93 94 95 96 97 98 99 100
  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.
101
  Lemma embed_persistently P : <pers> P  <pers> P.
102 103
  Proof. eapply bi_embed_mixin_persistently, bi_embed_mixin. Qed.
End embed_laws.
104

105 106 107 108
Section embed.
  Context `{BiEmbed PROP1 PROP2}.
  Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
  Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
109
  Implicit Types P Q R : PROP1.
110

111
  Global Instance embed_proper : Proper (() ==> ()) embed.
112
  Proof. apply (ne_proper _). Qed.
113
  Global Instance embed_flip_mono : Proper (flip () ==> flip ()) embed.
114
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
115 116 117 118 119 120
  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.

121
  Global Instance embed_inj : Inj () () embed.
122
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
    intros P Q EQ. apply bi.equiv_spec, conj; apply (inj embed); rewrite EQ //.
124 125
  Qed.

Ralf Jung's avatar
Ralf Jung committed
126
  Lemma embed_emp_valid (P : PROP1) : P%I  P.
127
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
128 129 130
    rewrite /bi_emp_valid. split=> HP.
    - by apply embed_emp_valid_inj.
    - by rewrite embed_emp_2 HP.
131 132
  Qed.

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

136
  Lemma embed_forall A (Φ : A  PROP1) :  x, Φ x   x, ⎡Φ x.
137
  Proof.
138
    apply bi.equiv_spec; split; [|apply embed_forall_2].
139 140
    apply bi.forall_intro=>?. by rewrite bi.forall_elim.
  Qed.
141
  Lemma embed_exist A (Φ : A  PROP1) :  x, Φ x   x, ⎡Φ x.
142
  Proof.
143
    apply bi.equiv_spec; split; [apply embed_exist_1|].
144 145
    apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
  Qed.
146 147 148 149 150
  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).
151
  Proof.
152 153
    apply bi.equiv_spec; split; [|apply embed_impl_2].
    apply bi.impl_intro_l. by rewrite -embed_and bi.impl_elim_r.
154
  Qed.
155
  Lemma embed_wand P Q : P - Q  (P - Q).
156
  Proof.
157 158
    apply bi.equiv_spec; split; [|apply embed_wand_2].
    apply bi.wand_intro_l. by rewrite -embed_sep bi.wand_elim_r.
159
  Qed.
160
  Lemma embed_pure φ : ⎡⌜φ⌝⎤  ⌜φ⌝.
161
  Proof.
162
    rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) embed_exist.
163
    do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|].
164
    rewrite -(_ : (emp  emp : PROP1)  True) ?embed_impl;
165 166 167
      last apply bi.True_intro.
    apply bi.impl_intro_l. by rewrite right_id.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
168

169 170 171 172
  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
173 174 175 176
  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.
177
  Lemma embed_absorbingly P : <absorb> P  <absorb> P.
178
  Proof. by rewrite embed_sep embed_pure. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
179 180 181 182 183
  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.

184
  Lemma embed_persistently_if P b : <pers>?b P  <pers>?b P.
185
  Proof. destruct b; simpl; auto using embed_persistently. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
186 187 188 189
  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.
190
  Proof. destruct b; simpl; auto using embed_affinely. Qed.
191 192
  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
193 194 195 196
  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.
197
  Proof. destruct b; simpl; auto using embed_intuitionistically. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
198

199 200
  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
201
  Global Instance embed_affine `{!BiEmbedEmp PROP1 PROP2} P : Affine P  Affine P.
202 203 204 205 206 207
  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.
208 209
  Proof.
    by split; [split|]; try apply _;
210
      [setoid_rewrite embed_and|rewrite embed_pure].
211
  Qed.
212 213
  Global Instance embed_or_homomorphism :
    MonoidHomomorphism bi_or bi_or () embed.
214 215
  Proof.
    by split; [split|]; try apply _;
216
      [setoid_rewrite embed_or|rewrite embed_pure].
217
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
218 219 220

  Global Instance embed_sep_entails_homomorphism :
    MonoidHomomorphism bi_sep bi_sep (flip ()) embed.
221
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
222 223
    split; [split|]; simpl; try apply _;
      [by setoid_rewrite embed_sep|by rewrite embed_emp_2].
224
  Qed.
225

Robbert Krebbers's avatar
Robbert Krebbers committed
226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261
  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.
262
End embed.
263

264 265
Section sbi_embed.
  Context `{SbiEmbed PROP1 PROP2}.
266
  Implicit Types P Q R : PROP1.
267

268
  Lemma embed_internal_eq (A : ofeT) (x y : A) : x  y  x  y.
269
  Proof.
270
    apply bi.equiv_spec; split; [apply embed_internal_eq_1|].
271
    etrans; [apply (bi.internal_eq_rewrite x y (λ y, x  y%I)); solve_proper|].
272
    rewrite -(bi.internal_eq_refl True%I) embed_pure.
273 274
    eapply bi.impl_elim; [done|]. apply bi.True_intro.
  Qed.
275 276 277 278
  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.
279

280 281 282
  (* Not an instance, since it may cause overlap *)
  Lemma bi_embed_plainly_emp `{!BiPlainly PROP1, !BiPlainly PROP2} :
    BiEmbedEmp PROP1 PROP2  BiEmbedPlainly PROP1 PROP2.
Robbert Krebbers's avatar
Robbert Krebbers committed
283
  Proof.
284 285
    intros. constructor=> P. rewrite !plainly_alt embed_internal_eq.
    by rewrite -embed_affinely -embed_emp embed_interal_inj.
Robbert Krebbers's avatar
Robbert Krebbers committed
286
  Qed.
287

Robbert Krebbers's avatar
Robbert Krebbers committed
288 289 290 291 292 293 294 295 296 297 298 299
  Lemma embed_plainly_1 `{!BiPlainly PROP1, !BiPlainly PROP2} P : ⎡■ P   P.
  Proof.
    assert ( P, <affine>  P   (<affine>  <affine> P  : PROP2)) as Hhelp.
    { intros P'. apply (anti_symm _).
      - by rewrite -bi.affinely_idemp (embed_affinely_2 P').
      - by rewrite (bi.affinely_elim P'). }
    assert (<affine>  emp   (emp : PROP2)) as Hemp.
    { apply (anti_symm _).
      - apply bi.affinely_elim_emp.
      - apply bi.and_intro; auto using embed_emp_2. }
    rewrite !plainly_alt embed_internal_eq. by rewrite Hhelp -Hemp -!bi.f_equiv.
  Qed.
300 301
  Lemma embed_plainly `{!BiPlainly PROP1, !BiPlainly PROP2,
    !BiEmbedPlainly PROP1 PROP2} P : ⎡■ P   P.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
  Proof.
303
    apply (anti_symm _). by apply embed_plainly_1. by apply embed_plainly_2.
Robbert Krebbers's avatar
Robbert Krebbers committed
304
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
305

306 307
  Lemma embed_plainly_if `{!BiPlainly PROP1, !BiPlainly PROP2,
    !BiEmbedPlainly PROP1 PROP2} p P : ⎡■?p P  ?p P.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
  Proof. destruct p; simpl; auto using embed_plainly. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
309 310 311
  Lemma embed_plainly_if_1 `{!BiPlainly PROP1, !BiPlainly PROP2} p P :
    ⎡■?p P  ?p P.
  Proof. destruct p; simpl; auto using embed_plainly_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
312

313 314
  Lemma embed_plain `{!BiPlainly PROP1, !BiPlainly PROP2} (P : PROP1) :
    Plain P  Plain (PROP:=PROP2) P.
Robbert Krebbers's avatar
Robbert Krebbers committed
315
  Proof. intros ?. by rewrite /Plain {1}(plain P) embed_plainly_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
316

317
  Global Instance embed_timeless P : Timeless P  Timeless P.
318
  Proof.
319
    intros ?. by rewrite /Timeless -embed_except_0 -embed_later timeless.
320
  Qed.
321
End sbi_embed.
Robbert Krebbers's avatar
Robbert Krebbers committed
322 323 324

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