-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathclosure_conversion_correct.v
2326 lines (2004 loc) · 118 KB
/
closure_conversion_correct.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
invariants 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 ClosureConversionCorrect (H : Heap).
Module Inv := Invariants H.
Import H Inv.Size.Util.C.LR.Sem.GC.Equiv Inv.Size.Util.C.LR.Sem.GC.Equiv.Defs
Inv.Size.Util.C.LR.Sem.GC Inv.Size.Util.C.LR.Sem Inv.Size.Util.C.LR
Inv.Size.Util.C Inv.Size.Util Inv.Size Inv.
Definition ct := Inv.Size.Util.clo_tag.
(** * Lemmas about [project_var] and [project_vars] *)
(** Correctness of [project_var] *)
Lemma project_var_correct GII GI k H1 rho1 H2 rho2 H2' rho2' b
Scope {_ : ToMSet Scope} Scope' Funs Funs' c Γ fenv FVs x C m :
(* well-formedness *)
project_var ct Scope Funs fenv c Γ FVs x C Scope' Funs' ->
(forall j, (H1, rho1) ⋞ ^ (Scope; k; j; GII; GI; b) (H2, rho2)) ->
(forall j, Fun_inv k j GII GI b rho1 H1 rho2 H2 Scope Funs fenv FVs) ->
(forall j, FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs) ->
Disjoint _ (Γ |: image fenv (Funs \\ Scope)) (FV Scope Funs FVs) ->
ctx_to_heap_env_CC C H2 rho2 H2' rho2' m ->
binding_in_map Scope rho1 ->
exists b',
(forall j, (H1, rho1) ⋞ ^ (Scope'; k; j; GII; GI; b') (H2', rho2')) /\
(forall j, Fun_inv k j GII GI b' rho1 H1 rho2' H2' Scope' Funs' fenv FVs) /\
(forall j, FV_inv k j GII GI b' rho1 H1 rho2' H2' c Scope' Funs' Γ FVs).
Proof with (now eauto with Ensembles_DB).
intros Hproj Hcc Hfun Hfv Hdis Hctx Hbin.
inv Hproj.
- inv Hctx. eexists. repeat (split; [ eassumption | ]). eassumption.
- inv Hctx. simpl in H13.
destruct (M.get x rho2) as [v1|] eqn:Hgetx; try congruence.
destruct (M.get (fenv x) rho2) as [v2|] eqn:Hgetg; try congruence. inv H13.
inv H14. inv H15.
edestruct (Hfun 0)
as (l1 & lenv & B1 & g1 & rhoc & B2 & g2 & Hget1 & Hdis'
& Hget2 & Hget3 & Hget4 & Henv & Heq);
try eassumption.
repeat subst_exp.
edestruct (alloc (Constr Inv.Size.Util.clo_tag
[FunPtr B2 g2; Loc lenv]) H2) as [l' H2''] eqn:Ha. inv H4.
assert (Hseq : FV (x |: Scope) Funs FVs <--> FV Scope Funs FVs).
{ unfold FV. rewrite <- (Union_assoc [set x] Scope Funs) at 1.
rewrite !(Union_commut [set x]) at 2.
rewrite !(Union_commut [set x] (Scope :|: Funs)) at 1.
do 2 rewrite <- Setminus_Union.
rewrite Union_Setminus_Included; try eauto with Ensembles_DB typeclass_instances.
rewrite (Union_Setminus_Included _ (Funs \\ Scope));
try eauto with Ensembles_DB typeclass_instances.
rewrite <- !Union_assoc.
rewrite Union_Same_set. reflexivity. eapply Singleton_Included.
right. left. constructor; eauto. }
assert (Hseq' : FV (x |: Scope) (Funs \\ [set x]) FVs <--> FV Scope Funs FVs).
{ unfold FV.
rewrite (Union_Setminus_Included (x |: Scope) Funs); tci; [| now eauto with Ensembles_DB ].
rewrite Setminus_Union. rewrite (Union_Same_set [set x] (x |: Scope)); [| now eauto with Ensembles_DB ].
rewrite (Union_Setminus_Included (x |: Scope) Funs); tci; [| now eauto with Ensembles_DB ].
rewrite <- (Union_assoc [set x] Scope Funs) at 2.
rewrite !(Union_commut [set x] (Scope :|: Funs)) at 1.
do 2 rewrite <- Setminus_Union.
rewrite Union_Setminus_Included; try eauto with Ensembles_DB typeclass_instances.
rewrite (Union_Setminus_Included Scope Funs); tci; [| now eauto with Ensembles_DB ].
rewrite !Setminus_Union.
rewrite <- !Union_assoc.
rewrite Union_Same_set. reflexivity. eapply Singleton_Included.
right. left. eassumption. }
exists (b {l1 ~> l}). split; [| split ].
+ intros j.
edestruct (Hfun j)
as (l1' & lenv' & B1' & g1' & rhoc' & B2' & g2' & Hget1' & Hdis'' & (* Hsub' & *)
Hget2' & Hget3' & Hget4' & Henv' & Heq');
try eassumption. unfold ct in *.
repeat subst_exp. rewrite H5 in Heq'. eapply cc_approx_env_P_union.
* intros y Hin. inv Hin. intros v1 Hget. repeat subst_exp.
eexists. rewrite M.gss. split. reflexivity.
eassumption.
* eapply cc_approx_env_P_set_not_in_P_r; [| eassumption ].
eapply cc_approx_env_heap_monotonic.
eapply HL.subheap_refl.
eapply HL.alloc_subheap. eassumption.
intros j'.
eapply cc_approx_env_rename_ext with (β := b).
now eapply Hcc.
eapply f_eq_subdomain_extend_not_In_S_r.
intros Hc. eapply Fun_inv_locs_Disjoint1. eapply (Hfun 0).
now constructor; eauto.
constructor; try eassumption.
eapply get_In_env_locs. now constructor; eauto. eassumption. reflexivity.
eapply reach'_set_monotonic; [| eassumption ].
eapply env_locs_monotonic... reflexivity.
+ intros j.
eapply Fun_inv_set_r; [ eapply Fun_inv_rename_ext | | ].
* eapply Fun_inv_subheap; try rewrite Hseq; try eassumption.
eapply well_formed_antimon; [| eapply FV_reach1; try eassumption; now tci ].
eapply reach'_set_monotonic. eapply env_locs_monotonic.
eapply Included_trans. eapply FV_Union1.
eapply Included_trans. eapply Included_Union_compat. reflexivity.
eapply FV_Setminus2. tci. rewrite Union_Same_set; [| now eauto with Ensembles_DB ].
eapply Union_Included; [| reflexivity ].
unfold FV. eapply Singleton_Included.
left; right. now constructor; eauto.
eapply Included_trans; [| eapply FV_dom1; try eassumption; now tci ].
eapply env_locs_monotonic.
eapply Included_trans. eapply FV_Union1.
eapply Included_trans. eapply Included_Union_compat. reflexivity.
eapply FV_Setminus2. tci. rewrite Union_Same_set; [| now eauto with Ensembles_DB ].
eapply Union_Included; [| reflexivity ].
unfold FV. eapply Singleton_Included.
left; right. now constructor; eauto.
eapply Included_trans; [| eapply reachable_in_dom ].
eapply Included_trans; [| eapply FV_image_reach; eassumption ].
eapply image_monotonic.
eapply Included_Setminus. eapply Disjoint_sym.
eapply Disjoint_Included_r; [| eapply Fun_inv_locs_Disjoint2; eauto ].
eapply reach'_set_monotonic. eapply post_set_monotonic. eapply env_locs_monotonic...
rewrite (reach_unfold H1 (env_locs _ _ )). eapply Included_Union_preserv_r.
eapply reach'_set_monotonic. eapply post_set_monotonic. eapply env_locs_monotonic...
eapply well_formed_antimon; [| eapply FV_reach2; try eassumption; now tci ].
eapply reach'_set_monotonic. eapply env_locs_monotonic. unfold FV_cc...
eapply Included_trans; [| eapply FV_dom2; try eassumption; now tci ].
eapply env_locs_monotonic. unfold FV_cc...
intros j'.
eapply Fun_inv_Scope_monotonic'; now tci.
now eapply HL.subheap_refl.
eapply HL.alloc_subheap. eassumption.
* eapply f_eq_subdomain_extend_not_In_S_r.
intros Hc. eapply Fun_inv_locs_Disjoint1. now eapply (Hfun 0). now constructor; eauto.
constructor; eauto.
eapply get_In_env_locs. reflexivity. eassumption. reflexivity.
eapply reach'_set_monotonic; [| eassumption ]. eapply env_locs_monotonic.
unfold FV. rewrite !Setminus_Union_distr. eapply Included_Union_preserv_l...
reflexivity.
* intros Hc. inv Hc. eauto.
* intros Hc. eapply Hdis. constructor. right.
eapply image_monotonic; [| eassumption ]...
left; right. now constructor; eauto.
+ intros j'.
eapply FV_inv_set_not_in_FVs_r.
eapply FV_inv_FV_eq.
now eapply X. now tci.
eapply FV_inv_heap_mon; [ | | ].
* eapply HL.subheap_refl.
* eapply HL.alloc_subheap. eassumption.
* intros j1. eapply FV_inv_rename_ext. now eapply Hfv.
eapply f_eq_subdomain_extend_not_In_S_l.
intros Hc. eapply Fun_inv_locs_Disjoint1. now eapply (Hfun 0). now constructor; eauto.
constructor; eauto.
eapply get_In_env_locs. constructor; eauto. eassumption. reflexivity.
eapply reach'_set_monotonic; [| eassumption ].
eapply env_locs_monotonic. unfold FV.
rewrite !Setminus_Union_distr.
eapply Included_Union_preserv_r. rewrite Setminus_Union.
rewrite (Union_commut _ [set x]).
rewrite (Union_Same_set [set x])...
reflexivity.
* rewrite Union_Setminus_Included.
rewrite <- Union_assoc. rewrite (Union_Same_set [set x]). reflexivity.
eapply Singleton_Included. now right. tci.
eapply Singleton_Included. now left.
* intros Hc. subst.
eapply Hdis. constructor. now left.
left. right; constructor; eauto.
- inv Hctx. inv H18.
assert (Hseq : FV (x |: Scope) Funs' FVs <--> FV Scope Funs' FVs).
{ unfold FV. rewrite <- (Union_assoc [set x] Scope Funs') at 1.
rewrite !(Union_commut [set x]) at 2.
rewrite !(Union_commut [set x] (Scope :|: Funs')) at 1.
do 2 rewrite <- Setminus_Union.
rewrite Union_Setminus_Included; try eauto with Ensembles_DB typeclass_instances.
rewrite (Union_Setminus_Included _ (Funs' \\ Scope));
try eauto with Ensembles_DB typeclass_instances.
rewrite <- !Union_assoc.
rewrite (Union_Same_set [set x]). reflexivity. eapply Singleton_Included.
right. right. constructor; eauto. eapply nthN_In. eassumption.
intros Hc. inv Hc; eauto. }
eexists. split; [| split ].
+ intros j.
edestruct (Hfv j) as (Hwf & Hkey & vs1 & loc_env & Hget1 & Hget2 & Hall).
repeat subst_exp. eapply cc_approx_env_P_union.
* edestruct (Forall2_P_nthN _ _ _ _ FVs _ N _ Hall H3) as (v2 & Hnth' & vs4 & Hget4 & Hrel).
intros Hc. now inv Hc.
intros y Hin v' Hget. inv Hin. rewrite M.gss.
repeat subst_exp. eexists. split. reflexivity.
eassumption.
* eapply cc_approx_env_P_set_not_in_P_r; try eassumption.
now eauto.
+ intros j. eapply Fun_inv_set_r.
now eapply Fun_inv_Scope_monotonic; tci.
now intros Hc; inv Hc; eauto.
intros Hin. eapply Hdis. constructor. right.
eapply image_monotonic; [| eassumption ]...
right. constructor; eauto. eapply nthN_In. eassumption.
intros Hc. inv Hc; eauto.
+ intros j.
edestruct (Hfv j) as (Hwf & Hkey & vs1 & loc_env & Hget1 & Hget2 & Hall).
split. rewrite env_locs_set_not_In. eassumption.
intros Hc. inv Hc.
eapply Hdis. constructor. now left.
right. constructor. eapply nthN_In. eassumption.
intros Hc; inv Hc; eauto. split.
rewrite Hseq. eassumption.
repeat eexists; eauto.
rewrite M.gso; eauto.
intros Hc. subst.
eapply Hdis. constructor. now left.
right. constructor. eapply nthN_In. eassumption.
intros Hc; inv Hc; eauto.
eapply Forall2_P_monotonic; [ eassumption | ]...
Grab Existential Variables. exact 0.
Qed.
(** Correctness of [project_vars] *)
Lemma project_vars_correct GII GI k H1 rho1 H2 rho2 H2' rho2' b
Scope {Hs : ToMSet Scope} Scope' Funs Funs' fenv c Γ FVs xs C m :
project_vars ct Scope Funs fenv c Γ FVs xs C Scope' Funs' ->
(forall j, (H1, rho1) ⋞ ^ (Scope; k; j; GII; GI; b) (H2, rho2)) ->
(forall j, Fun_inv k j GII GI b rho1 H1 rho2 H2 Scope Funs fenv FVs) ->
(forall j, FV_inv k j GII GI b rho1 H1 rho2 H2 c Scope Funs Γ FVs) ->
Disjoint _ (Γ |: image fenv (Funs \\ Scope)) (FV Scope Funs FVs) ->
ctx_to_heap_env_CC C H2 rho2 H2' rho2' m ->
binding_in_map (FV Scope Funs FVs) rho1 ->
exists b',
(forall j, (H1, rho1) ⋞ ^ (Scope'; k; j; GII; GI; b') (H2', rho2')) /\
(forall j, Fun_inv k j GII GI b' rho1 H1 rho2' H2' Scope' Funs' fenv FVs) /\
(forall j, FV_inv k j GII GI b' rho1 H1 rho2' H2' c Scope' Funs' Γ FVs).
Proof with (now eauto with Ensembles_DB).
intros Hvars.
revert b m H1 rho1 H2 rho2 H2' rho2'.
induction Hvars;
intros b m H1 rho1 H2 rho2 H2' rho2' Hcc Hfun Hfv
Hdis Hctx Hbin.
- inv Hctx. eexists. split; [| split ]; eauto.
- edestruct ctx_to_heap_env_CC_comp_ctx_f_l as [rho3 [H3 [m1 [m2 [Hctx2 [Hctx3 Heq]]]]]].
eassumption. subst.
edestruct project_var_correct as (b' & Hcc' & Hfun' & Hfv');
try eassumption.
eapply binding_in_map_antimon; [| eassumption ]...
eapply IHHvars; try eassumption.
+ eapply project_var_ToMSet; eassumption.
+ erewrite <- project_var_FV_eq; try eassumption.
eapply Disjoint_Included_l; [ | eapply Hdis ].
eapply Included_Union_compat; [reflexivity | ].
eapply image_monotonic. eapply Included_Setminus_compat.
eapply project_var_Funs_l. eassumption.
eapply project_var_Scope_l. eassumption.
+ erewrite <- project_var_FV_eq; try eassumption.
Qed.
Opaque Pre.
Lemma has_true_mut_fun_in_fundefs B f xs ft e :
has_true_mut_funs B ->
fun_in_fundefs B (f, ft, xs, e) ->
has_true_mut e.
Proof.
intros HB Hin. induction B; inv Hin.
- inv H. inv HB. eassumption.
- inv HB. eauto.
Qed.
Lemma Closure_conversion_fundefs_correct
(k : nat)
(* The IH *)
(IHexp :
forall m : nat,
m < k ->
forall (H1 H2 : heap block) (rho1 rho2 : env)
(e1 e2 : exp) (C : exp_ctx) (Scope : Ensemble var)
{Hs : ToMSet Scope}
(Funs : Ensemble var) (Hf : ToMSet Funs)
(FVs : list var) (fenv : positive -> positive)
(β : Inj) (c : cTag) (Γ : var) A δ,
(forall j : nat,
(H1, rho1) ⋞ ^ (Scope; m; j; PreG; PostG; β) (H2, rho2)) ->
(forall j : nat,
FV_inv m j PreG PostG β rho1 H1 rho2 H2 c Scope Funs Γ FVs) ->
(forall j : nat,
Fun_inv m j PreG PostG β rho1 H1 rho2 H2 Scope Funs fenv FVs) ->
Disjoint var (Γ |: image fenv (Funs \\ Scope))
(bound_var e1 :|: FV Scope Funs FVs) ->
binding_in_map (FV Scope Funs FVs) rho1 ->
unique_bindings e1 ->
has_true_mut e1 ->
Disjoint var (bound_var e1) (FV Scope Funs FVs) ->
Closure_conversion ct Scope Funs fenv c Γ FVs e1 e2 C ->
forall j : nat,
(e1, rho1, H1) ⪯ ^ (m; j; Pre (Funs :&: occurs_free e1 \\ Scope) A δ; PreG; Post 0 A δ; PostG) (C |[ e2 ]|, rho2, H2)) :
(* ************************************************ *)
forall B1 B2
(H1 H1' H2 : heap block) lenv (rho1 rho1c rho1' rho2 : env) b
(Scope Funs : Ensemble var) fenv (Hs : ToMSet Scope)
(Hf : ToMSet Funs) (FVs FVs': list var)
(c : cTag) (Γ' : var),
(* Environment invariants *)
closed (reach' H1 (env_locs rho1 (FV Scope Funs FVs))) H1 ->
closed (reach' H2 (env_locs rho2 (FV_cc Scope Funs fenv Γ'))) H2 ->
(forall j, Fun_inv k j PreG PostG b rho1 H1 rho2 H2 Scope Funs fenv FVs) ->
(* Free variables invariant for new fundefs *)
(forall j, FV_inv k j PreG PostG b rho1c H1 rho2 H2 c (Empty_set _) (Empty_set _) Γ' FVs') -> (* no scope, no funs yet *)
FromList FVs' <--> occurs_free_fundefs B1 ->
NoDup FVs' ->
unique_bindings_fundefs B1 ->
(* Freshness *)
Disjoint var (bound_var_fundefs B1) (FV Scope Funs FVs :|: FromList FVs') ->
Disjoint _ (Γ' |: image fenv (Funs \\ Scope)) (name_in_fundefs B1) ->
(* Properties of the new environment *)
get lenv H1 = Some (Env rho1c) ->
M.get Γ' rho2 = Some (Loc (b lenv)) ->
env_locs rho1c (Full_set _) \subset env_locs rho1 (FV Scope Funs FVs \\ (Funs \\ Scope)) ->
has_true_mut_funs B1 -> true_mut B1 ->
Closure_conversion_fundefs ct B1 c FVs' B1 B2 ->
def_closures B1 B1 rho1 H1 (Loc lenv) = (H1', rho1') ->
(forall j, Fun_inv k j PreG PostG b
rho1' H1' (def_funs B2 B2 rho2) H2
(Scope \\ name_in_fundefs B1) (name_in_fundefs B1 :|: Funs) (extend_fundefs' fenv B1 Γ') FVs).
Proof with (now eauto with Ensembles_DB).
Opaque cc_approx_exp.
induction k as [k IHk] using lt_wf_rec1.
intros B1 B2 H1 H1' H2 lenv rho1 rho1c rho1' rho2 b
Scope Funs fenv Hs Hf FVs FVs' c Γ' Hc1 Hc2
Hfun Hfvs'
Hfveq Hnd Hun1 Hfresh Hdis
Hgetenv1 Hgetenv2 Hincl Htme Htm Hccf1 Hclo j.
destruct (Hfvs' j) as (Hwf & Hkey & vs & lenv'' & Hgetlenv & Hget' & HallP).
simpl in Hclo.
unfold FV in Hkey.
rewrite !Union_Empty_set_neut_l, !Setminus_Empty_set_neut_r, !Union_Empty_set_neut_l in Hkey.
intros f1 Hin Hnin. repeat subst_exp.
edestruct (@Dec _ (name_in_fundefs B1) _ f1) as [ Hfin | Hfnin ].
- edestruct def_closures_exists as [lf [Hgetf [Hgetlf Hfresh']]]; try eassumption.
exists lf, lenv, (b lenv), B1, f1, B2, f1.
split; [ | split; [ | split; [ | split; [ | split; [ | split ] ] ] ]].
* eassumption.
* intros Hc.
assert (Hseq : (FV (Scope \\ name_in_fundefs B1)
(name_in_fundefs B1 :|: Funs) FVs \\ [set f1]) \subset
FV Scope Funs FVs \\ name_in_fundefs B1 :|: (name_in_fundefs B1 \\ [set f1])).
{ eapply Setminus_Included_Included_Union.
eapply Included_trans.
eapply FV_Setminus1. now tci.
eapply Included_trans. eapply Included_Union_compat. reflexivity.
eapply FV_Union2.
rewrite <- !Union_assoc. rewrite <- Union_Setminus.
rewrite !Union_assoc. rewrite <- Union_Setminus.
now eauto with Ensembles_DB. now tci. now tci. }
rewrite reach'_Union in Hc.
rewrite post_Singleton in Hc; [| eassumption ]. simpl in Hc.
rewrite Union_Empty_set_neut_l in Hc.
{ inv Hc.
- eapply reach'_set_monotonic in H; [| eapply env_locs_monotonic; eassumption ].
rewrite env_locs_Union, reach'_Union in H. inv H.
+ eapply reach'_set_monotonic in H0; [| eapply env_locs_def_funs; [ reflexivity | now eauto ] ].
rewrite <- well_formed_reach_subheap_same in H0.
eapply reachable_in_dom in H0. eapply Hfresh'. eassumption.
eapply well_formed_antimon; [| eapply well_formed'_closed; eassumption ].
eapply reach'_set_monotonic. eapply env_locs_monotonic...
eapply Included_trans; [| eapply env_locs_closed; eassumption ].
eapply Included_trans; [| eapply reach'_extensive ].
eapply env_locs_monotonic...
eapply well_formed_antimon; [| eapply well_formed'_closed; eassumption ].
eapply reach'_set_monotonic. eapply env_locs_monotonic...
eapply Included_trans; [| eapply env_locs_closed; eassumption ].
eapply Included_trans; [| eapply reach'_extensive ].
eapply env_locs_monotonic...
eapply def_funs_subheap. now eauto.
+ rewrite reach_unfold in H0. inv H0.
eapply def_closures_env_locs_fresh. eassumption.
eapply unique_bindings_fundefs_unique_functions.
eassumption. eassumption.
constructor; [| eassumption ]. rewrite env_locs_Singleton; eauto. reflexivity.
eapply reach'_set_monotonic in H;
[| eapply Included_trans; [eapply post_set_monotonic; eapply env_locs_monotonic
| eapply def_closures_post; eassumption ] ];
try now eauto with Ensembles_DB.
rewrite reach_unfold in H. inv H.
* inv H0. eapply Hfresh'. eexists; eauto.
* simpl in H0. rewrite post_Singleton in H0; [| eapply def_funs_subheap; now eauto ].
simpl in H0.
rewrite <- reach'_subheap in H0; [| | | eapply def_funs_subheap; now eauto ].
rewrite env_locs_key_set, Hkey in H0.
eapply reachable_in_dom in H0. contradiction.
eapply well_formed_antimon; [| eapply FV_inv_reach1; now apply Hfvs' ].
eapply reach'_set_monotonic. rewrite Union_Empty_set_neut_l, Setminus_Empty_set_neut_r.
eapply env_locs_monotonic. now eauto with Ensembles_DB.
eapply Included_trans; [| eapply FV_inv_dom1; now apply Hfvs' ].
eapply env_locs_monotonic. unfold FV.
rewrite !Union_Empty_set_neut_l, !Setminus_Empty_set_neut_r at 1...
eapply well_formed_antimon; [| eapply FV_inv_reach1; now apply Hfvs' ].
eapply reach'_set_monotonic. rewrite Union_Empty_set_neut_l, Setminus_Empty_set_neut_r.
rewrite env_locs_key_set, Hkey.
eapply env_locs_monotonic...
eapply Included_trans; [| eapply FV_inv_dom1; now apply Hfvs' ].
rewrite env_locs_key_set, Hkey.
eapply env_locs_monotonic.
rewrite !Union_Empty_set_neut_l, !Setminus_Empty_set_neut_r at 1...
- rewrite reach_unfold in H. inv H.
* inv H0. eapply Hfresh'. eexists; eauto.
* simpl in H0. rewrite post_Singleton in H0; [| eapply def_funs_subheap; now eauto ].
simpl in H0.
rewrite <- reach'_subheap in H0; [| | | eapply def_funs_subheap; now eauto ].
rewrite env_locs_key_set, Hkey in H0.
eapply reachable_in_dom in H0. contradiction.
eapply well_formed_antimon; [| eapply FV_inv_reach1; now apply Hfvs' ].
eapply reach'_set_monotonic. rewrite Union_Empty_set_neut_l, Setminus_Empty_set_neut_r.
eapply env_locs_monotonic. now eauto with Ensembles_DB.
eapply Included_trans; [| eapply FV_inv_dom1; now apply Hfvs' ].
eapply env_locs_monotonic. unfold FV.
rewrite !Union_Empty_set_neut_l, !Setminus_Empty_set_neut_r at 1...
eapply well_formed_antimon; [| eapply FV_inv_reach1; now apply Hfvs' ].
eapply reach'_set_monotonic. rewrite Union_Empty_set_neut_l, Setminus_Empty_set_neut_r.
rewrite env_locs_key_set, Hkey.
eapply env_locs_monotonic...
eapply Included_trans; [| eapply FV_inv_dom1; now apply Hfvs' ].
rewrite env_locs_key_set, Hkey.
eapply env_locs_monotonic.
rewrite !Union_Empty_set_neut_l, !Setminus_Empty_set_neut_r at 1... }
* erewrite def_funs_eq. reflexivity. reflexivity.
rewrite <- closure_conversion_fundefs_Same_set. eassumption. eassumption.
* eassumption.
* rewrite extend_fundefs'_get_s.
erewrite def_funs_neq. eassumption. reflexivity.
intros Hc. eapply Hdis.
rewrite closure_conversion_fundefs_Same_set.
constructor. now left. eassumption.
eassumption. eassumption.
* eapply FV_inv_cc_approx_clos; [ | | | | | ].
eapply FV_inv_heap_mon. eapply def_funs_subheap. now eauto.
now eapply HL.subheap_refl.
eassumption.
unfold FV in Hkey.
rewrite <- Hkey. eapply binding_in_map_key_set.
eassumption.
eapply def_funs_subheap; try eassumption. now eauto.
eassumption. reflexivity.
* destruct (alloc (Constr _ [FunPtr B2 f1; Loc (b lenv)]) H2)
as [lenv2 H2'] eqn:Ha'.
simpl cc_approx_val'. erewrite !(gas _ _ _ _ _ Ha'); eauto.
split; [ rewrite extend_gss; reflexivity |].
rewrite Hgetlf.
{ split.
(* Closure environment relation *)
- intros i Hlt.
eapply FV_inv_cc_approx_clos; [ | | eassumption | | eassumption | ].
eapply FV_inv_heap_mon. eapply def_funs_subheap. now eauto.
eapply HL.alloc_subheap. eassumption. intros j'.
eapply FV_inv_rename_ext; [ now eauto | ].
eapply f_eq_subdomain_extend_not_In_S_l.
intros Hc. eapply reachable_in_dom in Hc. contradiction.
eapply FV_inv_reach1. eassumption.
eapply FV_inv_dom1. eassumption.
reflexivity.
rewrite <- Hkey. now eapply binding_in_map_key_set.
eapply def_funs_subheap; try eassumption. now eauto.
rewrite extend_gso. reflexivity.
intros Hc; subst.
eapply def_funs_subheap in Hgetenv1; try now eauto.
congruence.
- intros b1 b2 lenv1 rhoc' rhoc1 rhoc2 H3 H3' H4 lr xs1 ft ef vs1 vs2.
intros Heq1 Hinj1 Heq2 Hinj2 Hf' Hget Hdef Hset Hlen.
edestruct Closure_conversion_fundefs_find_def as
(Γ'' & e2 & C' & Hfind & Hdisg & Hclo').
eassumption. eassumption.
assert (Hf1 : ~ In var (FromList xs1) Γ'' ).
{ intros Hc. eapply Hdisg... }
assert (Hf2 : ~ In var (name_in_fundefs B1) Γ'' ).
{ intros Hc. eapply Hdisg... }
assert (Ha : key_set rhoc' <--> key_set rho1c).
{ rewrite res_equiv_eq in Heq1. destruct Heq1 as [Hbeq1 Hres].
unfold id in *; subst.
eapply def_funs_subheap in Hgetenv1; eauto.
rewrite Hgetenv1, Hget in Hres. simpl in Hres.
eapply heap_env_equiv_key_set. symmetry. eassumption. }
edestruct (setlist_length rhoc1 (def_funs B2 B2 (M.empty value))
rhoc2 xs1 vs1 vs2)
as [rho2' Hset2]; [ eassumption (* add length vs1 = lngth v2 *)
| now apply Hset | ].
{ do 3 eexists. split; [| split ].
- eassumption.
- simpl. rewrite Hset2. reflexivity.
- intros i Hlt b' Hall Hfeq.
assert (Hwf1' : closed (reach' H3 (Union_list (map val_loc vs1))) H3).
{ (* eapply reach'_closed. *)
revert Hall. clear. revert vs2.
induction vs1; intros vs2 Hall.
- simpl. rewrite reach'_Empty_set.
intros x Hin. inv Hin.
- simpl. rewrite reach'_Union.
destruct vs2 as [| b vs2].
specialize (Hall 0). now inv Hall.
eapply closed_Union.
eapply reach'_closed.
eapply cc_approx_val_well_formed_reach1.
intros j. specialize (Hall j). inv Hall. rewrite cc_approx_val_eq in H2.
eassumption.
specialize (Hall 0). inv Hall.
eapply cc_approx_val_dom1. rewrite cc_approx_val_eq in H2.
eassumption.
eapply IHvs1. intros j. specialize (Hall j). inv Hall.
rewrite cc_approx_val_eq in H2. eassumption. }
assert (Hfvs'' : forall j2, FV_inv i j2 PreG PostG b' rhoc' H3 (M.set Γ'' (Loc lr) (M.empty value)) H4
c (Empty_set var) (Empty_set var) Γ'' FVs').
{ intros j2'.
eapply FV_inv_heap_f_eq_subdomain; [| eapply f_eq_subdomain_antimon; try eassumption ].
eapply FV_inv_heap_env_equiv with (H1 := H1') (H2 := H2').
eapply FV_inv_rho_swap with (rho2' := M.set Γ'' (Loc (b lenv)) (M.empty value)). tci.
eapply FV_inv_monotonic.
eapply FV_inv_heap_mon. eapply def_funs_subheap. now eauto.
eapply HL.alloc_subheap. eassumption.
intros j3. eapply FV_inv_rename_ext. eapply Hfvs'.
eapply f_eq_subdomain_extend_not_In_S_l. intros Hc. eapply reachable_in_dom in Hc.
contradiction.
eapply well_formed_antimon; [| eapply well_formed'_closed; eassumption ].
eapply reach'_set_monotonic. rewrite Union_Empty_set_neut_r, Setminus_Empty_set_neut_r.
eapply Included_trans. eapply Included_trans. eapply env_locs_monotonic with (S2 := Full_set _)...
eassumption. eapply env_locs_monotonic...
eapply Included_trans; [| eapply env_locs_closed; eassumption ].
rewrite Union_Empty_set_neut_r, Setminus_Empty_set_neut_r.
eapply Included_trans. eapply Included_trans. eapply env_locs_monotonic with (S2 := Full_set _)...
eassumption. eapply Included_trans; [| eapply reach'_extensive ]. eapply env_locs_monotonic...
reflexivity.
omega.
rewrite M.gss. eassumption.
rewrite res_equiv_eq in Heq1. simpl in Heq1. destruct Heq1 as [Hbeq Hres].
unfold id in *; subst.
eapply def_funs_subheap in Hgetenv1; eauto. rewrite Hgetenv1, Hget in Hres.
eassumption.
eapply injective_subdomain_antimon. eassumption.
rewrite (reach'_idempotent H3 [set lenv1]). eapply reach'_set_monotonic.
eapply Included_trans; [| eapply Included_post_reach' ]. rewrite post_Singleton; eauto.
reflexivity.
eapply heap_env_equiv_set. rewrite Setminus_Same_set_Empty_set.
split; intros x v Hin'; now inv Hin'.
eassumption.
eapply injective_subdomain_antimon. eassumption.
eapply reach'_set_monotonic. eapply Included_trans. eapply env_locs_set_Inlcuded'.
rewrite <- env_locs_Empty...
rewrite (reach_unfold H3 [set lenv1]), post_Singleton; eauto.
eapply Included_Union_preserv_r.
eapply reach'_set_monotonic. simpl.
rewrite env_locs_key_set, Ha, Hkey... }
edestruct (Hfvs'' j) as (Hwf'' & Hkey'' & vs1'' & loc_env'' & Hget1'' & Hget2'' & Hall'').
repeat subst_exp.
split.
+ intros Hgc2 g2 Hl2.
eapply PreSubsetCompat
with (Funs := name_in_fundefs B1 :&: occurs_free ef).
{ eapply GC_pre with (Scope := reach' H3 (env_locs rhoc2 (occurs_free ef :&: FromList xs1) :|:
(env_locs rhoc' (FromList FVs'))))
(xs2 := Γ'' :: xs1) (β := b').
- eassumption. (* TODO remove bogus arg *)
- eauto 20 with typeclass_instances.
- eassumption.
- eassumption.
- eassumption.
- eassumption.
- simpl. rewrite Hset2. reflexivity.
- eassumption.
- eassumption.
- rewrite M.gss in Hget1''. inv Hget1''. eassumption.
- eapply Forall2_P_Forall2 in Hall''.
erewrite <- Forall2_length; [| eassumption ].
rewrite !PS.cardinal_spec. erewrite Same_set_FromList_length'. reflexivity.
eassumption. eapply NoDupA_NoDup. eapply PS.elements_spec2w.
rewrite <- !FromSet_elements.
rewrite Hfveq. now eapply fundefs_fv_correct.
now eauto with Ensembles_DB.
- intros j1.
rewrite reach'_Union. eapply cc_approx_heap_union.
+ eapply cc_approx_env_cc_approx_heap. eassumption. eassumption.
intros j2. eapply cc_approx_env_P_setlist_l; try eassumption.
rewrite Setminus_Included_Empty_set. eapply cc_approx_env_Empty_set.
now eapply Included_Intersection_r.
eapply Forall2_monotonic; [| eapply Hall ].
intros. rewrite <- cc_approx_val_eq. now eapply H.
+ eapply cc_approx_heap_antimon; [| eapply FV_inv_heap_equiv; eassumption ].
eapply reach'_set_monotonic. eapply env_locs_monotonic...
- eapply Disjoint_Included_l.
eapply Included_Intersection_l.
eapply Disjoint_sym. eapply unique_bindings_fun_in_fundefs.
eapply find_def_correct. eassumption. eassumption.
- eapply unique_bindings_fundefs_unique_functions. eassumption.
- rewrite Closure_conversion_fv_cor at 3; [| eassumption ].
rewrite !env_locs_Union, !reach'_Union. eapply Union_Included. eapply Union_Included.
+ do 2 eapply Included_Union_preserv_l.
eapply reach'_heap_monotonic. eapply def_funs_subheap; eauto.
+ eapply find_def_correct in Hf'. assert (Hf'' := Hf').
eapply Htm in Hf'. inv Hf'.
* eapply Included_Union_preserv_r.
rewrite <- env_locs_setlist_Disjoint with (rho' := rhoc2); try eassumption.
rewrite def_closures_env_locs' with (rho1' := rhoc1); try eassumption.
rewrite Setminus_Disjoint.
eapply Included_trans; [| eapply reach'_heap_monotonic; eapply def_funs_subheap; now eauto ].
eapply reach'_set_monotonic.
eapply env_locs_monotonic. eapply Included_Intersection. rewrite <- H.
eapply Hfveq. reflexivity.
eapply Disjoint_sym. eapply Disjoint_Included; [| | eapply Hfresh ].
now eauto with Ensembles_DB.
eapply Union_Included.
eapply Included_trans; [| eapply fun_in_fundefs_bound_var_fundefs; eassumption ]...
now eapply name_in_fundefs_bound_var_fundefs.
eapply Disjoint_Included_l.
eapply Included_Intersection_r. now eauto with Ensembles_DB.
eapply Disjoint_Included_l.
eapply Included_Intersection_r. now eauto with Ensembles_DB.
* eapply Included_Union_preserv_l.
eapply Included_Union_preserv_r. destruct H as [ff Hinff].
rewrite <- env_locs_setlist_Disjoint with (rho' := rhoc2); try eassumption.
edestruct def_closures_exists as [lff [Hegtf [Hgetlff _]]]. eassumption.
inv Hinff. eassumption.
rewrite (reach_unfold H3'). eapply Included_Union_preserv_r.
rewrite (reach_unfold H3'). eapply Included_Union_preserv_r.
eapply Included_trans; [| eapply reach'_heap_monotonic; eapply def_funs_subheap; now eauto ].
eapply reach'_set_monotonic.
intros ll Hinll. eapply post_set_monotonic. eapply post_set_monotonic.
eapply get_In_env_locs.
rewrite Setminus_Disjoint. rewrite Intersection_commut. eassumption.
eapply Disjoint_sym. eapply unique_bindings_fun_in_fundefs.
eassumption. eassumption. eassumption.
simpl. erewrite post_Singleton; eauto. simpl. rewrite Union_Empty_set_neut_l.
erewrite post_Singleton; [| eapply def_funs_subheap; eauto ]. simpl.
rewrite env_locs_key_set, Hkey''. eapply env_locs_monotonic; [| eassumption ]...
eapply Disjoint_Included_l.
eapply Included_Intersection_r. now eauto with Ensembles_DB.
+ eapply Included_Union_preserv_l. eapply Included_Union_preserv_r.
rewrite Setminus_Disjoint, Intersection_commut. eapply reach'_extensive.
eapply Disjoint_sym. eapply unique_bindings_fun_in_fundefs.
eapply find_def_correct. eassumption. eassumption.
- eapply Included_trans. eapply reach'_set_monotonic.
eapply env_locs_monotonic. eapply Closure_conversion_cc_fv_cor.
eassumption. intros Hc; inv Hc; now eauto.
eapply Disjoint_sym. eapply unique_bindings_fun_in_fundefs.
eapply find_def_correct. eassumption. eassumption.
(* rewrite <- env_locs_setlist_Disjoint with (rho' := rhoc2) (S := (occurs_free ef :&: FromList xs1)); *)
(* try eassumption. *)
(* rewrite def_closures_env_locs' with (rho1' := rhoc1); try eassumption. *)
(* rewrite env_locs_key_set. rewrite Ha, Hkey. *)
rewrite Setminus_Disjoint.
eapply Included_trans. eapply reach'_set_monotonic.
eapply env_locs_set_Inlcuded'. rewrite !Setminus_Union_distr.
rewrite Setminus_Same_set_Empty_set, Union_Empty_set_neut_r.
rewrite !Setminus_Disjoint. rewrite env_locs_Union.
rewrite <- env_locs_setlist_Disjoint with (rho' := rho2') (S := (occurs_free ef :&: name_in_fundefs B1));
try eassumption.
assert (Hlem : env_locs (def_funs B2 B2 (M.empty value)) (occurs_free ef :&: name_in_fundefs B1) <-->
Empty_set _).
{ rewrite env_locs_def_funs'; [ | | reflexivity ]; tci. rewrite <- env_locs_Empty. reflexivity. }
rewrite Hlem. rewrite Union_Empty_set_neut_r.
rewrite !reach'_Union. eapply Union_Included.
+ eapply FV_inv_image_reach_eq in Hfvs''.
rewrite image_Union. rewrite Hfvs''. rewrite env_locs_set_In.
rewrite Setminus_Same_set_Empty_set. rewrite <- !env_locs_Empty, Union_Empty_set_neut_r.
rewrite reach_unfold... reflexivity.
+ rewrite image_Union. eapply Included_Union_preserv_r. eapply Included_Union_preserv_l.
rewrite cc_approx_env_image_reach. reflexivity.
intros j1. eapply cc_approx_env_P_setlist_l; try eassumption.
rewrite Setminus_Included_Empty_set. eapply cc_approx_env_Empty_set.
now eapply Included_Intersection_r.
eapply Forall2_monotonic; [| eapply Hall ].
intros. rewrite <- cc_approx_val_eq. now eapply H.
eapply binding_in_map_antimon; [| eapply binding_in_map_setlist with (S := Empty_set _);
try eassumption ].
eapply Included_trans; [ eapply Included_Intersection_r | ]...
intros x Hinx. inv Hinx.
+ eapply Disjoint_Included_l.
eapply Included_Intersection_r.
eapply Disjoint_sym. eapply unique_bindings_fun_in_fundefs.
eapply find_def_correct. eassumption. eassumption.
+ eapply Disjoint_Singleton_r. intros Hc; inv Hc; eauto.
+ eapply Disjoint_Singleton_r. intros Hc; inv Hc; eauto.
+ eapply Disjoint_sym. eapply unique_bindings_fun_in_fundefs.
eapply find_def_correct. eassumption. eassumption. }
now eauto with Ensembles_DB.
+ intros j0. eapply cc_approx_exp_rel_mon_post.
eapply cc_approx_exp_rel_mon_pre.
eapply IHexp with (Scope := (FromList xs1)) (Funs := name_in_fundefs B1)
(fenv := extend_fundefs' id B1 Γ'')
(β := b');
[ | | | | | | | | | eassumption ].
* eassumption.
* intros j1.
eapply cc_approx_env_P_set_not_in_P_r.
eapply cc_approx_env_heap_monotonic; [| | ].
eapply def_funs_subheap. now eauto.
now eapply HL.subheap_refl.
intros j2. eapply cc_approx_env_P_setlist_l.
rewrite Setminus_Same_set_Empty_set.
eapply cc_approx_env_Empty_set.
eapply Forall2_monotonic; [| now apply Hall ].
intros x1 x2 HR.
rewrite cc_approx_val_eq in *.
eapply HR. eassumption.
eassumption.
eassumption.
* intros j1.
eapply Proper_FV_inv_Scope;
[ rewrite <- (Union_Empty_set_neut_r (FromList xs1)); reflexivity | | | | ];
try reflexivity.
eapply setlist_FV_inv; [| | eassumption ]. tci.
eapply Proper_FV_inv_Funs;
[ rewrite <- (Union_Empty_set_neut_r (name_in_fundefs B1)); reflexivity | | | ];
try reflexivity.
eapply def_closures_FV_inv; [| | eassumption ]. tci.
intros j2.
eapply FV_inv_rho_swap. tci. eapply Hfvs''. rewrite !M.gss. reflexivity.
* intros j1.
eapply Proper_Fun_inv_Scope;
[ rewrite <- (Union_Empty_set_neut_r (FromList xs1)); reflexivity | | | | ];
try reflexivity.
eapply Fun_inv_Scope_Disjoint.
edestruct (setlist_length (def_funs B2 B2 (M.empty value))
(M.set Γ'' (Loc lr)
(def_funs B2 B2 (M.empty value))))
as [rho2'' Hset''].
reflexivity. eassumption.
eapply Fun_inv_suffle_setlist_l; try eassumption.
eapply Fun_inv_setlist_r; try eassumption.
eapply Fun_inv_suffle_def_funs_l.
eapply Fun_inv_setlist_l; try eassumption.
eapply Proper_Fun_inv_Scope;
[ rewrite <- (Setminus_Disjoint (Empty_set var) (name_in_fundefs B1))
| | | | ];
try reflexivity; eauto with Ensembles_DB.
eapply Proper_Fun_inv_Funs;
[ rewrite <- (Union_Empty_set_neut_r (name_in_fundefs B1)); reflexivity | | | ];
try reflexivity; eauto with Ensembles_DB.
assert (Hwf1 : closed (reach' H3 (env_locs rhoc' (FromList FVs'))) H3).
{ eapply reach'_closed.
eapply well_formed_antimon; [| eapply FV_inv_reach1; eassumption ].
eapply reach'_set_monotonic. eapply env_locs_monotonic.
unfold FV...
eapply Included_trans; [| eapply FV_inv_dom1; eassumption ].
eapply env_locs_monotonic... }
assert (Hwf3 : closed (reach' H4 [set lr]) H4).
{ eapply reach'_closed.
eapply well_formed_antimon; [| eapply FV_inv_reach2; eapply Hfvs'' ].
rewrite env_locs_set_In. eapply reach'_set_monotonic...
reflexivity.
eapply Included_trans; [| eapply FV_inv_dom2; eassumption ].
rewrite env_locs_set_In... }
(* IH fundefs *)
{ eapply IHk with (Scope := Empty_set _); try eassumption; tci.
- intros; eauto.
eapply IHexp with (Scope := Scope0) (Funs := Funs0); eauto. omega.
- unfold FV. rewrite !Union_Empty_set_neut_r, !Setminus_Empty_set_neut_r,
!Union_Empty_set_neut_l at 1.
eassumption.
- unfold FV_cc.
rewrite !image_id, !Union_Empty_set_neut_l, !Setminus_Empty_set_neut_r,
!Union_Empty_set_neut_l at 1.
rewrite env_locs_set_In, <- env_locs_Empty, Union_Empty_set_neut_r.
eassumption. reflexivity.
- intros j2 x Hnin1 Hin2. inv Hin2.
- unfold FV.
rewrite !Union_Empty_set_neut_r, !Setminus_Empty_set_neut_r,
!Union_Empty_set_neut_l at 1.
eapply Disjoint_Included_r; [| eassumption ]...
- rewrite image_id. rewrite Setminus_Empty_set_neut_r, Union_Empty_set_neut_r.
eapply Disjoint_Singleton_l. eassumption.
- rewrite M.gss.
eapply res_equiv_locs_eq in Heq1.
eapply res_equiv_locs_eq in Heq2.
rewrite <- Hfeq.
unfold compose, id in *. rewrite <- Heq1.
rewrite extend_gso. rewrite <- Heq2. reflexivity.
intros Hc; subst. eapply Hfresh'. eexists. eassumption.
eapply reach'_extensive. reflexivity.
eassumption. eassumption. (* XXX remove extra params *)
- unfold FV.
rewrite !Union_Empty_set_neut_r, !Setminus_Empty_set_neut_r,
!Union_Empty_set_neut_l at 1.
rewrite env_locs_key_set, Ha, Hkey. reflexivity. }
rewrite Setminus_Empty_set_neut_r. eapply unique_bindings_fun_in_fundefs.
eapply find_def_correct. eassumption. eassumption.
rewrite Setminus_Empty_set_neut_r.
eapply Disjoint_Included_l; [| eapply Disjoint_sym;
eapply def_closures_env_locs_Disjoint;
eassumption ].
rewrite <- well_formed_reach_subheap_same; [| |
| eapply def_funs_subheap; now eauto ].
eapply reachable_in_dom; [ | ].
eapply well_formed'_closed. eassumption.
eapply Included_trans; [| eapply env_locs_closed; eassumption ].
eapply reach'_extensive.
eapply well_formed'_closed. eassumption.
eapply Included_trans; [| eapply env_locs_closed; eassumption ].
eapply reach'_extensive.
rewrite <- closure_conversion_fundefs_Same_set; eassumption.
rewrite Setminus_Empty_set_neut_r. eapply unique_bindings_fun_in_fundefs.
eapply find_def_correct. eassumption. eassumption.
rewrite Setminus_Empty_set_neut_r.
eapply Disjoint_Included_r. eapply extend_fundefs'_image.
eapply Disjoint_Singleton_r. eassumption.
rewrite <- env_locs_setlist_Disjoint; [| eassumption | ].
eapply Disjoint_Included_r;
[| eapply def_closures_env_locs_Disjoint; eassumption ].
rewrite <- well_formed_reach_subheap_same;
[ | | | now eapply def_funs_subheap; eauto ].
eapply Included_trans; [| eapply env_locs_closed; eassumption ].
eapply reach'_set_monotonic. eapply env_locs_setlist_In. eassumption.
eapply well_formed_antimon; [| eapply well_formed'_closed; eassumption ].
eapply reach'_set_monotonic. eapply env_locs_setlist_In. eassumption.
eapply Included_trans; [| eapply env_locs_closed; eassumption ].
eapply Included_trans. eapply env_locs_setlist_In. eassumption.
eapply reach'_extensive.
eapply Disjoint_sym. eapply unique_bindings_fun_in_fundefs.
eapply find_def_correct. eassumption. eassumption.
* rewrite (Union_commut [set Γ'']), (Union_Same_set _ [set Γ'']).
eapply Disjoint_Singleton_l. intros Hc.
inv Hc. eapply Hdisg...
eapply Hdisg. eapply Included_trans; [| | eassumption ]. reflexivity.
unfold FV...
eapply Included_trans. eapply image_monotonic. eapply Setminus_Included.
eapply Included_trans. eapply extend_fundefs'_image. reflexivity.
* unfold FV. rewrite <- !Union_assoc.
eapply binding_in_map_setlist; [| eassumption ].
eapply binding_in_map_antimon. eapply Included_Union_compat.
eapply Setminus_Included. eapply Setminus_Included.
eapply binding_in_map_def_closures; [| eassumption ].
eapply binding_in_map_antimon.
rewrite <- Hkey. reflexivity. rewrite <- Ha.
eapply binding_in_map_key_set.
* eapply unique_bindings_fun_in_fundefs.
eapply find_def_correct. eassumption. eassumption.
* eapply has_true_mut_fun_in_fundefs. eassumption.
eapply find_def_correct; eassumption.
* unfold FV. eapply Union_Disjoint_r.
eapply Union_Disjoint_r.
eapply unique_bindings_fun_in_fundefs.
eapply find_def_correct. eassumption. eassumption.
eapply Disjoint_Included_r. eapply Setminus_Included.
eapply unique_bindings_fun_in_fundefs.
eapply find_def_correct. eassumption. eassumption.
eapply Disjoint_Included_r. eapply Setminus_Included.
eapply Disjoint_Included; [| | eapply Hfresh ].
now eauto with Ensembles_DB.
eapply Included_trans; [| eapply fun_in_fundefs_bound_var_fundefs;
eapply find_def_correct; eassumption ]...
* intros [[H0 rho0] e0] [[H00 rho00] e00]. unfold PreG.
intros Hyp. eapply Hyp.
* intros [[[[H0 rho0] e0] c0] m0] [[[[H00 rho00] e00] c00] m00]. unfold PreG.
intros Hyp. eapply Hyp.
} }