introduce_hyp.v 12.9 KB
Newer Older
1
2
From iris.proofmode Require Import base coq_tactics reduction tactics.
From iris_automation Require Import env_utils util_classes solve_defs tele_utils.
3
From iris_automation.steps Require Import namer_tacs pure_solver.
4
5
6
7
8
9
10
11
12
From iris.bi Require Import bi telescopes.

Import bi.

Section mergable.
  Context {PROP : bi}.
  Implicit Types P : PROP.

  Lemma merge_and_consume P1 C p P2 P3 R:
13
    MergableConsume P1 C 
14
15
16
17
18
19
    C p P2 P3 
    ?p P2  (P3 - R)  P1 - R.
  Proof.
    move => Hmerge HC /=. (* /Hmerge {Hmerge} /= HPs.*)
    iIntros "[HP2 HPR] HP1".
    iApply "HPR".
20
    iApply mergable_consume; [done | iFrame].
21
22
23
  Qed.

  Lemma merge_no_consume P1 C p P2 P3 R :
24
    MergablePersist P1 C 
25
26
27
28
29
30
    C p P2 P3 
    ?p P2  (?p P2  P1 -  P3 - R)  P1 - R.
  Proof.
    move => Hmerge HC /=.
    iIntros "[HP2 HPR] HP1".
    iAssert ( P3)%I with "[HP1 HP2]" as "#HP3".
31
    { iApply mergable_persist; [done | iFrame]. }
32
33
34
35
36
37
    by iApply ("HPR" with "[$HP1 $HP2]").
  Qed.

End mergable.


38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
Section mergable_env.
  Context {PROP : bi}.

  Class MergableEnv (Δ : envs PROP) (P : PROP) (M : PROP) :=
    mergable_env : (of_envs Δ)  P   M.

  Instance mergable_env_base Δ P : 
    BiAffine PROP 
    MergableEnv Δ P True | 999.
  Proof. rewrite /MergableEnv; eauto. Qed.

  Instance mergable_env_cons Δ P C mi p P2 P3 M PR :
    BiAffine PROP 
    MergablePersist P C 
    FindInExtendedContext Δ (λ p P2, C p P2 P3) mi p P2 
    MergableEnv (envs_option_delete true mi p Δ) P M 
    MakeAnd M P3 PR 
    MergableEnv Δ P PR | 100.
    (* TODO: can this be done for nonaffine? *)
  Proof.
    rewrite /MergablePersist /MergableEnv /MakeAnd => HA HCP HΔ.
    apply (ficext_satisfies) in HΔ as HC.
    apply (findinextcontext_spec true) in HΔ.
    rewrite HΔ => {HΔ}.
    rewrite -assoc => HΔ <-.
    iIntros "(HP2 & HΔ & HP)".
    rewrite intuitionistically_and.
    iAssert ( M)%I as "#HM".
    { iClear "HP2". iStopProof. by rewrite HΔ. }
    iFrame "HM". iClear "HM".
    iClear "HΔ".
    iStopProof.
    rewrite comm HCP //.
  Qed.

End mergable_env.


76
77
78
79
80
Section lemmas.
  Context {PROP : bi}.

  Implicit Types P Q : PROP.

81
82
  Lemma introduce_hyp_premise P Q :
    (P - Q)  IntroduceHyp P Q.
83
84
  Proof. by rewrite /IntroduceHyp /=. Qed.

85
  Lemma introduce_hyp_premise_sep P P1 P2 Q :
86
    IntoSepCareful P P1 P2 
87
    IntroduceHyp P1 (IntroduceHyp P2 Q)  IntroduceHyp P Q.
88
89
90
91
92
93
  Proof.
    rewrite /IntoSepCareful /IntroduceHyp /= => ->.
    iIntros "HPQ [HP1 HP2]".
    by iApply ("HPQ" with "HP1").
  Qed.

94
  Lemma introduce_hyp_premise_tele_exist {TT} P R Q :
95
    IntoTExist P TT R 
96
    IntroduceVars (TT := TT) $ tele_map (λ R, IntroduceHyp R Q) R  IntroduceHyp P Q.
97
98
99
100
101
102
103
104
105
106
107
108
  Proof.
    rewrite /IntoTExist /IntroduceHyp /IntroduceVars /= => ->.
    iIntros "HRQ".
    iDestruct 1 as (tt) "HR".
    iSpecialize ("HRQ" $! tt).
    rewrite tele_map_app.
    by iApply "HRQ".
  Qed.

  (* Currently, IntoTExist cannot handle dependent exists. 
  For IntroduceHyp, we can overcome this by introducing the exists one by one: *)

109
  Lemma introduce_hyp_premise_exist (P Q : PROP) {A : Type} (R : A  PROP) :
110
    IntoExistCareful P R 
111
    IntroduceVars (TT := [tele_pair A]) (λ a, IntroduceHyp (R a) Q)  IntroduceHyp P Q.
112
113
114
115
116
117
118
  Proof.
    rewrite /IntoExistCareful /IntroduceHyp /IntroduceVars /= => ->.
    iIntros "HRQ".
    iDestruct 1 as (r) "HR".
    by iApply "HRQ".
  Qed.

119
  Lemma introduce_hyp_premise_or P P1 P2 Q : 
120
    IntoOr P P1 P2 
121
    IntroduceHyp P1 Q  IntroduceHyp P2 Q  IntroduceHyp P Q.
122
123
124
125
126
127
128
129
130
  Proof. 
    rewrite /IntroduceHyp /IntoOr /= => ->. 
    iIntros "HPQ [HP1|HP2]".
    - iDestruct "HPQ" as "[HPQ1 _ ]".
      by iApply "HPQ1".
    - iDestruct "HPQ" as "[_ HPQ2]".
      by iApply "HPQ2".
  Qed.

131
  Lemma introduce_hyp_mergable_consume p P C Q R S :
132
    MergableConsume Q C 
133
    C p P R 
134
    ?p P  IntroduceHyp R S  IntroduceHyp Q S.
135
136
137
138
139
  Proof.
    rewrite /IntroduceHyp /= => Hmerge HC.
    eapply merge_and_consume => //.
  Qed.

140
  Lemma introduce_hyp_mergable_no_consume p P C Q R S :
141
    MergablePersist Q C 
142
    C p P R 
143
    ?p P  (?p P  Q - IntroduceHyp ( R) S)  IntroduceHyp Q S.
144
145
146
147
148
  Proof.
    rewrite /IntroduceHyp /= => Hmerge HC.
    eapply merge_no_consume => //.
  Qed.

149
  Lemma introduce_hyp_premise_intuit P P' Q :
150
151
    IntoPersistent false P P' 
    Affine P 
152
    ( P' - Q)  IntroduceHyp P Q.
153
154
155
156
157
158
159
160
161
  Proof.
    rewrite /IntoPersistent /IntroduceHyp /= => -.
    iIntros (HPP' HP) "HP'Q HP".
    iApply "HP'Q".
    iStopProof.
    rewrite /bi_intuitionistically.
    by apply affinely_intro.
  Qed.

162
  Lemma introduce_hyp_drop_modal P M P' C Q :
163
164
165
    IntoModal false P M P' 
    DropModal M Q C 
    C P' 
166
    IntroduceHyp P' Q  IntroduceHyp P Q.
167
168
169
170
171
172
173
174
175
176
177
178
179
  Proof.
    rewrite /IntoModal /DropModal /IntroduceHyp /= => -> HQ /HQ //.
  Qed.

End lemmas.

Section coq_tactics.
  Context {PROP : bi}.

  Implicit Types P Q : PROP.

  Lemma tac_introduce_hyp_premise_sep Δ P P1 P2 Q :
    IntoSepCareful P P1 P2 
180
181
    envs_entails Δ $ IntroduceHyp P1 (IntroduceHyp P2 Q) 
    envs_entails Δ $ IntroduceHyp P Q.
182
183
184
185
186
187
188
  Proof.
    rewrite envs_entails_eq => HΔΔ' ->.
    apply introduce_hyp_premise_sep, _.
  Qed.

  Lemma tac_introduce_hyp_premise_exist Δ P {A} (R : A  PROP) Q:
    IntoExistCareful P R 
189
190
    envs_entails Δ $ IntroduceVars (TT := [tele_pair A]) (λ a, IntroduceHyp (R a) Q) 
    envs_entails Δ $ IntroduceHyp P Q.
191
192
193
194
195
196
197
  Proof.
    rewrite envs_entails_eq => HPR ->.
    by eapply introduce_hyp_premise_exist.
  Qed.

  Lemma tac_introduce_hyp_premise_or Δ P P1 P2 Q :
    IntoOr P P1 P2 
198
199
200
    envs_entails Δ $ IntroduceHyp P1 Q 
    envs_entails Δ $ IntroduceHyp P2 Q 
    envs_entails Δ $ IntroduceHyp P Q.
201
202
203
204
205
206
207
208
209
210
  Proof.
    rewrite envs_entails_eq => HP HΔ1 HΔ2.
    rewrite -introduce_hyp_premise_or.
    by apply and_intro.
  Qed.

  Lemma tac_introduce_hyp_premise_modal Δ P M P' C Q :
    IntoModal false P M P' 
    DropModal M Q C 
    C P' 
211
212
    envs_entails Δ $ IntroduceHyp P' Q 
    envs_entails Δ $ IntroduceHyp P Q.
213
214
215
216
217
  Proof.
    rewrite envs_entails_eq => HP HQC HCP ->.
    by eapply introduce_hyp_drop_modal.
  Qed.

218
219
220
221
222
223
224
225
226
227
228
  Lemma tac_introduce_hyp_merge_consume Δ P1 R C mi p P2 P3 :
    TCAnd (MergableConsume P1 C) (FindInExtendedContext Δ (λ p P2, C p P2 P3) mi p P2) 
    envs_entails (envs_option_delete true mi p Δ) $ IntroduceHyp P3 R 
    envs_entails Δ $ IntroduceHyp P1 R.
  Proof.
    rewrite envs_entails_eq => [[HP1 HP2]] HΔ.
    rewrite (findinextcontext_spec true) HΔ.
    eapply introduce_hyp_mergable_consume => //.
    by eapply ficext_satisfies in HP2.
  Qed.

229
230
  (* TODO: phrase this as a match, without an extra Δ'. This will make proofs smaller, thus Qed faster.
        See also https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/224 . Also check the tactics below *)
231
  Lemma tac_introduce_hyp_merge_persist j Δ P1 a P1' R C mi p P2 P3 :
232
    TCAnd (MergablePersist P1 C) (FindInExtendedContext Δ (λ p P2, C p P2 P3) mi p P2) 
233
234
    TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
        (TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1)) 
235
236
237
238
    match envs_add_fresh a j P1' Δ with
    | Some Δ' => envs_entails Δ' $ IntroduceHyp ( P3)%I R
    | _ => False
    end 
239
    envs_entails Δ $ IntroduceHyp P1 R.
240
  Proof.
241
242
    rewrite envs_entails_eq /IntroduceHyp => [[HP1 HP2]] HP1p' HΔR.
    destruct (envs_add_fresh a j P1' Δ) as [Δ'| ] eqn:HΔ''; last done.
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
    iIntros "HΔ' HP1".
    assert (P1  ?a P1') as HP1_ent.
    { revert HP1p'. case => [[HP1P1' HP1a] ->| [-> ->] ] //=.
      unfold bi_intuitionistically.
      rewrite -HP1P1' /=. unfold bi_affinely. iIntros "H"; iSplit => //. }
    iAssert ( P3)%I as "#HP3"; last first. (* 'iEnough' *)
    { rewrite (envs_add_fresh_sound Δ) //.
      rewrite HP1_ent.
      iSpecialize ("HΔ'" with "HP1"). 
      by iApply (HΔR with "HΔ'"). }
    rewrite (findinextcontext_spec true).
    iDestruct "HΔ'" as "[HP2 _]".
    iCombine "HP1 HP2" as "HP".
    rewrite mergable_persist; last first.
    { by eapply ficext_satisfies in HP2. }
    done.
  Qed.

261
  Lemma tac_introduce_hyp_merge_env j Δ P1 a P1' R P3 :
262
263
264
    MergableEnv Δ P1 P3 
    TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
        (TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1)) 
265
266
267
268
    match envs_add_fresh a j P1' Δ with
    | Some Δ' => envs_entails Δ' $ IntroduceHyp ( P3)%I R
    | _ => False
    end 
269
270
    envs_entails Δ $ IntroduceHyp P1 R.
  Proof.
271
272
    rewrite envs_entails_eq /IntroduceHyp => HΔ HP1p' HΔR.
    destruct (envs_add_fresh a j P1' Δ) as [Δ'| ] eqn:HΔ''; last done.
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
    iIntros "HΔ' HP1".
    assert (P1  ?a P1') as HP1_ent.
    { revert HP1p'. case => [[HP1P1' HP1a] ->| [-> ->] ] //=.
      unfold bi_intuitionistically.
      rewrite -HP1P1' /=. unfold bi_affinely. iIntros "H"; iSplit => //. }
    iAssert ( P3)%I as "#HP3"; last first. (* 'iEnough' *)
    { rewrite (envs_add_fresh_sound Δ) //.
      rewrite HP1_ent.
      iSpecialize ("HΔ'" with "HP1"). 
      by iApply (HΔR with "HΔ'"). }
    iCombine "HΔ' HP1" as "H".
    rewrite HΔ.
    eauto.
  Qed.

288
289
290
291
292
293
294
295
296
297
298
299
300
  Global Instance mergable_persist_from_box P C :
    MergablePersist P C 
    MergablePersist ( P)%I C | 5.
  Proof.
    rewrite /MergablePersist => HPC p P2 P3 /HPC <-.
    iIntros "[#$ $]".
  Qed.
  Global Instance mergable_consume_from_box P C :
    MergableConsume P C 
    MergableConsume ( P)%I C | 5.
  Proof.
    rewrite /MergableConsume => HPC p P2 P3 /HPC <-.
    iIntros "[#$ $]".
301
302
  Qed.

303
  Lemma tac_introduce_hyp_not_mergable j Δ P1 a P1' R : 
304
305
    TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
        (TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1)) 
306
307
308
309
    match envs_add_fresh a j P1' Δ with
    | Some Δ' => envs_entails Δ' $ R
    | _ => False
    end 
310
    envs_entails Δ $ IntroduceHyp P1 R.
311
  Proof.
312
313
    rewrite envs_entails_eq /IntroduceHyp => HP1p' HΔR.
    destruct (envs_add_fresh a j P1' Δ) as [Δ'| ] eqn:HΔ''; last done.
314
315
316
317
318
    rewrite (envs_add_fresh_sound Δ) // HΔR.
    apply bi.wand_mono => //.
    revert HP1p'. case => [[HP1P1' HP1a] ->| [-> ->] ] //=.
    unfold bi_intuitionistically.
    rewrite -HP1P1' /=. unfold bi_affinely. iIntros "H"; iSplit => //.
319
320
  Qed.

321
  Lemma tac_introduce_hyp_premise_pure Δ P φ Q ba :
322
    IntoPure P φ 
323
324
325
326
327
    TCIf (Affine P) (TCEq ba true) (TCEq ba false) 
    match (if ba then Some Δ else envs_add_fresh false None True%I Δ) with
    | Some Δ' => φ  envs_entails Δ' Q
    | _ => False
    end 
328
    envs_entails Δ $ IntroduceHyp P Q.
329
330
  Proof.
    rewrite envs_entails_eq => HPφ HP.
331
    destruct HP as [HP ->| ->].
332
333
334
335
336
337
338
    - assert (IntoPersistent false P ⌜φ⌝).
      { rewrite /IntoPersistent /= HPφ.
        by rewrite -(persistently_if_pure true φ) /= persistently_idemp. }
      rewrite -introduce_hyp_premise_intuit => HΔφ.
      iIntros "HΔ %".
      by iApply HΔφ.
    - rewrite /IntroduceHyp.
339
      destruct (envs_add_fresh false None True Δ) as [Δ'| ] eqn:HΔ''; last done.
340
341
342
      rewrite HPφ => Hφ.
      apply bi.wand_intro_l.
      apply bi.wand_elim_l', bi.pure_elim' => /Hφ.
343
344
      apply envs_add_fresh_sound in HΔ''.
      rewrite HΔ'' /= => <-.
345
346
      apply bi.wand_intro_r.
      rewrite bi.wand_elim_r //.
347
348
349
350
  Qed.

  Lemma tac_introduce_hyp_premise_emp Δ Q :
    envs_entails Δ Q 
351
    envs_entails Δ $ IntroduceHyp emp%I Q.
352
  Proof. 
353
    rewrite envs_entails_eq => ->.
354
355
356
357
358
    by rewrite -introduce_hyp_premise left_id. 
  Qed.

End coq_tactics.

359
Ltac simplifySolveSepPureHyp := 
360
361
362
363
364
365
366
367
368
369
370
371
372
373
  match goal with
  | |- ?φ  ?P => 
    first
    [ let H := fresh "H" in assert (¬φ) as H by trySolvePure; by move => /H
    (* tries to prove ¬φ, to eliminate contradictory cases *)
    | lazymatch φ with
      | True => intros _
      | ?a = ?a => intros _
      | _ => intros; simplify_eq; subst
      end]
  end.

Ltac introduceHypStep namer_tac :=
  first
374
  [notypeclasses refine (tac_introduce_hyp_premise_emp _ _ _ )
375
376
377
378
379
380
  |notypeclasses refine (tac_introduce_hyp_premise_sep _ _ _ _ _ _ _); [ iSolveTC | ]
  |notypeclasses refine (tac_introduce_hyp_premise_exist _ _ _ _ _ _); [ iSolveTC | simpl]
  |notypeclasses refine (tac_introduce_hyp_premise_or _ _ _ _ _ _ _ _ ); [ iSolveTC | simpl | simpl]
  |notypeclasses refine (tac_introduce_hyp_premise_modal _ _ _ _ _ _ _ _ _ _); 
    [iSolveTC | iSolveTC | simpl; iSolveTC | ]
  (* rules below this do actual introduction of separation logic premises *)
381
382
  |notypeclasses refine (tac_introduce_hyp_premise_pure _ _ _ _ _ _ _ _); 
    [ iSolveTC | iSolveTC | simpl; simplifySolveSepPureHyp ]
383
384
  |notypeclasses refine (tac_introduce_hyp_merge_consume _ _ _ _ _ _ _ _ _ _); 
    [iSolveTC | register_delete namer_tac; simpl ]
385
  | lazymatch goal with
386
    | |- envs_entails ?Δ (IntroduceHyp ?P _) =>
387
      let j := namer_tac NameTac.GetName Δ P in first
388
389
390
391
      [notypeclasses refine (tac_introduce_hyp_merge_persist j _ _ _ _ _ _ _ _ _ _ _ _ _);
        [iSolveTC | iSolveTC | simpl ]
      |notypeclasses refine (tac_introduce_hyp_not_mergable j _ _ _ _ _ _ _);
        [iSolveTC | simpl ] ]
392
    end].
393