-
Notifications
You must be signed in to change notification settings - Fork 0
/
invariants.v
2199 lines (1886 loc) · 92.3 KB
/
invariants.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
From SFS Require Import cps cps_util set_util identifiers ctx Ensembles_util
List_util functions tactics map_util.
From SFS Require Import heap heap_defs heap_equiv space_sem
cc_log_rel closure_conversion closure_conversion_util bounds GC.
From Coq Require Import ZArith.Znumtheory Relations.Relations Arith.Wf_nat
Lists.List MSets.MSets MSets.MSetRBT Numbers.BinNums
NArith.BinNat PArith.BinPos Sets.Ensembles Omega Permutation.
Import ListNotations.
Open Scope ctx_scope.
Open Scope fun_scope.
Close Scope Z_scope.
Module Invariants (H : Heap).
Module Size := Size H.
Import H Size.Util.C.LR.Sem.GC.Equiv Size.Util.C.LR.Sem.GC.Equiv.Defs
Size.Util.C.LR.Sem.GC Size.Util.C.LR.Sem Size.Util.C.LR Size.Util.C
Size.Util Size.
(** Invariant about the free variables *)
Definition FV_inv (k j : nat) (IP : GIInv) (P : GInv) (b : Inj)
(rho1 : env) (H1 : heap block) (rho2 : env) (H2 : heap block)
(c : cTag) (Scope Funs : Ensemble var) (Γ : var) (FVs : list var) : Prop :=
well_formed (reach' H2 (env_locs rho2 [set Γ])) H2 /\ (* True when the environment is created *)
key_set rho1 <--> FV Scope Funs FVs /\
exists (vs : list value) (l : loc),
M.get Γ rho2 = Some (Loc l) /\
get l H2 = Some (Constr c vs) /\
Forall2_P (Scope :|: Funs)
(fun (x : var) (v2 : value) =>
exists v1, M.get x rho1 = Some v1 /\
Res (v1, H1) ≺ ^ ( k ; j ; IP ; P ; b) Res (v2, H2)) FVs vs.
(** Invariant about the functions currently in scope not yet packed as closures *)
Definition Fun_inv k j GI GP b rho1 H1 rho2 H2 Scope Funs fenv FVs :=
forall f, ~ f \in Scope -> f \in Funs ->
exists l1 lenv1 lenv2 B1 g1 B2 g2,
M.get f rho1 = Some (Loc l1) /\
(* Funs locations are fresh, and there are no references to them *)
~ l1 \in (reach' H1 ((env_locs rho1 (FV Scope Funs FVs \\ [set f])) :|: post H1 [set l1])) /\
M.get f rho2 = Some (FunPtr B2 g2) /\
get l1 H1 = Some (Clos (FunPtr B1 g1) (Loc lenv1)) /\
M.get (fenv f) rho2 = Some (Loc lenv2) /\
(* Environments are related (before allocation) *)
(lenv1, H1) << ^ (k; j; GI; GP; b) (lenv2, H2) /\
(* We can alloc a related function *)
let '(l2, H2') := alloc (Constr Size.Util.clo_tag [FunPtr B2 g2; Loc lenv2]) H2 in
Res (Loc l1, H1) ≺ ^ (k; j; GI; GP; b{l1 ~> l2}) Res (Loc l2, H2').
(** Version without the logical relation. Useful when we're only interested in other invariants. *)
(** Invariant about the free variables *)
Definition FV_inv_weak (rho1 : env) (rho2 : env) (H2 : heap block)
(c : cTag) (Scope Funs : Ensemble var) (Γ : var) (FVs : list var) : Prop :=
exists (vs : list value) (l : loc),
M.get Γ rho2 = Some (Loc l) /\
get l H2 = Some (Constr c vs) /\
Forall2_P (Scope :|: Funs)
(fun (x : var) (v2 : value) =>
exists v1, M.get x rho1 = Some v1) FVs vs.
Definition Fun_inv_weak rho1 rho2 Scope Funs fenv :=
forall f, ~ f \in Scope -> f \in Funs ->
exists l1 lenv B g,
M.get f rho1 = Some (Loc l1) /\
M.get f rho2 = Some (FunPtr B g) /\
M.get (fenv f) rho2 = Some (Loc lenv).
(** * Lemmas about [FV_inv] *)
Lemma Forall2_P_Forall2 {A B : Type} S P (ls1 : list A) (ls2 : list B) :
Forall2_P S P ls1 ls2 ->
Disjoint A S (FromList ls1) ->
Forall2 P ls1 ls2.
Proof with (now eauto with Ensembles_DB).
intros Hall Hd. induction Hall.
- now constructor.
- constructor.
+ eapply H. intros Hc. eapply Hd. constructor; eauto.
now left.
+ eapply IHHall.
eapply Disjoint_Included_r; eauto.
normalize_sets...
Qed.
Lemma key_set_get S `{_ : ToMSet S} x rho :
x \in S ->
M.get x rho = M.get x (restrict_env (@mset S _) rho).
Proof.
intros Hin.
assert (Hset : Restrict_env S rho (restrict_env (@mset S _) rho)).
{ eapply restrict_env_correct. eapply H. }
destruct Hset as [Hin' [Hs1 Hs2]].
eapply Hin'. eassumption.
Qed.
Lemma key_set_binding_in_map S `{_ : ToMSet S} (rho : env) :
binding_in_map S rho ->
key_set (restrict_env (@mset S _) rho) <--> S.
Proof.
intros Hbin.
split.
eapply key_set_Restrict_env. eapply restrict_env_correct.
now eapply H.
intros x Hin. edestruct Hbin as [v Hget]. eassumption.
unfold In, key_set. rewrite <- key_set_get; [| eassumption ].
now rewrite Hget.
Qed.
Lemma FV_inv_cc_approx_clos (k j : nat) (IP : GIInv) (P : GInv) (b : Inj)
(rho1 : env) (H1 : heap block) (rho2 : env) (H2 : heap block)
(c : cTag) (Γ : var) (FVs : list var) l1 l2 :
FV_inv k j IP P b rho1 H1 rho2 H2 c (Empty_set _) (Empty_set _) Γ FVs ->
binding_in_map (FromList FVs) rho1 ->
NoDup FVs ->
get l1 H1 = Some (Env rho1) ->
M.get Γ rho2 = Some (Loc l2) ->
l2 = b l1 ->
(l1, H1) << ^ (k; j; IP; P; b) (l2, H2).
Proof with (now eauto with Ensembles_DB).
intros (Hwf & Hkey & vs & l' & Hget1 & Hget2 & Hall) Hbin Hnd Hget1' Hget2' Hbeq.
subst_exp.
clear Hget1. split. reflexivity.
do 4 eexists.
split; [| split; [| split; [| split ]]]; try eassumption.
- rewrite Hkey. unfold FV.
rewrite !Union_Empty_set_neut_l.
rewrite !Setminus_Empty_set_neut_r.
rewrite !Union_Empty_set_neut_l.
reflexivity.
- eapply Forall2_monotonic_strong; [| eapply Forall2_P_Forall2; try eassumption ].
intros x1 x2 Hin1 Hin2 [[l1' |] [Hget1 Hcc1]]; try contradiction.
eexists; split; eauto.
rewrite cc_approx_val_eq. eassumption.
now eauto with Ensembles_DB.
Qed.
Lemma FV_inv_j_monotonic (k j' j : nat) (GII : GIInv) (GI : GInv) (b : Inj)
(rho1 : env) (H1 : heap block) (rho2 : env) (H2 : heap block)
(c : cTag) (Scope Funs : Ensemble var) (Γ : var) (FVs : list var) :
FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs ->
j' <= j ->
FV_inv k j' GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs.
Proof.
intros Hfv Hlt.
destruct Hfv as (Hwf & Hkey & v & vs & Hget1 & Hget2 & Hall).
split. eassumption.
split. eassumption.
repeat eexists; eauto.
eapply Forall2_P_monotonic_strong; [| eassumption ].
intros x1 x2 Hin1 Hin3 Hnp [v' [Hget Hres]]; eauto.
eexists; split; eauto.
eapply cc_approx_val_j_monotonic; eauto.
Qed.
Lemma FV_inv_monotonic (k k' j : nat) (GII : GIInv) (GI : GInv) (b : Inj)
(rho1 : env) (H1 : heap block) (rho2 : env) (H2 : heap block)
(c : cTag) (Scope Funs : Ensemble var) (Γ : var) (FVs : list var) :
FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs ->
k' <= k ->
FV_inv k' j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs.
Proof.
intros Hfv Hlt.
destruct Hfv as (Hwf & Hkey & v & vs & Hget1 & Hget2 & Hall).
split. eassumption.
split. eassumption.
repeat eexists; eauto.
eapply Forall2_P_monotonic_strong; [| eassumption ].
intros x1 x2 Hin1 Hin3 Hnp [v' [Hget Hres]]; eauto.
eexists; split; eauto.
eapply cc_approx_val_monotonic; eauto.
Qed.
Lemma FV_inv_weak_in_FV_inv k j P1 P2 rho1 H1 rho2 H2 β c Scope Funs Γ FVs :
FV_inv k j P1 P2 β rho1 H1 rho2 H2 c Scope Funs Γ FVs ->
FV_inv_weak rho1 rho2 H2 c Scope Funs Γ FVs.
Proof.
intros (Hwf & Hkey & x1 & x2 & Hget1 & Hget2 & Hall).
repeat eexists; eauto.
eapply Forall2_P_monotonic_strong; [| eassumption ].
intros ? ? ? ? ? [? [? ? ]]. eexists; eauto.
Qed.
Lemma Fun_inv_weak_in_Fun_inv k j P1 P2 rho1 H1 rho2 H2 β
Scope Funs fenv FVs :
Fun_inv k j P1 P2 β rho1 H1 rho2 H2 Scope Funs fenv FVs ->
Fun_inv_weak rho1 rho2 Scope Funs fenv.
Proof.
intros Hfun x Hin Hnin.
edestruct Hfun as (l1 & lenv & B1 & g1 & rhoc & B2 & g2 & Hget1 & Hsub (* & Hdis *)
& Hget2 & Hget3 & Hget4 & Henv & Heq); try eassumption.
repeat eexists; eauto.
Qed.
Lemma FV_inv_dom1 k P1 P2 rho1 H1 rho2 H2 b c
Scope Funs Γ FVs :
(forall j, FV_inv k j P1 P2 b rho1 H1 rho2 H2 c Scope Funs Γ FVs) ->
env_locs rho1 (FromList FVs \\ (Scope :|: Funs)) \subset dom H1.
Proof.
intros Hres l [x1 [Hgetx1 Heq1]].
destruct (M.get x1 rho1) as [ [|] | ] eqn:Hgety; try inv Heq1.
edestruct (Hres 0) as (Hwf & Hkey & vs1 & loc_env & Hget1 & Hget2 & Hall).
edestruct (@Forall2_P_exists loc) with (x := x1) as [v2 [Hin'' Hv]]; try eassumption.
now eapply Hgetx1.
now eapply Hgetx1.
destruct Hv as [v1' [Hgety' Hv']]. repeat subst_exp.
eapply cc_approx_val_dom1. eassumption. reflexivity.
Qed.
Lemma FV_inv_dom2 k P1 P2 rho1 H1 rho2 H2 b c
Scope Funs Γ FVs :
(forall j, FV_inv k j P1 P2 b rho1 H1 rho2 H2 c Scope Funs Γ FVs) ->
env_locs rho2 [set Γ] \subset dom H2.
Proof.
intros Hres l [x2 [Hgetx2 Heq1]].
destruct (M.get x2 rho2) as [ [|] | ] eqn:Hgety; try inv Heq1.
inv Hgetx2.
edestruct (Hres 0) as (Hwf & Hkey & vs1 & loc_env & Hget1 & Hget2 & Hall).
repeat subst_exp. eexists; eauto.
Qed.
Lemma FV_inv_reach1 k P1 P2 rho1 H1 rho2 H2 b c
Scope Funs Γ FVs :
(forall j, FV_inv k j P1 P2 b rho1 H1 rho2 H2 c Scope Funs Γ FVs) ->
well_formed (reach' H1 (env_locs rho1 (FromList FVs \\ (Scope :|: Funs)))) H1.
Proof.
intros Hres l1 b1 [n [_ Hp]].
edestruct post_n_exists_Singleton as [lr [Hin Hp']].
eassumption.
destruct Hin as [x1 [Hin1 Heq1]].
destruct (M.get x1 rho1) as [ [|] | ] eqn:Hgety; try inv Heq1.
edestruct (Hres (1 + n)) as (Hwf & Hkey & vs1 & loc_env & Hget1 & Hget2 & Hall).
edestruct (@Forall2_P_exists loc) with (x := x1) as [v2 [Hin Hv]]; try eassumption.
now eapply Hin1.
now eapply Hin1.
destruct Hv as [v1' [Hgety' Hv1]]. repeat subst_exp.
eapply cc_approx_val_post_n_cc with (v1 := Loc lr) (j := 1) in Hp';
[| eapply cc_approx_val_j_monotonic; try eassumption; omega ].
intros Hget.
inv Hp'.
eapply cc_approx_val_well_formed_post1 with (v1 := Loc l1) (j := 0).
eassumption. reflexivity. eassumption.
eapply Included_trans; [| eapply cc_approx_clos_post_dom1 ]; try eassumption.
rewrite post_Singleton; try eassumption. reflexivity.
Qed.
Lemma FV_inv_reach2 k j P1 P2 rho1 H1 rho2 H2 b c
Γ FVs :
FV_inv k j P1 P2 b rho1 H1 rho2 H2 c (Empty_set _) (Empty_set _) Γ FVs ->
well_formed (reach' H2 (env_locs rho2 [set Γ])) H2.
Proof.
intros (Henv & _). eassumption.
Qed.
Lemma FV_inv_image_reach k P1 P2 rho1 H1 rho2 H2 b c
Scope Funs Γ FVs :
(forall j, FV_inv k j P1 P2 b rho1 H1 rho2 H2 c Scope Funs Γ FVs) ->
image b (reach' H1 (env_locs rho1 (FromList FVs \\ (Scope :|: Funs)))) \subset
reach' H2 (post H2 (env_locs rho2 [set Γ])).
Proof.
intros Hres l' [l [Hin Heq]]; subst.
destruct Hin as [n [_ Hp]].
edestruct post_n_exists_Singleton as [l1 [Hin Hp']]; try eassumption.
edestruct (Hres n) as (Hwf & Hkey & vs1 & loc_env & Hget1 & Hget2 & Hall).
rewrite env_locs_Singleton; eauto.
simpl. rewrite post_Singleton; eauto. simpl. subst.
destruct Hin as [y [Hin' Hall']].
destruct (M.get y rho1) as [ [|] | ] eqn:Hgety; try inv Hall'.
inv Hin'.
edestruct (@Forall2_P_exists loc) with (x := y) as [v2 [Hin'' Hv]]; try eassumption.
destruct Hv as [v1' [Hgety' Hv]]. repeat subst_exp.
edestruct v2 as [ l2' |]; try contradiction.
eapply reach'_set_monotonic.
eapply In_Union_list. eapply in_map. eassumption.
eapply cc_approx_val_image_eq with (v1 := Loc l1); try eassumption;
[| eexists; split; eauto; eexists; split; eauto; now constructor ].
intros j.
edestruct (Hres j) as (vs1' & loc_env' & Hget1' & Hget2' & Hall').
repeat subst_exp.
edestruct (@Forall2_P_exists loc) with (x := y) as [v2' [Hin2' Hv']];
[| | now apply Hall' |]; try eassumption.
destruct Hv' as [v1' [Hgety' Hv']]. repeat subst_exp.
assert (Heq1 : v2' = Loc (b l1)).
{ destruct v2'; try contradiction.
destruct Hv' as [Heqv _]. subst. reflexivity. }
assert (Heq2 : l2' = b l1).
{ destruct Hv as [Heqv _]. subst. reflexivity. }
subst. repeat subst_exp. eassumption.
Qed.
Lemma FV_inv_image_reach_eq k P1 P2 rho1 H1 rho2 H2 b c
Γ FVs :
(forall j, FV_inv k j P1 P2 b rho1 H1 rho2 H2 c (Empty_set _) (Empty_set _) Γ FVs) ->
image b (reach' H1 (env_locs rho1 (FromList FVs))) <-->
reach' H2 (post H2 (env_locs rho2 [set Γ])).
Proof with (now eauto with Ensembles_DB).
intros Hres.
edestruct (Hres 0) as (Hwf & Hkey & vs1 & loc_env & Hget1 & Hget2 & Hall).
rewrite env_locs_Singleton; eauto. simpl. rewrite post_Singleton; eauto.
simpl.
eapply Forall2_P_Forall2 in Hall.
assert (Hallj : forall j, Forall2
(fun (x : var) (v2 : value) =>
exists v1 : value,
M.get x rho1 = Some v1 /\
Res (v1, H1) ≺ ^ (k; j; P1; P2; b) Res (v2, H2)) FVs vs1).
{ intros j'.
edestruct (Hres j') as (Hwf' & Hkey' & vs1' & loc_env' & Hget1' & Hget2' & Hall').
repeat subst_exp. eapply Forall2_P_Forall2. eassumption.
now eauto with Ensembles_DB. }
eapply Forall2_forall in Hallj.
clear Hget1 Hget2 Hall Hres Hkey. induction Hallj.
- normalize_sets. rewrite !env_locs_Empty_set, !reach'_Empty_set, image_Empty_set...
- simpl. normalize_sets. rewrite !env_locs_Union, !reach'_Union, !image_Union.
eapply Same_set_Union_compat.
destruct (H 0) as [v1 [Hgetx _]].
rewrite env_locs_Singleton; eauto.
eapply cc_approx_val_image_eq.
intros j.
destruct (H j) as [v1' [Hgetx' Hij]]. repeat subst_exp. eassumption.
eassumption.
- tci.
- now eauto with Ensembles_DB.
Qed.
Lemma FV_inv_heap_equiv k Scope Funs P1 P2 rho1 H1 rho2 H2 b c
Γ FVs j :
(forall j, FV_inv k j P1 P2 b rho1 H1 rho2 H2 c Scope Funs Γ FVs) ->
reach' H1 (env_locs rho1 (FromList FVs \\ (Scope :|: Funs))) |- H1 ≼ ^ (k; j; P1; P2; b) H2.
Proof with (now eauto with Ensembles_DB).
intros Hres.
edestruct (Hres 0) as (Hwf & Hkey & vs1 & loc_env & Hget1 & Hget2 & Hall).
intros l [m [_ Hp]].
edestruct post_n_exists_Singleton as [l' [Hpl Hrl]]; try eassumption.
edestruct Hpl as [x1 [Hgetx2 Hinx]].
destruct (M.get x1 rho1) as [[ l1 | ] | ] eqn:Hgetx1; try contradiction.
inv Hinx.
edestruct (Hres (m + j)) as (Hwf'' & Hkey'' & vs1'' & loc_env'' & Hget1'' & Hget2'' & Hall'').
repeat subst_exp.
inv Hgetx2.
eapply Forall2_P_exists in Hall''; try eassumption.
edestruct Hall'' as [y1 [Hnin [v1 [Hgetv1 Hcc1]]]].
repeat subst_exp.
eapply cc_approx_val_post_n_cc; eassumption.
Qed.
(* TODO move *)
Lemma FV_Union1_eq Scope Funs FVs S {_ : Decidable S}:
FV (S :|: Scope) Funs FVs <-->
S :|: FV Scope Funs FVs.
Proof.
unfold FV. rewrite <- !Union_assoc.
rewrite (Union_commut S Scope).
rewrite (Union_commut S (Scope :|: Funs)).
do 2 rewrite <- Setminus_Union.
rewrite !Union_assoc.
rewrite (Union_Setminus_Included _ _ S); tci.
rewrite (Union_Setminus_Included _ _ S); tci.
reflexivity.
now eauto with Ensembles_DB.
now eauto with Ensembles_DB.
Qed.
Lemma key_set_set {A} x (v : A) rho :
key_set (M.set x v rho) <--> x |: key_set rho.
Proof.
split; intros y; unfold In, key_set; destruct (Coqlib.peq x y); subst;
try rewrite !M.gss; eauto.
- intros _. now left.
- rewrite !M.gso; eauto. intros H.
right. eassumption.
- rewrite !M.gso; eauto. intros H.
inv H. inv H0. now exfalso; eauto. eassumption.
Qed.
Lemma FV_inv_set_not_in_FVs_l (k j : nat) (GII : GIInv) (GI : GInv) (b : Inj)
(rho1 : env) (H1 : heap block) (rho2 : env) (H2 : heap block)
(c : cTag) (Scope Funs : Ensemble var) (Γ : var) (FVs : list var) x v :
FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs ->
FV_inv k j GII GI b (M.set x v rho1) H1 rho2 H2 c (x |: Scope) Funs Γ FVs.
Proof.
intros (Hwf & Hkey & x1 & x2 & Hget1 & Hget2 & Hall).
split; eauto. split; eauto.
rewrite key_set_set, FV_Union1_eq, Hkey. reflexivity.
now tci.
repeat eexists; eauto.
eapply Forall2_P_monotonic_strong; [| eapply Forall2_P_monotonic;
[ eassumption |] ].
intros y1 v2 Hin Hnin Hp [v1 [Hget Hall1]].
eexists; split; eauto.
rewrite M.gso; eauto.
intros Hc; subst. eapply Hp; eauto. now left; left.
now eauto with Ensembles_DB.
Qed.
Lemma FV_inv_set_not_in_FVs_r (k j : nat) (GII : GIInv) (GI : GInv) (b : Inj)
(rho1 : env) (H1 : heap block) (rho2 : env) (H2 : heap block)
(c : cTag) (Scope Funs : Ensemble var) (Γ : var) (FVs : list var) x v :
FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs ->
x <> Γ ->
FV_inv k j GII GI b rho1 H1 (M.set x v rho2) H2 c Scope Funs Γ FVs.
Proof.
intros (Hwf & Hkey & x1 & x2 & Hget1 & Hget2 & Hall) Hnin.
split; eauto.
rewrite env_locs_set_not_In; eauto. now intros Hc; inv Hc; eauto.
split. eassumption.
rewrite M.gso; eauto.
Qed.
Lemma FV_inv_set_not_in_FVs (k j : nat) (GII : GIInv) (GI : GInv) (b : Inj)
(rho1 : env) (H1 : heap block) (rho2 : env) (H2 : heap block)
(c : cTag) (Scope Funs : Ensemble var) (Γ : var) (FVs : list var) x y v v' :
FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs ->
y <> Γ ->
FV_inv k j GII GI b (M.set x v rho1) H1 (M.set y v' rho2) H2 c (x |: Scope) Funs Γ FVs.
Proof.
intros. eapply FV_inv_set_not_in_FVs_r; eauto.
eapply FV_inv_set_not_in_FVs_l; eauto.
Qed.
(** [FV_inv] is heap monotonic *)
Lemma FV_inv_heap_mon (k j : nat) (GII : GIInv) (GI : GInv) (b : Inj)
(rho1 : env) (H1 H1' : heap block) (rho2 : env) (H2 H2' : heap block)
(c : cTag) (Scope Funs : Ensemble var) (Γ : var) (FVs : list var) :
H1 ⊑ H1' ->
H2 ⊑ H2' ->
(forall j, FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs ) ->
FV_inv k j GII GI b rho1 H1' rho2 H2' c Scope Funs Γ FVs.
Proof.
intros Hs1 Hs2.
intros Henv. edestruct (Henv 0) as (Hwf & Hkey & x1 & x2 & Hget1 & Hget2 & Hall).
split; [| split ].
- rewrite <- reach'_subheap.
eapply well_formed_subheap.
eassumption.
eapply reachable_in_dom.
eassumption.
rewrite env_locs_Singleton; eauto. eapply Singleton_Included.
eexists; eassumption.
eassumption. eassumption.
rewrite env_locs_Singleton; eauto. eapply Singleton_Included.
eexists; eassumption.
eassumption.
- eassumption.
- repeat eexists; eauto.
eapply Forall2_P_monotonic_strong; [| eassumption ].
intros y1 v2 Hin1 Hin2 Hp [v1 [Hget3 Hrel]].
eexists; split; eauto.
eapply cc_approx_val_heap_monotonic; try eassumption.
intros j'.
edestruct (Henv j') as (Hwf' & Hkey' & x1' & x2' & Hget1' & Hget2' & Hall').
repeat subst_exp.
edestruct (Forall2_P_exists _ _ _ _ _ Hin1 Hp Hall') as [v1' [Hin' [v2' [Hget2' Hp']]]]. repeat subst_exp.
destruct v2'; [| contradiction ].
eapply cc_approx_val_loc_eq in Hrel. subst.
assert (Hrel := Hp').
eapply cc_approx_val_loc_eq in Hrel. subst.
eassumption.
Qed.
(** [FV_inv] under rename extension *)
Lemma FV_inv_rename_ext (k j : nat) (GII : GIInv) (GI : GInv) (b b' : Inj)
(rho1 : env) (H1 H2 : heap block) (rho2 : env)
(c : cTag) (Scope Funs : Ensemble var) (Γ : var) (FVs : list var) :
FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs ->
f_eq_subdomain (reach' H1 (env_locs rho1 (FromList FVs \\ (Scope :|: Funs)))) b' b ->
FV_inv k j GII GI b' rho1 H1 rho2 H2 c Scope Funs Γ FVs.
Proof.
intros (Hwf & Hkey & x1 & x2 & Hget1 & Hget2 & Hall) Hfeq.
split. eassumption. split. eassumption. repeat eexists; eauto.
eapply Forall2_P_monotonic_strong; [| eassumption ].
intros y1 v2 Hin1 Hin2 Hp [v1 [Hget3 Hrel]].
eexists; split; eauto.
eapply cc_approx_val_rename_ext; try eassumption.
eapply f_eq_subdomain_antimon; try eassumption.
eapply reach'_set_monotonic.
eapply get_In_env_locs; eauto.
constructor; eauto.
Qed.
(** [FV_inv] monotonic *)
(* Lemma FV_inv_Scope_mon (k j : nat) (GII : GIInv) (GI : GInv) (b : Inj) *)
(* (rho1 : env) (H1 H2 : heap block) (rho2 : env) *)
(* (c : cTag) (Scope Scope' Funs : Ensemble var) (Γ : var) (FVs : list var) : *)
(* FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs -> *)
(* Scope \subset Scope' -> *)
(* FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope' Funs Γ FVs. *)
(* Proof. *)
(* intros (Hwf & Hkey & x1 & x2 & Hget1 & Hget2 & Hall) Hfeq. *)
(* split. eassumption. split. eassumption. repeat eexists; eauto. *)
(* eapply Forall2_P_monotonic. eassumption. *)
(* now eauto with Ensembles_DB. *)
(* Qed. *)
(* Lemma FV_inv_Funs_mon (k j : nat) (GII : GIInv) (GI : GInv) (b : Inj) *)
(* (rho1 : env) (H1 H2 : heap block) (rho2 : env) *)
(* (c : cTag) (Scope Funs Funs' : Ensemble var) (Γ : var) (FVs : list var) : *)
(* FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs -> *)
(* Funs \subset Funs' -> *)
(* FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs' Γ FVs. *)
(* Proof. *)
(* intros (Hwf & Hkey & x1 & x2 & Hget1 & Hget2 & Hall) Hfeq. *)
(* split. eassumption. split. eassumption. repeat eexists; eauto. *)
(* eapply Forall2_P_monotonic. eassumption. *)
(* now eauto with Ensembles_DB. *)
(* Qed. *)
(* Lemma FV_inv_mon (k j : nat) (GII : GIInv) (GI : GInv) (b : Inj) *)
(* (rho1 : env) (H1 H2 : heap block) (rho2 : env) *)
(* (c : cTag) (Scope Scope' Funs Funs' : Ensemble var) (Γ : var) (FVs : list var) : *)
(* FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs -> *)
(* Scope :|: Funs \subset Scope' :|: Funs' -> *)
(* FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope' Funs' Γ FVs. *)
(* Proof. *)
(* intros (Hwf & x1 & x2 & Hget1 & Hget2 & Hall) Hfeq. *)
(* split. eassumption. repeat eexists; eauto. *)
(* eapply Forall2_P_monotonic. eassumption. *)
(* now eauto with Ensembles_DB. *)
(* Qed. *)
Lemma FV_inv_FV_eq (k j : nat) (GII : GIInv) (GI : GInv) (b : Inj)
(rho1 : env) (H1 H2 : heap block) (rho2 : env)
(c : cTag) (Scope Scope' Funs Funs' : Ensemble var)
{_ : ToMSet Scope} {_ : ToMSet Scope'}
(Γ : var) FVs :
FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs ->
Scope :|: Funs <--> Scope' :|: Funs' ->
FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope' Funs' Γ FVs.
Proof.
intros (Hwf & Hkey & x1 & x2 & Hget1 & Hget2 & Hall) Hfeq.
split. eassumption. split.
unfold FV in *.
rewrite <- Hfeq. rewrite (Union_Setminus_Included Scope' Funs'), <- Hfeq.
rewrite <- (Union_Setminus_Included Scope Funs) at 1.
eassumption. tci. reflexivity. tci. reflexivity.
repeat eexists; eauto.
eapply Forall2_P_monotonic. eassumption.
rewrite Hfeq. reflexivity.
Qed.
Instance Proper_FV_inv_Funs k j GI GP b rho1 H1 rho2 H2 c Scope :
Proper (Same_set _ ==> eq ==> eq ==> iff)
(FV_inv k j GI GP b rho1 H1 rho2 H2 c Scope).
Proof.
intros S1 S2 Hseq x1 x2 Heq1 y1 y2 Heq2; subst.
split; intros (Hwf & Hkey & vs & l & Hget1 & Hget2 & Hall1).
split. eassumption. split. unfold FV. rewrite <- !Hseq at 1. eassumption.
do 2 eexists.
split. eassumption.
split. eassumption.
eapply Forall2_P_monotonic; eauto. rewrite Hseq. reflexivity.
split. eassumption. split. unfold FV. rewrite !Hseq at 1. eassumption.
do 2 eexists.
split. eassumption.
split. eassumption.
eapply Forall2_P_monotonic; eauto. rewrite Hseq. reflexivity.
Qed.
Instance Proper_FV_inv_Scope k j GI GP b rho1 H1 rho2 H2 c :
Proper (Same_set _ ==> eq ==> eq ==> eq ==> iff)
(FV_inv k j GI GP b rho1 H1 rho2 H2 c).
Proof.
intros S1 S2 Hseq x1 x2 Heq1 y1 y2 Heq2 z1 z2 Heq3; subst.
split; intros (Hwf & Hkey & vs & l & Hget1 & Hget2 & Hall1).
split. eassumption. split. unfold FV. rewrite <- !Hseq at 1.
eassumption.
do 2 eexists.
split. eassumption.
split. eassumption.
eapply Forall2_P_monotonic; eauto. rewrite Hseq. reflexivity.
split. eassumption. split. unfold FV. rewrite !Hseq at 1. eassumption.
do 2 eexists.
split. eassumption.
split. eassumption.
eapply Forall2_P_monotonic; eauto. rewrite Hseq. reflexivity.
Qed.
Lemma Fun_inv_image_reach k P1 P2 rho1 H1 rho2 H2 b
Scope Funs fenv FVs :
(forall j, Fun_inv k j P1 P2 b rho1 H1 rho2 H2 Scope Funs fenv FVs) ->
image b (reach' H1 (post H1 (env_locs rho1 (Funs \\ Scope)))) \subset
reach' H2 (env_locs rho2 (image fenv (Funs \\ Scope))).
Proof.
intros Hres l' [l [Hin Heq]].
destruct Hin as [n [_ Hp]].
edestruct post_n_exists_Singleton as [l1 [Hin Hp']]; try eassumption.
edestruct Hin as [l2 [b1 [Henv [Hgetl1 Hinl1]]]].
edestruct Henv as [x1 [Hinx Hm]].
destruct (M.get x1 rho1) as [[l3|] | ] eqn:Hgetx; inv Hm.
inv Hinx.
edestruct (Hres n) as (l1' & lenv & l2' & g1 & rhoc & B2 & g2 & Hget1 & Hdis' (* & Hsub *)
& Hget2 & Hget3 & Hget4 & Henv' & Heq').
eassumption. eassumption.
repeat subst_exp.
simpl in Hinl1.
rewrite Union_Empty_set_neut_l in Hinl1.
inv Hinl1.
eapply reach'_set_monotonic; [| eapply cc_approx_clos_image_eq ].
eapply Singleton_Included. eexists (fenv x1). split.
eexists. split; [| reflexivity ]. now constructor; eauto.
rewrite Hget4. reflexivity.
intros j.
edestruct (Hres j) as (l1'' & lenv' & l2'' & g1' & rhoc' & B2' & g2' & Hget1' & Hdis'' (* & Hsub *)
& Hget2' & Hget3' & Hget4' & Henv'' & Heq'').
eassumption. eassumption.
repeat subst_exp. eassumption.
eexists. split; [| reflexivity ]. eexists; split; try eassumption. now constructor.
Qed.
Lemma FV_image_reach k P1 P2 rho1 H1 rho2 H2 b c
Scope Funs Γ fenv FVs :
(forall j, (H1, rho1) ⋞ ^ (Scope; k; j; P1; P2; b) (H2, rho2)) ->
(forall j, Fun_inv k j P1 P2 b rho1 H1 rho2 H2 Scope Funs fenv FVs) ->
(forall j, FV_inv k j P1 P2 b rho1 H1 rho2 H2 c Scope Funs Γ FVs) ->
image b (reach' H1 (env_locs rho1 (FV Scope Funs FVs)) \\ env_locs rho1 (Funs \\ Scope)) \subset
reach' H2 (env_locs rho2 (Scope :|: image fenv (Funs \\ Scope) :|: [set Γ])).
Proof with (now eauto with Ensembles_DB).
intros Hcc Hfun Henv l' [l [Hin Heq]]; subst.
unfold FV in Hin.
rewrite !env_locs_Union, !reach'_Union, !Setminus_Union_distr in Hin.
inv Hin. inv H.
+ eapply reach'_set_monotonic; [| eapply cc_approx_env_image_reach_included; try eassumption ].
eapply env_locs_monotonic...
eexists. split; eauto. inv H0. eassumption.
+ rewrite !env_locs_Union, !reach'_Union. left. right.
eapply Fun_inv_image_reach. eassumption.
eexists. split; eauto.
rewrite reach_unfold, Setminus_Union_distr in H0.
rewrite Setminus_Same_set_Empty_set, Union_Empty_set_neut_l in H0.
inv H0; eassumption.
+ rewrite !env_locs_Union, !reach'_Union. right.
rewrite reach_unfold. right.
eapply FV_inv_image_reach. eassumption.
eexists; split; eauto.
inv H. eassumption.
Qed.
Lemma def_closures_FV_inv' Scope Funs FVs Γ k j GIP GP b B1 B2 envc c rho1 H1 rho1' H1' rho2 H2 :
(forall j, FV_inv k j GIP GP b rho1 H1 rho2 H2 c Scope Funs Γ FVs) ->
def_closures B1 B2 rho1 H1 envc = (H1', rho1') ->
FV_inv k j GIP GP b rho1' H1' rho2 H2 c (name_in_fundefs B1 :|: Scope) Funs Γ FVs.
Proof with (now eauto with Ensembles_DB).
revert H1 rho1 H1' rho1' j.
induction B1; intros H1 rho1 H1' rho1' j Hfv Hdef.
- simpl in Hdef.
destruct (def_closures B1 B2 rho1 H1) as (H1'', rho1'') eqn:Hdef'.
destruct (alloc (Clos _ _) H1'') as [la H1a] eqn:Hal.
inv Hdef.
simpl. eapply Proper_FV_inv_Scope. rewrite <- Union_assoc. reflexivity. reflexivity.
reflexivity. reflexivity.
eapply FV_inv_set_not_in_FVs_l.
eapply FV_inv_heap_mon; [ | | ].
* eapply HL.alloc_subheap. eassumption.
* eapply HL.subheap_refl.
* intros j'.
eapply IHB1 in Hdef'.
eassumption.
eassumption.
- inv Hdef. simpl.
eapply Proper_FV_inv_Scope. rewrite Union_Empty_set_neut_l. reflexivity.
reflexivity. reflexivity. reflexivity. auto.
Qed.
Lemma def_funs_FV_inv Scope Funs Γ FVs c k j GIP GP b B1 B2 rho1 H1 rho2 H2 :
FV_inv k j GIP GP b rho1 H1 rho2 H2 c Scope Funs Γ FVs ->
name_in_fundefs B1 \subset Scope :|: Funs ->
~ Γ \in name_in_fundefs B1 ->
FV_inv k j GIP GP b rho1 H1 (def_funs B1 B2 rho2) H2 c Scope Funs Γ FVs.
Proof with (now eauto with Ensembles_DB).
induction B1; intros Hcc Hsub Hnin.
- simpl def_funs.
eapply FV_inv_set_not_in_FVs_r.
eapply IHB1. eassumption.
eapply Included_trans; [| eassumption ]...
intros Hc. eapply Hnin; now right.
intros Hc; inv Hc. eapply Hnin; now left.
- simpl. eassumption.
Qed.
Lemma FV_inv_env_constr k j PG QG b rho1 H1 rho2 H2 c FVs Γ lenv vs1 vs2 :
key_set rho1 <--> FromList FVs ->
M.get Γ rho2 = Some (Loc lenv) ->
get lenv H2 = Some (Constr c vs2) ->
getlist FVs rho1 = Some vs1 ->
(forall j, Forall2
(fun v1 v2 : value =>
Res (v1, H1) ≺ ^ (k; j; PG; QG; b) Res (v2, H2)) vs1 vs2) ->
FV_inv k j PG QG b rho1 H1 rho2 H2 c (Empty_set _) (Empty_set _) Γ FVs.
Proof.
intros Hkey Hget1 Hget2 Hgl Hall.
split; [| split ].
- rewrite env_locs_Singleton; [| eassumption ]. simpl.
rewrite reach_unfold. eapply well_formed_Union.
+ intros x bl Hinx Hget. inv Hinx. repeat subst_exp. simpl.
eapply Forall2_dom2. exact 0. eassumption. eassumption. (* XXX redundant params *)
eapply Forall2_forall. tci. eassumption.
+ rewrite post_Singleton; [| eassumption ]. simpl.
eapply Forall2_reach2. eassumption. exact Some. (* XXX redundant params *)
eapply Forall2_forall. tci. eassumption.
- rewrite Hkey.
+ unfold FV. rewrite !Union_Empty_set_neut_l, !Setminus_Empty_set_neut_r, Union_Empty_set_neut_l.
reflexivity.
- do 2 eexists. split; [| split ]; try eassumption.
specialize (Hall j). revert Hgl Hall. clear.
intros Hgl Hall. revert FVs Hgl.
induction Hall; intros FVs Hgl.
+ destruct FVs as [| x FVs ]; try inv Hgl.
now constructor.
destruct (M.get x rho1) eqn:Hgetx; try congruence.
destruct (getlist FVs rho1) eqn:Hgetlst; try congruence.
+ destruct FVs as [| z FVs ]; try inv Hgl.
destruct (M.get z rho1) eqn:Hgetx; try congruence.
destruct (getlist FVs rho1) eqn:Hgetlst; try congruence.
inv H3. constructor; eauto.
Qed.
(** * Lemmas about [Fun_inv] *)
Lemma Fun_inv_set_r k j GI GP b rho1 H1 rho2 H2 Scope Funs fenv FVs f v :
Fun_inv k j GI GP b rho1 H1 rho2 H2 Scope Funs fenv FVs ->
~ f \in (Funs \\ Scope) -> ~ f \in (image fenv (Funs \\ Scope)) ->
Fun_inv k j GI GP b rho1 H1 (M.set f v rho2) H2 Scope Funs fenv FVs.
Proof.
intros Hfun Hnin1 Hnin2 x Hnin Hin.
edestruct Hfun as (l1 & lenv & B1 & g1 & rhoc & B2 & g2 & Hget1 & Hsub (* & Hdis *)
& Hget2 & Hget3 & Hget4 & Henv & Heq).
eassumption. eassumption.
destruct Henv as [Hbeq Henv]. subst.
do 7 eexists. repeat split; try eassumption. rewrite M.gso. eassumption.
intros Hc. subst. eapply Hnin1; eauto. now constructor; eauto.
rewrite M.gso; try eassumption.
intros Hc; subst. eapply Hnin2. eexists; split; constructor; eauto.
Qed.
Lemma Fun_inv_set_l k j GI GP b rho1 H1 rho2 H2 Scope Funs fenv FVs f v :
Fun_inv k j GI GP b rho1 H1 rho2 H2 Scope Funs fenv FVs ->
Disjoint _ (val_loc v) (dom H1) ->
(* post H1 (val_loc v) \subset reach' H1 (env_locs rho1 Scope) -> *)
Fun_inv k j GI GP b (M.set f v rho1) H1 rho2 H2 (f |: Scope) Funs fenv FVs.
Proof with (now eauto with Ensembles_DB).
intros Hfun Hnin1 (* Hin1 *) x Hnin Hin.
edestruct Hfun as (l1 & lenv & B1 & g1 & rhoc & B2 & g2 & Hget1 & Hsub (* & Hdis *)
& Hget2 & Hget3 & Hget4 & Henv & Heq).
intros Hc. eapply Hnin. right. eassumption. eassumption.
destruct Henv as [Hbeq Henv]. subst.
do 7 eexists. repeat split; try eassumption. rewrite M.gso. eassumption.
intros Hc. subst. eapply Hnin; now eauto.
repeat subst_exp.
intros Hc; subst. eapply Hsub.
rewrite reach'_Union in *. inv Hc; [| now eauto ].
left.
eapply reach'_set_monotonic in H; [| eapply env_locs_set_Inlcuded' ].
rewrite reach'_Union in H. inv H.
- rewrite reach_unfold in H0. inv H0.
+ exfalso. eapply Hnin1. constructor; eauto. eexists; eauto.
+ rewrite post_Disjoint in H; [| eassumption ].
rewrite reach'_Empty_set in H.
now inv H.
- eapply reach'_set_monotonic; [| eassumption ].
eapply env_locs_monotonic. unfold FV.
rewrite !Setminus_Union_distr.
eapply Included_Union_compat; [| now eauto with Ensembles_DB ].
eapply Included_Union_compat; [| now eauto with Ensembles_DB ].
rewrite Setminus_Union, (Union_commut [set x]), <- Setminus_Union.
rewrite Setminus_Same_set_Empty_set. rewrite Setminus_Empty_set_abs_r...
Qed.
Lemma Fun_inv_set_l_alt k j GI GP b rho1 H1 rho2 H2 Scope Funs fenv FVs f v :
Fun_inv k j GI GP b rho1 H1 rho2 H2 Scope Funs fenv FVs ->
val_loc v \subset reach' H1 (env_locs rho1 Scope) ->
(* f \in Scope -> *)
Fun_inv k j GI GP b (M.set f v rho1) H1 rho2 H2 (f |: Scope) Funs fenv FVs.
Proof with (now eauto with Ensembles_DB).
intros Hfun Hnin1 x Hnin Hin.
edestruct Hfun as (l1 & lenv & B1 & g1 & rhoc & B2 & g2 & Hget1 & Hsub (* & Hdis *)
& Hget2 & Hget3 & Hget4 & Henv & Heq).
intros Hc. eapply Hnin. right. eassumption. eassumption.
destruct Henv as [Hbeq Henv]. subst.
do 7 eexists. repeat split; try eassumption. rewrite M.gso. eassumption.
intros Hc. subst. eapply Hnin; now eauto.
repeat subst_exp.
intros Hc; subst. eapply Hsub.
rewrite reach'_Union in *. inv Hc; [| now eauto ].
left.
eapply reach'_set_monotonic in H; [| eapply env_locs_set_Inlcuded' ].
rewrite reach'_Union in H. inv H.
- rewrite reach'_idempotent. eapply reach'_set_monotonic; [| eassumption ].
eapply Included_trans. eassumption.
eapply reach'_set_monotonic. eapply env_locs_monotonic.
unfold FV. rewrite !Setminus_Union_distr. do 2 eapply Included_Union_preserv_l.
rewrite Setminus_Disjoint. reflexivity. eapply Disjoint_Singleton_r. eauto.
- eapply reach'_set_monotonic; [| eassumption ].
eapply env_locs_monotonic.
eapply Included_trans. eapply Included_Setminus_compat.
eapply Included_Setminus_compat. eapply FV_Union1.
reflexivity. reflexivity.
rewrite Setminus_Union. rewrite (Union_commut [set x] [set f]), <- Setminus_Union.
rewrite Setminus_Union_distr. rewrite Setminus_Same_set_Empty_set, Union_Empty_set_neut_l...
Qed.
Lemma Fun_inv_Scope_monotonic k j GI GP b rho1 H1 rho2 H2 Scope S Funs Γ FVs {_ : Decidable S}:
Fun_inv k j GI GP b rho1 H1 rho2 H2 Scope Funs Γ FVs ->
FV (S :|: Scope) Funs FVs <--> FV Scope Funs FVs ->
Fun_inv k j GI GP b rho1 H1 rho2 H2 (S :|: Scope) Funs Γ FVs.
Proof with (now eauto with Ensembles_DB).
intros Hfun Heq y Hin Hnin.
edestruct Hfun as (l1 & lenv & B1 & g1 & rhoc & B2 & g2 & Hget1 & Hsub (* & Hdis *)
& Hget2 & Hget3 & Hget4 & Henv & Heq').
now eauto. eassumption.
destruct Henv as [Hbeq Henv]. subst.
do 7 eexists. repeat split; try eassumption.
intros Hc. eapply Hsub. rewrite <- Heq. eassumption.
Qed.
Lemma Fun_inv_monotonic k k' j GI GP b rho1 H1 rho2 H2 Scope Funs fenv FVs :
Fun_inv k j GI GP b rho1 H1 rho2 H2 Scope Funs fenv FVs ->
k' <= k ->
Fun_inv k' j GI GP b rho1 H1 rho2 H2 Scope Funs fenv FVs.
Proof with (now eauto with Ensembles_DB).
intros Hfun Hleq x Hin Hnin.
edestruct Hfun as (l1 & lenv & B1 & g1 & rhoc & B2 & g2 & Hget1 & Hsub (* & Hdis *)
& Hget2 & Hget3 & Hget4 & Henv & Heq).
eassumption. eassumption.
do 7 eexists. repeat (split; [ eassumption |]). split.
eapply cc_approx_clos_monotonic; eassumption.
destruct (alloc (Constr Size.Util.clo_tag [FunPtr B2 g2; Loc B1]) H2).
eapply cc_approx_val_monotonic; eassumption.
Qed.
Lemma Fun_inv_Scope_monotonic' k j GI GP b rho1 H1 rho2 H2 Scope S Funs Γ FVs {_ : Decidable S}:
Fun_inv k j GI GP b rho1 H1 rho2 H2 Scope Funs Γ FVs ->
FV (S :|: Scope) (Funs \\ S) FVs <--> FV Scope Funs FVs ->
Fun_inv k j GI GP b rho1 H1 rho2 H2 (S :|: Scope) (Funs \\ S) Γ FVs.
Proof with (now eauto with Ensembles_DB).
intros Hfun Heq y Hin Hnin.
edestruct Hfun as (l1 & lenv & B1 & g1 & rhoc & B2 & g2 & Hget1 & Hsub (* & Hdis *)
& Hget2 & Hget3 & Hget4 & Henv & Heq').
now eauto. inv Hnin. eassumption.
destruct Henv as [Hbeq Henv]. subst.
do 7 eexists. repeat split; try eassumption.
intros Hc. eapply Hsub. rewrite <- Heq. eassumption.
Qed.
Lemma Fun_inv_dom1 k GI GP rho1 H1 rho2 H2 b
Scope Funs Γ FVs :
(forall j, Fun_inv k j GI GP b rho1 H1 rho2 H2 Scope Funs Γ FVs) ->
env_locs rho1 (Funs \\ Scope) \subset dom H1.
Proof.
intros Hres l [x1 [Hgetx1 Heq1]].
destruct (M.get x1 rho1) as [ [|] | ] eqn:Hgety; try inv Heq1.
edestruct (Hres 0) as (l1 & lenv & B1 & g1 & rhoc & B2 & g2 & Hget1 & Hsub (* & Hdis *)
& Hget2 & Hget3 & Hget4 & Henv & Heq).
now eapply Hgetx1. now eapply Hgetx1.
destruct Henv as [Hbeq Henv]. subst.
edestruct (alloc (Constr Size.Util.clo_tag [FunPtr B2 g2; Loc (b lenv)]) H2) as [l2 H2'] eqn:Ha.
repeat subst_exp.
eapply cc_approx_val_dom1. eassumption. reflexivity.
Qed.
Lemma Fun_inv_dom2 k GI GP rho1 H1 rho2 H2 b
Scope Funs Γ FVs :
(forall j, Fun_inv k j GI GP b rho1 H1 rho2 H2 Scope Funs Γ FVs) ->
env_locs rho2 (Funs \\ Scope) \subset dom H2.
Proof.
intros Hres l [x2 [Hgetx1 Heq1]].
destruct (M.get x2 rho2) as [ [|] | ] eqn:Hgety; try inv Heq1.
edestruct (Hres 0) as (l1 & lenv & B1 & g1 & rhoc & B2 & g2 & Hget1 & Hsub (* & Hdis *)
& Hget2 & Hget3 & Hget4 & Henv & Heq).
now eapply Hgetx1. now eapply Hgetx1.
repeat subst_exp.
Qed.
Lemma Fun_inv_reach1 k GI GP rho1 H1 rho2 H2 b
Scope Funs Γ FVs :
(forall j, Fun_inv k j GI GP b rho1 H1 rho2 H2 Scope Funs Γ FVs) ->
well_formed (reach' H1 (env_locs rho1 (Funs \\ Scope))) H1.
Proof.
intros Hres l b1 [n [_ Hp]] Hget.
edestruct post_n_exists_Singleton as [lr [Hin' Hp']].
eassumption.
destruct Hin' as [x1 [Hin1 Heq1]].
destruct (M.get x1 rho1) as [ [|] | ] eqn:Hgety; try inv Heq1.
edestruct (Hres (1 + n))
as (l1 & lenv & B1 & g1 & rhoc & B2 & g2 & Hget1 & Hsub (* & Hdis *)
& Hget2 & Hget3 & Hget4 & Henv & Heq).
now eapply Hin1. now eapply Hin1. repeat subst_exp.
destruct Henv as [Hbeq Henv]. subst.
assert (Hp'' := Hp').
edestruct (alloc (Constr Size.Util.clo_tag [FunPtr B2 g2; Loc (b lenv)]) H2) as [l2 H2'] eqn:Ha.
eapply cc_approx_val_post_n_cc with (v1 := Loc l1) (j := 1) in Hp';
[| eapply cc_approx_val_j_monotonic; try eassumption; omega ].
intros Hget1.
eapply cc_approx_val_well_formed_post1 with (v1 := Loc l1) (j := n); try eassumption.
eapply cc_approx_val_j_monotonic. eassumption. omega.
Qed.
Lemma Fun_inv_reach2 k GI GP rho1 H1 rho2 H2 b
Scope Funs Γ FVs :
(forall j, Fun_inv k j GI GP b rho1 H1 rho2 H2 Scope Funs Γ FVs) ->
well_formed (reach' H2 (env_locs rho2 (Funs \\ Scope))) H2.
Proof.
intros Hres l b1 [n [_ Hp]] Hget.
edestruct post_n_exists_Singleton as [lr [Hin' Hp']].