-
Notifications
You must be signed in to change notification settings - Fork 0
/
JaIrisSoundness.v
3547 lines (3324 loc) · 132 KB
/
JaIrisSoundness.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
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
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
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
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
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
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
Require Import String.
Require Import NPeano.
Require Import PeanoNat.
Require Import Coq.Strings.Ascii.
Require FMapWeakList.
Require Export Coq.Structures.OrderedTypeEx.
Require Import Lists.List.
Import ListNotations.
Require Import JaSyntax.
Require Import JaTypes.
Require Import JaProgram.
Require Import JaEnvs.
Require Import Jafun.
Require Import JaIrisCommon.
Require Import JaIrisPermutation.
Require Import JaEval.
Require Import JaIris.
Require Import JaSubtype.
Require Import Bool.
Require Import Classical_Prop.
Require Import Classical_Pred_Type.
Require Export FMapAVL.
Require Export Coq.Structures.OrderedTypeEx.
Require Import FMapFacts.
Module HeapFacts := JaIrisCommon.HeapFacts.
Module StrMapFacts := JaIrisCommon.StrMapFacts.
Module NatMapFacts := JaIrisCommon.NatMapFacts.
Module JFXIdMapFacts := Facts JFXIdMap.
Definition JFISemanticallyImplies (gamma : JFITypeEnv) (s : JFITerm) (p : JFITerm) (CC : JFProgram) :=
forall env this h,
JFIGammaMatchEnv h gamma env ->
JFIHeapSatisfiesInEnv h s env this CC ->
JFIHeapSatisfiesInEnv h p env this CC.
Definition JFISemanticallyImpliesOuter (gamma : JFITypeEnv) (s : JFIOuterTerm) (p : JFIOuterTerm) (CC : JFProgram) :=
forall env this h,
(JFIGammaMatchEnv h gamma env) ->
(JFIHeapSatisfiesOuterInEnv h s env this CC) ->
JFIHeapSatisfiesOuterInEnv h p env this CC.
Ltac unfoldSubstitutions :=
unfold JFITermSubstituteVals;
unfold JFITermSubstituteVar;
unfold JFITermSubstituteVal;
unfold JFIExprSubstituteVar;
unfold JFIValSubstituteVal;
unfold JFIStringSubstitute;
simpl.
Lemma LocNotNullIff : forall loc,
(exists n, loc = JFLoc n) <-> (loc <> null).
Proof.
intro loc .
split.
+ intros (n & loc_is_n).
rewrite loc_is_n.
unfold not.
discriminate.
+ intros loc_is_not_null.
destruct loc.
++ exfalso.
apply loc_is_not_null.
trivial.
++ exists n.
trivial.
Qed.
(* =============== StrMap Lemmas =============== *)
Lemma StrMap_in_find_iff : forall t m x,
(StrMap.In x m) <-> (exists e : t, StrMap.find x m = Some e).
Proof.
intros t m x.
split.
+ intros x_in_m.
apply StrMapFacts.elements_in_iff in x_in_m.
destruct x_in_m as ( e & e_in_elements ).
apply StrMapFacts.elements_mapsto_iff in e_in_elements.
apply StrMapFacts.find_mapsto_iff in e_in_elements.
exists e.
exact e_in_elements.
+ intros find_gives_some.
apply StrMapFacts.elements_in_iff.
destruct find_gives_some as ( e & find_gives_e).
exists e.
apply StrMapFacts.elements_mapsto_iff.
apply StrMapFacts.find_mapsto_iff.
exact find_gives_e.
Qed.
(* =============== Gamma Match Env Lemmas =============== *)
Lemma ExtendedGammaMatchesExtendedEnv : forall x l type env gamma h,
(JFIGammaMatchEnv h gamma env) ->
(JFILocOfType l h type) ->
(JFIGammaMatchEnv h (JFIGammaAdd x type gamma) ((StrMap.add x l env))).
Proof.
intros x l type env gamma h.
intros gamma_match_env loc_of_type.
unfold JFIGammaAdd.
unfold JFIGammaMatchEnv.
intros var_name.
split.
+ split;
(intros x_in;
apply StrMapFacts.add_in_iff in x_in;
apply StrMapFacts.add_in_iff;
rewrite <- String.eqb_eq in *;
destruct (String.eqb x var_name); auto;
destruct x_in as [ false_eq_true | var_in]; try discriminate false_eq_true;
apply or_intror;
assert (in_iff := (proj1 (gamma_match_env var_name)));
apply in_iff;
assumption).
+ intros var_loc var_type var_is_some_type.
intros var_is_some_loc.
rewrite StrMapFacts.find_mapsto_iff, StrMapFacts.add_o in var_is_some_type, var_is_some_loc.
destruct (StrMapFacts.eq_dec x var_name).
++ injection var_is_some_type as type_eq_var_type.
injection var_is_some_loc as l_eq_var_loc.
rewrite <- type_eq_var_type, <- l_eq_var_loc.
assumption.
++ apply (proj2 (gamma_match_env var_name)); rewrite StrMapFacts.find_mapsto_iff; try assumption.
Qed.
Lemma StrictlyExtendedGammaMatchesExtendedEnv : forall x l type env gamma gamma_x h,
(JFIGammaMatchEnv h gamma env) ->
(JFILocOfType l h type) ->
(JFIGammaAddNew x type gamma = Some gamma_x) ->
(JFIGammaMatchEnv h gamma_x ((StrMap.add x l env))).
Proof.
intros x l type env gamma gamma_x h.
intros gamma_match_env loc_of_type add_new_x.
replace gamma_x with (StrMap.add x type gamma).
+ apply ExtendedGammaMatchesExtendedEnv.
++ exact gamma_match_env.
++ exact loc_of_type.
+ unfold JFIGammaAddNew in add_new_x.
destruct (StrMap.mem (elt:=JFClassName) x gamma).
++ discriminate add_new_x.
++ injection add_new_x. trivial.
Qed.
(* Framework for heap satisfying equivalence lemmas *)
Definition HeapEnvEquivalent h h' env env' this this' t CC :=
JFIHeapSatisfiesInEnv h t env this CC <-> JFIHeapSatisfiesInEnv h' t env' this' CC.
Definition HeapEnvEquivalentOuter h h' env env' this this' t CC :=
JFIHeapSatisfiesOuterInEnv h t env this CC <-> JFIHeapSatisfiesOuterInEnv h' t env' this' CC.
Lemma TrueEquivalence : forall h h' env env' this this' CC,
HeapEnvEquivalent h h' env env' this this' JFITrue CC.
Proof.
intros.
easy.
Qed.
Hint Resolve TrueEquivalence : core.
Lemma FalseEquivalence : forall h h' env env' this this' CC,
HeapEnvEquivalent h h' env env' this this' JFIFalse CC.
Proof.
intros.
easy.
Qed.
Hint Resolve FalseEquivalence : core.
Lemma AndPreservesEquivalence : forall h h' env env' this this' t1 t2 CC,
HeapEnvEquivalent h h' env env' this this' t1 CC ->
HeapEnvEquivalent h h' env env' this this' t2 CC ->
HeapEnvEquivalent h h' env env' this this' (JFIAnd t1 t2) CC.
Proof.
intros h h' env env' this this' t1 t2 CC.
intros t1_equivalence t2_equivalence.
unfold HeapEnvEquivalent in *.
split; intro; split; destruct H.
+ now apply t1_equivalence.
+ now apply t2_equivalence.
+ now apply t1_equivalence.
+ now apply t2_equivalence.
Qed.
Hint Resolve AndPreservesEquivalence : core.
Lemma OrPreservesEquivalence : forall h h' env env' this this' t1 t2 CC,
HeapEnvEquivalent h h' env env' this this' t1 CC ->
HeapEnvEquivalent h h' env env' this this' t2 CC ->
HeapEnvEquivalent h h' env env' this this' (JFIOr t1 t2) CC.
Proof.
intros h h' env env' this this' t1 t2 CC.
intros t1_equivalence t2_equivalence.
unfold HeapEnvEquivalent in *.
split; intro; simpl; destruct H.
+ apply or_introl; now apply t1_equivalence.
+ apply or_intror; now apply t2_equivalence.
+ apply or_introl; now apply t1_equivalence.
+ apply or_intror; now apply t2_equivalence.
Qed.
Hint Resolve OrPreservesEquivalence : core.
Lemma ImpliesPreservesEquivalence : forall h h' env env' this this' t1 t2 CC,
HeapEnvEquivalent h h' env env' this this' t1 CC ->
HeapEnvEquivalent h h' env env' this this' t2 CC ->
HeapEnvEquivalent h h' env env' this this' (JFIImplies t1 t2) CC.
Proof.
intros h h' env env' this this' t1 t2 CC.
intros t1_equivalence t2_equivalence.
unfold HeapEnvEquivalent in *.
split; intro; simpl; destruct H.
+ apply or_introl. intro. apply H. now apply t1_equivalence.
+ apply or_intror; now apply t2_equivalence.
+ apply or_introl. intro. apply H. now apply t1_equivalence.
+ apply or_intror; now apply t2_equivalence.
Qed.
Hint Resolve ImpliesPreservesEquivalence : core.
(* =============== Env Lemmas =============== *)
Lemma DifferentVarIsFresh : forall v w,
(w <> JFIVar v) -> JFIVarFreshInVal v w.
Proof.
intros v w.
intros w_is_not_v.
unfold JFIVarFreshInVal.
destruct w; try trivial.
unfold not.
intros v_eq_x.
apply f_equal with (f := fun x => JFIVar x) in v_eq_x.
symmetry in v_eq_x.
exact (w_is_not_v v_eq_x).
Qed.
Lemma AddingFreshVarPreservesValToLoc : forall x l val env this,
(JFIVarFreshInVal x val) ->
JFIValToLoc val env this = JFIValToLoc val (StrMap.add x l env) this.
Proof.
intros x l val env this.
intros x_fresh.
unfold JFIValToLoc.
destruct val as [ | | loc]; trivial.
+ symmetry.
apply StrMapFacts.add_neq_o.
unfold JFIVarFreshInVal in x_fresh.
exact x_fresh.
Qed.
Lemma AddingFreshVarPreservesHeapSatisfyingEq : forall val1 val2 x l env this h CC,
(JFIVarFreshInTerm x (JFIEq val1 val2)) ->
((JFIHeapSatisfiesInEnv h (JFIEq val1 val2) env this CC) <->
JFIHeapSatisfiesInEnv h (JFIEq val1 val2) (StrMap.add x l env) this CC).
Proof.
intros val1 val2 x l env this h CC.
intros x_fresh.
split.
+ intros h_satisfies_eq.
simpl.
simpl in h_satisfies_eq.
replace (JFIValToLoc val1 (StrMap.add x l env) this) with (JFIValToLoc val1 env this).
replace (JFIValToLoc val2 (StrMap.add x l env) this) with (JFIValToLoc val2 env this).
++ exact h_satisfies_eq.
++ apply AddingFreshVarPreservesValToLoc.
apply x_fresh.
++ apply AddingFreshVarPreservesValToLoc.
apply x_fresh.
+ intros h_satisfies_eq.
simpl.
simpl in h_satisfies_eq.
now rewrite <-2!AddingFreshVarPreservesValToLoc with (x := x) (l := l) in h_satisfies_eq; try apply x_fresh.
Qed.
Lemma AddingFreshVarPreservesHeapSatisfyingFieldEq : forall obj field val x l env this h CC,
(JFIVarFreshInTerm x (JFIFieldEq obj field val)) ->
((JFIHeapSatisfiesInEnv h (JFIFieldEq obj field val) env this CC) <->
JFIHeapSatisfiesInEnv h (JFIFieldEq obj field val) (StrMap.add x l env) this CC).
Proof.
intros obj field val x l env this h CC.
intros (x_fresh_in_obj & x_fresh_in_val).
split.
+ intros h_satisfies_eq.
simpl.
simpl in h_satisfies_eq.
now rewrite <-2!AddingFreshVarPreservesValToLoc.
+ intros h_satisfies_eq.
simpl.
simpl in h_satisfies_eq.
now rewrite <-2!AddingFreshVarPreservesValToLoc in h_satisfies_eq.
Qed.
Definition EnvEq (env1 : JFITermEnv) (env2 : JFITermEnv) :=
forall x, StrMap.find x env1 = StrMap.find x env2.
Definition EqualEnvsEquivalentInTermForHeap (t : JFITerm) CC :=
forall h env1 env2 this,
(EnvEq env1 env2) -> ((JFIHeapSatisfiesInEnv h t env1 this CC) <-> (JFIHeapSatisfiesInEnv h t env2 this CC)).
Definition EqualEnvsEquivalentInOuterTermForHeap (t : JFIOuterTerm) CC :=
forall h env1 env2 this,
(EnvEq env1 env2) -> ((JFIHeapSatisfiesOuterInEnv h t env1 this CC) <-> (JFIHeapSatisfiesOuterInEnv h t env2 this CC)).
Lemma EnvEqSymmetry : forall env1 env2,
(EnvEq env1 env2) -> (EnvEq env2 env1).
Proof.
intros env1 env2.
intros env1_eq_env2.
unfold EnvEq.
intros x.
symmetry.
apply env1_eq_env2.
Qed.
Lemma AddPreservesEnvEq : forall x l env1 env2,
(EnvEq env1 env2) -> (EnvEq (StrMap.add x l env1) (StrMap.add x l env2)).
Proof.
intros x l env1 env2.
intros env1_eq_env2.
intros y.
rewrite 2!StrMapFacts.add_o.
destruct (StrMapFacts.eq_dec x y); trivial.
Qed.
Lemma RemovePreservesEnvEq : forall x env1 env2,
(EnvEq env1 env2) -> (EnvEq (StrMap.remove x env1) (StrMap.remove x env2)).
Proof.
intros x env1 env2.
intros env_eq.
intros y.
rewrite 2!StrMapFacts.remove_o.
destruct (StrMapFacts.eq_dec x y); trivial.
Qed.
Lemma AddOrderChangePreservesEnvEq : forall x1 l1 x2 l2 env,
(x2 <> x1) ->
EnvEq (StrMap.add x1 l1 (StrMap.add x2 l2 env)) (StrMap.add x2 l2 (StrMap.add x1 l1 env)).
Proof.
intros x1 l1 x2 l2 env.
intros x2_neq_x1.
unfold EnvEq.
intros x.
destruct (Classical_Prop.classic (x1 = x)) as [x1_eq_x | x1_neq_x].
+ rewrite StrMapFacts.add_eq_o.
symmetry.
rewrite StrMapFacts.add_neq_o.
rewrite StrMapFacts.add_eq_o.
++ trivial.
++ exact x1_eq_x.
++ replace x with x1.
exact x2_neq_x1.
++ exact x1_eq_x.
+ destruct (Classical_Prop.classic (x2 = x)) as [x2_eq_x | x2_neq_x].
++ rewrite StrMapFacts.add_neq_o.
rewrite StrMapFacts.add_eq_o.
symmetry.
rewrite StrMapFacts.add_eq_o.
+++ trivial.
+++ exact x2_eq_x.
+++ exact x2_eq_x.
+++ exact x1_neq_x.
++ rewrite StrMapFacts.add_neq_o.
rewrite StrMapFacts.add_neq_o.
symmetry.
rewrite StrMapFacts.add_neq_o.
rewrite StrMapFacts.add_neq_o.
+++ trivial.
+++ exact x1_neq_x.
+++ exact x2_neq_x.
+++ exact x2_neq_x.
+++ exact x1_neq_x.
Qed.
Lemma EnvEqGivesValSubstEnvEq : forall env1 env2 this v,
(EnvEq env1 env2) ->
(JFIValSubstituteEnv env1 this v = JFIValSubstituteEnv env2 this v).
Proof.
intros env1 env2 this v.
intros env_eq.
destruct v as [ | x]; try destruct x.
+ rewrite 2!ValEnvSubstitutionPreservesVLoc.
trivial.
+ destruct (Classical_Prop.classic (StrMap.In x env1)) as [x_in_env1 | x_not_in_env1].
++ apply StrMap_in_find_iff in x_in_env1 as (l & x_l_in_env1).
assert (x_l_in_env2 := env_eq x).
rewrite x_l_in_env1 in x_l_in_env2.
symmetry in x_l_in_env2.
rewrite 2!ValEnvSubstitutionReplacesVarInEnv with (l := l); trivial.
++ rewrite 2!(ValEnvSubstitutionPreservesVarNotInEnv); try assumption; trivial.
intros x_in_env2.
apply StrMapFacts.not_find_mapsto_iff in x_not_in_env1 as x_is_none.
apply StrMap_in_find_iff in x_in_env2 as (l & x_is_l).
rewrite <- (env_eq x) in x_is_l.
rewrite x_is_none in x_is_l.
discriminate x_is_l.
+ now rewrite 2!ValEnvSubstitutionSubstitutesThis.
Qed.
Lemma EnvEqGivesMapValSubstEq : forall env1 env2 this vs,
(EnvEq env1 env2) ->
(map (JFIValSubstituteEnv env1 this) vs = map (JFIValSubstituteEnv env2 this) vs).
Proof.
intros env1 env2 this vs.
intros env_eq.
induction vs; try trivial.
rewrite 2!List.map_cons.
rewrite IHvs.
rewrite EnvEqGivesValSubstEnvEq with (env2 := env2); trivial.
Qed.
Lemma EnvEqGivesExprSubstEnvEq : forall e env1 env2 this,
(EnvEq env1 env2) ->
(JFIExprSubstituteEnv env1 this e = JFIExprSubstituteEnv env2 this e).
Proof.
intros e.
induction e; intros env1 env2 this env_eq; simpl;
try rewrite ?(EnvEqGivesValSubstEnvEq env1 env2);
try rewrite (EnvEqGivesMapValSubstEq env1 env2);
try assumption;
trivial.
+ rewrite (IHe1 env1 env2); try assumption.
rewrite (IHe2 (StrMap.remove x env1) (StrMap.remove x env2)); trivial.
apply RemovePreservesEnvEq; try assumption.
+ rewrite <- (IHe1 env1 env2), <- (IHe2 env1 env2); try assumption.
trivial.
+ destruct vx.
rewrite (EnvEqGivesValSubstEnvEq env1 env2); try assumption.
trivial.
+ destruct vx.
rewrite (EnvEqGivesValSubstEnvEq env1 env2); try assumption.
trivial.
+ rewrite (IHe1 env1 env2); try assumption.
rewrite (IHe2 (StrMap.remove x env1) (StrMap.remove x env2)); trivial.
apply RemovePreservesEnvEq; try assumption.
Qed.
Lemma EnvEqGivesEvalEq : forall confs h e hn ex res env1 env2 this CC,
(EnvEq env1 env2) ->
(JFIEvalInEnv h e confs hn ex res env1 this CC) ->
(JFIEvalInEnv h e confs hn ex res env2 this CC).
Proof.
intros confs.
induction confs; intros h e hn ex res env1 env2 this CC env_eq.
+ unfold JFIEvalInEnv, JFIEval, JFIPartialEval.
intros (h_eq & f_eq).
rewrite h_eq.
split; trivial.
rewrite <- f_eq.
symmetry.
rewrite EnvEqGivesExprSubstEnvEq with (env2 := env2); trivial.
+ intros e_eval.
unfold JFIEvalInEnv, JFIEval, JFIPartialEval in *.
destruct a.
fold JFIPartialEval in *.
destruct e_eval as (h_eq & f_eq & red_is_some).
rewrite h_eq, <-f_eq in *.
apply EnvEqSymmetry in env_eq.
split; try split; try rewrite EnvEqGivesExprSubstEnvEq with (env2 := env1); try trivial.
Qed.
Lemma EnvEqGivesExistsImplication : forall h type x t env1 env2 this CC,
(EnvEq env1 env2) ->
(EqualEnvsEquivalentInOuterTermForHeap t CC) ->
(JFIHeapSatisfiesOuterInEnv h (JFIExists type x t) env1 this CC) ->
JFIHeapSatisfiesOuterInEnv h (JFIExists type x t) env2 this CC.
Proof.
intros h type x t env1 env2 this CC.
intros env1_eq_env2 t_equivalence h_satisfies_exists_t.
simpl.
simpl in h_satisfies_exists_t.
destruct h_satisfies_exists_t as ( loc & (loc_of_type & h_satisfies_t)).
unfold EqualEnvsEquivalentInTermForHeap in t_equivalence.
exists loc.
split.
+ exact loc_of_type.
+ apply (t_equivalence h (StrMap.add x loc env1) (StrMap.add x loc env2)).
++ apply AddPreservesEnvEq.
exact env1_eq_env2.
++ exact h_satisfies_t.
Qed.
Lemma EnvEqGivesHoareImplication : forall h t1 e ex v t2 env1 env2 this CC,
(EnvEq env1 env2) ->
(EqualEnvsEquivalentInTermForHeap t1 CC) ->
(EqualEnvsEquivalentInTermForHeap t2 CC) ->
(JFIHeapSatisfiesInEnv h (JFIHoare t1 e ex v t2) env1 this CC) ->
JFIHeapSatisfiesInEnv h (JFIHoare t1 e ex v t2) env2 this CC.
Proof.
intros h t1 e ex v t2 env1 env2 this CC.
intros env_eq t1_equivalence t2_equivalence.
simpl.
intros h_satisfies_hoare h_satisfies_t1.
assert (h_satisfies_t1_in_env1 := proj2 (t1_equivalence h env1 env2 this env_eq) h_satisfies_t1).
destruct (h_satisfies_hoare h_satisfies_t1_in_env1) as
(confs & hn & res_ex & res & eval & ex_eq & hn_satisfies_t2).
exists confs, hn, res_ex, res.
split; try split; try easy.
+ now apply EnvEqGivesEvalEq with (env1 := env1).
+ apply (t2_equivalence hn (StrMap.add v res env1) (StrMap.add v res env2)); try assumption.
now apply AddPreservesEnvEq.
Qed.
Lemma EnvEqGivesEqualValToLoc : forall val env1 env2 this,
(EnvEq env1 env2) ->
(JFIValToLoc val env1 this) = (JFIValToLoc val env2 this).
Proof.
unfold JFIValToLoc.
now destruct val.
Qed.
Lemma EnvEqGivesEqImplication : forall h env1 env2 this val1 val2 CC,
(EnvEq env1 env2) ->
(JFIHeapSatisfiesInEnv h (JFIEq val1 val2) env1 this CC) ->
JFIHeapSatisfiesInEnv h (JFIEq val1 val2) env2 this CC.
Proof.
intros h env1 env2 this val1 val2 CC.
intros env_eq.
apply EnvEqSymmetry in env_eq.
simpl.
now rewrite EnvEqGivesEqualValToLoc with (val := val1) (env2 := env2),
EnvEqGivesEqualValToLoc with (val := val2) (env2 := env2).
Qed.
Lemma EnvEqGivesFieldEqImplication : forall h env1 env2 this obj field val CC,
(EnvEq env1 env2) ->
(JFIHeapSatisfiesInEnv h (JFIFieldEq obj field val) env1 this CC) ->
JFIHeapSatisfiesInEnv h (JFIFieldEq obj field val) env2 this CC.
Proof.
intros h env1 env2 this obj field val CC.
intros env_eq.
apply EnvEqSymmetry in env_eq.
simpl.
now rewrite EnvEqGivesEqualValToLoc with (val := obj) (env2 := env2),
EnvEqGivesEqualValToLoc with (val := val) (env2 := env2).
Qed.
Lemma EnvEqGivesSepImplication : forall h t1 t2 env1 env2 this CC,
(EnvEq env1 env2) ->
(EqualEnvsEquivalentInTermForHeap t1 CC) ->
(EqualEnvsEquivalentInTermForHeap t2 CC) ->
(JFIHeapSatisfiesInEnv h (JFISep t1 t2) env1 this CC) ->
JFIHeapSatisfiesInEnv h (JFISep t1 t2) env2 this CC.
Proof.
intros h t1 t2 env1 env2 this CC.
intros env_eq t1_equivalence t2_equivalence.
simpl.
intros (h1 & h2 & hs_consistent & disjoint_unions & h1_satisfies_t1 & h2_satisfies_t2).
exists h1, h2.
split; [ | split; [ | split]]; try easy.
now apply (t1_equivalence h1 env1 env2).
now apply (t2_equivalence h2 env1 env2).
Qed.
Lemma EnvEqGivesWandImplication : forall h t1 t2 env1 env2 this CC,
(EnvEq env1 env2) ->
(EqualEnvsEquivalentInTermForHeap t1 CC) ->
(EqualEnvsEquivalentInTermForHeap t2 CC) ->
(JFIHeapSatisfiesInEnv h (JFIWand t1 t2) env1 this CC) ->
JFIHeapSatisfiesInEnv h (JFIWand t1 t2) env2 this CC.
Proof.
intros h t1 t2 env1 env2 this CC.
intros env_eq t1_equivalence t2_equivalence.
simpl.
intros wand h' h'_consistent disjoint_h_h' h'_satisfies_t1.
unfold EqualEnvsEquivalentInTermForHeap in t1_equivalence.
apply (t1_equivalence h' env1 env2 this env_eq) in h'_satisfies_t1.
destruct (wand h' h'_consistent disjoint_h_h' h'_satisfies_t1) as (h_h' & union_h_h' & h_h'_satisfies_t2).
apply (t2_equivalence h_h' env1 env2 this env_eq) in h_h'_satisfies_t2.
now exists h_h'.
Qed.
Lemma EqualEnvsAreEquivalent : forall t CC h env1 env2 this,
(EnvEq env1 env2) -> HeapEnvEquivalent h h env1 env2 this this t CC.
Proof.
intros t CC.
induction t; intros h env1 env2 this env1_eq_env2; auto.
(* JFIHoare *)
+ split; apply EnvEqGivesHoareImplication; try assumption.
exact (EnvEqSymmetry env1 env2 env1_eq_env2).
(* JFIEq *)
+ split; apply EnvEqGivesEqImplication; try assumption.
exact (EnvEqSymmetry env1 env2 env1_eq_env2).
(* JFIFieldEq *)
+ split; apply EnvEqGivesFieldEqImplication; try assumption.
exact (EnvEqSymmetry env1 env2 env1_eq_env2).
(* JFISep*)
+ split; apply EnvEqGivesSepImplication; try assumption.
exact (EnvEqSymmetry env1 env2 env1_eq_env2).
(* JFIWand *)
+ split; apply EnvEqGivesWandImplication; try assumption.
exact (EnvEqSymmetry env1 env2 env1_eq_env2).
Qed.
Lemma EnvOrderChangePreservesHeapSatisfying : forall h t x1 l1 x2 l2 env this CC,
(x1 <> x2) ->
(JFIHeapSatisfiesInEnv h t (StrMap.add x1 l1 (StrMap.add x2 l2 env)) this CC) <->
(JFIHeapSatisfiesInEnv h t (StrMap.add x2 l2 (StrMap.add x1 l1 env)) this CC).
Proof.
intros h t x1 l1 x2 l2 env this CC.
intros x1_neq_x2.
apply EqualEnvsAreEquivalent.
apply AddOrderChangePreservesEnvEq.
apply neq_symmetry.
exact x1_neq_x2.
Qed.
Lemma FreshEnvOrderChangePreservesHeapSatisfying : forall h t x1 l1 x2 l2 env this CC,
(JFIVarFreshInTerm x1 t) ->
(JFIHeapSatisfiesInEnv h t (StrMap.add x1 l1 (StrMap.add x2 l2 env)) this CC) <->
(JFIHeapSatisfiesInEnv h t (StrMap.add x2 l2 (StrMap.add x1 l1 env)) this CC).
Proof.
Admitted.
Definition FreshVarPreservesTermSatysfying t CC :=
forall h x l env this,
JFIVarFreshInTerm x t ->
JFIHeapSatisfiesInEnv h t env this CC <->
JFIHeapSatisfiesInEnv h t (StrMap.add x l env) this CC.
Lemma FreshVarPreservesEval : forall h e confs hn ex res x l env this CC,
JFIVarFreshInExpr x e ->
JFIEvalInEnv h e confs hn ex res env this CC <->
JFIEvalInEnv h e confs hn ex res (StrMap.add x l env) this CC.
Proof.
Admitted.
Lemma FreshVarPreservesHoareSatystying : forall t1 e ex v t2 CC,
FreshVarPreservesTermSatysfying t1 CC ->
FreshVarPreservesTermSatysfying t2 CC ->
FreshVarPreservesTermSatysfying (JFIHoare t1 e ex v t2) CC.
Proof.
intros t1 e ex v t2 CC.
intros IH_t1 IH_t2.
unfold FreshVarPreservesTermSatysfying.
intros h x l env this x_fresh_in_hoare.
simpl in x_fresh_in_hoare.
destruct (String.eqb v x); destruct x_fresh_in_hoare.
destruct H0 as (x_fresh_in_t2 & x_fresh_in_e).
assert (t1_preserves := IH_t1 h x l env this H).
simpl.
split.
+ intros h_satisfies_hoare_in_env.
intros h_satisfies_t1.
apply t1_preserves in h_satisfies_t1.
destruct (h_satisfies_hoare_in_env h_satisfies_t1)
as (confs & hn & res_ex & res & eval & ex_eq & hn_satisfies_t2).
exists confs, hn, res_ex, res.
assert (t2_preserves := IH_t2 hn x l (StrMap.add v res env) this x_fresh_in_t2).
split; try split; try easy.
++ now apply FreshVarPreservesEval.
++ apply FreshEnvOrderChangePreservesHeapSatisfying with (x1 := x); try assumption.
now apply t2_preserves.
+ intros h_satisfies_hoare_in_env.
intros h_satisfies_t1.
apply t1_preserves in h_satisfies_t1.
destruct (h_satisfies_hoare_in_env h_satisfies_t1)
as (confs & hn & res_ex & res & eval & ex_eq & hn_satisfies_t2).
exists confs, hn, res_ex, res.
assert (t2_preserves := IH_t2 hn x l (StrMap.add v res env) this x_fresh_in_t2).
split; try split; try easy.
++ now apply FreshVarPreservesEval in eval.
++ apply t2_preserves.
now apply FreshEnvOrderChangePreservesHeapSatisfying.
Qed.
Lemma FreshVarPreservesSepSatystying : forall t1 t2 CC,
FreshVarPreservesTermSatysfying t1 CC ->
FreshVarPreservesTermSatysfying t2 CC ->
FreshVarPreservesTermSatysfying (JFISep t1 t2) CC.
Proof.
intros t1 t2 CC.
intros t1_preserves t2_preserves.
unfold FreshVarPreservesTermSatysfying.
intros h x l env this (x_fresh_in_t1 & x_fresh_in_t2).
split.
+ simpl.
intros (h1 & h2 & hs_consistent & disjoint_union & h1_satisfies_t1 & h2_satisfies_t2).
assert (h1_satisfies_t1_in_env_x := proj1 (t1_preserves h1 x l env this x_fresh_in_t1) h1_satisfies_t1).
assert (h2_satisfies_t2_in_env_x := proj1 (t2_preserves h2 x l env this x_fresh_in_t2) h2_satisfies_t2).
now exists h1, h2.
+ simpl.
intros (h1 & h2 & hs_consistent & disjoint_union & h1_satisfies_t1 & h2_satisfies_t2).
assert (h1_satisfies_t1_in_env := proj2 (t1_preserves h1 x l env this x_fresh_in_t1) h1_satisfies_t1).
assert (h2_satisfies_t2_in_env := proj2 (t2_preserves h2 x l env this x_fresh_in_t2) h2_satisfies_t2).
now exists h1, h2.
Qed.
Lemma FreshVarPreservesWandSatystying : forall t1 t2 CC,
FreshVarPreservesTermSatysfying t1 CC ->
FreshVarPreservesTermSatysfying t2 CC ->
FreshVarPreservesTermSatysfying (JFIWand t1 t2) CC.
Proof.
intros t1 t2 CC.
intros t1_preserves t2_preserves.
unfold FreshVarPreservesTermSatysfying.
intros h x l env this (x_fresh_in_t1 & x_fresh_in_t2).
split.
+ intros h_satisfies_wand h' h'_consistent h_h'_disjoint h'_satisfies_t1.
apply t1_preserves in h'_satisfies_t1; try assumption.
destruct (h_satisfies_wand h' h'_consistent h_h'_disjoint h'_satisfies_t1) as (h_h' & h_h'_union & h_h'_satisfies_t2).
exists h_h'.
unfold FreshVarPreservesTermSatysfying in t2_preserves.
now apply t2_preserves with (x := x) (l := l) in h_h'_satisfies_t2; try assumption.
+ intros h_satisfies_wand h' h'_consistent h_h'_disjoint h'_satisfies_t1.
apply t1_preserves with (x := x) (l := l) in h'_satisfies_t1; try assumption.
destruct (h_satisfies_wand h' h'_consistent h_h'_disjoint h'_satisfies_t1) as (h_h' & h_h'_union & h_h'_satisfies_t2).
exists h_h'.
unfold FreshVarPreservesTermSatysfying in t2_preserves.
now apply t2_preserves with (x := x) (l := l) in h_h'_satisfies_t2; try assumption.
Qed.
Lemma AddingFreshVarPreservesHeapSatisfying : forall q CC h x l env this,
JFIVarFreshInTerm x q ->
HeapEnvEquivalent h h env (StrMap.add x l env) this this q CC.
Proof.
intros t CC.
induction t; intros h x l env this x_fresh; try destruct x_fresh; auto.
(* JFIHoare *)
+ apply FreshVarPreservesHoareSatystying; assumption.
(* JFIEq *)
+ split;
now apply AddingFreshVarPreservesHeapSatisfyingEq with (x := x) (l := l).
(* JFIFieldEq *)
+ split;
apply AddingFreshVarPreservesHeapSatisfyingFieldEq with (x := x) (l := l);
exact (conj H H0).
(* JFISep*)
+ now apply FreshVarPreservesSepSatystying.
(* JFIWand *)
+ now apply FreshVarPreservesWandSatystying.
Qed.
Lemma AddingFreshVarPreservesHeapSatisfyingOuter : forall q CC h x l env this,
JFIVarFreshInOuterTerm x q ->
HeapEnvEquivalentOuter h h env (StrMap.add x l env) this this q CC.
Proof.
Admitted.
Lemma HeapSatisfiesSubstIffVarMovedToEnv : forall h x v l p env this CC,
(StrMap.find v env = Some l) ->
(JFIHeapSatisfiesOuterInEnv h (JFIOuterTermSubstituteVal x (JFIVar v) p) env this CC <->
JFIHeapSatisfiesOuterInEnv h p (StrMap.add x l env) this CC).
Proof.
Admitted.
Lemma HeapSatisfiesSubstIffThisMovedToEnv : forall h p x env this CC,
JFIHeapSatisfiesOuterInEnv h (JFIOuterTermSubstituteVal x JFIThis p) env this CC <->
JFIHeapSatisfiesOuterInEnv h p (StrMap.add x (JFLoc this) env) this CC.
Proof.
Admitted.
(* =============== Equality Lemmas =============== *)
Lemma EqSymmetry : forall h v1 v2 env this CC,
(JFIHeapSatisfiesInEnv h (JFIEq v1 v2) env this CC) ->
JFIHeapSatisfiesInEnv h (JFIEq v2 v1) env this CC.
Proof.
intros h v1 v2 env this CC.
intros v1_eq_v2.
unfold JFIHeapSatisfiesInEnv.
unfold JFIHeapSatisfiesInEnv in v1_eq_v2.
now destruct (JFIValToLoc v1 env), (JFIValToLoc v2 env).
Qed.
(* =============== Soundness of basic logical rules =============== *)
Lemma AsmRuleSoundness : forall gamma p CC,
JFISemanticallyImplies gamma p p CC.
Proof.
intros gamma p CC.
intros env this h gamma_match_env h_satisfies_p.
exact h_satisfies_p.
Qed.
Lemma TransRuleSoundness : forall gamma p q r CC,
(JFISemanticallyImplies gamma p q CC) ->
(JFISemanticallyImplies gamma q r CC) ->
JFISemanticallyImplies gamma p r CC.
Proof.
intros gamma p q r CC.
intros p_implies_q.
intros q_implies_r.
intros env this h gamma_match_env h_satisfies_p.
unfold JFISemanticallyImplies in p_implies_q.
apply (q_implies_r env this h gamma_match_env).
apply (p_implies_q env this h gamma_match_env).
exact h_satisfies_p.
Qed.
Lemma ValIsLoc : forall v h gamma env this,
FreeVarsInValAreInGamma v gamma ->
JFIGammaMatchEnv h gamma env ->
exists l, JFIValToLoc v env this = Some l.
Proof.
intros v h gamma env this.
intros free_in_v gamma_match_env.
destruct v.
+ now exists null.
+ now exists (JFLoc this).
+ unfold FreeVarsInValAreInGamma in free_in_v.
assert (var_in_gamma := free_in_v var).
apply (gamma_match_env var) in var_in_gamma as var_in_env; try easy.
apply StrMapFacts.elements_in_iff in var_in_env as (l & var_l); try easy.
exists l.
now apply StrMapFacts.elements_mapsto_iff, StrMapFacts.find_mapsto_iff in var_l.
Qed.
Lemma EqReflRuleSoundness : forall gamma p v CC,
FreeVarsInValAreInGamma v gamma ->
JFISemanticallyImplies gamma p (JFIEq v v) CC.
Proof.
intros gamma p v CC.
intros free_vars_in_v env this h gamma_match_env h_satisfies_p.
unfold JFIHeapSatisfiesInEnv.
destruct (ValIsLoc v h gamma env this) as (l & v_is_l); try easy.
now rewrite v_is_l.
Qed.
Lemma EqSymRuleSoundness : forall gamma p v1 v2 CC,
JFISemanticallyImplies gamma p (JFIEq v1 v2) CC ->
JFISemanticallyImplies gamma p (JFIEq v2 v1) CC.
Proof.
intros gamma p v1 v2 CC.
intros v1_eq_v2.
intros env this h gamma_match_env h_satisfies_p.
apply EqSymmetry.
now apply (v1_eq_v2 env this h).
Qed.
Lemma FalseElimRuleSoundness : forall gamma p q CC,
(JFISemanticallyImplies gamma p JFIFalse CC) ->
JFISemanticallyImplies gamma p q CC.
Proof.
intros gamma p q CC.
intros p_implies_false.
intros env this h gamma_match_env h_satisfies_p.
set (h_satisfies_false := p_implies_false env this h gamma_match_env h_satisfies_p).
simpl in h_satisfies_false.
destruct h_satisfies_false.
Qed.
Lemma TrueIntroRuleSoundness : forall gamma p CC,
JFISemanticallyImplies gamma p JFITrue CC.
Proof.
intros gamma p CC.
intros env this h gamma_match_env h_satisfies_p.
unfold JFIHeapSatisfiesInEnv.
trivial.
Qed.
Lemma AndIntroRuleSoundness : forall gamma p q r CC,
(JFISemanticallyImplies gamma r p CC) ->
(JFISemanticallyImplies gamma r q CC) ->
JFISemanticallyImplies gamma r (JFIAnd p q) CC.
Proof.
intros gamma p q r CC.
intros r_implies_p r_implies_q.
intros env this h gamma_match_env h_satisfies_r.
simpl.
split.
now apply r_implies_p.
now apply r_implies_q.
Qed.
Lemma AndElimRuleSoundness : forall gamma p q r CC,
(JFISemanticallyImplies gamma r (JFIAnd p q) CC) ->
JFISemanticallyImplies gamma r p CC /\ JFISemanticallyImplies gamma r q CC.
Proof.
intros gamma p q r CC.
intros r_implies_p_and_q.
split;
intros env this h gamma_match_env h_satisfies_r;
now apply r_implies_p_and_q.
Qed.
Lemma OrIntroRuleSoundness : forall gamma p q r CC,
(JFISemanticallyImplies gamma r p CC \/ JFISemanticallyImplies gamma r q CC) ->
JFISemanticallyImplies gamma r (JFIOr p q) CC.
Proof.
intros gamma p q r CC.
intros [r_implies_p | r_implies_q]; intros env this h gamma_match_env h_satisfies_r; simpl.
now apply or_introl, r_implies_p.
now apply or_intror, r_implies_q.
Qed.
Lemma OrElimRuleSoundness : forall gamma p q r s CC,
(JFISemanticallyImplies gamma s (JFIOr p q) CC) ->
(JFISemanticallyImplies gamma (JFIAnd s p) r CC) ->
(JFISemanticallyImplies gamma (JFIAnd s q) r CC) ->
JFISemanticallyImplies gamma s r CC.
Proof.
intros gamma p q r s CC.
intros s_implies_p_or_q s_and_p_implies_r s_and_q_implies_r.
intros env this h gamma_match_env h_satisfies_s.
set (p_or_q := s_implies_p_or_q env this h gamma_match_env h_satisfies_s).
destruct p_or_q as [h_satisfies_p | h_satisfies_q].
+ now apply (s_and_p_implies_r env this h gamma_match_env).
+ now apply (s_and_q_implies_r env this h gamma_match_env).
Qed.
Lemma ImpliesIntroRuleSoundness : forall gamma p q r CC,
(JFISemanticallyImplies gamma (JFIAnd r p) q CC) ->
JFISemanticallyImplies gamma r (JFIImplies p q) CC.
Proof.
intros gamma p q r CC.
intros r_and_p_implies_q.
intros env this h gamma_match_env h_satisfies_r.
simpl.
simpl in r_and_p_implies_q.
apply Classical_Prop.imply_to_or.
intros h_satisfies_p.
now apply r_and_p_implies_q.
Qed.
Lemma ImpliesElimRuleSoundness : forall gamma p q r CC,
(JFISemanticallyImplies gamma r (JFIImplies p q) CC) ->
(JFISemanticallyImplies gamma r p CC) ->
JFISemanticallyImplies gamma r q CC.
Proof.
intros gamma p q r CC.
intros r_implies_p_implies_q r_implies_p.
intros env this h gamma_match_env h_satisfies_r.
apply (Classical_Prop.or_to_imply (JFIHeapSatisfiesInEnv h p env this CC)).
now apply r_implies_p_implies_q.
now apply r_implies_p.
Qed.
(* =============h gamma_match_env===============*)
Lemma EqualHeapsAreEquivalent : forall t CC h1 h2 env this,
(HeapEq h1 h2) ->
((JFIHeapSatisfiesInEnv h1 t env this CC) <-> (JFIHeapSatisfiesInEnv h2 t env this CC)).
Proof.
Admitted.
Lemma InSuperheap : forall h1 h2 l,
JFISubheap h1 h2 -> Heap.In l h1 -> Heap.In l h2.
Proof.
intros h1 h2 l.
intros subheap_h1_h2 l_in_h1.
unfold JFISubheap in subheap_h1_h2.
apply HeapFacts.elements_in_iff in l_in_h1.
apply HeapFacts.elements_in_iff.
destruct l_in_h1 as (o & l_o_h1).
exists o.
apply HeapFacts.elements_mapsto_iff in l_o_h1.
apply HeapFacts.elements_mapsto_iff.
apply (subheap_h1_h2 l o l_o_h1).
Qed.
Lemma SubheapTransitive : forall h1 h2 h3,
(JFISubheap h1 h2) -> (JFISubheap h2 h3) -> (JFISubheap h1 h3).
Proof.
intros h1 h2 h3.
intros subheap_h1_h2 subheap_h2_h3.
intros l o l_o_h1.
apply (subheap_h2_h3 l o).
now apply (subheap_h1_h2 l o).
Qed.
Lemma UnionSubheap : forall h1 h2 h12 h,
(JFIHeapsUnion h1 h2 h12) ->
(JFISubheap h12 h) <-> (JFISubheap h1 h /\ JFISubheap h2 h).
Proof.
intros h1 h2 h12 h.
intros (subheap_h1_h12 & subheap_h2_h12 & union_h1_h2).
split.
intros subheap_h12_h.
split.
+ intros l o l_o_h1.
apply (subheap_h12_h l o).
now apply (subheap_h1_h12 l o).
+ intros l o l_o_h2.
apply (subheap_h12_h l o).
now apply (subheap_h2_h12 l o).
+ intros (subheap_h1_h & subheap_h2_h).
intros l o l_o_h12.
apply HeapFacts.elements_mapsto_iff in l_o_h12.
assert (l_in_h12 : exists o, InA (Heap.eq_key_elt (elt:=Obj))
(l, o) (Heap.elements (elt:=Obj) h12)).
now exists o.
apply HeapFacts.elements_in_iff in l_in_h12.
destruct (union_h1_h2 l l_in_h12).
++ apply (subheap_h1_h l o).
apply HeapFacts.elements_in_iff in H.
destruct H as (o' & l_o'_h1).
apply HeapFacts.elements_mapsto_iff in l_o'_h1.
apply HeapFacts.elements_mapsto_iff in l_o_h12.
assert (l_o'_h12 := l_o'_h1).
apply subheap_h1_h12 in l_o'_h12.
apply HeapFacts.find_mapsto_iff in l_o_h12.
apply HeapFacts.find_mapsto_iff in l_o'_h12.
rewrite l_o'_h12 in l_o_h12.
injection l_o_h12 as o_eq_o'.
now rewrite o_eq_o' in *.
++ apply (subheap_h2_h l o).
apply HeapFacts.elements_in_iff in H.
destruct H as (o' & l_o'_h2).