-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathclosure_conversion_util.v
1840 lines (1690 loc) · 76.4 KB
/
closure_conversion_util.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
(* Syntactic properties of closure conversion. Part of the CertiCoq project.
* Author: Zoe Paraskevopoulou, 2016
*)
From SFS Require Import cps cps_util set_util identifiers ctx
Ensembles_util List_util functions tactics.
From SFS Require Import closure_conversion heap heap_defs space_sem compat.
From SFS Require Import Coqlib.
From Coq Require Import ZArith.Znumtheory ArithRing Relations.Relations Arith.Wf_nat
Lists.List MSets.MSets MSets.MSetRBT Numbers.BinNums
NArith.BinNat PArith.BinPos Sets.Ensembles Omega.
Import ListNotations.
Open Scope ctx_scope.
Open Scope fun_scope.
Close Scope Z_scope.
(** * Syntactic Properties of the closure conversion relation *)
Instance Proper_FV1 : Proper (Same_set _ ==> eq ==> eq ==> Same_set _) FV.
Proof.
intros s1 s2 Hseq s3 s4 Hseq' x1 x2 Heq; subst; unfold FV;
rewrite !Hseq at 1; reflexivity.
Qed.
Instance Proper_FV_cc : Proper (Same_set _ ==> eq ==> eq ==> eq ==> Same_set _) FV_cc.
Proof.
intros s1 s2 Hseq s3 s4 Hseq' x1 x2 Heq x3 x4 Heq'; subst; unfold FV_cc;
rewrite !Hseq at 1; reflexivity.
Qed.
Instance Proper_FV2 S : Proper (Same_set _ ==> eq ==> Same_set _) (FV S).
Proof.
intros s1 s2 Hseq x1 x2 Heq; subst; unfold FV.
rewrite !Hseq at 1. reflexivity.
Qed.
Instance Proper_FV_cc2 S : Proper (Same_set _ ==> eq ==> eq ==> Same_set _) (FV_cc S).
Proof.
intros s1 s2 Hseq x1 x2 Heq x3 x4 Heq'; subst; unfold FV_cc;
rewrite !Hseq at 1. reflexivity.
Qed.
Instance Proper_FV_cc3 S Funs : Proper (f_eq ==> eq ==> Same_set _) (FV_cc S Funs).
Proof.
intros f1 f2 Hfeq x1 x2 Heq; subst; unfold FV_cc.
rewrite Hfeq. reflexivity.
Qed.
(** [FV] and [FV_cc] lemmas *)
Lemma FV_Union1 Scope Funs FVs S :
FV (S :|: Scope) Funs FVs \subset
S :|: FV Scope Funs FVs.
Proof.
unfold FV.
now eauto 20 with Ensembles_DB.
Qed.
Lemma FV_cc_Union1 Scope Funs fenv Γ S :
FV_cc (S :|: Scope) Funs fenv Γ \subset
S :|: FV_cc Scope Funs fenv Γ.
Proof.
unfold FV_cc.
now eauto 20 with Ensembles_DB.
Qed.
Lemma FV_Union2 Scope Funs FVs S :
FV Scope (S :|: Funs) FVs \subset
S :|: FV Scope Funs FVs.
Proof with (now eauto with Ensembles_DB).
unfold FV.
eapply Union_Included.
eapply Union_Included.
now eauto with Ensembles_DB.
rewrite Setminus_Union_distr.
now eauto with Ensembles_DB.
now eauto with Ensembles_DB.
Qed.
Lemma FV_cc_Union2 Scope Funs fenv Γ S :
FV_cc Scope (S :|: Funs) fenv Γ \subset
S :|: (image fenv S) :|: FV_cc Scope Funs fenv Γ.
Proof with (now eauto with Ensembles_DB).
unfold FV_cc.
rewrite !Setminus_Union_distr at 1.
rewrite !image_Union.
eapply Union_Included.
eapply Union_Included.
eapply Union_Included...
eapply Union_Included...
now eauto with Ensembles_DB.
Qed.
Lemma FV_cc_Setminus1 Scope Funs fenv Γ S {Hd : Decidable S} :
FV_cc (Scope \\ S) Funs fenv Γ \subset
S :|: (image fenv S) :|: FV_cc Scope Funs fenv Γ.
Proof.
unfold FV_cc.
eapply Union_Included;
[| now eauto with Ensembles_DB ]...
eapply Union_Included.
eapply Union_Included;
[ now eauto with Ensembles_DB |].
eapply Included_trans.
eapply Setminus_Setminus_Included. eassumption.
eapply Union_Included;
now eauto with Ensembles_DB.
eapply Included_trans.
eapply image_monotonic.
eapply Setminus_Setminus_Included. eassumption.
rewrite image_Union.
eapply Union_Included;
now eauto with Ensembles_DB.
Qed.
Lemma FV_cc_Setminus2 Scope Funs fenv Γ S {Hd : Decidable S} :
FV_cc Scope (Funs \\ S) fenv Γ \subset
FV_cc Scope Funs fenv Γ.
Proof.
unfold FV_cc.
eapply Union_Included;
[| now eauto with Ensembles_DB ]...
eapply Union_Included. now eauto with Ensembles_DB.
eapply Included_Union_preserv_l. eapply Included_Union_preserv_r.
now eauto with Ensembles_DB.
Qed.
Lemma FV_Setminus1 Scope Funs FVs S {Hd : Decidable S} :
FV (Scope \\ S) Funs FVs \subset
S :|: FV Scope Funs FVs.
Proof.
unfold FV.
eapply Union_Included.
eapply Union_Included;
[ now eauto with Ensembles_DB |].
eapply Included_trans.
eapply Setminus_Setminus_Included. eassumption.
eapply Union_Included;
now eauto with Ensembles_DB.
eapply Included_trans.
rewrite Union_commut. rewrite <- !Setminus_Union.
eapply Setminus_Setminus_Included. eassumption.
rewrite Setminus_Union, Union_commut.
now eauto with Ensembles_DB.
Qed.
Lemma FV_cc_Funs_monotonic Scope Funs Funs' fenv Γ :
Funs' \subset Funs ->
FV_cc Scope Funs' fenv Γ \subset FV_cc Scope Funs fenv Γ.
Proof.
unfold FV_cc. intros Hsub.
eapply Included_Union_compat; [| reflexivity ].
eapply Included_Union_compat.
eapply Included_Union_compat. reflexivity.
now eauto with Ensembles_DB.
eapply image_monotonic. now eauto with Ensembles_DB.
Qed.
Lemma FV_Setminus2 Scope Funs FVs S {Hd : Decidable S} :
FV Scope (Funs \\ S) FVs \subset
S :|: FV Scope Funs FVs.
Proof.
unfold FV.
eapply Union_Included.
eapply Union_Included;
[ now eauto with Ensembles_DB |].
now eauto with Ensembles_DB.
rewrite <- !Setminus_Union.
eapply Included_trans. eapply Setminus_Setminus_Included.
eassumption. now eauto with Ensembles_DB.
Qed.
Lemma extend_fundefs'_get_s f B x z :
z \in name_in_fundefs B ->
extend_fundefs' f B x z = x.
Proof.
intros Heq. unfold extend_fundefs'.
destruct (Dec z); eauto.
exfalso; eauto.
Qed.
Lemma extend_fundefs'_get_o f B x z :
~ z \in name_in_fundefs B ->
extend_fundefs' f B x z = f z.
Proof.
intros Heq. unfold extend_fundefs'.
destruct (Dec z); eauto.
exfalso; eauto.
Qed.
Lemma extend_fundefs'_image f B x :
image (extend_fundefs' f B x) (name_in_fundefs B) \subset [set x].
Proof.
intros y Hin.
destruct Hin as [z [Hin' Heq]].
rewrite extend_fundefs'_get_s in Heq. subst; eauto.
eassumption.
Qed.
Lemma extend_fundefs'_image_Included f B x S :
image (extend_fundefs' f B x) S \subset x |: image f S.
Proof.
intros y Hin.
destruct Hin as [z [Hin' Heq]].
unfold extend_fundefs' in *.
destruct (Dec z); subst; eauto.
right. eexists; split; eauto.
Qed.
Lemma extend_fundefs'_image_Included' f B x S :
image (extend_fundefs' f B x) S \subset x |: image f (S \\ name_in_fundefs B).
Proof.
intros y Hin.
destruct Hin as [z [Hin' Heq]].
unfold extend_fundefs' in *.
destruct (Dec z); subst; eauto.
right. eexists; split; eauto. constructor; eauto.
Qed.
Lemma extend_fundefs'_same_funs f B B' x :
name_in_fundefs B <--> name_in_fundefs B' ->
f_eq (extend_fundefs' f B x) (extend_fundefs' f B' x).
Proof.
intros Heq y. unfold extend_fundefs'. destruct Heq.
destruct (@Dec _ (name_in_fundefs B) _ y);
destruct (@Dec _ (name_in_fundefs B') _ y); eauto.
eapply H in n. now exfalso; eauto.
eapply H0 in n0. now exfalso; eauto.
Qed.
Lemma FV_cc_extend_fundefs Scope Funs fenv B x Γ :
FV_cc Scope Funs (extend_fundefs' fenv B x) Γ \subset
[set x] :|: FV_cc Scope Funs fenv Γ.
Proof with (now eauto with Ensembles_DB).
unfold FV_cc.
eapply Union_Included.
eapply Union_Included.
eapply Union_Included...
eapply Included_trans. eapply extend_fundefs'_image_Included...
now eauto with Ensembles_DB.
now eauto with Ensembles_DB.
Qed.
(** ** Proof that after closure conversion all functions are closed *)
Section CCUtils.
Variable clo_tag : cTag.
Lemma project_var_Scope Scope Scope' Funs Funs' fenv c Γ FVs x C :
project_var clo_tag Scope Funs fenv c Γ FVs x C Scope' Funs' ->
Scope' \subset x |: Scope.
Proof with now eauto with Ensembles_DB functions_BD.
intros Hvar; inv Hvar...
Qed.
Lemma project_vars_Scope Scope Scope' Funs Funs' fenv c Γ FVs xs C :
project_vars clo_tag Scope Funs fenv c Γ FVs xs C Scope' Funs' ->
Scope' \subset FromList xs :|: Scope.
Proof with now eauto with Ensembles_DB functions_BD.
intros Hvar; induction Hvar.
- eauto with Ensembles_DB.
- eapply Included_trans. eassumption.
rewrite FromList_cons. eapply Union_Included.
now eauto with Ensembles_DB.
eapply Included_trans. eapply project_var_Scope.
eassumption. now eauto with Ensembles_DB.
Qed.
Lemma project_var_Scope_l Scope Scope' Funs Funs' fenv c Γ FVs x C :
project_var clo_tag Scope Funs fenv c Γ FVs x C Scope' Funs' ->
Scope \subset Scope'.
Proof with now eauto with Ensembles_DB functions_BD.
intros Hvar; inv Hvar...
Qed.
Lemma project_vars_Scope_l Scope Scope' Funs Funs' fenv c Γ FVs xs C :
project_vars clo_tag Scope Funs fenv c Γ FVs xs C Scope' Funs' ->
Scope \subset Scope'.
Proof with now eauto with Ensembles_DB functions_BD.
intros Hvar; induction Hvar.
- eauto with Ensembles_DB.
- eapply Included_trans.
eapply project_var_Scope_l; eassumption.
eassumption.
Qed.
Lemma project_var_Funs Scope Scope' Funs Funs' fenv c Γ FVs x C :
project_var clo_tag Scope Funs fenv c Γ FVs x C Scope' Funs' ->
Funs \subset x |: Funs'.
Proof with now eauto with Ensembles_DB functions_BD.
intros Hvar; inv Hvar; try eauto with Ensembles_DB.
rewrite Union_Setminus_Included; eauto with Ensembles_DB typeclass_instances.
Qed.
Lemma project_vars_Funs Scope Scope' Funs Funs' fenv c Γ FVs xs C :
project_vars clo_tag Scope Funs fenv c Γ FVs xs C Scope' Funs' ->
Funs \subset FromList xs :|: Funs'.
Proof with now eauto with Ensembles_DB functions_BD.
intros Hvar; induction Hvar.
- eauto with Ensembles_DB.
- eapply Included_trans. eapply project_var_Funs. eassumption.
rewrite FromList_cons. eapply Union_Included.
now eauto with Ensembles_DB.
eapply Included_trans. eassumption.
now eauto with Ensembles_DB.
Qed.
Lemma project_var_Funs_l Scope Scope' Funs Funs' fenv c Γ FVs x C :
project_var clo_tag Scope Funs fenv c Γ FVs x C Scope' Funs' ->
Funs' \subset Funs.
Proof with now eauto with Ensembles_DB functions_BD.
intros Hvar; inv Hvar...
Qed.
Lemma project_vars_Funs_l Scope Scope' Funs Funs' fenv c Γ FVs xs C :
project_vars clo_tag Scope Funs fenv c Γ FVs xs C Scope' Funs' ->
Funs' \subset Funs.
Proof with now eauto with Ensembles_DB functions_BD.
intros Hvar; induction Hvar.
- eauto with Ensembles_DB.
- eapply Included_trans. eassumption.
eapply project_var_Funs_l; eassumption.
Qed.
Lemma project_var_occurs_free_ctx_Included Scope Scope' Funs Funs' fenv c Γ FVs x C e F:
project_var clo_tag Scope Funs fenv c Γ FVs x C Scope' Funs' ->
occurs_free e \subset x |: F ->
(FV_cc Scope Funs fenv Γ) \subset F ->
(occurs_free (C |[ e ]|)) \subset F.
Proof with now eauto with Ensembles_DB functions_BD.
intros Hproj Hsub Hsub'. inv Hproj.
- eapply Included_trans. eassumption.
eapply Union_Included; [| reflexivity ].
eapply Singleton_Included. eapply Hsub'. left. left. now left.
- simpl. normalize_occurs_free. rewrite !FromList_cons, !FromList_nil.
rewrite Union_Empty_set_neut_r. eapply Union_Included.
eapply Union_Included.
+ eapply Singleton_Included.
eapply Hsub'.
left. left. right. constructor; eassumption.
+ eapply Included_trans; [| eassumption ].
eapply Included_Union_preserv_l.
eapply Included_Union_preserv_r.
eapply Singleton_Included. now eapply In_image.
+ eapply Included_trans. eapply Included_Setminus_compat.
eassumption. reflexivity.
rewrite Setminus_Union_distr...
- simpl. normalize_occurs_free.
eapply Union_Included. eapply Singleton_Included.
eapply Hsub'. right. reflexivity.
eapply Included_trans. eapply Included_Setminus_compat.
eassumption. reflexivity.
rewrite Setminus_Union_distr...
Qed.
Lemma project_var_Union_eq (Scope Scope' Funs Funs' : Ensemble var)
(fenv : var -> var) (c : cTag) (Γ : var) (FVs : list var)
(xs : var) (C1 : exp_ctx) :
project_var clo_tag Scope Funs fenv c Γ FVs xs C1 Scope' Funs' ->
~ xs \in FromList FVs ->
Scope' :|: Funs' <--> Scope :|: Funs.
Proof.
intros Hv Hnin. assert (Hv' := Hv). inv Hv.
- reflexivity.
- rewrite (Union_commut [set xs]), <- Union_assoc.
rewrite <- Union_Setminus_Same_set. reflexivity.
tci. now eapply Singleton_Included.
- exfalso. eapply Hnin. eapply nthN_In. eassumption.
Qed.
Lemma project_var_In Scope Scope' Funs Funs' fenv c Γ FVs x C :
project_var clo_tag Scope Funs fenv c Γ FVs x C Scope' Funs' ->
x \in Scope'.
Proof.
intros Hvar; inv Hvar; eauto.
Qed.
Lemma project_vars_In Scope Scope' Funs Funs' fenv c Γ FVs xs C :
project_vars clo_tag Scope Funs fenv c Γ FVs xs C Scope' Funs' ->
FromList xs \subset Scope'.
Proof with (now eauto with Ensembles_DB).
intros Hvar; induction Hvar; eauto.
- rewrite FromList_nil...
- rewrite FromList_cons.
eapply Union_Included; [| eassumption ].
eapply Singleton_Included.
eapply project_vars_Scope_l. eassumption.
eapply project_var_In. eassumption.
Qed.
Ltac normalize_sets :=
match goal with
| [|- context[FromList []]] => rewrite FromList_nil
| [|- context[FromList(_ :: _)]] => rewrite FromList_cons
| [|- context[FromList(_ ++ _)]] => rewrite FromList_app
| [|- context[FromList [_ ; _]]] => rewrite FromList_cons
| [|- context[Union _ _ (Empty_set _)]] =>
rewrite Union_Empty_set_neut_r
| [|- context[Union _ (Empty_set _) _]] =>
rewrite Union_Empty_set_neut_l
| [|- context[Setminus _ (Empty_set _) _]] =>
rewrite Setminus_Empty_set_abs_r
| [|- context[Setminus _ _ (Empty_set _)]] =>
rewrite Setminus_Empty_set_neut_r
| [ H : context[FromList []] |- _] => rewrite FromList_nil in H
| [ H : context[FromList(_ :: _)] |- _] => rewrite FromList_cons in H
| [ H : context[FromList(_ ++ _)] |- _] => rewrite FromList_app in H
| [ H : context[FromList [_ ; _]] |- _] => rewrite FromList_cons in H
| [ H : context[Union _ _ (Empty_set _)] |- _ ] =>
rewrite Union_Empty_set_neut_r in H
| [ H : context[Union _ (Empty_set _) _] |- _] =>
rewrite Union_Empty_set_neut_l in H
| [ H : context[Setminus _ (Empty_set _) _] |- _] =>
rewrite Setminus_Empty_set_abs_r in H
| [ H : context[Setminus _ _ (Empty_set _)] |- _] =>
rewrite Setminus_Empty_set_neut_r in H
end.
Lemma project_vars_occurs_free_ctx_Included Scope Scope' Funs Funs' fenv c Γ
FVs xs C e F:
project_vars clo_tag Scope Funs fenv c Γ FVs xs C Scope' Funs' ->
occurs_free e \subset (FromList xs) :|: F ->
(FV_cc Scope Funs fenv Γ) \subset F ->
(occurs_free (C |[ e ]|)) \subset F.
Proof with (now eauto with Ensembles_DB).
intros Hproj.
revert F. induction Hproj; intros F Hsub Hsub'; repeat normalize_sets.
- simpl...
- rewrite <- app_ctx_f_fuse.
eapply project_var_occurs_free_ctx_Included; try eassumption.
eapply IHHproj.
eapply Included_trans. eassumption.
now eauto with Ensembles_DB.
eapply Included_trans.
eapply Included_Union_compat.
eapply Included_Union_compat.
eapply Included_Union_compat.
eapply project_var_Scope. eassumption.
eapply Included_Setminus_compat.
eapply project_var_Funs_l. eassumption.
eapply project_var_Scope_l. eassumption.
eapply image_monotonic.
eapply Included_Setminus_compat.
eapply project_var_Funs_l. eassumption.
eapply project_var_Scope_l. eassumption.
reflexivity.
rewrite <- !(Union_assoc [set y]).
eapply Included_Union_compat. reflexivity. eassumption.
Qed.
Lemma project_var_free_funs_in_exp Scope Scope' Funs Funs' fenv c Γ FVs x C B e :
project_var clo_tag Scope Funs fenv c Γ FVs x C Scope' Funs' ->
(funs_in_exp B (C |[ e ]|) <-> funs_in_exp B e).
Proof.
intros Hvar; inv Hvar; [ split; now eauto | | ];
(split; intros Hf; [ now inv Hf | now constructor ]).
Qed.
Lemma project_vars_free_funs_in_exp Scope Scope' Funs Funs' fenv c Γ FVs xs C B e :
project_vars clo_tag Scope Funs fenv c Γ FVs xs C Scope' Funs' ->
(funs_in_exp B (C |[ e ]|) <-> funs_in_exp B e).
Proof.
intros Hvar; induction Hvar; [ now eauto |].
rewrite <- app_ctx_f_fuse, project_var_free_funs_in_exp; eassumption.
Qed.
Lemma project_var_FV_cc Scope Scope' Funs Funs' fenv c Γ FVs x C :
project_var clo_tag Scope Funs fenv c Γ FVs x C Scope' Funs' ->
FV_cc Scope' Funs' fenv Γ \subset x |: FV_cc Scope Funs fenv Γ.
Proof with (now eauto with Ensembles_DB).
intros Hvar; induction Hvar.
- simpl...
- eapply Included_trans. eapply FV_cc_Union1.
eapply Included_trans. eapply Included_Union_compat. reflexivity.
eapply FV_cc_Setminus2.
eauto with Ensembles_DB typeclass_instances. reflexivity.
- eapply Included_trans. eapply FV_cc_Union1. reflexivity.
Qed.
Lemma project_vars_FV_cc Scope Scope' Funs Funs' c Γ FVs xs C fenv :
project_vars clo_tag Scope Funs fenv c Γ FVs xs C Scope' Funs' ->
FV_cc Scope' Funs' fenv Γ \subset FromList xs :|: FV_cc Scope Funs fenv Γ.
Proof with (now eauto with Ensembles_DB).
intros Hvar; induction Hvar.
- simpl...
- eapply Included_trans. eassumption.
eapply Included_trans. eapply Included_Union_compat.
reflexivity. eapply project_var_FV_cc. eassumption.
normalize_sets...
Qed.
Lemma closure_conversion_fundefs_Same_set c Funs FVs B1 B2 :
Closure_conversion_fundefs clo_tag Funs c FVs B1 B2 ->
Same_set _ (name_in_fundefs B1) (name_in_fundefs B2).
Proof.
intros Hcc. induction Hcc.
- simpl. rewrite IHHcc. reflexivity.
- simpl. reflexivity.
Qed.
Lemma Closure_conversion_occurs_free_Included_mut :
(forall e Scope Funs fenv c Γ FVs e' C
(Hcc : Closure_conversion clo_tag Scope Funs fenv c Γ FVs e e' C),
occurs_free (C |[ e' ]|) \subset FV_cc Scope Funs fenv Γ) /\
(forall B c Funs FVs B'
(Hcc: Closure_conversion_fundefs clo_tag Funs c FVs B B'),
(occurs_free_fundefs B') \subset (name_in_fundefs Funs) \\ (name_in_fundefs B')).
Proof with now eauto with Ensembles_DB functions_BD.
exp_defs_induction IHe IHl IHB; intros; inv Hcc.
- eapply project_vars_occurs_free_ctx_Included;
[ eassumption | | now apply Included_refl ].
rewrite occurs_free_Econstr.
apply Union_Included. now eauto with Ensembles_DB.
apply Setminus_Included_Included_Union.
eapply Included_trans. eapply IHe. eassumption.
eapply Included_trans.
eapply FV_cc_Union1. rewrite Union_commut. eapply Included_Union_compat; [| reflexivity ].
eapply Included_trans. eapply project_vars_FV_cc. eassumption.
now eauto with Ensembles_DB.
- eapply project_var_occurs_free_ctx_Included;
[ eassumption | | now apply Included_refl ].
inv H10.
rewrite occurs_free_Ecase_nil...
- inv H10. destruct y as [c' e'].
inv H1. simpl in H; subst.
destruct H0 as [C' [e'' [Heq Hcce]]]. simpl in Heq; subst.
eapply Included_trans. now eapply occurs_free_Ecase_ctx_app.
apply Union_Included.
+ eapply project_var_occurs_free_ctx_Included;
[ eassumption | | now apply Included_refl ].
eapply Included_trans. eapply IHe. eassumption.
eapply project_var_FV_cc. eassumption.
+ eapply IHl. econstructor; eauto.
- eapply project_var_occurs_free_ctx_Included;
[ eassumption | | now apply Included_refl ].
rewrite occurs_free_Eproj.
eapply Union_Included. now eauto with Ensembles_DB.
apply Setminus_Included_Included_Union.
eapply Included_trans. eapply IHe. eassumption.
eapply Included_trans.
eapply FV_cc_Union1. rewrite Union_commut. eapply Included_Union_compat; [| reflexivity ].
eapply Included_trans. eapply project_var_FV_cc. eassumption.
now eauto with Ensembles_DB.
- rewrite <- app_ctx_f_fuse. simpl.
eapply project_vars_occurs_free_ctx_Included;
[ eassumption | | now apply Included_refl ].
normalize_occurs_free. eapply Union_Included.
now eauto with Ensembles_DB. normalize_occurs_free.
rewrite Setminus_Union_distr. eapply Union_Included.
eapply Included_trans. eapply Included_Setminus_compat.
eapply IHB. eassumption.
reflexivity. rewrite closure_conversion_fundefs_Same_set; [| eassumption ].
now eauto with Ensembles_DB.
do 2 eapply Setminus_Included_Included_Union.
eapply Included_trans. eapply IHe. eassumption.
eapply Included_trans. eapply FV_cc_Union2.
do 3 (rewrite closure_conversion_fundefs_Same_set with (B1 := f2) at 1;
[| eassumption ]).
eapply Union_Included.
eapply Union_Included.
now eauto with Ensembles_DB.
eapply Included_trans. rewrite extend_fundefs'_same_funs.
eapply extend_fundefs'_image. eapply closure_conversion_fundefs_Same_set.
eassumption.
now eauto with Ensembles_DB.
eapply Included_trans. eapply FV_cc_Setminus1. now eauto with typeclass_instances.
eapply Union_Included.
eapply Union_Included.
now eauto with Ensembles_DB.
rewrite <- (closure_conversion_fundefs_Same_set) at 1 ; [| eassumption ].
eapply Included_trans. eapply extend_fundefs'_image. now eauto with Ensembles_DB.
eapply Included_trans. eapply FV_cc_extend_fundefs.
eapply Union_Included.
now eauto with Ensembles_DB.
eapply Included_trans.
eapply project_vars_FV_cc.
eassumption.
now eauto with Ensembles_DB.
- eapply project_vars_occurs_free_ctx_Included;
[ eassumption | | now apply Included_refl ].
unfold AppClo. repeat normalize_occurs_free. repeat normalize_sets.
apply Union_Included. eauto with Ensembles_DB.
apply Setminus_Included_Included_Union.
apply Union_Included. eauto with Ensembles_DB.
apply Setminus_Included_Included_Union.
eauto 7 with Ensembles_DB.
- eapply project_vars_occurs_free_ctx_Included;
[ eassumption | | now apply Included_refl ].
rewrite occurs_free_Eprim.
apply Union_Included; [ now eauto with Ensembles_DB |].
apply Setminus_Included_Included_Union.
eapply Included_trans. eapply IHe. eassumption.
eapply Included_trans.
eapply FV_cc_Union1. rewrite Union_commut. eapply Included_Union_compat; [| reflexivity ].
eapply Included_trans. eapply project_vars_FV_cc. eassumption.
now eauto with Ensembles_DB.
- eapply project_var_occurs_free_ctx_Included;
[ eassumption | | now apply Included_refl ].
rewrite occurs_free_Ehalt...
- eapply Included_Setminus.
constructor. intros v' Hc. inv Hc.
now eapply fun_names_not_free_in_fundefs; eauto.
rewrite occurs_free_fundefs_Fcons.
apply Union_Included.
+ apply Setminus_Included_Included_Union.
eapply Included_trans. eapply IHe. eassumption.
unfold FV_cc. simpl.
rewrite FromList_cons.
eapply Union_Included; [ | now eauto with Ensembles_DB ].
rewrite <- (Union_assoc (FromList l)). eapply Union_Included.
now eauto with Ensembles_DB.
eapply Union_Included.
(* eapply Included_trans. eapply Included_Setminus_compat. *)
(* eapply Ensembles_util.Included_Intersection_l. reflexivity. *)
now eauto with Ensembles_DB.
eapply Included_trans. eapply image_monotonic.
now eapply Setminus_Included.
(* eapply Included_trans. now eapply Setminus_Included. *)
(* eapply Ensembles_util.Included_Intersection_l. *)
eapply Included_trans. eapply extend_fundefs'_image.
now eauto with Ensembles_DB.
+ apply Setminus_Included_Included_Union.
eapply Included_trans. eapply IHB. eassumption.
now eauto with Ensembles_DB.
- rewrite occurs_free_fundefs_Fnil. now apply Included_Empty_set.
Qed.
Corollary Closure_conversion_occurs_free_Included :
(forall e Scope Funs fenv c Γ FVs e' C
(Hcc : Closure_conversion clo_tag Scope Funs fenv c Γ FVs e e' C),
occurs_free (C |[ e' ]|) \subset (FV_cc Scope Funs fenv Γ)).
Proof.
now eapply Closure_conversion_occurs_free_Included_mut.
Qed.
Corollary Closure_conversion_occurs_free_fundefs_Included :
(forall B Funs c FVs B'
(Hcc: Closure_conversion_fundefs clo_tag Funs c FVs B B'),
Included _ (occurs_free_fundefs B') (Setminus _ (name_in_fundefs Funs) (name_in_fundefs B'))).
Proof.
intros.
eapply Closure_conversion_occurs_free_Included_mut; eauto.
Qed.
Lemma project_var_occurs_free_eq Scope Scope' Funs Funs' fenv c Γ FVs x C e:
project_var clo_tag Scope Funs fenv c Γ FVs x C Scope' Funs' ->
occurs_free (C |[ e ]|) \subset x |: occurs_free e :|: image fenv (Funs \\ Scope) :|:
(match FVs with [] => Empty_set _ | _ => [set Γ] end).
Proof with now eauto with Ensembles_DB functions_BD.
intros Hvar. inv Hvar.
- simpl. now eauto with Ensembles_DB.
- simpl. normalize_occurs_free. rewrite FromList_cons, FromList_singleton.
eapply Union_Included.
eapply Union_Included.
now eauto with Ensembles_DB.
eapply Singleton_Included. left. right. eexists; split; eauto.
now constructor; eauto.
now eauto with Ensembles_DB.
- simpl. destruct FVs. simpl in H1. congruence. normalize_occurs_free...
Qed.
Lemma project_vars_occurs_free_eq Scope Scope' Funs Funs' fenv c Γ FVs xs C e:
project_vars clo_tag Scope Funs fenv c Γ FVs xs C Scope' Funs' ->
occurs_free (C |[ e ]|) \subset FromList xs :|: occurs_free e :|: image fenv (Funs \\ Scope) :|:
(match FVs with [] => Empty_set _ | _ => [set Γ] end).
Proof with (now eauto with Ensembles_DB).
intros Hvars; induction Hvars. simpl...
simpl. rewrite <- app_ctx_f_fuse.
eapply Included_trans. eapply project_var_occurs_free_eq. eassumption.
normalize_sets.
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included; [ now eauto with Ensembles_DB | ].
eapply Included_trans. eassumption.
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included; [ now eauto with Ensembles_DB | ].
eapply Included_Union_preserv_l. eapply Included_Union_preserv_r.
eapply image_monotonic.
eapply Included_Setminus_compat. eapply project_var_Funs_l. eassumption.
eapply Included_trans. eapply project_var_Scope_l. eassumption. reflexivity.
Qed.
Lemma Closure_conversion_fv_sub e Scope Funs fenv c Γ FVs e' C
(Hcc : Closure_conversion clo_tag Scope Funs fenv c Γ FVs e e' C) :
occurs_free (C |[ e' ]|) \subset (occurs_free e) :|: image fenv (Funs \\ Scope) :|:
(match FVs with [] => Empty_set _ | _ => [set Γ] end).
Proof with (now eauto with Ensembles_DB).
revert Scope Funs fenv c Γ FVs e' C Hcc; induction e using exp_ind';
intros Scope Funs fenv c' Γ FVs e' C Hcc; inv Hcc.
- repeat normalize_occurs_free.
eapply Included_trans. eapply project_vars_occurs_free_eq.
eassumption. eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included. now eauto with Ensembles_DB.
normalize_occurs_free.
eapply Union_Included. now eauto with Ensembles_DB.
eapply Included_trans. eapply Included_Setminus_compat.
eapply IHe; eassumption. reflexivity.
rewrite !Setminus_Union_distr.
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included. now eauto with Ensembles_DB.
eapply Included_trans. eapply Setminus_Included.
eapply Included_Union_preserv_l.
eapply Included_Union_preserv_r. eapply image_monotonic.
eapply Included_Setminus_compat. eapply project_vars_Funs_l. eassumption.
eapply Included_trans. eapply project_vars_Scope_l. eassumption.
now eauto with Ensembles_DB.
- inv H10.
eapply Included_trans. eapply project_var_occurs_free_eq.
eassumption.
rewrite !occurs_free_Ecase_nil at 1...
- inv H10. destruct y as [c'' e'].
destruct H1 as [Heq [C' [e0' [Heq1 Hcc']]]]. simpl in *. subst.
normalize_occurs_free.
eapply Included_trans. eapply occurs_free_Ecase_ctx_app.
eapply Union_Included.
+ eapply Included_trans. eapply project_var_occurs_free_eq. eassumption.
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included. now eauto with Ensembles_DB.
eapply Included_trans. eapply IHe. eassumption.
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included. now eauto with Ensembles_DB.
eapply Included_Union_preserv_l.
eapply Included_Union_preserv_r. eapply image_monotonic.
eapply Included_Setminus_compat. eapply project_var_Funs_l. eassumption.
eapply Included_trans. eapply project_var_Scope_l. eassumption.
reflexivity.
+ eapply Included_trans. eapply IHe0. econstructor. eassumption.
eassumption.
now eauto with Ensembles_DB.
- repeat normalize_occurs_free.
eapply Included_trans. eapply project_var_occurs_free_eq.
eassumption. eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included. now eauto with Ensembles_DB.
normalize_occurs_free.
eapply Union_Included. now eauto with Ensembles_DB.
eapply Included_trans. eapply Included_Setminus_compat.
eapply IHe; eassumption. reflexivity.
rewrite !Setminus_Union_distr.
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included. now eauto with Ensembles_DB.
eapply Included_trans. eapply Setminus_Included.
eapply Included_Union_preserv_l.
eapply Included_Union_preserv_r. eapply image_monotonic.
eapply Included_Setminus_compat. eapply project_var_Funs_l. eassumption.
eapply Included_trans. eapply project_var_Scope_l. eassumption.
now eauto with Ensembles_DB.
- simpl. rewrite <- app_ctx_f_fuse.
simpl.
eapply Included_trans. eapply project_vars_occurs_free_eq.
eassumption. repeat normalize_occurs_free. rewrite <- !H1 at 1.
repeat (eapply Union_Included; [| now eauto with Ensembles_DB ]).
eapply Union_Included. now eauto with Ensembles_DB.
eapply Union_Included. now eauto with Ensembles_DB.
rewrite !Setminus_Union_distr.
eapply Union_Included.
eapply Setminus_Included_Included_Union.
eapply Included_trans. eapply Closure_conversion_occurs_free_fundefs_Included. eassumption.
rewrite <- !closure_conversion_fundefs_Same_set with (B1 := f2) (B2 := B') at 1; [| eassumption ]...
do 2 eapply Setminus_Included_Included_Union.
eapply Included_trans. eapply IHe; eassumption.
rewrite <- !closure_conversion_fundefs_Same_set with (B1 := f2) (B2 := B') at 1; [| eassumption ].
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included.
rewrite <- !Union_assoc. eapply Included_Union_preserv_r.
rewrite (Union_commut). rewrite <- !Union_assoc.
do 3 eapply Included_Union_preserv_r.
rewrite Union_Setminus_Included; tci; now eauto with Ensembles_DB.
eapply Included_trans. eapply extend_fundefs'_image_Included'.
eapply Union_Included. now eauto with Ensembles_DB.
do 3 eapply Included_Union_preserv_l.
eapply Included_Union_preserv_r.
eapply image_monotonic. rewrite !Setminus_Union_distr.
eapply Union_Included. now eauto with Ensembles_DB.
eapply Setminus_Included_Included_Union.
eapply Included_trans. eapply Setminus_Setminus_Included. tci.
eapply Included_Union_compat; [| reflexivity ].
eapply Included_Setminus_compat. eapply project_vars_Funs_l. eassumption.
eapply Included_trans. eapply project_vars_Scope_l. eassumption.
now eauto with Ensembles_DB.
- eapply Included_trans.
eapply project_vars_occurs_free_eq.
eassumption. eapply Union_Included; [| now eauto with Ensembles_DB ].
unfold AppClo; repeat normalize_occurs_free. normalize_sets.
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included; [ now eauto with Ensembles_DB |].
eapply Union_Included; [ now eauto with Ensembles_DB |].
rewrite Setminus_Union_distr.
eapply Union_Included; [ now eauto with Ensembles_DB |].
normalize_sets. rewrite !Setminus_Union_distr.
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included; [| now eauto with Ensembles_DB ]...
- repeat normalize_occurs_free.
eapply Included_trans. eapply project_vars_occurs_free_eq.
eassumption. eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included. now eauto with Ensembles_DB.
normalize_occurs_free.
eapply Union_Included. now eauto with Ensembles_DB.
eapply Included_trans. eapply Included_Setminus_compat.
eapply IHe; eassumption. reflexivity.
rewrite !Setminus_Union_distr.
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included. now eauto with Ensembles_DB.
eapply Included_trans. eapply Setminus_Included.
eapply Included_Union_preserv_l.
eapply Included_Union_preserv_r. eapply image_monotonic.
eapply Included_Setminus_compat. eapply project_vars_Funs_l. eassumption.
eapply Included_trans. eapply project_vars_Scope_l. eassumption.
now eauto with Ensembles_DB.
- repeat normalize_occurs_free.
eapply Included_trans. eapply project_var_occurs_free_eq.
eassumption. rewrite !occurs_free_Ehalt at 1...
Qed.
Corollary Closure_conversion_cc_fv_cor e Scope c Γ FVs e' C B
(Hcc : Closure_conversion clo_tag Scope (name_in_fundefs B)
(extend_fundefs' id B Γ) c Γ FVs e e' C) :
~ Γ \in Scope :|: (name_in_fundefs B) ->
Disjoint _ (name_in_fundefs B) Scope ->
occurs_free (C |[ e' ]|) \subset
((occurs_free e) :&: Scope) :|: ((occurs_free e) :&: (name_in_fundefs B \\ Scope)) :|: [set Γ].
Proof with (now eauto with Ensembles_DB).
intros Hc Hdis.
assert (Hcc' := Hcc). eapply Closure_conversion_fv_sub in Hcc'.
assert (Hsub1 : occurs_free (C |[ e' ]|) \subset
occurs_free e :|: [set Γ]).
{ eapply Included_trans. eassumption.
eapply Union_Included; [| destruct FVs; now eauto with Ensembles_DB ].
eapply Union_Included; [ now eauto with Ensembles_DB | ].
eapply Included_trans. eapply image_monotonic. eapply Setminus_Included.
eapply Included_trans. eapply extend_fundefs'_image.
now eauto with Ensembles_DB. }
rewrite (Setminus_Disjoint _ Scope); [| eassumption ].
eapply Closure_conversion_occurs_free_Included in Hcc.
assert (Hsub2 : occurs_free (C |[ e' ]|) \subset
Scope :|: (name_in_fundefs B \\ Scope) :|: [set Γ]).
{ eapply Included_trans. now apply Hcc.
eapply Union_Included; [| now eauto with Ensembles_DB ].
eapply Union_Included; [ now eauto with Ensembles_DB | ].
eapply Included_trans. eapply image_monotonic. eapply Setminus_Included.
eapply Included_trans. eapply extend_fundefs'_image.
now eauto with Ensembles_DB. }
eapply Included_trans. eapply Included_Intersection. now eapply Hsub1. now eapply Hsub2.
rewrite <- Union_Intersection_distr. eapply Included_Union_compat; [| reflexivity ].
rewrite Intersection_commut. rewrite Intersection_Union_distr. eapply Included_Union_compat.
rewrite !(Intersection_commut _ (occurs_free e)). reflexivity.
rewrite Intersection_commut. eapply Included_Intersection_compat...
Qed.
Lemma Closure_conversion_closed_fundefs_mut :
(forall e Scope Funs fenv c Γ FVs e' C
(Hcc : Closure_conversion clo_tag Scope Funs fenv c Γ FVs e e' C),
closed_fundefs_in_exp (C |[ e' ]|)) /\
(forall B Funs c FVs B'
(Hcc: Closure_conversion_fundefs clo_tag Funs c FVs B B'),
closed_fundefs_in_fundefs B').
Proof.
exp_defs_induction IHe IHl IHB; intros; inv Hcc.
- intros B HB. rewrite project_vars_free_funs_in_exp in HB; [| eassumption ].
inv HB. eapply IHe; eassumption.
- inv H10.
intros B HB. rewrite project_var_free_funs_in_exp in HB; [| eassumption ].
inv HB. inv H3.
- inv H10. destruct H1 as [Heq [C' [e' [Heq' Hcc']]]]. destruct y as [t e''].
simpl in *; subst.
intros B HB. rewrite project_var_free_funs_in_exp in HB; [| eassumption ].
inv HB. inv H4.
+ inv H. eapply IHe; eassumption.
+ eapply IHl. now econstructor; eauto.
rewrite project_var_free_funs_in_exp.
econstructor; eassumption. eassumption.
- intros B HB. rewrite project_var_free_funs_in_exp in HB; [| eassumption ].
inv HB. eapply IHe; eassumption.
- rewrite <- app_ctx_f_fuse. intros B HB.
rewrite project_vars_free_funs_in_exp in HB; [| eassumption ].
simpl in HB. inv HB. inv H5.
+ split; [| now apply Included_Empty_set ].
eapply Included_trans.
eapply Closure_conversion_occurs_free_Included_mut. eassumption.
rewrite closure_conversion_fundefs_Same_set; [| eassumption ].
rewrite Setminus_Same_set_Empty_set. now apply Included_Empty_set.
+ eapply IHe; eassumption.
+ eapply IHB; eassumption.
- intros B HB. rewrite project_vars_free_funs_in_exp in HB; [| eassumption ].
inv HB. inv H1. inv H4.
- intros B HB. rewrite project_vars_free_funs_in_exp in HB; [| eassumption ].
inv HB. eapply IHe; eassumption.
- intros B HB. rewrite project_var_free_funs_in_exp in HB; [| eassumption ].
inv HB.
- intros B HB. inv HB.
+ eapply IHe; eassumption.
+ eapply IHB; eassumption.
- intros B HB. inv HB.
Qed.
(** * Lemmas about [project_var] and [project_vars] *)
(* Lemma project_var_free_set_Included Scope c Γ FVs x x' C S S' :
project_var Scope c Γ FVs S x x' C S' ->
Included _ S' S.
Proof with now eauto with Ensembles_DB.
intros Hproj. inv Hproj...
Qed.
Lemma project_vars_free_set_Included Scope c Γ FVs xs xs' C S S' :
project_vars Scope c Γ FVs S xs xs' C S' ->
Included _ S' S.
Proof.
intros Hproj. induction Hproj.
- now apply Included_refl.
- eapply Included_trans. eassumption.
eapply project_var_free_set_Included. eassumption.
Qed.
Lemma project_var_not_In_free_set Scope c Γ FVs x x' C S S' :
project_var Scope c Γ FVs S x x' C S' ->
Disjoint _ S Scope ->
~ In _ S' x'.
Proof.
intros Hproj Hd. inv Hproj; intros Hc.
- eapply Hd. constructor; eauto.
- inv Hc. exfalso. eauto.
Qed.
Lemma project_vars_not_In_free_set Scope c Γ FVs xs xs' C S S' :
project_vars Scope c Γ FVs S xs xs' C S' ->
Disjoint _ S Scope ->
Disjoint _ S' (FromList xs').
Proof.
intros Hproj Hd. induction Hproj.
- constructor. intros x Hc. inv Hc. rewrite FromList_nil in H0.
eapply not_In_Empty_set. eassumption.
- rewrite FromList_cons. eapply Disjoint_sym.
eapply Union_Disjoint_l.
+ eapply Disjoint_Included_r_sym.
eapply project_vars_free_set_Included; eassumption.
eapply Disjoint_Singleton_r.
eapply project_var_not_In_free_set; eassumption.
+ eapply Disjoint_sym. eapply IHHproj.
eapply Disjoint_Included_l.
eapply project_var_free_set_Included. eassumption.
eassumption.
Qed.
*)
Lemma project_var_FV_eq Scope Scope' Funs Funs' fenv c Γ FVs x C :
project_var clo_tag Scope Funs fenv c Γ FVs x C Scope' Funs' ->
FV Scope Funs FVs <--> FV Scope' Funs' FVs.
Proof.
unfold FV. intros Hvar. inv Hvar; eauto.
- reflexivity.
- rewrite !(Union_commut [set x] Scope) at 2.
rewrite (Union_Setminus_Included _ _ [set x]); eauto with Ensembles_DB typeclass_instances.
rewrite Setminus_Union.
rewrite (Union_Same_set [set x] (Scope :|: [set x])); eauto with Ensembles_DB typeclass_instances.
rewrite <- (Setminus_Union Funs ).
rewrite (Union_Setminus_Included _ _ [set x]); eauto with Ensembles_DB typeclass_instances.
rewrite <- (Union_assoc Scope [set x] Funs).
rewrite (Union_Same_set [set x] Funs); eauto with Ensembles_DB typeclass_instances.
rewrite (Union_commut [set x]). rewrite <- (Union_assoc _ [set x] (Funs \\ Scope)).
rewrite (Union_Same_set [set x] (Funs \\ Scope)); eauto with Ensembles_DB typeclass_instances.
- rewrite !(Union_commut [set x] Scope) at 2.
rewrite <- (Union_assoc Scope [set x] Funs').