embedding.v 10.9 KB
Newer Older
1
From iris.algebra Require Import monoid.
2
From iris.bi Require Import interface derived_laws big_op plainly updates.
3
4
From stdpp Require Import hlist.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
14
(* Mixins allow us to create instances easily without having to use Program *)
15
16
17
18
19
20
21
22
23
24
Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
  bi_embed_mixin_ne : NonExpansive embed;
  bi_embed_mixin_mono : Proper (() ==> ()) embed;
  bi_embed_mixin_entails_inj :> Inj () () embed;
  bi_embed_mixin_emp : emp  emp;
  bi_embed_mixin_impl_2 P Q : (P  Q)  P  Q;
  bi_embed_mixin_forall_2 A (Φ : A  PROP1) : ( x, ⎡Φ x)   x, Φ x;
  bi_embed_mixin_exist_1 A (Φ : A  PROP1) :  x, Φ x   x, ⎡Φ x;
  bi_embed_mixin_sep P Q : P  Q  P  Q;
  bi_embed_mixin_wand_2 P Q : (P - Q)  P - Q;
25
  bi_embed_mixin_persistently P : <pers> P  <pers> P
26
27
28
29
30
31
}.

Class BiEmbed (PROP1 PROP2 : bi) := {
  bi_embed_embed :> Embed PROP1 PROP2;
  bi_embed_mixin : BiEmbedMixin PROP1 PROP2 bi_embed_embed;
}.
32
33
Hint Mode BiEmbed ! - : typeclass_instances.
Hint Mode BiEmbed - ! : typeclass_instances.
34
Arguments bi_embed_embed : simpl never.
35

36
37
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
38
39
  embed_later P : ⎡▷ P   P;
  embed_interal_inj (PROP' : sbi) (P Q : PROP1) : P  Q  (P  Q : PROP');
40
}.
41
42
Hint Mode SbiEmbed ! - - : typeclass_instances.
Hint Mode SbiEmbed - ! - : typeclass_instances.
43

44
45
46
47
48
49
50
51
52
53
54
55
56
57
Class BiEmbedBUpd (PROP1 PROP2 : bi)
      `{BiEmbed PROP1 PROP2, BiBUpd PROP1, BiBUpd PROP2} := {
  embed_bupd  P : |==> P  bupd (PROP:=PROP2) P
}.
Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances.
Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances.

Class BiEmbedFUpd (PROP1 PROP2 : sbi)
      `{BiEmbed PROP1 PROP2, BiFUpd PROP1, BiFUpd PROP2} := {
  embed_fupd E1 E2 P : |={E1,E2}=> P  fupd (PROP:=PROP2) E1 E2 P
}.
Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.

58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
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.
  Global Instance embed_entails_inj : Inj () () embed.
  Proof. eapply bi_embed_mixin_entails_inj, bi_embed_mixin. Qed.
  Lemma embed_emp : emp  emp.
  Proof. eapply bi_embed_mixin_emp, bi_embed_mixin. Qed.
  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.
82
  Lemma embed_persistently P : <pers> P  <pers> P.
83
84
  Proof. eapply bi_embed_mixin_persistently, bi_embed_mixin. Qed.
End embed_laws.
85

86
87
88
89
Section embed.
  Context `{BiEmbed PROP1 PROP2}.
  Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
  Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
90
  Implicit Types P Q R : PROP1.
91

92
  Global Instance embed_proper : Proper (() ==> ()) embed.
93
  Proof. apply (ne_proper _). Qed.
94
  Global Instance embed_flip_mono : Proper (flip () ==> flip ()) embed.
95
  Proof. solve_proper. Qed.
96
  Global Instance embed_inj : Inj () () embed.
97
  Proof.
98
    intros P Q EQ. apply bi.equiv_spec, conj; apply (inj embed);
99
100
101
    rewrite EQ //.
  Qed.

102
  Lemma embed_valid (P : PROP1) : P%I  P.
103
  Proof.
104
    by rewrite /bi_valid -embed_emp; split=>?; [apply (inj embed)|f_equiv].
105
106
  Qed.

107
  Lemma embed_forall A (Φ : A  PROP1) :  x, Φ x   x, ⎡Φ x.
108
  Proof.
109
    apply bi.equiv_spec; split; [|apply embed_forall_2].
110
111
    apply bi.forall_intro=>?. by rewrite bi.forall_elim.
  Qed.
112
  Lemma embed_exist A (Φ : A  PROP1) :  x, Φ x   x, ⎡Φ x.
113
  Proof.
114
    apply bi.equiv_spec; split; [apply embed_exist_1|].
115
116
    apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
  Qed.
117
118
119
120
121
  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).
122
  Proof.
123
124
    apply bi.equiv_spec; split; [|apply embed_impl_2].
    apply bi.impl_intro_l. by rewrite -embed_and bi.impl_elim_r.
125
  Qed.
126
  Lemma embed_wand P Q : P - Q  (P - Q).
127
  Proof.
128
129
    apply bi.equiv_spec; split; [|apply embed_wand_2].
    apply bi.wand_intro_l. by rewrite -embed_sep bi.wand_elim_r.
130
  Qed.
131
  Lemma embed_pure φ : ⎡⌜φ⌝⎤  ⌜φ⌝.
132
  Proof.
133
    rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) embed_exist.
134
    do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|].
135
    rewrite -(_ : (emp  emp : PROP1)  True) ?embed_impl;
136
137
138
      last apply bi.True_intro.
    apply bi.impl_intro_l. by rewrite right_id.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
139

140
141
142
143
  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.
144
  Lemma embed_affinely P : <affine> P  <affine> P.
145
  Proof. by rewrite embed_and embed_emp. Qed.
146
  Lemma embed_absorbingly P : <absorb> P  <absorb> P.
147
  Proof. by rewrite embed_sep embed_pure. Qed.
148
149
  Lemma embed_intuitionistically P : ⎡□ P   P.
  Proof. rewrite embed_and embed_emp embed_persistently //. Qed.
150
  Lemma embed_persistently_if P b : <pers>?b P  <pers>?b P.
151
  Proof. destruct b; simpl; auto using embed_persistently. Qed.
152
  Lemma embed_affinely_if P b : <affine>?b P  <affine>?b P.
153
  Proof. destruct b; simpl; auto using embed_affinely. Qed.
154
155
  Lemma embed_intuitionistically_if P b : ⎡□?b P  ?b P.
  Proof. destruct b; simpl; auto using embed_intuitionistically. Qed.
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
  Lemma embed_hforall {As} (Φ : himpl As PROP1):
    bi_hforall Φ⎤  bi_hforall (hcompose embed Φ).
  Proof. induction As=>//. rewrite /= embed_forall. by do 2 f_equiv. Qed.
  Lemma embed_hexist {As} (Φ : himpl As PROP1):
    bi_hexist Φ⎤  bi_hexist (hcompose embed Φ).
  Proof. induction As=>//. rewrite /= embed_exist. by do 2 f_equiv. Qed.

  Global Instance embed_persistent P : Persistent P  Persistent P.
  Proof. intros ?. by rewrite /Persistent -embed_persistently -persistent. Qed.
  Global Instance embed_affine P : Affine P  Affine P.
  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.
172
173
  Proof.
    by split; [split|]; try apply _;
174
      [setoid_rewrite embed_and|rewrite embed_pure].
175
  Qed.
176
177
  Global Instance embed_or_homomorphism :
    MonoidHomomorphism bi_or bi_or () embed.
178
179
  Proof.
    by split; [split|]; try apply _;
180
      [setoid_rewrite embed_or|rewrite embed_pure].
181
  Qed.
182
183
  Global Instance embed_sep_homomorphism :
    MonoidHomomorphism bi_sep bi_sep () embed.
184
185
  Proof.
    by split; [split|]; try apply _;
186
      [setoid_rewrite embed_sep|rewrite embed_emp].
187
  Qed.
188

189
  Lemma embed_big_sepL {A} (Φ : nat  A  PROP1) l :
190
191
    [ list] kx  l, Φ k x  [ list] kx  l, ⎡Φ k x.
  Proof. apply (big_opL_commute _). Qed.
192
  Lemma embed_big_sepM `{Countable K} {A} (Φ : K  A  PROP1) (m : gmap K A) :
193
194
    [ map] kx  m, Φ k x  [ map] kx  m, ⎡Φ k x.
  Proof. apply (big_opM_commute _). Qed.
195
  Lemma embed_big_sepS `{Countable A} (Φ : A  PROP1) (X : gset A) :
196
197
    [ set] y  X, Φ y  [ set] y  X, ⎡Φ y.
  Proof. apply (big_opS_commute _). Qed.
198
  Lemma embed_big_sepMS `{Countable A} (Φ : A  PROP1) (X : gmultiset A) :
199
200
    [ mset] y  X, Φ y  [ mset] y  X, ⎡Φ y.
  Proof. apply (big_opMS_commute _). Qed.
201
End embed.
202

203
204
Section sbi_embed.
  Context `{SbiEmbed PROP1 PROP2}.
205
  Implicit Types P Q R : PROP1.
206

207
  Lemma embed_internal_eq (A : ofeT) (x y : A) : x  y  x  y.
208
  Proof.
209
    apply bi.equiv_spec; split; [apply embed_internal_eq_1|].
210
    etrans; [apply (bi.internal_eq_rewrite x y (λ y, x  y%I)); solve_proper|].
211
    rewrite -(bi.internal_eq_refl True%I) embed_pure.
212
213
    eapply bi.impl_elim; [done|]. apply bi.True_intro.
  Qed.
214
215
216
217
  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.
218

Robbert Krebbers's avatar
Robbert Krebbers committed
219
220
221
222
223
224
225
226
227
228
229
230
  Lemma embed_plainly `{!BiPlainly PROP1, !BiPlainly PROP2} P : ⎡■ P   P.
  Proof.
    rewrite !plainly_alt embed_internal_eq. apply (anti_symm _).
    - rewrite -embed_affinely -embed_emp. apply bi.f_equiv, _.
    - by rewrite -embed_affinely -embed_emp embed_interal_inj.
  Qed.
  Lemma embed_plainly_if `{!BiPlainly PROP1, !BiPlainly PROP2} p P : ⎡■?p P  ?p P.
  Proof. destruct p; simpl; auto using embed_plainly. Qed.

  Lemma embed_plain `{!BiPlainly PROP1, !BiPlainly PROP2} P : Plain P  Plain P.
  Proof. intros ?. by rewrite /Plain -embed_plainly -plain. Qed.

231
  Global Instance embed_timeless P : Timeless P  Timeless P.
232
  Proof.
233
    intros ?. by rewrite /Timeless -embed_except_0 -embed_later timeless.
234
  Qed.
235
End sbi_embed.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
237
238

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