introduce_hyp.v 16 KB
Newer Older
1
From iris.proofmode Require Import base coq_tactics reduction tactics.
2
3
From diaframe Require Import env_utils util_classes solve_defs tele_utils.
From diaframe.steps Require Import namer_tacs pure_solver.
4
5
6
7
From iris.bi Require Import bi telescopes.

Import bi.

8
9
10
11
(* This file contains 'case 2' of Diaframe's proof search strategy: introducing wands.
   In addition to the paper, this also includes using MergableConsume and
   MergablePersist instances to optimally merge the context *)

12
13
14
15
16
Section mergable.
  Context {PROP : bi}.
  Implicit Types P : PROP.

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

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

End mergable.


42
Section mergable_env. (* WIP *)
43
44
45
  Context {PROP : bi}.

  Class MergableEnv (Δ : envs PROP) (P : PROP) (M : PROP) :=
46
    mergable_env : (of_envs Δ)  P  <pers> M.
47
48
49
50
51
52
53
54
55
56
57
58

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

  Instance mergable_env_cons Δ P C mi p P2 P3 M PR :
    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.
  Proof.
59
    rewrite /MergablePersist /MergableEnv /MakeAnd => HCP HΔ.
60
61
62
63
64
    apply (ficext_satisfies) in HΔ as HC.
    apply (findinextcontext_spec true) in HΔ.
    rewrite HΔ => {HΔ}.
    rewrite -assoc => HΔ <-.
    iIntros "(HP2 & HΔ & HP)".
65
66
67
    iSplit.
    - iClear "HP2". iApply HΔ. by iFrame.
    - iClear "HΔ". iApply HCP => //. by iFrame.
68
69
70
71
72
  Qed.

End mergable_env.


73
74
75
76
77
Section lemmas.
  Context {PROP : bi}.

  Implicit Types P Q : PROP.

78
  Lemma introduce_hyp_premise_sep P P1 P2 Q :
79
    IntoSepCareful P P1 P2 
80
    IntroduceHyp P1 (IntroduceHyp P2 Q)  IntroduceHyp P Q.
81
  Proof.
82
    unseal_diaframe; rewrite /IntoSepCareful /= => ->.
83
84
85
86
    iIntros "HPQ [HP1 HP2]".
    by iApply ("HPQ" with "HP1").
  Qed.

87
  Lemma introduce_hyp_premise_tele_exist {TT} P R Q :
88
    IntoTExist P TT R 
89
    IntroduceVars (TT := TT) $ tele_map (λ R, IntroduceHyp R Q) R  IntroduceHyp P Q.
90
  Proof.
91
    unseal_diaframe; rewrite /IntoTExist /= => ->.
92
93
94
95
96
97
98
99
100
101
    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: *)

102
  Lemma introduce_hyp_premise_exist (P Q : PROP) {A : Type} (R : A  PROP) :
103
    IntoExistCareful P R 
104
    IntroduceVars (TT := [tele_pair A]) (λ a, IntroduceHyp (R a) Q)  IntroduceHyp P Q.
105
  Proof.
106
    unseal_diaframe; rewrite /IntoExistCareful /= => ->.
107
108
109
110
111
    iIntros "HRQ".
    iDestruct 1 as (r) "HR".
    by iApply "HRQ".
  Qed.

112
  Lemma introduce_hyp_premise_or P P1 P2 Q : 
113
    IntoOr P P1 P2 
114
    IntroduceHyp P1 Q  IntroduceHyp P2 Q  IntroduceHyp P Q.
115
  Proof. 
116
    unseal_diaframe; rewrite /IntoOr /= => ->. 
117
118
119
120
121
122
123
    iIntros "HPQ [HP1|HP2]".
    - iDestruct "HPQ" as "[HPQ1 _ ]".
      by iApply "HPQ1".
    - iDestruct "HPQ" as "[_ HPQ2]".
      by iApply "HPQ2".
  Qed.

124
  Lemma introduce_hyp_mergable_consume p P C Q R S :
125
    MergableConsume Q C 
126
    C p P R 
127
    ?p P  IntroduceHyp R S  IntroduceHyp Q S.
128
  Proof.
129
    unseal_diaframe => Hmerge HC.
130
131
132
    eapply merge_and_consume => //.
  Qed.

133
  Lemma introduce_hyp_mergable_no_consume p P C Q R S :
134
    MergablePersist Q C 
135
    C p P R 
136
    ?p P  (?p P  Q - IntroduceHyp ( R) S)  IntroduceHyp Q S.
137
  Proof.
138
    unseal_diaframe => /= Hmerge HC.
139
140
141
    eapply merge_no_consume => //.
  Qed.

142
  Lemma introduce_hyp_premise_intuit P P' Q :
143
144
    IntoPersistent false P P' 
    Affine P 
145
    ( P' - Q)  IntroduceHyp P Q.
146
  Proof.
147
    unseal_diaframe; rewrite /IntoPersistent /= => -.
148
149
150
151
152
153
154
    iIntros (HPP' HP) "HP'Q HP".
    iApply "HP'Q".
    iStopProof.
    rewrite /bi_intuitionistically.
    by apply affinely_intro.
  Qed.

155
  Lemma introduce_hyp_drop_modal P M P' C Q :
156
157
158
    IntoModal false P M P' 
    DropModal M Q C 
    C P' 
159
    IntroduceHyp P' Q  IntroduceHyp P Q.
160
  Proof.
161
    unseal_diaframe; rewrite /IntoModal /DropModal /= => -> HQ /HQ //.
162
163
164
165
166
167
168
169
170
171
172
  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 
173
174
    envs_entails Δ $ IntroduceHyp P1 (IntroduceHyp P2 Q) 
    envs_entails Δ $ IntroduceHyp P Q.
175
176
177
178
179
180
181
  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 
182
183
    envs_entails Δ $ IntroduceVars (TT := [tele_pair A]) (λ a, IntroduceHyp (R a) Q) 
    envs_entails Δ $ IntroduceHyp P Q.
184
185
186
187
188
189
190
  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 
191
192
193
    envs_entails Δ $ IntroduceHyp P1 Q 
    envs_entails Δ $ IntroduceHyp P2 Q 
    envs_entails Δ $ IntroduceHyp P Q.
194
195
196
197
198
199
200
201
202
203
  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' 
204
205
    envs_entails Δ $ IntroduceHyp P' Q 
    envs_entails Δ $ IntroduceHyp P Q.
206
207
208
209
210
  Proof.
    rewrite envs_entails_eq => HP HQC HCP ->.
    by eapply introduce_hyp_drop_modal.
  Qed.

211
212
213
214
215
216
217
218
219
220
221
  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.

222
  Lemma tac_introduce_hyp_merge_persist j Δ P1 a P1' R C mi p P2 P3 :
223
    TCAnd (MergablePersist P1 C) (FindInExtendedContext Δ (λ p P2, C p P2 P3) mi p P2) 
224
225
    TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
        (TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1)) 
226
227
228
229
    match envs_add_fresh a j P1' Δ with
    | Some Δ' => envs_entails Δ' $ IntroduceHyp ( P3)%I R
    | _ => False
    end 
230
    envs_entails Δ $ IntroduceHyp P1 R.
231
  Proof.
232
    unseal_diaframe; rewrite envs_entails_eq => [[HP1 HP2]] HP1p' HΔR.
233
    destruct (envs_add_fresh a j P1' Δ) as [Δ'| ] eqn:HΔ''; last done.
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
    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.

252
  Lemma tac_introduce_hyp_merge_env j Δ P1 a P1' R P3 :
253
254
255
    MergableEnv Δ P1 P3 
    TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
        (TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1)) 
256
257
258
259
    match envs_add_fresh a j P1' Δ with
    | Some Δ' => envs_entails Δ' $ IntroduceHyp ( P3)%I R
    | _ => False
    end 
260
261
    envs_entails Δ $ IntroduceHyp P1 R.
  Proof.
262
    unseal_diaframe; rewrite envs_entails_eq => HΔ HP1p' HΔR.
263
    destruct (envs_add_fresh a j P1' Δ) as [Δ'| ] eqn:HΔ''; last done.
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
    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.

279
280
281
282
283
284
285
286
287
288
289
290
291
  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 "[#$ $]".
292
293
  Qed.

294
  Lemma tac_introduce_hyp_not_mergable j Δ P1 a P1' R : 
295
296
    TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
        (TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1)) 
297
298
299
300
    match envs_add_fresh a j P1' Δ with
    | Some Δ' => envs_entails Δ' $ R
    | _ => False
    end 
301
    envs_entails Δ $ IntroduceHyp P1 R.
302
  Proof.
303
    unseal_diaframe; rewrite envs_entails_eq => HP1p' HΔR.
304
    destruct (envs_add_fresh a j P1' Δ) as [Δ'| ] eqn:HΔ''; last done.
305
306
307
308
309
    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 => //.
310
311
  Qed.

312
  Lemma tac_introduce_hyp_premise_pure Δ P φ Q ba :
313
    IntoPure P φ 
314
315
316
317
318
    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 
319
    envs_entails Δ $ IntroduceHyp P Q.
320
321
  Proof.
    rewrite envs_entails_eq => HPφ HP.
322
    destruct HP as [HP ->| ->].
323
324
325
326
327
328
    - 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Δφ.
329
    - unseal_diaframe.
330
      destruct (envs_add_fresh false None True Δ) as [Δ'| ] eqn:HΔ''; last done.
331
332
333
      rewrite HPφ => Hφ.
      apply bi.wand_intro_l.
      apply bi.wand_elim_l', bi.pure_elim' => /Hφ.
334
335
      apply envs_add_fresh_sound in HΔ''.
      rewrite HΔ'' /= => <-.
336
337
      apply bi.wand_intro_r.
      rewrite bi.wand_elim_r //.
338
339
340
341
  Qed.

  Lemma tac_introduce_hyp_premise_emp Δ Q :
    envs_entails Δ Q 
342
    envs_entails Δ $ IntroduceHyp emp%I Q.
343
  Proof. 
344
345
    unseal_diaframe; rewrite envs_entails_eq => ->.
    by rewrite left_id. 
346
347
348
349
  Qed.

End coq_tactics.

350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441

Fixpoint revert_idents {PROP : bi} (js : list ident) Δ G : option (envs PROP * PROP) :=
  match js with
  | [] => Some (Δ, G)
  | j :: js =>
    '(Δ', G')  revert_idents js Δ G;
    '(p, H)  envs_lookup j Δ';
    Some (envs_delete true j p Δ', IntroduceHyp H G')
  end.

Lemma revert_idents_sound {PROP : bi} (js : list ident) Δ (G : PROP) :
  match revert_idents js Δ G with
  | Some (Δ', G') => envs_entails Δ' G'
  | _ => False
  end 
  envs_entails Δ G.
Proof.
  rewrite envs_entails_eq.
  revert Δ G.
  induction js as [|j js] => //.
  move => Δ G. cbn.
  destruct (revert_idents _ _ _) as [[Δ' G']|] eqn:HΔG => //=.
  destruct (envs_lookup _ _) as [[p P]|] eqn:HjΔ => //=.
  move => HΔP.
  apply IHjs. rewrite HΔG.
  rewrite envs_lookup_sound //.
  apply bi.wand_elim_r'.
  rewrite HΔP. unseal_diaframe.
  by rewrite bi.intuitionistically_if_elim.
Qed.

(* some ltacs to collect hypotheses which should be reintroduced *)
Ltac collect_env_occs x Γi acci :=
  let rec mthd Γ acc :=
    lazymatch Γ with
    | Enil => acc
    | Esnoc ?Γ' ?i ?H =>
      lazymatch H with
      | context [x] => 
        let result := mthd Γ' acc in
        constr:(i::result)
      | _ => mthd Γ' acc
      end
    end
  in mthd Γi acci.

Ltac collect_envs_occs x Δ :=
  let init := constr:(@nil ident) in
  let Γs := eval cbn in (env_spatial Δ) in
  let result_s := collect_env_occs x Γs init in
  let Γp := eval cbn in (env_intuitionistic Δ) in
  collect_env_occs x Γp result_s.

Ltac my_subst x :=
  assert_succeeds (subst x);
  lazymatch goal with
  | |- envs_entails ?Δ ?G =>
    let result := collect_envs_occs x Δ in
    refine (revert_idents_sound result Δ G _); simpl;
    subst x
  end.

(* adapted from stdpp's simplify_eq *)
Tactic Notation "simplify_hyp_eq" :=
  match goal with
  | |- ?Htype  ?G => 
    let H := fresh "H" in
    intro H;
    repeat
    match type of H with
    | _  _ => by case H; try clear H
    | _ = _  False => by case H; try clear H
    | ?x = _ => my_subst x
    | _ = ?x => my_subst x
    | _ = _ => discriminate H
    | _  _ => apply leibniz_equiv in H
    | ?f _ = ?f _ => apply (inj f) in H
    | ?f _ _ = ?f _ _ => apply (inj2 f) in H; destruct H
      (* before [injection] to circumvent bug #2939 in some situations *)
    | ?f _ = ?f _ => progress injection H as H
      (* first hyp will be named [H], subsequent hyps will be given fresh names *)
    | ?f _ _ = ?f _ _ => progress injection H as H
    | ?f _ _ _ = ?f _ _ _ => progress injection H as H
    | ?f _ _ _ _ = ?f _ _ _ _ => progress injection H as H
    | ?f _ _ _ _ _ = ?f _ _ _ _ _ => progress injection H as H
    | ?f _ _ _ _ _ _ = ?f _ _ _ _ _ _ => progress injection H as H
    | ?x = ?x => clear H
    | @existT ?A _ _ _ = existT _ _ =>
       apply (Eqdep_dec.inj_pair2_eq_dec _ (decide_rel (=@{A}))) in H
    end
  end.

442
Ltac simplifySolveSepPureHyp := 
443
  lazymatch goal with
444
445
446
447
448
449
450
  | |- ?φ  ?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 _
451
      | _ => simplify_hyp_eq
452
453
454
      end]
  end.

455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
Ltac introduceHypEmp := 
  notypeclasses refine (tac_introduce_hyp_premise_emp _ _ _ ).

Ltac introduceHypPure := 
  notypeclasses refine (tac_introduce_hyp_premise_pure _ _ _ _ _ _ _ _); 
  [ iSolveTC | iSolveTC | simpl; simplifySolveSepPureHyp ].

Ltac introduceHypSep := 
  notypeclasses refine (tac_introduce_hyp_premise_sep _ _ _ _ _ _ _); [ iSolveTC | ].

Ltac introduceHypExist := 
  notypeclasses refine (tac_introduce_hyp_premise_exist _ _ _ _ _ _); [ iSolveTC | simpl].

Ltac introduceHypOr :=
  notypeclasses refine (tac_introduce_hyp_premise_or _ _ _ _ _ _ _ _ ); [ iSolveTC | simpl | simpl].

471
Ltac introduceHypStep namer_tac :=
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
  lazymatch goal with
  | |- envs_entails ?Δ (IntroduceHyp ?P ?G) =>
    lazymatch P with
    | bi_emp => introduceHypEmp
    | bi_sep _ _ => introduceHypSep
    | bi_exist _ => introduceHypExist
    | bi_or _ _ => introduceHypOr
    | bi_pure ?φ => 
      lazymatch φ with
      | ?φl  ?φr => introduceHypSep
      | ?φl  ?φr => introduceHypOr
      | _ => introduceHypPure
      end
    | _ =>
      first
      [introduceHypEmp
      |introduceHypSep
      |introduceHypExist
      |introduceHypOr
      |notypeclasses refine (tac_introduce_hyp_premise_modal _ _ _ _ _ _ _ _ _ _); 
        [iSolveTC | iSolveTC | simpl; iSolveTC | ]
      (* rules below this do actual introduction of separation logic premises *)
      |introduceHypPure
      |notypeclasses refine (tac_introduce_hyp_merge_consume _ _ _ _ _ _ _ _ _ _); 
        [iSolveTC | register_delete namer_tac; simpl ]
      | let j := namer_tac NameTac.GetName Δ P in first
        [notypeclasses refine (tac_introduce_hyp_merge_persist j _ _ _ _ _ _ _ _ _ _ _ _ _);
          [iSolveTC | iSolveTC | simpl ]
        |notypeclasses refine (tac_introduce_hyp_not_mergable j _ _ _ _ _ _ _);
          [iSolveTC | simpl ] ]
      ]
    end
  end.
505