coq_tactics.v 49.4 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
From iris.bi Require Export bi.
From iris.bi Require Import tactics.
3
From iris.proofmode Require Export base environments classes.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Import bi.
6
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

8 9
Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
10 11
Record envs (PROP : bi) :=
  Envs { env_persistent : env PROP; env_spatial : env PROP }.
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13 14 15 16
Add Printing Constructor envs.
Arguments Envs {_} _ _.
Arguments env_persistent {_} _.
Arguments env_spatial {_} _.

Robbert Krebbers's avatar
Robbert Krebbers committed
17
Record envs_wf {PROP} (Δ : envs PROP) := {
Robbert Krebbers's avatar
Robbert Krebbers committed
18 19 20 21 22
  env_persistent_valid : env_wf (env_persistent Δ);
  env_spatial_valid : env_wf (env_spatial Δ);
  envs_disjoint i : env_persistent Δ !! i = None  env_spatial Δ !! i = None
}.

23
Definition of_envs {PROP} (Δ : envs PROP) : PROP :=
24
  (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
25
Instance: Params (@of_envs) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Arguments of_envs : simpl never.
27

28
Definition envs_entails {PROP} (Δ : envs PROP) (Q : PROP) : Prop :=
29
  of_envs Δ  Q.
30
Arguments envs_entails {_} _ _%I : simpl never.
31 32 33
Typeclasses Opaque envs_entails.
Instance: Params (@envs_entails) 1.

Robbert Krebbers's avatar
Robbert Krebbers committed
34
Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
35 36 37
  env_persistent_Forall2 : env_Forall2 R (env_persistent Δ1) (env_persistent Δ2);
  env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
38

39
Definition envs_dom {PROP} (Δ : envs PROP) : list ident :=
40
  env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
41

42
Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44
  let (Γp,Γs) := Δ in
  match env_lookup i Γp with
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46
  | Some P => Some (true, P)
  | None => P  env_lookup i Γs; Some (false, P)
Robbert Krebbers's avatar
Robbert Krebbers committed
47 48
  end.

49
Definition envs_delete {PROP} (i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
Robbert Krebbers's avatar
Robbert Krebbers committed
50 51
  let (Γp,Γs) := Δ in
  match p with
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53
  | true => Envs (env_delete i Γp) Γs
  | false => Envs Γp (env_delete i Γs)
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55
  end.

56
Definition envs_lookup_delete {PROP} (i : ident)
Robbert Krebbers's avatar
Robbert Krebbers committed
57
    (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59 60
  let (Γp,Γs) := Δ in
  match env_lookup_delete i Γp with
  | Some (P,Γp') => Some (true, P, Envs Γp' Γs)
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  | None => ''(P,Γs')  env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
Robbert Krebbers's avatar
Robbert Krebbers committed
62 63
  end.

64
Fixpoint envs_lookup_delete_list {PROP} (js : list ident) (remove_persistent : bool)
Robbert Krebbers's avatar
Robbert Krebbers committed
65
    (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
66 67 68
  match js with
  | [] => Some (true, [], Δ)
  | j :: js =>
Robbert Krebbers's avatar
Robbert Krebbers committed
69 70 71
     ''(p,P,Δ')  envs_lookup_delete j Δ;
     let Δ' := if p : bool then (if remove_persistent then Δ' else Δ) else Δ' in
     ''(q,Hs,Δ'')  envs_lookup_delete_list js remove_persistent Δ';
72 73 74
     Some (p && q, P :: Hs, Δ'')
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
75
Definition envs_snoc {PROP} (Δ : envs PROP)
76
    (p : bool) (j : ident) (P : PROP) : envs PROP :=
77 78 79
  let (Γp,Γs) := Δ in
  if p then Envs (Esnoc Γp j P) Γs else Envs Γp (Esnoc Γs j P).

Robbert Krebbers's avatar
Robbert Krebbers committed
80 81
Definition envs_app {PROP : bi} (p : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83 84 85 86 87
  let (Γp,Γs) := Δ in
  match p with
  | true => _  env_app Γ Γs; Γp'  env_app Γ Γp; Some (Envs Γp' Γs)
  | false => _  env_app Γ Γp; Γs'  env_app Γ Γs; Some (Envs Γp Γs')
  end.

88
Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
Robbert Krebbers's avatar
Robbert Krebbers committed
89
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
90 91 92 93 94 95
  let (Γp,Γs) := Δ in
  match p with
  | true => _  env_app Γ Γs; Γp'  env_replace i Γ Γp; Some (Envs Γp' Γs)
  | false => _  env_app Γ Γp; Γs'  env_replace i Γ Γs; Some (Envs Γp Γs')
  end.

96
Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
Robbert Krebbers's avatar
Robbert Krebbers committed
97
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
98 99 100
  if eqb p q then envs_simple_replace i p Γ Δ
  else envs_app q Γ (envs_delete i p Δ).

Robbert Krebbers's avatar
Robbert Krebbers committed
101
Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103
  if env_spatial Δ is Enil then true else false.

Robbert Krebbers's avatar
Robbert Krebbers committed
104
Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
105 106
  Envs (env_persistent Δ) Enil.

Robbert Krebbers's avatar
Robbert Krebbers committed
107
Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
108 109
  Envs Enil (env_spatial Δ).

Robbert Krebbers's avatar
Robbert Krebbers committed
110
Fixpoint envs_split_go {PROP}
111
    (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
112 113 114
  match js with
  | [] => Some (Δ1, Δ2)
  | j :: js =>
Robbert Krebbers's avatar
Robbert Krebbers committed
115 116
     ''(p,P,Δ1')  envs_lookup_delete j Δ1;
     if p : bool then envs_split_go js Δ1 Δ2 else
117 118
     envs_split_go js Δ1' (envs_snoc Δ2 false j P)
  end.
119 120
(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
   if [d = Left] then [result = (hyps named js, remaining hyps)] *)
121
Definition envs_split {PROP} (d : direction)
122
    (js : list ident) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
123
  ''(Δ1,Δ2)  envs_split_go js Δ (envs_clear_spatial Δ);
124
  if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
125

Robbert Krebbers's avatar
Robbert Krebbers committed
126
(* Coq versions of the tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128 129 130 131 132 133
Section bi_tactics.
Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.

Lemma of_envs_eq Δ :
134
  of_envs Δ = (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
135 136
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
137 138 139 140 141 142 143 144 145 146
Lemma envs_lookup_delete_Some Δ Δ' i p P :
  envs_lookup_delete i Δ = Some (p,P,Δ')
   envs_lookup i Δ = Some (p,P)  Δ' = envs_delete i p Δ.
Proof.
  rewrite /envs_lookup /envs_delete /envs_lookup_delete.
  destruct Δ as [Γp Γs]; rewrite /= !env_lookup_delete_correct.
  destruct (Γp !! i), (Γs !! i); naive_solver.
Qed.

Lemma envs_lookup_sound Δ i p P :
147 148
  envs_lookup i Δ = Some (p,P) 
  of_envs Δ  ?p P  of_envs (envs_delete i p Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
149
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
  rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
152 153
  - rewrite pure_True ?left_id; last (destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh).
154 155
    rewrite (env_lookup_perm Γp) //= affinely_persistently_and.
    by rewrite and_sep_affinely_persistently -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
157 158 159 160
    rewrite pure_True ?left_id; last (destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh).
    rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
Lemma envs_lookup_persistent_sound Δ i P :
162
  envs_lookup i Δ = Some (true,P)  of_envs Δ   P  of_envs Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
Proof.
164
  intros. rewrite -persistently_and_affinely_sep_l. apply and_intro; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
  rewrite envs_lookup_sound //; simpl.
166
  by rewrite -persistently_and_affinely_sep_l and_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
167 168 169
Qed.

Lemma envs_lookup_split Δ i p P :
170
  envs_lookup i Δ = Some (p,P)  of_envs Δ  ?p P  (?p P - of_envs Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
171
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
  rewrite /envs_lookup /of_envs=>?. apply pure_elim_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
174 175
  - rewrite pure_True // left_id (env_lookup_perm Γp) //=
            affinely_persistently_and and_sep_affinely_persistently.
176
    cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
177
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
178
    rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
179 180 181 182
    cancel [P]. apply wand_intro_l. solve_sep_entails.
Qed.

Lemma envs_lookup_delete_sound Δ Δ' i p P :
183
  envs_lookup_delete i Δ = Some (p,P,Δ')  of_envs Δ  ?p P  of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.

186
Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
187 188
  envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ') 
  of_envs Δ  ?p [] Ps  of_envs Δ'.
189 190
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
191
  { by rewrite affinely_persistently_emp left_id. }
192 193 194
  destruct (envs_lookup_delete j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
  apply envs_lookup_delete_Some in Hj as [Hj ->].
  destruct (envs_lookup_delete_list js rp _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
195
  rewrite -affinely_persistently_if_sep_2 -assoc. destruct q1; simpl.
196
  - destruct rp.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
    + rewrite envs_lookup_sound //; simpl.
198
      by rewrite IH // (affinely_persistently_affinely_persistently_if q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
199
    + rewrite envs_lookup_persistent_sound //.
200 201
      by rewrite IH // (affinely_persistently_affinely_persistently_if q2).
  - rewrite envs_lookup_sound // IH //; simpl. by rewrite affinely_persistently_if_elim.
202 203
Qed.

204 205 206 207 208 209 210 211 212 213 214 215 216 217
Lemma envs_lookup_snoc Δ i p P :
  envs_lookup i Δ = None  envs_lookup i (envs_snoc Δ p i P) = Some (p, P).
Proof.
  rewrite /envs_lookup /envs_snoc=> ?.
  destruct Δ as [Γp Γs], p, (Γp !! i); simplify_eq; by rewrite env_lookup_snoc.
Qed.
Lemma envs_lookup_snoc_ne Δ i j p P :
  i  j  envs_lookup i (envs_snoc Δ p j P) = envs_lookup i Δ.
Proof.
  rewrite /envs_lookup /envs_snoc=> ?.
  destruct Δ as [Γp Γs], p; simplify_eq; by rewrite env_lookup_snoc_ne.
Qed.

Lemma envs_snoc_sound Δ p i P :
218
  envs_lookup i Δ = None  of_envs Δ  ?p P - of_envs (envs_snoc Δ p i P).
219
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
  rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_l=> Hwf.
221 222
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
  apply wand_intro_l; destruct p; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
  - apply and_intro; [apply pure_intro|].
224
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
225
      intros j; destruct (ident_beq_reflect j i); naive_solver.
226
    + by rewrite affinely_persistently_and and_sep_affinely_persistently assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
  - apply and_intro; [apply pure_intro|].
228
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
229
      intros j; destruct (ident_beq_reflect j i); naive_solver.
230 231 232
    + solve_sep_entails.
Qed.

233
Lemma envs_app_sound Δ Δ' p Γ :
234 235
  envs_app p Γ Δ = Some Δ' 
  of_envs Δ  (if p then  [] Γ else [] Γ) - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
  rewrite /of_envs /envs_app=> ?; apply pure_elim_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
238 239 240
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
241
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
242 243 244 245
    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      naive_solver eauto using env_app_fresh.
    + rewrite (env_app_perm _ _ Γp') //.
246
      rewrite big_opL_app affinely_persistently_and and_sep_affinely_persistently.
247
      solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
248 249
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
250
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
251 252 253
    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      naive_solver eauto using env_app_fresh.
254
    + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
255 256
Qed.

257
Lemma envs_app_singleton_sound Δ Δ' p j Q :
258
  envs_app p (Esnoc Enil j Q) Δ = Some Δ'  of_envs Δ  ?p Q - of_envs Δ'.
259 260
Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
261 262
Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
263
  of_envs (envs_delete i p Δ)  (if p then  [] Γ else [] Γ) - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
264 265
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
Robbert Krebbers's avatar
Robbert Krebbers committed
266
  apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
267 268
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
270 271 272 273
    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
    + rewrite (env_replace_perm _ _ Γp') //.
274
      rewrite big_opL_app affinely_persistently_and and_sep_affinely_persistently.
275
      solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
276 277
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
278
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
279 280 281
    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
282
    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
283 284
Qed.

285 286
Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' 
287
  of_envs (envs_delete i p Δ)  ?p Q - of_envs Δ'.
288 289
Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
290 291
Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
292
  of_envs Δ  ?p P  ((if p then  [] Γ else [] Γ) - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
293 294
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

295 296 297
Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' 
298
  of_envs Δ  ?p P  (?p Q - of_envs Δ').
299 300 301 302
Proof.
  intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
303
Lemma envs_replace_sound' Δ Δ' i p q Γ :
304
  envs_replace i p q Γ Δ = Some Δ' 
305
  of_envs (envs_delete i p Δ)  (if q then  [] Γ else [] Γ) - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
306 307 308 309 310 311
Proof.
  rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
  - apply envs_app_sound.
Qed.

312 313
Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q :
  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' 
314
  of_envs (envs_delete i p Δ)  ?q Q - of_envs Δ'.
315 316
Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
317 318
Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P)  envs_replace i p q Γ Δ = Some Δ' 
319
  of_envs Δ  ?p P  ((if q then  [] Γ else [] Γ) - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
320 321
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

322 323 324
Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
  envs_lookup i Δ = Some (p,P) 
  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' 
325
  of_envs Δ  ?p P  (?q Q - of_envs Δ').
326 327
Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.

328 329
Lemma envs_lookup_envs_clear_spatial Δ j :
  envs_lookup j (envs_clear_spatial Δ)
Robbert Krebbers's avatar
Robbert Krebbers committed
330
  = ''(p,P)  envs_lookup j Δ; if p : bool then Some (p,P) else None.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
Proof.
332 333 334
  rewrite /envs_lookup /envs_clear_spatial.
  destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto.
  by destruct (Γs !! j).
Robbert Krebbers's avatar
Robbert Krebbers committed
335 336
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
337
Lemma envs_clear_spatial_sound Δ :
338
  of_envs Δ  of_envs (envs_clear_spatial Δ)  [] env_spatial Δ.
339
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
340 341 342
  rewrite /of_envs /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
  rewrite right_id -persistent_and_sep_assoc. apply and_intro; [|done].
  apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
343 344
Qed.

345
Lemma env_spatial_is_nil_affinely_persistently Δ :
346
  env_spatial_is_nil Δ = true  of_envs Δ   of_envs Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
347 348
Proof.
  intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
349 350
  rewrite !right_id {1}affinely_and_r persistently_and.
  by rewrite persistently_affinely persistently_idemp persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
351
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
352

353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372
Lemma envs_lookup_envs_delete Δ i p P :
  envs_wf Δ 
  envs_lookup i Δ = Some (p,P)  envs_lookup i (envs_delete i p Δ) = None.
Proof.
  rewrite /envs_lookup /envs_delete=> -[?? Hdisj] Hlookup.
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - rewrite env_lookup_env_delete //. revert Hlookup.
    destruct (Hdisj i) as [->| ->]; [|done]. by destruct (Γs !! _).
  - rewrite env_lookup_env_delete //. by destruct (Γp !! _).
Qed.
Lemma envs_lookup_envs_delete_ne Δ i j p :
  i  j  envs_lookup i (envs_delete j p Δ) = envs_lookup i Δ.
Proof.
  rewrite /envs_lookup /envs_delete=> ?. destruct Δ as [Γp Γs],p; simplify_eq/=.
  - by rewrite env_lookup_env_delete_ne.
  - destruct (Γp !! i); simplify_eq/=; by rewrite ?env_lookup_env_delete_ne.
Qed.

Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' :
  ( j P, envs_lookup j Δ1 = Some (false, P)  envs_lookup j Δ2 = None) 
Robbert Krebbers's avatar
Robbert Krebbers committed
373
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') 
374
  of_envs Δ1  of_envs Δ2  of_envs Δ1'  of_envs Δ2'.
375 376 377
Proof.
  revert Δ1 Δ2 Δ1' Δ2'.
  induction js as [|j js IH]=> Δ1 Δ2 Δ1' Δ2' Hlookup HΔ; simplify_eq/=; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
378 379
  apply pure_elim with (envs_wf Δ1)=> [|Hwf].
  { by rewrite /of_envs !and_elim_l sep_elim_l. }
380 381 382 383 384 385 386 387 388 389
  destruct (envs_lookup_delete j Δ1)
    as [[[[] P] Δ1'']|] eqn:Hdel; simplify_eq; auto.
  apply envs_lookup_delete_Some in Hdel as [??]; subst.
  rewrite envs_lookup_sound //; rewrite /= (comm _ P) -assoc.
  rewrite -(IH _ _ _ _ _ HΔ); last first.
  { intros j' P'; destruct (decide (j = j')) as [->|].
    - by rewrite (envs_lookup_envs_delete _ _ _ P).
    - rewrite envs_lookup_envs_delete_ne // envs_lookup_snoc_ne //. eauto. }
  rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto.
Qed.
390
Lemma envs_split_sound Δ d js Δ1 Δ2 :
391
  envs_split d js Δ = Some (Δ1,Δ2)  of_envs Δ  of_envs Δ1  of_envs Δ2.
392
Proof.
393
  rewrite /envs_split=> ?. rewrite -(idemp bi_and (of_envs Δ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
394
  rewrite {2}envs_clear_spatial_sound.
395 396
  rewrite (env_spatial_is_nil_affinely_persistently (envs_clear_spatial _)) //.
  rewrite -persistently_and_affinely_sep_l.
397
  rewrite (and_elim_l (bi_persistently _)%I)
398
          persistently_and_affinely_sep_r affinely_persistently_elim.
399 400 401
  destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
  apply envs_split_go_sound in HΔ as ->; last first.
  { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
402
  destruct d; simplify_eq/=; solve_sep_entails.
403 404
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
405
Global Instance envs_Forall2_refl (R : relation PROP) :
406 407
  Reflexive R  Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
408
Global Instance envs_Forall2_sym (R : relation PROP) :
409 410
  Symmetric R  Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
411
Global Instance envs_Forall2_trans (R : relation PROP) :
412 413
  Transitive R  Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
414
Global Instance envs_Forall2_antisymm (R R' : relation PROP) :
415 416
  AntiSymm R R'  AntiSymm (envs_Forall2 R) (envs_Forall2 R').
Proof. intros ??? [??] [??]; constructor; by eapply (anti_symm _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
417
Lemma envs_Forall2_impl (R R' : relation PROP) Δ1 Δ2 :
418 419 420
  envs_Forall2 R Δ1 Δ2  ( P Q, R P Q  R' P Q)  envs_Forall2 R' Δ1 Δ2.
Proof. intros [??] ?; constructor; eauto using env_Forall2_impl. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
421
Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
422
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
423 424
  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; apply and_mono; simpl in *.
  - apply pure_mono=> -[???]. constructor;
425 426 427
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
428 429
Global Instance of_envs_proper :
  Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
430
Proof.
431 432
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
433
Qed.
434
Global Instance Envs_proper (R : relation PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
435
  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs PROP).
436 437
Proof. by constructor. Qed.

438
Global Instance envs_entails_proper :
439
  Proper (envs_Forall2 () ==> () ==> iff) (@envs_entails PROP).
440 441
Proof. solve_proper. Qed.
Global Instance envs_entails_flip_mono :
442
  Proper (envs_Forall2 () ==> flip () ==> flip impl) (@envs_entails PROP).
443 444
Proof. rewrite /envs_entails=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
445
(** * Adequacy *)
446
Lemma tac_adequate P : envs_entails (Envs Enil Enil) P  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
447
Proof.
448
  intros <-. rewrite /of_envs /= persistently_True_emp affinely_persistently_emp left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
449
  apply and_intro=> //. apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
450 451 452
Qed.

(** * Basic rules *)
453 454 455 456 457 458 459
Class AffineEnv (Γ : env PROP) := affine_env : Forall Affine Γ.
Global Instance affine_env_nil : AffineEnv Enil.
Proof. constructor. Qed.
Global Instance affine_env_snoc Γ i P :
  Affine P  AffineEnv Γ  AffineEnv (Esnoc Γ i P).
Proof. by constructor. Qed.

460 461 462 463
(* If the BI is affine, no need to walk on the whole environment. *)
Global Instance affine_env_bi `(AffineBI PROP) Γ : AffineEnv Γ | 0.
Proof. induction Γ; apply _. Qed.

464
Instance affine_env_spatial Δ :
465 466 467
  AffineEnv (env_spatial Δ)  Affine ([] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.

468 469
Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ)  of_envs Δ  emp.
Proof. intros. by rewrite (affine (of_envs Δ)). Qed.
470

Robbert Krebbers's avatar
Robbert Krebbers committed
471 472 473
Lemma tac_assumption Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
  FromAssumption p P Q 
474 475
  (if env_spatial_is_nil Δ' then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) 
476
  of_envs Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
477
Proof.
478
  intros ?? H. rewrite envs_lookup_delete_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
479
  destruct (env_spatial_is_nil Δ') eqn:?.
480
  - by rewrite (env_spatial_is_nil_affinely_persistently Δ') // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
481
  - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
482
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
483 484 485 486

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
487 488
  envs_entails Δ' Q 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
489
Proof.
490
  rewrite /envs_entails=> ?? <-. rewrite envs_simple_replace_singleton_sound //.
491
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
492
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
493

Robbert Krebbers's avatar
Robbert Krebbers committed
494
Lemma tac_clear Δ Δ' i p P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
495 496
  envs_lookup_delete i Δ = Some (p,P,Δ') 
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
497 498
  (envs_entails Δ' Q) 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
499
Proof.
500 501
  rewrite /envs_entails=> ?? HQ. rewrite envs_lookup_delete_sound //.
  by destruct p; rewrite /= HQ sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
502
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
503 504

(** * False *)
505 506
Lemma tac_ex_falso Δ Q : envs_entails Δ False  envs_entails Δ Q.
Proof. by rewrite /envs_entails -(False_elim Q). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
507

Robbert Krebbers's avatar
Robbert Krebbers committed
508 509 510
Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
  P = False%I 
511
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
512
Proof.
513
  rewrite /envs_entails => ??. subst. rewrite envs_lookup_sound //; simpl.
514
  by rewrite affinely_persistently_if_elim sep_elim_l False_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
515 516
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
517
(** * Pure *)
518 519
Lemma tac_pure_intro Δ Q φ : FromPure Q φ  φ  envs_entails Δ Q.
Proof. intros ??. rewrite /envs_entails -(from_pure Q). by apply pure_intro. Qed.
520

Robbert Krebbers's avatar
Robbert Krebbers committed
521
Lemma tac_pure Δ Δ' i p P φ Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
522 523
  envs_lookup_delete i Δ = Some (p, P, Δ') 
  IntoPure P φ 
524
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
525
  (φ  envs_entails Δ' Q)  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
526
Proof.
527 528
  rewrite /envs_entails=> ?? HPQ HQ.
  rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
529
  - rewrite (into_pure P) -persistently_and_affinely_sep_l persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
530
    by apply pure_elim_l.
531
  - destruct HPQ.
532
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
533
      by apply pure_elim_l.
534 535
    + rewrite (into_pure P) (persistent_absorbingly_affinely  _ %I) absorbingly_sep_lr.
      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
536 537
Qed.

538 539
Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝  Q)  (φ  envs_entails Δ Q).
Proof. rewrite /envs_entails. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
540

541 542
(** * Persistence and plainness modalities *)
Class IntoPlainEnv (Γ1 Γ2 : env PROP) := {
543
  into_plain_env_subenv : env_subenv Γ2 Γ1;
544
  into_plain_env_plain : Plain ([] Γ2);
545 546 547 548 549 550 551 552 553 554 555 556
}.

Global Instance into_plain_env_nil : IntoPlainEnv Enil Enil.
Proof. constructor. constructor. simpl; apply _. Qed.
Global Instance into_plain_env_snoc_plain Γ1 Γ2 i P :
  Plain P  IntoPlainEnv Γ1 Γ2 
  IntoPlainEnv (Esnoc Γ1 i P) (Esnoc Γ2 i P) | 1.
Proof. intros ? [??]; constructor. by constructor. simpl; apply _. Qed.
Global Instance into_plain_env_snoc_skip Γ1 Γ2 i P :
  IntoPlainEnv Γ1 Γ2  IntoPlainEnv (Esnoc Γ1 i P) Γ2 | 2.
Proof. intros [??]; constructor. by constructor. done. Qed.

557
Lemma into_plain_env_sound Γ1 Γ2 :
558
  IntoPlainEnv Γ1 Γ2  of_envs (Envs Γ1 Enil)  bi_plainly $ of_envs $ Envs Γ2 Enil.
559
Proof.
560 561 562 563 564 565 566
  intros [Hsub ?]. rewrite !of_envs_eq plainly_and plainly_pure /=. f_equiv.
  { f_equiv=>-[/= ???]. split; auto. by eapply env_subenv_wf. }
  rewrite !(right_id emp%I). trans ( [] Γ2)%I.
  - do 2 f_equiv. clear -Hsub.
    induction Hsub as [|????? IH|????? IH]=>//=; rewrite IH //. apply and_elim_r.
  - by rewrite {1}(plain ([] Γ2)) affinely_elim plainly_affinely
               plainly_persistently persistently_plainly.
567 568
Qed.

569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588
Class IntoAlwaysEnvs (pe : bool) (pl : bool) (Δ1 Δ2 : envs PROP) := {
  into_persistent_envs_persistent :
    if pl then IntoPlainEnv (env_persistent Δ1) (env_persistent Δ2)
    else env_persistent Δ1 = env_persistent Δ2;
  into_persistent_envs_spatial :
    if pe || pl then env_spatial Δ2 = Enil else env_spatial Δ1 = env_spatial Δ2
}.

Global Instance into_always_false_false Δ : IntoAlwaysEnvs false false Δ Δ.
Proof. by split. Qed.
Global Instance into_always_envs_true_false Γp Γs :
  IntoAlwaysEnvs true false (Envs Γp Γs) (Envs Γp Enil).
Proof. by split. Qed.
Global Instance into_always_envs_x_true Γp1 Γp2 Γs1 pe :
  IntoPlainEnv Γp1 Γp2 
  IntoAlwaysEnvs pe true (Envs Γp1 Γs1) (Envs Γp2 Enil).
Proof. destruct pe; by split. Qed.

Lemma tac_always_intro Δ Δ' a pe pl Q Q' :
  FromAlways a pe pl Q' Q 
589
  (if a then AffineEnv (env_spatial Δ') else TCTrue) 
590
  IntoAlwaysEnvs pe pl Δ' Δ 
591
  (envs_entails Δ Q)  envs_entails Δ' Q'.
Robbert Krebbers's avatar
Robbert Krebbers committed
592
Proof.
593 594 595 596
  rewrite /envs_entails => ? Haffine [Hep Hes] HQ.
  rewrite -(from_always a pe pl Q') -HQ.
  trans (bi_affinely_if a (of_envs Δ'));
    [destruct a=>//; by apply: affinely_intro|f_equiv].
597 598 599 600 601 602 603 604 605 606
  destruct pl; [|destruct pe].
  - rewrite (envs_clear_spatial_sound Δ') into_plain_env_sound sep_elim_l.
    destruct Δ as [Δ ?]. rewrite orb_true_r /= in Hes. rewrite Hes /=.
    destruct pe=>/= //. by rewrite persistently_plainly.
  - rewrite (envs_clear_spatial_sound Δ') /= /envs_clear_spatial Hep.
    destruct Δ as [Δ ?]. simpl in Hes. subst. simpl.
    rewrite -(sep_elim_l (bi_persistently _)). f_equiv.
    rewrite {1}(env_spatial_is_nil_affinely_persistently (Envs Δ Enil)) //.
    by rewrite affinely_elim.
  - destruct Δ, Δ'; simpl in *. by subst.
607
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
608 609

Lemma tac_persistent Δ Δ' i p P P' Q :
610
  envs_lookup i Δ = Some (p, P) 
611
  IntoPersistent p P P' 
612
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
613
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
614
  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
615
Proof.
616
  rewrite /envs_entails=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=.
617 618 619
  destruct p; simpl.
  - by rewrite -(into_persistent _ P) /= wand_elim_r.
  - destruct HPQ.
620
    + rewrite -(affine_affinely P) (_ : P = bi_persistently_if false P)%I //
621 622
              (into_persistent _ P) wand_elim_r //.
    + rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent _ P).
623 624
      by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
                 absorbingly_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
625 626 627
Qed.

(** * Implication and wand *)
628
Lemma envs_app_singleton_sound_foo Δ Δ' p j Q :
629
  envs_app p (Esnoc Enil j Q) Δ = Some Δ'  of_envs Δ  ?p Q  of_envs Δ'.
630 631
Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.

632
Lemma tac_impl_intro Δ Δ' i P P' Q :
633
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
634
  envs_app false (Esnoc Enil i P') Δ = Some Δ' 
635
  FromAffinely P' P 
636
  envs_entails Δ' Q  envs_entails Δ (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
637
Proof.
638
  rewrite /envs_entails => ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
639
  - rewrite (env_spatial_is_nil_affinely_persistently Δ) //; simpl. apply impl_intro_l.
640
    rewrite envs_app_singleton_sound //; simpl.
641 642
    rewrite -(from_affinely P') -affinely_and_lr.
    by rewrite persistently_and_affinely_sep_r affinely_persistently_elim wand_elim_r.
643
  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
644
    by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
645 646
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
647
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
648
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
649
  envs_entails Δ' Q  envs_entails Δ (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
650
Proof.
651 652
  rewrite /envs_entails => ?? <-.
  rewrite envs_app_singleton_sound //=. apply impl_intro_l.
653
  rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent false P).
654
  by rewrite persistently_and_affinely_sep_l wand_elim_r.
655 656
Qed.
Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
657
  (φ  envs_entails Δ ⌜ψ⌝)  envs_entails Δ ⌜φ  ψ⌝.
658
Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
659 660
Lemma tac_impl_intro_pure Δ P φ Q :
  IntoPure P φ  (φ  envs_entails Δ Q)  envs_entails Δ (P  Q).
661 662
Proof.
  intros. apply impl_intro_l. rewrite (into_pure P). by apply pure_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
663
Qed.
664

665 666
Lemma tac_impl_intro_drop Δ P Q : envs_entails Δ Q  envs_entails Δ (P  Q).
Proof. rewrite /envs_entails=> ?. apply impl_intro_l. by rewrite and_elim_r. Qed.