-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathheap_equiv.v
4164 lines (3801 loc) · 177 KB
/
heap_equiv.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
(* Heap equivalence definitions for L6. Part of the CertiCoq project.
* Author: Zoe Paraskevopoulou, 2016
*)
From Coq Require Import NArith.BinNat Relations.Relations MSets.MSets
MSets.MSetRBT Lists.List omega.Omega Sets.Ensembles Relations.Relations
Classes.Morphisms.
From SFS Require Import cps cps_util set_util List_util Ensembles_util functions
identifiers tactics map_util.
From SFS Require Import heap heap_defs.
From SFS Require Import Coqlib.
Import ListNotations.
Open Scope Ensembles_scope.
Module HeapEquiv (H : Heap).
Module Defs := HeapDefs H.
Import H Defs.HL Defs.
(** Formalization of heap equivalence *)
(** Syntactic approximation of results with fuel *)
Fixpoint res_approx_fuel (n : nat) (r1 : (loc -> loc) * res) (r2 : (loc -> loc) * res) : Prop :=
let '(b1, (v1, H1)) := r1 in
let '(b2, (v2, H2)) := r2 in
match v1, v2 with
| Loc l1, Loc l2 =>
b2 l2 = b1 l1 /\
match get l1 H1 with
| Some (Constr c vs1) =>
exists vs2,
get l2 H2 = Some (Constr c vs2) /\
forall i, (i < n)%nat ->
match n with
| 0%nat => True
| S n' =>
Forall2
(fun l1 l2 => res_approx_fuel (n'-(n'-i)) (b1, (l1, H1)) (b2, (l2, H2))) vs1 vs2
end
| Some (Clos v1 v2) =>
exists v1' v2',
get l2 H2 = Some (Clos v1' v2') /\
forall i, (i < n)%nat ->
match n with
| 0%nat => True
| S n' =>
res_approx_fuel (n'-(n'-i)) (b1, (v1, H1)) (b2, (v1', H2)) /\
res_approx_fuel (n'-(n'-i)) (b1, (v2, H1)) (b2, (v2', H2))
end
| Some (Env rho1) =>
exists rho2, get l2 H2 = Some (Env rho2) /\
(forall x, (exists v1 v2, M.get x rho1 = Some v1 /\
M.get x rho2 = Some v2 /\
(forall i, (i < n)%nat ->
match n with
| 0%nat => True
| S n' => res_approx_fuel (n'-(n'-i)) (b1, (v1, H1)) (b2, (v2, H2))
end)) \/
(M.get x rho1 = None /\ M.get x rho2 = None))
| None => True
end
| FunPtr B1 f1, FunPtr B2 f2 => f1 = f2 /\ B1 = B2
| _, _ => False
end.
(** Result equivalence. Two results represent the exact same value *)
Definition res_equiv (r1 : (loc -> loc) * res) (r2 : (loc -> loc) * res) : Prop :=
forall n, res_approx_fuel n r1 r2 /\ res_approx_fuel n r2 r1.
Notation "r1 ≈_( b1 , b2 ) r2 " := (res_equiv (b1, r1) (b2, r2)) (at level 70, no associativity).
Definition ans_equiv (b1 : loc -> loc) (a1 : ans) (b2 : loc -> loc) (a2 : ans) :=
match a1, a2 with
| Res r1, Res r2 => r1 ≈_(b1, b2) r2
| OOT, OOT => True
| _, _ => False
end.
(** Approximation lifted to the environments *)
Definition heap_env_approx (S : Ensemble var) p1 p2 : Prop :=
let '(b1, (H1, rho1)) := p1 in
let '(b2, (H2, rho2)) := p2 in
forall x l, x \in S ->
M.get x rho1 = Some l ->
exists l', M.get x rho2 = Some l' /\
(l, H1) ≈_(b1, b2) (l', H2).
(** Equivalence lifted to the environments *)
Definition heap_env_equiv S p1 p2 : Prop :=
heap_env_approx S p1 p2 /\
heap_env_approx S p2 p1.
Notation "S |- p1 ⩪_( b1 , b2 ) p2" := (heap_env_equiv S (b1, p1) (b2, p2))
(at level 70, no associativity).
Definition block_equiv (p1 : (loc -> loc) * heap block * block) (p2 : (loc -> loc) * heap block * block) :=
let '(b1, H1, bl1) := p1 in
let '(b2, H2, bl2) := p2 in
match bl1, bl2 with
| Constr c1 vs1, Constr c2 vs2 =>
c1 = c2 /\ Forall2 (fun v1 v2 => (v1, H1) ≈_(b1, b2) (v2, H2)) vs1 vs2
| Clos v1 v2, Clos v1' v2' =>
(v1, H1) ≈_(b1, b2) (v1', H2) /\ (v2, H1) ≈_(b1, b2) (v2', H2)
| Env rho1, Env rho2 => Full_set _ |- (H1, rho1) ⩪_(b1, b2) (H2, rho2)
| _, _ => False
end.
Definition heap_equiv (S : Ensemble loc) p1 p2 : Prop :=
let '(b1, H1) := p1 in
let '(b2, H2) := p2 in
forall l, l \in S -> (Loc (b2 l), H1) ≈_( b1 , b2 ) (Loc (b1 l), H2).
Notation "S |- H1 ≃_( b1 , b2 ) H2" := (heap_equiv S (b1, H1) (b2, H2))
(at level 70, no associativity).
(** Equivalent definition, unfolding the recursion *)
Definition res_approx_fuel' (n : nat) r1 r2 : Prop :=
let '(b1, (v1, H1)) := r1 in
let '(b2, (v2, H2)) := r2 in
match v1, v2 with
| Loc l1, Loc l2 =>
b1 l1 = b2 l2 /\
match get l1 H1 with
| Some (Constr c vs1) =>
exists vs2,
get l2 H2 = Some (Constr c vs2) /\
forall i, (i < n)%nat ->
Forall2 (fun l1 l2 => res_approx_fuel i (b1, (l1, H1)) (b2, (l2, H2))) vs1 vs2
| Some (Clos v1 v2) =>
exists v1' v2',
get l2 H2 = Some (Clos v1' v2') /\
forall i, (i < n)%nat ->
res_approx_fuel i (b1, (v1, H1)) (b2, (v1', H2)) /\
res_approx_fuel i (b1, (v2, H1)) (b2, (v2', H2))
| Some (Env rho1) =>
exists rho2,
get l2 H2 = Some (Env rho2) /\
(forall x, (exists v1 v2, M.get x rho1 = Some v1 /\
M.get x rho2 = Some v2 /\
(forall i, (i < n)%nat ->
res_approx_fuel i (b1, (v1, H1)) (b2, (v2, H2)))) \/
(M.get x rho1 = None /\ M.get x rho2 = None))
| None => True
end
| FunPtr B1 f1, FunPtr B2 f2 => f1 = f2 /\ B1 = B2
| _, _ => False
end.
(** Equivalence of the two definitions *)
Lemma res_approx_fuel_eq n r1 r2 :
res_approx_fuel n r1 r2 <-> res_approx_fuel' n r1 r2.
Proof.
destruct n; destruct r1 as [b1 [[l1 | B1 f1] H1]]; destruct r2 as [b2 [[l2 | B2 f2] H2]]; simpl.
- destruct (get l1 H1) as [[c1 vs1 | v1 v2 | rho1]|]; [| | | now firstorder ].
+ split.
* intros [Heq1 [vs [H _ ]]]. split; eauto. eexists. split; eauto.
intros; omega.
* intros [Heq1 [vs [H _ ]]]. split; eauto.
+ split.
* intros [Heq1 [v1' [v2' [H _ ]]]]. split; eauto. eexists. eexists. split; eauto.
intros; omega.
* intros [Heq1 [v1' [v2' [H _ ]]]]. split; eauto.
+ split.
* intros [Heq [vs [H Hb]]]. split; eauto. eexists. split; eauto.
intros x. destruct (Hb x) as [Hb1 | Hb1]; eauto.
destruct Hb1 as [v1 [v2 [Hget1 [Hget2 Ht]]]].
left. repeat eexists; eauto. intros; omega.
* intros [Heq [vs [H Hb]]]. split; eauto. eexists. split; eauto.
intros x. destruct (Hb x) as [Hb1 | Hb1]; eauto.
destruct Hb1 as [v1 [v2 [Hget1 [Hget2 Ht]]]].
left. repeat eexists; eauto.
- split; eauto.
- split; eauto.
- now firstorder.
- destruct (get l1 H1) as [[c1 vs1 | v1 v2 | rho1 ]|]; [| | | now firstorder ].
+ split.
* intros [Heq1 [vs [H Hi]]]. split; eauto. eexists. split; eauto.
intros i Hlt.
assert (Heq : (i = n - (n - i))%nat) by omega. rewrite Heq.
eauto.
* intros [Heq1 [vs [H Hin]]]. split; eauto. eexists. split; eauto.
intros i Hlt.
assert (Heq : (i = n - (n - i))%nat) by omega. rewrite <- Heq.
eauto.
+ split.
* intros [Heq1 [v1' [v2' [H Hi]]]]. split; eauto.
eexists. eexists. split; eauto.
intros i Hlt.
assert (Heq : (i = n - (n - i))%nat) by omega. rewrite Heq.
eauto.
* intros [Ηeq1 [v1' [v2' [H Hin]]]]. split; eauto. eexists. eexists. split; eauto.
intros i Hlt.
assert (Heq : (i = n - (n - i))%nat) by omega. rewrite <- Heq.
eauto.
+ split.
* intros [Heq1 [vs [H Hb ]]]. split; eauto. eexists. split; eauto.
intros x. destruct (Hb x) as [Hb1 | Hb1]; eauto.
destruct Hb1 as [v1 [v2 [Hget1 [Hget2 Ht]]]].
left. repeat eexists; eauto.
intros i Hlt.
assert (Heq : (i = n - (n - i))%nat) by omega. rewrite Heq.
eauto.
* intros [Heq1 [vs [H Hb]]]. split; eauto. eexists. split; eauto.
intros x. destruct (Hb x) as [Hb1 | Hb1]; eauto.
destruct Hb1 as [v1 [v2 [Hget1 [Hget2 Ht]]]].
left. repeat eexists; eauto.
intros i Hlt.
assert (Heq : (i = n - (n - i))%nat) by omega. rewrite <- Heq.
eauto.
- split; eauto.
- split; eauto.
- now firstorder.
Qed.
Opaque res_approx_fuel.
(** Equivalent definition for [res_equiv] *)
Definition res_equiv' r1 r2 : Prop :=
let '(b1, (v1, H1)) := r1 in
let '(b2, (v2, H2)) := r2 in
match v1, v2 with
| Loc l1, Loc l2 =>
b1 l1 = b2 l2 /\
match get l1 H1, get l2 H2 with
| Some bl1, Some bl2 => block_equiv (b1, H1, bl1) (b2, H2, bl2)
| None, None => True
| _, _ => False
end
| FunPtr B1 f1, FunPtr B2 f2 =>
B1 = B2 /\ f1 = f2
| _, _ => False
end.
Lemma res_equiv_eq r1 r2 :
res_equiv r1 r2 <-> res_equiv' r1 r2.
Proof.
destruct r1 as [b1 [[l1 | B1 f1] H1]]; destruct r2 as [b2 [[l2 | B2 f2] H2]]; simpl.
unfold res_equiv. split.
- intros H. assert (H0 := H 0%nat).
rewrite !res_approx_fuel_eq in H0.
destruct H0 as [Hal Har].
simpl in *. destruct (get l1 H1) as [ v |] eqn:Hget1.
+ destruct v as [c1 vs1 | v1 v2 | rho1 ].
* destruct Hal as [Heq1 [vs2 [Hget2 Hi]]].
rewrite Hget2 in Har.
destruct Har as [Heq2 [vs1' [Hget1' Hi']]]. inv Hget1'.
rewrite Hget2. split; eauto. split; eauto.
eapply Forall2_forall. constructor. exact 0%nat.
intros n. specialize (H (S n)). rewrite !res_approx_fuel_eq in H.
edestruct H as [Hal' Har']. simpl in Hal', Har'.
rewrite Hget1 in Hal'. rewrite Hget2 in Har'.
destruct Hal' as [Heq1' [vs2' [Hget2' Hi2]]]. subst_exp.
destruct Har' as [Heq2' [vs1 [Hget1' Hi1]]]. subst_exp.
eapply Forall2_conj.
eapply Hi2. omega.
eapply Forall2_flip. eapply Hi1. omega.
* destruct Hal as [Heq1 [v1' [v2' [Hget2 Hi]]]].
rewrite Hget2 in Har.
destruct Har as [Heq2 [v1'' [v2'' [Hget1' Hi']]]]. inv Hget1'.
rewrite Hget2.
split; eauto. split.
intros n. specialize (H (S n)). rewrite !res_approx_fuel_eq in H.
edestruct H as [Hal' Har']. simpl in Hal', Har'.
rewrite Hget1 in Hal'. rewrite Hget2 in Har'.
destruct Hal' as [Heq1' [v3 [v4 [Hget2' Hi2]]]]. subst_exp.
destruct Har' as [Heq2' [v3' [v4' [Hget1' Hi1]]]]. repeat subst_exp.
split. eapply Hi2. omega. eapply Hi1. omega.
intros n. specialize (H (S n)). rewrite !res_approx_fuel_eq in H.
edestruct H as [Hal' Har']. simpl in Hal', Har'.
rewrite Hget1 in Hal'. rewrite Hget2 in Har'.
destruct Hal' as [Heq1' [v3 [v4 [Hget2' Hi2]]]]. subst_exp.
destruct Har' as [Heq2' [v3' [v4' [Hget1' Hi1]]]]. repeat subst_exp.
split. eapply Hi2. omega. eapply Hi1. omega.
* destruct Hal as [Heq1 [rho2 [Hget2 Hi1]]].
rewrite Hget2 in Har.
destruct Har as [Heq2 [rho1' [Hget1' Hi2]]]. inv Hget1'.
rewrite Hget2. split; eauto. split; eauto; intros x l _ Hget.
{ destruct (Hi1 x) as [[v1 [v2 [Hgetv1 [Hgetv2 Hi]]]] | [Hn1 Hn2]]; try congruence.
subst_exp. eexists; split; eauto.
intros n.
specialize (H (S n)). rewrite !res_approx_fuel_eq in H.
edestruct H as [Hal' Har']. simpl in Hal', Har'.
rewrite Hget1 in Hal'. rewrite Hget2 in Har'.
destruct Hal' as [Heq1' [rho2' [Hget2' Hin2]]]. subst_exp.
destruct Har' as [Heq2' [rho1 [Hget1' Hin1]]]. repeat subst_exp.
destruct (Hin1 x) as [[v1' [v2' [Hgetv1' [Hgetv2' Hi1']]]] | [Hn1 Hn2]]; try congruence.
repeat subst_exp.
destruct (Hin2 x) as [[v1'' [v2'' [Hgetv1' [Hgetv2' Hi2']]]] | [Hn1 Hn2]]; try congruence.
repeat subst_exp. split; eauto. }
{ destruct (Hi1 x) as [[v1 [v2 [Hgetv1 [Hgetv2 Hi]]]] | [Hn1 Hn2]]; try congruence.
subst_exp. eexists; split; eauto.
intros n.
specialize (H (S n)). rewrite !res_approx_fuel_eq in H.
edestruct H as [Hal' Har']. simpl in Hal', Har'.
rewrite Hget1 in Hal'. rewrite Hget2 in Har'.
destruct Hal' as [Heq1' [rho2' [Hget2' Hin2]]]. subst_exp.
destruct Har' as [Heq2' [rho1 [Hget1' Hin1]]]. repeat subst_exp.
destruct (Hin1 x) as [[v1' [v2' [Hgetv1' [Hgetv2' Hi1']]]] | [Hn1 Hn2]]; try congruence.
repeat subst_exp.
destruct (Hin2 x) as [[v1'' [v2'' [Hgetv1' [Hgetv2' Hi2']]]] | [Hn1 Hn2]]; try congruence.
repeat subst_exp. split; eauto. }
+ destruct (get l2 H2); eauto.
destruct b.
destruct Har as [Heq1 [vs2 [Heq _]]]; discriminate.
destruct Har as [Heq2 [v1' [v2' [Heq _]]]]; discriminate.
destruct Har as [Heq2 [vs2 [Heq _]]]; discriminate.
- destruct (get l1 H1) eqn:Hget1.
+ destruct b as [ c vs1 | v1 v2 | rho1 B1 off1 ].
* destruct (get l2 H2) eqn:Hget2; try now firstorder.
destruct b as [c' vs2 | |]; try now firstorder.
intros [Heq1 [Heq Hall]] n. subst. rewrite !res_approx_fuel_eq.
simpl. rewrite Hget1, Hget2. split.
split; eauto. eexists. split. reflexivity.
intros. eapply Forall2_monotonic; [| eassumption ].
now intros v1 v2 [Hl Hr]; eauto.
split; eauto.
eexists. split. reflexivity.
intros. eapply Forall2_flip. eapply Forall2_monotonic; [| eassumption ].
now intros v1 v2 [Hl Hr]; eauto.
* destruct (get l2 H2) eqn:Hget2; try now firstorder.
destruct b as [ | v1' v2' |]; try now firstorder.
intros [Heq1 [H1' H2']] n. rewrite !res_approx_fuel_eq.
simpl. rewrite Hget1, Hget2. split.
split; eauto.
eexists. eexists. split. reflexivity.
intros. split; eauto. eapply H1'. eapply H2'.
split; eauto.
eexists. eexists. split. reflexivity.
intros. split; eauto. eapply H1'. eapply H2'.
* destruct (get l2 H2) eqn:Hget2; try now firstorder.
destruct b as [ | | rho2]; try now firstorder.
intros [Heq' [Hl Hr]] n. rewrite !res_approx_fuel_eq.
simpl. rewrite Hget1, Hget2. split.
split; eauto.
eexists. split. reflexivity.
intros x.
destruct (M.get x rho1) as [v1|] eqn:Hgetv1.
edestruct Hl as [v2 [Hgetv2 Hi]]; try eassumption.
now constructor.
left; repeat eexists; eauto. intros. now eapply Hi.
destruct (M.get x rho2) as [v2|] eqn:Hgetv2; eauto.
edestruct Hr as [v1 [Hgetv1' Hi']]; try eassumption.
now constructor. congruence.
split; eauto. eexists. split. reflexivity.
intros x.
destruct (M.get x rho1) as [v1|] eqn:Hgetv1.
edestruct Hl as [v2 [Hgetv2 Hi]]; try eassumption.
now constructor.
left; repeat eexists; eauto. intros. now eapply Hi.
destruct (M.get x rho2) as [v2|] eqn:Hgetv2; eauto.
edestruct Hr as [v1 [Hgetv1' Hi']]; try eassumption.
now constructor. congruence.
+ destruct (get l2 H2) eqn:Hget2; try now firstorder.
intros. rewrite !res_approx_fuel_eq. simpl.
rewrite Hget1, Hget2; eauto. firstorder.
- split; try contradiction.
intros Heq. destruct (Heq 0%nat) as [Hl Hr].
rewrite res_approx_fuel_eq in *. contradiction.
- split; try contradiction.
intros Heq. destruct (Heq 0%nat) as [Hl Hr].
rewrite res_approx_fuel_eq in *. contradiction.
- split.
+ intros Heq. destruct (Heq 0%nat) as [Hl Hr].
rewrite res_approx_fuel_eq in *. inv Hl. split; eauto.
+ intros [Hl1 Hr2]; subst.
split; eauto; rewrite res_approx_fuel_eq; simpl; split; eauto.
Qed.
Lemma res_equiv_locs_eq (S : Ensemble var) (b1 b2 : loc -> loc) (H1 H2 : heap block)
(l1 l2 : loc):
(Loc l1, H1) ≈_( b1, b2) (Loc l2, H2) ->
b1 l1 = b2 l2.
Proof.
intros Heq. rewrite res_equiv_eq in Heq.
destruct Heq as [Heq _]. eassumption.
Qed.
(** * Lemmas about [res_approx] and [res_equiv] *)
(** Preorder and equivalence properties of [res_approx] and [res_equiv] *)
(*
Lemma heap_equiv_res_approx (S : Ensemble loc) (β1 β2 : loc -> loc)
(H1 H2 : heap block)
(v : value) (n : nat) :
S |- H1 ≃_(β1, β2) H2 ->
(val_loc v) \subset S ->
res_approx_fuel n (β1, (v, H1)) (β2, (v, H2)).
Proof.
intros [Heq1 Heq2] Hin.
destruct v as [l | B f]; rewrite res_approx_fuel_eq; [| now split; eauto ].
edestruct Heq1 as [Hbeq Heq1'].
eapply Hin. reflexivity.
simpl; destruct (get l H1) eqn:Hget; eauto.
edestruct Heq1' as [bl2 [Hget2 Heq]]. reflexivity.
destruct b; destruct bl2; try contradiction.
- destruct Heq as [Heq Hin2]; subst. split; eauto. eexists; split; eauto.
intros.
eapply Forall2_monotonic; eauto. simpl.
intros ? ? [Ha1 Ha2]; eauto.
- destruct Heq as [Hv1 Hv2]. split; eauto. eexists. eexists.
split; eauto. intros; split; eauto.
now eapply Hv1. now eapply Hv2.
- split; eauto. eexists; split; eauto.
intros x. destruct Heq as [Hal Har].
destruct (M.get x e) eqn:Hgetx1; destruct (M.get x e0) eqn:Hgetx2;
simpl in *; eauto.
+ left. repeat eexists; eauto.
edestruct Hal as [l' [Hgetx2' Ha]]; eauto.
now constructor. subst_exp. intros i Hleq; destruct (Ha i); eassumption.
+ edestruct Hal as [l' [Hgetx2' Ha]]; eauto.
now constructor. congruence.
+ edestruct Har as [l' [Hgetx2' Ha]]; eauto.
now constructor. congruence.
Qed.
*)
Lemma Preorder_res_approx_fuel i :
preorder ((loc -> loc) * res) (res_approx_fuel i).
Proof.
constructor.
- induction i as [i IHi] using lt_wf_rec.
intros [β [v H1]]. rewrite res_approx_fuel_eq. destruct v.
simpl. destruct (get l H1) eqn:Hgetl; eauto.
destruct b as [c vs | vq vw | rho B f].
+ split; eauto. eexists; split; eauto.
intros i' Hlt.
eapply Forall2_refl; intros l'. eapply IHi in Hlt.
specialize (Hlt (β, (l', H1))). eassumption.
+ split; eauto. eexists; eexists; split; eauto.
intros i' Hlt.
split. specialize (IHi i' Hlt (β, (vq, H1))). eapply IHi; eauto.
specialize (IHi i' Hlt (β, (vw, H1))). eapply IHi; eauto.
+ split; eauto. eexists; split; eauto.
intros x.
destruct (M.get x rho) eqn:heq; eauto.
* left. do 2 eexists; repeat split; eauto.
intros.
specialize (IHi i0 H (β, (v, H1))). eapply IHi; eauto.
+ split; eauto.
- induction i as [i IHi] using lt_wf_rec1.
intros [β1 [v1 H1]] [β2 [v2 H2]] [β3 [v3 H3]] Hap1 Hap2. rewrite res_approx_fuel_eq in *.
simpl in *.
destruct v1 as [l1 | B1 f1]; destruct v2 as [l2 | B2 f2]; destruct v3 as [l3 | B3 f3];
try contradiction.
{ destruct (get l1 H1) eqn:Hget1; eauto.
destruct b as [c vs1 | vq vw | rho1 B f].
+ edestruct Hap1 as [Heq1 [vs2 [Hget2 Hall2]]]. rewrite Hget2 in Hap2.
destruct Hap2 as [Heq2 [vs3 [Hget3 Hall3]]].
split; eauto. congruence. eexists; split; eauto.
intros i' Hlt.
eapply Forall2_trans_strong; eauto. intros v1 v2 v3 Hv1 Hv2.
specialize (IHi i' Hlt (β1, (v1, H1)) (β2, (v2, H2)) (β3, (v3, H3))).
eapply IHi; eauto.
+ edestruct Hap1 as [Heq1 [vq' [vw' [Hget Hall2]]]]. rewrite Hget in Hap2.
destruct Hap2 as [Heq2 [vq'' [vw'' [Hget' Hall3]]]].
split. congruence. eexists; eexists; split; eauto.
intros i' Hlt.
split; eauto.
specialize (IHi i' Hlt (β1, (vq, H1)) (β2, (vq', H2)) (β3, (vq'', H3))).
eapply IHi; eauto. now eapply Hall2; eauto.
now eapply Hall3; eauto.
specialize (IHi i' Hlt (β1, (vw, H1)) (β2, (vw', H2)) (β3, (vw'', H3))).
eapply IHi; eauto. now eapply Hall2; eauto.
now eapply Hall3; eauto.
+ edestruct Hap1 as [Heq1 [rho2 [Hget2 Hall2]]]. rewrite Hget2 in Hap2.
destruct Hap2 as [Heq2 [rho33 [Hget3 Hall3]]].
split. congruence. eexists; split; eauto.
intros x.
edestruct Hall2 with (x := x) as [[l1' [l2' [Hgetl1 [Hgetl2 Hi]]]] | [Hn1 Hn2]]; eauto.
* edestruct Hall3 with (x := x) as [[l2'' [l3' [Hgetl2' [Hgetl3 Hi']]]] | [Hn1 Hn2]]; eauto.
subst_exp. subst_exp.
left; repeat eexists; eauto. subst_exp.
intros.
specialize (IHi i0 H (β1, (l1', H1)) (β2, (l2'', H2)) (β3, (l3', H3))).
eapply IHi; eauto.
congruence.
* edestruct Hall3 as [[l2'' [l3' [Hgetl2' [Hgetl3 Hi']]]] | [Hn2' Hn3]]; eauto.
congruence.
+ destruct Hap1; destruct Hap2. split; eauto. congruence. }
{ inv Hap1; inv Hap2. split; eauto. }
Qed.
Instance Equivalence_res_equiv : Equivalence res_equiv.
Proof.
constructor.
- intros res; split; eapply Preorder_res_approx_fuel.
- intros res res' H n. destruct (H n) as [H1 H2]. split; eauto.
- intros res1 res2 res3 H1 H2. intros n.
destruct (H1 n) as [Ht1 Ht2]; destruct (H2 n) as [Ht3 Ht4];
split.
now eapply Preorder_res_approx_fuel; eauto.
now eapply Preorder_res_approx_fuel; eauto.
Qed.
Instance Equivalence_heap_env_equiv S : Equivalence (heap_env_equiv S).
Proof.
constructor.
- intros [b [H rho]]; split; intros l Hget; eexists; split; eauto; reflexivity.
- intros [b [H rho]] [b' [H' rho']] H1; split; intros v l Hin Hget;
eapply H1; eauto.
- edestruct Equivalence_res_equiv; eauto.
intros [b [H rho]] [b' [H' rho']] [b'' [H'' rho'']] H1 H2; split; intros v l Hin Hget.
edestruct H1 as [H1' _]; eauto. edestruct H1' as [v1 [Hget1 Hres1]]; eauto.
edestruct H2 as [H2' _]; eauto. edestruct H2' as [v2 [Hget2 Hres2]]; eauto.
edestruct H2 as [_ H2']; eauto. edestruct H2' as [v2 [Hget2 Hres2]]; eauto.
edestruct H1 as [_ H1']; eauto. edestruct H1' as [v1 [Hget1 Hres1]]; eauto.
Qed.
(** * Lemmas about [block_equiv] **)
Instance Reflexive_block_equiv : Reflexive block_equiv.
Proof.
intros [[i H] b]. destruct b; simpl; eauto; try reflexivity.
split; eauto. eapply Forall2_refl; now eauto with typeclass_instances.
split; reflexivity.
Qed.
Instance Transitive_block_equiv : Transitive block_equiv.
Proof.
intros [[i1 H1] b1] [[i2 H2] b2] [[i3 H3] b3] Hb1 Hb2.
destruct b1; destruct b2; try contradiction;
destruct b3; try contradiction.
- destruct Hb1 as [Heq1 Hb1].
destruct Hb2 as [Heq2 Hb2].
subst. split; eauto.
eapply Forall2_trans_strong; try eassumption.
simpl; intros. eapply Equivalence_Transitive; eauto.
- destruct Hb1 as [Heq1 Hb1].
destruct Hb2 as [Heq2 Hb2].
split; eapply Equivalence_Transitive; eauto.
- simpl in *.
eapply Equivalence_Transitive; eauto.
Qed.
Instance Symmetric_block_equiv : Symmetric block_equiv.
Proof.
intros [[i1 H1] b1] [[i2 H2] b2] Hb.
destruct b1; destruct b2; try contradiction.
- destruct Hb as [Heq1 Hb1].
subst. split; eauto.
eapply Forall2_symm_strong; try eassumption.
simpl; intros. symmetry. eauto.
- destruct Hb as [Heq1 Heq2].
split; symmetry; eauto.
- simpl in *. symmetry; eauto.
Qed.
(*
Instance Equivalence_heap_equiv S : Equivalence (heap_equiv S).
Proof.
constructor.
- intros [b H].
split; intros x Hin; split; try reflexivity; intros bl Hget;
eexists; split; eauto; reflexivity.
- intros [b1 H1] [b2 H2] [Hs1 Hs2].
split; intros x Hin.
edestruct Hs1 as [Hbeq1 Hh1]; eauto.
edestruct Hs2 as [Hbeq2 Hh2]; eauto.
- intros [b1 H1] [b2 H2] [b3 H3] [Hs1 Hs2] [Hs2' Hs3].
split; intros x Hin.
edestruct Hs1 as [Hbeq1 Hh1]; eauto.
edestruct Hs2' as [Hbeq2 Hh2]; eauto.
split. congruence. intros bl Hget.
edestruct (Hh1 bl Hget) as [bl2 [Hget2 Hh2']].
edestruct (Hh2 bl2 Hget2) as [bl3 [Hget3 Hh3']].
eexists; split; eauto.
now eapply Transitive_block_equiv; eauto.
edestruct Hs2 as [Hbeq1 Hh1]; eauto.
edestruct Hs3 as [Hbeq2 Hh2]; eauto.
split. congruence. intros bl Hget.
edestruct (Hh2 bl Hget) as [bl2 [Hget2 Hh2']].
edestruct (Hh1 bl2 Hget2) as [bl3 [Hget3 Hh3']].
eexists; split; eauto.
now eapply Transitive_block_equiv; eauto.
Qed.
Lemma heap_env_approx_heap_equiv (S : Ensemble var) (H1 H2 : heap block) (b1 b2 : loc -> loc) (rho : env) :
(env_locs rho S) |- H1 ≃_(b1, b2) H2 ->
heap_env_approx S (b2, (H2, rho)) (b1, (H1, rho)).
Proof.
intros [Heq1 Heq2] x v Hin Hget.
eexists; split; eauto.
rewrite res_equiv_eq. simpl.
destruct v as [l | B f]; [| now split; eauto ].
destruct (get l H1) eqn:Heq.
- edestruct Heq1 as [Hb2 Heq1'].
eexists; split; eauto. rewrite Hget. reflexivity.
split; eauto. edestruct Heq1' as [bl2 [Hget2 Hbl2]]; eauto. rewrite Hget2.
simpl in Hbl2. destruct b; destruct bl2; try contradiction.
destruct Hbl2 as [Heqc Hall]; subst; split; eauto.
eapply Forall2_symm_strong; [| eassumption ].
simpl; intros.
now eapply Equivalence.equiv_symmetric; eauto.
destruct Hbl2 as [Hb'1 Hb'2].
split; eauto; now symmetry; eauto.
now symmetry; eauto.
- edestruct Heq2 as [Hb2 Heq1'].
eexists; split; eauto. rewrite Hget. reflexivity.
split; eauto.
destruct (get l H2) eqn:HgetH2; eauto.
edestruct Heq1' as [bl2 [Hget2 Hbl2]]; eauto.
congruence.
Qed.
Corollary heap_env_equiv_heap_equiv (S : Ensemble var) (H1 H2 : heap block) (b1 b2 : loc -> loc)
(rho : env) :
(env_locs rho S) |- H1 ≃_(b1, b2) H2 ->
S |- (H1, rho) ⩪_(b1, b2) (H2, rho).
Proof.
intros. split; eapply heap_env_approx_heap_equiv; simpl; try eassumption.
symmetry. eassumption.
Qed.
Lemma heap_equiv_res_equiv (S : Ensemble loc) (H1 H2 : heap block) (b1 b2 : loc -> loc)
(v : value) :
S |- H1 ≃_(b1, b2) H2 ->
(val_loc v) \subset S ->
(v, H1) ≈_(b1, b2) (v, H2).
Proof.
intros Heq Hin m.
split. eapply heap_equiv_res_approx; eauto.
eapply heap_equiv_res_approx; eauto. symmetry.
eassumption.
Qed.
*)
Lemma heap_env_approx_empty S H1 H2 rho2 b1 b2 :
heap_env_approx S (b1, (H1, M.empty _)) (b2, (H2, rho2)).
Proof.
intros x Hin v Hget.
rewrite M.gempty in Hget. congruence.
Qed.
Lemma heap_env_equiv_empty S H1 H2 b1 b2 :
S |- (H1, M.empty _) ⩪_(b1, b2) (H2, M.empty _).
Proof.
split; eapply heap_env_approx_empty.
Qed.
(** Heap equivalences respect functional extensionality *)
Instance Proper_res_approx_f_eq_l : Proper (eq ==> RelProd f_eq eq ==> eq ==> iff) res_approx_fuel.
Proof.
intros j i Heq1 [b1 [r1 H1]] [b1' [r1' H1']] [Heq2 Heq3] [b2 [r2 H2]] [b2' [r2' H2']] Heq4.
inv Heq3; inv Heq4. split.
- revert b1 b1' r1' H1' b2' r2' H2' Heq2.
induction i as [i IHi] using lt_wf_rec; intros b1 b1' r1 H1 b2 r2 H2 Heq2.
rewrite !res_approx_fuel_eq in *.
destruct r1 as [ l1 | B1 f1]; destruct r2 as [ l2 | V2 f2]; try contradiction.
+ simpl. destruct (get l1 H1) as [b | ] eqn:Hgetl1; eauto.
destruct b as [c vs | vq vw | rho ].
* intros [Heqb [vs2 [Hgetl2 Hi]]]. split.
rewrite <- Heq2. eassumption.
repeat eexists; eauto.
intros i' Hlt.
eapply Forall2_monotonic; [| eapply Hi; eassumption ].
intros. eapply IHi; eassumption.
* intros [Heqb [v1 [v2 [Hgetl2 Hi]]]]. split.
rewrite <- Heq2. eassumption.
repeat eexists; eauto.
eapply IHi; try eassumption. eapply Hi. eassumption.
eapply IHi; try eassumption. eapply Hi. eassumption.
* intros [Heqb [rho2 [Hgetl2 Hall]]]. split.
rewrite <- Heq2. eassumption.
eexists; split; eauto. intros x. destruct (Hall x) as [[v1 [v2 [Hget1 [Hget2 Hs]]]] | Hn]; eauto.
left. repeat eexists; eauto.
* intros [Heq _]; split; eauto. rewrite <- Heq2. eauto.
+ simpl; eauto.
- revert b1 b1' r1' H1' b2' r2' H2' Heq2.
induction i as [i IHi] using lt_wf_rec; intros b1 b1' r1 H1 b2 r2 H2 Heq2.
rewrite !res_approx_fuel_eq in *.
destruct r1 as [ l1 | B1 f1]; destruct r2 as [ l2 | V2 f2]; try contradiction.
+ simpl. destruct (get l1 H1) as [b | ] eqn:Hgetl1; eauto.
destruct b as [c vs | vq vw | rho ].
* intros [Heqb [vs2 [Hgetl2 Hi]]]. split.
rewrite Heq2. eassumption.
repeat eexists; eauto.
intros i' Hlt.
eapply Forall2_monotonic; [| eapply Hi; eassumption ].
intros. eapply IHi; eassumption.
* intros [Heqb [v1 [v2 [Hgetl2 Hi]]]]. split.
rewrite Heq2. eassumption.
repeat eexists; eauto.
eapply IHi; try eassumption. eapply Hi. eassumption.
eapply IHi; try eassumption. eapply Hi. eassumption.
* intros [Heqb [rho2 [Hgetl2 Hall]]]. split.
rewrite Heq2. eassumption.
eexists; split; eauto. intros x. destruct (Hall x) as [[v1 [v2 [Hget1 [Hget2 Hs]]]] | Hn]; eauto.
left. repeat eexists; eauto.
* intros [Heq _]; split; eauto. rewrite Heq2. eauto.
+ simpl; eauto.
Qed.
Instance Proper_res_approx_f_eq_r : Proper (eq ==> eq ==> RelProd f_eq eq ==> iff) res_approx_fuel.
Proof.
intros j i Heq1 [b1 [r1 H1]] [b1' [r1' H1']] Heq2 [b2 [r2 H2]] [b2' [r2' H2']] [Heq3 Heq4].
inv Heq2; inv Heq4. split.
- revert b1' r1' H1' b2 b2' r2' H2' Heq3.
induction i as [i IHi] using lt_wf_rec; intros b1 r1 H1 b2 b2' r2 H2 Heq2.
rewrite !res_approx_fuel_eq in *.
destruct r1 as [ l1 | B1 f1]; destruct r2 as [ l2 | V2 f2]; try contradiction.
+ simpl. destruct (get l1 H1) as [b | ] eqn:Hgetl1; eauto.
destruct b as [c vs | vq vw | rho ].
* intros [Heqb [vs2 [Hgetl2 Hi]]]. split.
rewrite <- Heq2. eassumption.
repeat eexists; eauto.
intros i' Hlt.
eapply Forall2_monotonic; [| eapply Hi; eassumption ].
intros. eapply IHi; eassumption.
* intros [Heqb [v1 [v2 [Hgetl2 Hi]]]]. split.
rewrite <- Heq2. eassumption.
repeat eexists; eauto.
eapply IHi; try eassumption. eapply Hi. eassumption.
eapply IHi; try eassumption. eapply Hi. eassumption.
* intros [Heqb [rho2 [Hgetl2 Hall]]]. split.
rewrite <- Heq2. eassumption.
eexists; split; eauto. intros x. destruct (Hall x) as [[v1 [v2 [Hget1 [Hget2 Hs]]]] | Hn]; eauto.
left. repeat eexists; eauto.
* intros [Heq _]; split; eauto. rewrite <- Heq2. eauto.
+ simpl; eauto.
- revert b1' r1' H1' b2 b2' r2' H2' Heq3.
induction i as [i IHi] using lt_wf_rec; intros b1 r1 H1 b2 b2' r2 H2 Heq2.
rewrite !res_approx_fuel_eq in *.
destruct r1 as [ l1 | B1 f1]; destruct r2 as [ l2 | V2 f2]; try contradiction.
+ simpl. destruct (get l1 H1) as [b | ] eqn:Hgetl1; eauto.
destruct b as [c vs | vq vw | rho ].
* intros [Heqb [vs2 [Hgetl2 Hi]]]. split.
rewrite Heq2. eassumption.
repeat eexists; eauto.
intros i' Hlt.
eapply Forall2_monotonic; [| eapply Hi; eassumption ].
intros. eapply IHi; eassumption.
* intros [Heqb [v1 [v2 [Hgetl2 Hi]]]]. split.
rewrite Heq2. eassumption.
repeat eexists; eauto.
eapply IHi; try eassumption. eapply Hi. eassumption.
eapply IHi; try eassumption. eapply Hi. eassumption.
* intros [Heqb [rho2 [Hgetl2 Hall]]]. split.
rewrite Heq2. eassumption.
eexists; split; eauto. intros x. destruct (Hall x) as [[v1 [v2 [Hget1 [Hget2 Hs]]]] | Hn]; eauto.
left. repeat eexists; eauto.
* intros [Heq _]; split; eauto. rewrite Heq2. eauto.
+ simpl; eauto.
Qed.
Instance Proper_res_equiv_f_eq_l : Proper (RelProd f_eq eq ==> eq ==> iff) res_equiv.
Proof.
intros [b1 [r1 H1]] [b1' [r1' H1']] Heq1 [b2 [r2 H2]] [b2' [r2' H2']] Heq2. inv Heq2.
split; intros H n; specialize (H n).
rewrite <- !Heq1. eassumption.
rewrite !Heq1. eassumption.
Qed.
Instance Proper_res_equiv_f_eq_r : Proper (eq ==> RelProd f_eq eq ==> iff) res_equiv.
Proof.
intros [b1 [r1 H1]] [b1' [r1' H1']] Heq1 [b2 [r2 H2]] [b2' [r2' H2']] Heq2. inv Heq1.
split; intros H n; specialize (H n).
rewrite <- !Heq2. eassumption.
rewrite !Heq2. eassumption.
Qed.
Instance Proper_heap_env_approx_f_eq_l : Proper (eq ==> RelProd f_eq eq ==> eq ==> iff) heap_env_approx.
Proof.
intros s1 s2 hseq [b1 [H1 rho1]] [b2 [H2 rho2]] [Heq1 Heq2] [b1' [H1' p1']] [b2' [H2' p2']] Heq'.
inv Heq2; inv Heq'.
subst; split; intros Ha x v Hin Hget; edestruct Ha as [v' [Hget' Hres]]; eauto; eexists; split; eauto.
assert (Heq : (f_eq * eq)%signature (b1, (v, H2)) (b2, (v, H2))) by (split; eauto).
rewrite Heq in Hres. eassumption.
assert (Heq : (f_eq * eq)%signature (b1, (v, H2)) (b2, (v, H2))) by (split; eauto).
rewrite Heq. eassumption.
Qed.
Instance Proper_heap_env_approx_f_eq_r : Proper (eq ==> eq ==> RelProd f_eq eq ==> iff) heap_env_approx.
Proof.
intros s1 s2 hseq [b1 [H1 rho1]] [b2 [H2 rho2]] Heq [b1' [H1' p1']] [b2' [H2' p2']] [Heq1 Heq2].
inv Heq2; inv Heq.
subst; split; intros Ha x v Hin Hget; edestruct Ha as [v' [Hget' Hres]]; eauto; eexists; split; eauto.
assert (Heq : (f_eq * eq)%signature (b1', (v', H2')) (b2', (v', H2'))) by (split; eauto).
rewrite <- Heq. eassumption.
assert (Heq : (f_eq * eq)%signature (b1', (v', H2')) (b2', (v', H2'))) by (split; eauto).
rewrite Heq. eassumption.
Qed.
Instance Proper_heap_env_equiv_f_eq_l : Proper (eq ==> RelProd f_eq eq ==> eq ==> iff) heap_env_equiv.
Proof.
intros s1 s2 hseq [b1 [H1 rho1]] [b2 [H2 rho2]] [Heq1 Heq2] [b1' [H1' p1']] [b2' [H2' p2']] Heq'.
inv Heq2; inv Heq'.
assert (Heq : (f_eq * eq)%signature (b1, (H2, rho2)) (b2, (H2, rho2))) by (split; eauto).
split; intros [Hh1 Hh2]. split; rewrite <- Heq; eassumption.
split; rewrite Heq; eassumption.
Qed.
Instance Proper_heap_env_equiv_f_eq_r : Proper (eq ==> eq ==> RelProd f_eq eq ==> iff) heap_env_equiv.
Proof.
intros s1 s2 hseq [b1 [H1 rho1]] [b2 [H2 rho2]] Heq' [b1' [H1' p1']] [b2' [H2' p2']] [Heq1 Heq2].
inv Heq2; inv Heq'.
assert (Heq : (f_eq * eq)%signature (b1', (H2', p2')) (b2', (H2', p2'))) by (split; eauto).
split; intros [Hh1 Hh2]. split; rewrite <- Heq; eassumption.
split; rewrite Heq; eassumption.
Qed.
Instance Proper_block_equiv_f_eq_l : Proper (RelProd (RelProd f_eq eq) eq ==> eq ==> iff) block_equiv.
Proof.
intros [[b1 H1] bl1] [[b2 H2] bl2] [[Heq1 Heq2] Heq3] [[b1' H1'] bl1'] [[b2' H2'] bl2'] Heq';
inv Heq'; inv Heq2; inv Heq3; simpl in *; subst.
destruct bl2 as [c vs | vq vw | rho ]; destruct bl2' as [c' vs' | vq' vw' | rho' ];
[| now firstorder | now firstorder | now firstorder | | now firstorder | now firstorder | now firstorder | ].
- split; intros [Heq1' Hres].
split; eauto.
eapply Forall2_monotonic; try eassumption. intros v1 v2 Hres'.
assert (Heq : (f_eq * eq)%signature (b1, (v1, H2)) (b2, (v1, H2))) by (split; eauto).
rewrite <- Heq. eassumption.
split; eauto.
eapply Forall2_monotonic; try eassumption. intros v1 v2 Hres'.
assert (Heq : (f_eq * eq)%signature (b1, (v1, H2)) (b2, (v1, H2))) by (split; eauto).
rewrite Heq. eassumption.
- assert (Heq : (f_eq * eq)%signature (b1, (vq, H2)) (b2, (vq, H2))) by (split; eauto).
rewrite Heq.
assert (Heq' : (f_eq * eq)%signature (b1, (vw, H2)) (b2, (vw, H2))) by (split; eauto).
rewrite Heq'. reflexivity.
- assert (Heq : (f_eq * eq)%signature (b1, (H2, rho)) (b2, (H2, rho))) by (split; eauto).
rewrite Heq. reflexivity.
Qed.
Instance Proper_block_equiv_f_eq_r : Proper (eq ==> RelProd (RelProd f_eq eq) eq ==> iff) block_equiv.
Proof.
intros [[b1 H1] bl1] [[b2 H2] bl2] Heq' [[b1' H1'] bl1'] [[b2' H2'] bl2'] [[Heq1 Heq2] Heq3];
inv Heq'; inv Heq2; inv Heq3; simpl in *; subst.
destruct bl2 as [c vs | vq vw | rho ]; destruct bl2' as [c' vs' | vq' vw' | rho' ];
[| now firstorder | now firstorder | now firstorder | | now firstorder | now firstorder | now firstorder | ].
- split; intros [Heq1' Hres].
split; eauto.
eapply Forall2_monotonic; try eassumption. intros v1 v2 Hres'.
assert (Heq : (f_eq * eq)%signature (b1', (v2, H2')) (b2', (v2, H2'))) by (split; eauto).
rewrite <- Heq. eassumption.
split; eauto.
eapply Forall2_monotonic; try eassumption. intros v1 v2 Hres'.
assert (Heq : (f_eq * eq)%signature (b1', (v2, H2')) (b2', (v2, H2'))) by (split; eauto).
rewrite Heq. eassumption.
- assert (Heq : (f_eq * eq)%signature (b1', (vq', H2')) (b2', (vq', H2'))) by (split; eauto).
rewrite Heq.
assert (Heq' : (f_eq * eq)%signature (b1', (vw', H2')) (b2', (vw', H2'))) by (split; eauto).
rewrite Heq'. reflexivity.
- assert (Heq : (f_eq * eq)%signature (b1', (H2', rho')) (b2', (H2', rho'))) by (split; eauto).
rewrite Heq. reflexivity.
Qed.
(* Instance Proper_heap_approx_f_eq_l : Proper (eq ==> RelProd f_eq eq ==> eq ==> iff) heap_approx. *)
(* Proof. *)
(* intros s1 s2 hseq [b1 H1] [b2 H2] [Heq1 Heq2] [b1' H1'] [b2' H2'] Heq'; inv Heq'. *)
(* compute in Heq2. subst. *)
(* split. *)
(* intros Ha bl Hin. edestruct Ha as [Hb Hh]. eassumption. *)
(* split; eauto. now rewrite <- Heq1; eauto. intros bl1 Hget1. *)
(* edestruct Hh as [bl2 [Hget2 Hbl2]]; eauto. eexists; split; eauto. *)
(* assert (Heq : ((f_eq * eq) * eq)%signature ((b1, H2), bl1) ((b2, H2), bl1)) by (split; eauto). *)
(* rewrite <- Heq. eassumption. *)
(* intros Ha bl Hin. edestruct Ha as [Hb Hh]. eassumption. *)
(* split; eauto. now rewrite Heq1; eauto. intros bl1 Hget1. *)
(* edestruct Hh as [bl2 [Hget2 Hbl2]]; eauto. eexists; split; eauto. *)
(* assert (Heq : ((f_eq * eq) * eq)%signature ((b1, H2), bl1) ((b2, H2), bl1)) by (split; eauto). *)
(* rewrite Heq. eassumption. *)
(* Qed. *)
(* Instance Proper_heap_approx_f_eq_r : Proper (eq ==> eq ==> RelProd f_eq eq ==> iff) heap_approx. *)
(* Proof. *)
(* intros s1 s2 hseq [b1 H1] [b2 H2] Heq' [b1' H1'] [b2' H2'] [Heq1 Heq2]; inv Heq'. *)
(* compute in Heq2. subst. *)
(* split. *)
(* intros Ha bl Hin. edestruct Ha as [Hb Hh]. eassumption. *)
(* split; eauto. now rewrite <- Heq1; eauto. intros bl1 Hget1. *)
(* edestruct Hh as [bl2 [Hget2 Hbl2]]; eauto. eexists; split; eauto. *)
(* assert (Heq : ((f_eq * eq) * eq)%signature ((b1', H2'), bl2) ((b2', H2'), bl2)) by (split; eauto). *)
(* rewrite <- Heq. eassumption. *)
(* intros Ha bl Hin. edestruct Ha as [Hb Hh]. eassumption. *)
(* split; eauto. now rewrite Heq1; eauto. intros bl1 Hget1. *)
(* edestruct Hh as [bl2 [Hget2 Hbl2]]; eauto. eexists; split; eauto. *)
(* assert (Heq : ((f_eq * eq) * eq)%signature ((b1', H2'), bl2) ((b2', H2'), bl2)) by (split; eauto). *)
(* rewrite Heq. eassumption. *)
(* Qed. *)
Instance Proper_heap_equiv_f_eq_r : Proper (eq ==> eq ==> RelProd f_eq eq ==> iff) heap_equiv.
Proof.
intros s1 s2 hseq [b1 H1] [b2 H2] Heq' [b1' H1'] [b2' H2'] Heq. inv Heq'. destruct Heq. inv H0.
simpl in H1. subst.
split; intros Heqh x Hin.
assert (Heqp : (f_eq * eq)%signature (b1', (Loc (b2 x), H2')) (b2', (Loc (b2 x), H2')))
by (split; eauto).
rewrite <- Heqp, <- H. eapply Heqh. eassumption.
assert (Heqp : (f_eq * eq)%signature (b1', (Loc (b2 x), H2')) (b2', (Loc (b2 x), H2')))
by (split; eauto).
rewrite Heqp, H. eapply Heqh. eassumption.
Qed.
Instance Proper_heap_equiv_f_eq_l : Proper (eq ==> RelProd f_eq eq ==> eq ==> iff) heap_equiv.
Proof.
intros s1 s2 hseq [b1 H1] [b2 H2] Heq' [b1' H1'] [b2' H2'] Heq. inv Heq'. destruct Heq. inv H0.
simpl in H3. subst.
split; intros Heqh x Hin. rewrite <- H.
assert (Heqp : (f_eq * eq)%signature (b1, (Loc (b1' x), H2)) (b2, (Loc (b1' x), H2))) by (split; eauto).
simpl. rewrite <- Heqp. eapply Heqh. eassumption.
assert (Heqp : (f_eq * eq)%signature (b1, (Loc (b1' x), H2)) (b2, (Loc (b1' x), H2)))
by (split; eauto).
simpl. rewrite Heqp, H. simpl. eapply Heqh. eassumption.
Qed.
Lemma heap_env_approx_res_approx
(S : Ensemble var) (β : loc -> loc)
(H1 H2 : heap block) (rho1 rho2 : M.t value) l :
heap_env_approx S (β, (H1, rho1)) (id, (H2, rho2)) ->
l \in env_locs rho1 S ->
(Loc l, H1) ≈_(β, id) (Loc (β l), H2).
Proof.
intros Henv [x [Heq1 Heq2]].
destruct (M.get x rho1) as [[l1|] |] eqn:Hget; inv Heq2.
edestruct Henv as [v2 [Hget2 Hres]]; eauto.
assert (Hres' := Hres). rewrite res_equiv_eq in Hres.
destruct v2 as [l2|]; try contradiction. simpl in Hres.
destruct Hres as [Hres'' _]. unfold id in *; subst.
eassumption.
Qed.
Lemma heap_env_equiv_res_equiv
(S : Ensemble var) (β : loc -> loc)
(H1 H2 : heap block) (rho1 rho2 : M.t value) l :
S |- (H1, rho1) ⩪_(id, β) (H2, rho2) ->
l \in env_locs rho2 S ->
(Loc (β l), H1) ≈_(id, β) (Loc l, H2).
Proof.
intros Henv Hin.
symmetry. eapply heap_env_approx_res_approx.
destruct Henv. eassumption.
eassumption.
Qed.
(** Horizontal composition of injections *)
Lemma res_approx_f_compose_l (β1 β2 β3 β4 : loc -> loc)
(H1 H2 H3 : heap block)
(v1 v2 v3 : value) (n : nat) :
res_approx_fuel' n (β1, (v1, H1)) (β2 ∘ β4, (v2, H2)) ->
res_approx_fuel' n (β4, (v2, H2)) (β3, (v3, H3)) ->
res_approx_fuel' n (β1, (v1, H1)) (β2 ∘ β3, (v3, H3)).
Proof.
revert v1 v2 v3 H1 H2 H3. induction n as [n IHn] using lt_wf_rec1;
intros v1 v2 v3 H1 H2 H3 Hres1 Hres2.
destruct v1 as [l1 | B1 f1]; destruct v2 as [l2 | B2 f2]; destruct v3 as [l3 | B3 f3];
try now firstorder.
- simpl in Hres1, Hres2. simpl. destruct (get l1 H1) as [b1 |] eqn:Hget1; eauto.
destruct b1 as [c1 vs1 | v1 v2 | rho1 ].
+ destruct Hres1 as [Hbs1 [vs2 [Hget2 Hi]]].
rewrite Hget2 in Hres2.
destruct Hres2 as [Hbs2 [vs3 [Hget3 Hj]]].
simpl. split.
unfold compose, id in *. congruence.
eexists; split; eauto. intros i' Hlt.
eapply Forall2_trans_strong; [| now eapply Hi; eauto | now eapply Hj; eauto ].
simpl. intros l1' l2' l3' Hr1 Hr2.
rewrite res_approx_fuel_eq in *. eapply IHn; eauto.
+ destruct Hres1 as [Hbs1 [v1' [v2' [Hget2 Hi]]]].
rewrite Hget2 in Hres2.
destruct Hres2 as [Hbs2 [v1'' [v2'' [Hget3 Hj]]]].
simpl. split.
unfold compose, id in *. congruence.
eexists; eexists; split; eauto. intros i' Hlt.
rewrite !res_approx_fuel_eq in *.
split; eapply IHn; try eassumption; rewrite <- !res_approx_fuel_eq.
now eapply Hi; eauto.