-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathUntangle.v
1089 lines (987 loc) · 37 KB
/
Untangle.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
Require Import Psatz.
Require Import PeanoNat.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Export SystemFR.ScalaDepSugar.
Require Export SystemFR.ReducibilitySubtype.
Require Export SystemFR.EquivalentContext.
Require Export SystemFR.TOpenTClose.
Require Export SystemFR.TermListReducible.
Require Export SystemFR.FVLemmasClose.
Require Export SystemFR.WFLemmasClose.
Require Export SystemFR.Existss.
Require Export SystemFR.NormalizationPi.
Require Export SystemFR.NormalizationExists.
Require Export SystemFR.NormalizationList.
Require Export SystemFR.Trail.
Opaque reducible_values.
Definition incomparable_keys keys : Prop :=
forall key1 key2, key1 ∈ keys -> key2 ∈ keys ->
key1 = key2 \/ (~ prefix key1 key2 /\ ~ prefix key2 key1).
Inductive untangle: context -> tree -> tree -> Prop :=
| UntangleFreshen:
forall Γ T0 T T' template xs ys keys m x,
is_erased_type template ->
is_erased_type T0 ->
wf template 0 ->
wf T0 1 ->
subset (fv T0) (support Γ) ->
~ x ∈ fv_context Γ ->
Forall (fun key => [ key : T_key ]v) keys ->
functional (combine ys keys) ->
functional (combine keys ys) ->
incomparable_keys keys ->
~ m ∈ fv template ->
length keys = length xs ->
length ys = length xs ->
(forall y, y ∈ ys -> y ∈ support Γ -> False) ->
(forall y, y ∈ ys -> y ∈ fv template -> False) ->
(forall x, x ∈ xs -> x ∈ support Γ -> False) ->
(forall x, x ∈ fv template -> x ∈ xs \/ x ∈ support Γ) ->
T = substitute template
(List.combine xs (List.map (fun key => select key (fvar m term_var)) keys)) ->
T' = substitute template
(List.combine xs (List.map (fun y => fvar y term_var) ys)) ->
untangle ((x, T_tree) :: Γ)
(open 0 T0 (fvar x term_var))
(open 0 (close 0 T m) (fvar x term_var)) ->
untangle Γ (T_exists T_tree T0) (T_exists_vars ys T_tree T')
| UntangleAbstract:
forall Γ T A x T0,
is_erased_type A ->
is_erased_type T ->
is_erased_type T0 ->
wf T0 1 ->
wf T 1 ->
wf A 0 ->
subset (fv A) (support Γ) ->
subset (fv T) (support Γ) ->
subset (fv T0) (support Γ) ->
~ x ∈ fv_context Γ ->
[ Γ ⊫ tnil : A ] ->
untangle ((x, T_tree) :: Γ)
(open 0 T0 (fvar x term_var))
(open 0 (shift_open 0 T (tlookup A (lvar 0 term_var))) (fvar x term_var)) ->
untangle Γ (T_exists T_tree T0) (T_exists A T)
| UntanglePi:
forall Γ S S' T T' x,
is_erased_type T ->
is_erased_type T' ->
wf T 1 ->
wf T' 1 ->
subset (fv T) (support Γ) ->
subset (fv T') (support Γ) ->
~ x ∈ pfv S term_var ->
~ x ∈ pfv S' term_var ->
~ x ∈ pfv_context Γ term_var ->
untangle Γ S S' ->
untangle ((x, S') :: Γ) (open 0 T (fvar x term_var)) (open 0 T' (fvar x term_var)) ->
untangle Γ (T_arrow S T) (T_arrow S' T')
| UntangleExists:
forall Γ S S' T T' x,
is_erased_type T ->
is_erased_type T' ->
wf T 1 ->
wf T' 1 ->
subset (fv T) (support Γ) ->
subset (fv T') (support Γ) ->
~ x ∈ pfv S' term_var ->
~ x ∈ pfv_context Γ term_var ->
untangle Γ S S' ->
untangle ((x, S') :: Γ) (open 0 T (fvar x term_var)) (open 0 T' (fvar x term_var)) ->
untangle Γ (T_exists S T) (T_exists S' T')
| UntangleCons:
forall Γ H H' T T',
is_erased_type T ->
is_erased_type T' ->
wf T 0 ->
wf T' 0 ->
untangle Γ H H' ->
untangle Γ T T' ->
untangle Γ (Cons H T) (Cons H' T')
| UntangleListMatch:
forall Γ T1 T2 T1' T2' t x y,
wf T2 2 ->
wf T2' 2 ->
is_erased_type T2 ->
is_erased_type T2' ->
subset (fv T2) (support Γ) ->
subset (fv T2') (support Γ) ->
wf t 0 ->
x <> y ->
~ x ∈ fv_context Γ ->
~ y ∈ fv_context Γ ->
~ x ∈ fv T2 ->
~ x ∈ fv T2' ->
~ y ∈ fv T2 ->
~ y ∈ fv T2' ->
untangle Γ T1 T1' ->
untangle ((x, T_top) :: (y, List) :: Γ)
(open 0 (open 1 T2 (fvar x term_var)) (fvar y term_var))
(open 0 (open 1 T2' (fvar x term_var)) (fvar y term_var)) ->
untangle Γ (List_Match t T1 T2) (List_Match t T1' T2')
| UntangleSingleton:
forall Γ T T' t,
untangle Γ T T' ->
untangle Γ (T_singleton T t) (T_singleton T' t)
| UntangleRefl: forall Γ T, untangle Γ T T
.
Lemma list_map_subst:
forall l f t m v,
(forall e, e ∈ l -> m ∈ fv e -> False) ->
List.map (fun e => app f (pp (psubstitute e ((m, v) :: nil) term_var) t)) l =
List.map (fun e => app f (pp e t)) l.
Proof.
induction l; repeat step || t_substitutions || t_equality; eauto.
Qed.
Lemma list_map_subst2:
forall l f m v,
(forall e, e ∈ l -> m ∈ fv e -> False) ->
List.map (fun key => app f (psubstitute (select key (fvar m term_var))
((m, v) :: nil) term_var)) l =
List.map (fun key => app f (select key v)) l.
Proof.
induction l; repeat step || t_substitutions || rewrite psubstitute_select || t_equality; eauto.
Qed.
Lemma combine_equivalent_wfs1:
forall ts1 ts2 xs,
length xs = length ts1 ->
length xs = length ts2 ->
(forall t1 t2, (t1, t2) ∈ combine ts1 ts2 -> [ t1 ≡ t2 ]) ->
wfs (combine xs ts1) 0.
Proof.
induction ts1; destruct ts2; destruct xs;
repeat step || list_utils || list_utils2; eauto.
unshelve epose proof (H1 a t _); steps; t_closer.
Qed.
Lemma combine_equivalent_wfs2:
forall ts1 ts2 xs,
length xs = length ts1 ->
length xs = length ts2 ->
(forall t1 t2, (t1, t2) ∈ combine ts1 ts2 -> [ t1 ≡ t2 ]) ->
wfs (combine xs ts2) 0.
Proof.
induction ts1; destruct ts2; destruct xs;
repeat step || list_utils || list_utils2; eauto.
unshelve epose proof (H1 a t _); steps; t_closer.
Qed.
Lemma combine_wfs3:
forall xs ts,
(forall x t, (x, t) ∈ combine xs ts -> wf t 0) ->
wfs (combine xs ts) 0.
Proof.
induction xs; destruct ts;
repeat step || list_utils || list_utils2; eauto.
Qed.
Lemma combine_wfs4:
forall xs ts,
(forall t, t ∈ ts -> wf t 0) ->
wfs (combine xs ts) 0.
Proof.
induction xs; destruct ts;
repeat step || list_utils || list_utils2; eauto.
Qed.
Lemma combine_wfs5:
forall xs ts,
Forall (fun v => wf v 0) ts ->
wfs (combine xs ts) 0.
Proof.
intros; apply combine_wfs4; apply Forall_forall; auto.
Qed.
Lemma combine_equivalent_is_erased_term:
forall xs ts,
Forall is_erased_term ts ->
erased_terms (combine xs ts).
Proof.
induction xs; destruct ts;
repeat step || list_utils || list_utils2; eauto.
Qed.
Lemma combine_closed_mapping:
forall xs ts tag,
Forall (fun t => pfv t tag = nil) ts ->
pclosed_mapping (combine xs ts) tag.
Proof.
induction xs; destruct ts;
repeat step || list_utils || list_utils2; eauto.
Qed.
Lemma reducibility_equivalent_substititions_helper:
forall xs T ρ v ts1 ts2,
[ ρ ⊨ v : psubstitute T (combine xs ts1) term_var ]v ->
valid_interpretation ρ ->
length ts1 = length xs ->
length ts2 = length xs ->
is_erased_type T ->
wf T 0 ->
(forall t1 t2, (t1, t2) ∈ combine ts1 ts2 -> [ t1 ≡ t2 ]) ->
Forall (fun v => wf v 0) ts1 ->
Forall (fun v => wf v 0) ts2 ->
Forall (fun v => pfv v term_var = nil) ts1 ->
Forall (fun v => pfv v term_var = nil) ts2 ->
Forall is_erased_term ts1 ->
Forall is_erased_term ts2 ->
(forall x, x ∈ fv T -> x ∈ xs) ->
[ ρ ⊨ v : psubstitute T (combine xs ts2) term_var ]v.
Proof.
induction xs; repeat step || t_substitutions.
rewrite <- (open_close2 T a 0) by auto.
rewrite substitute_open3; steps;
try solve [ apply combine_equivalent_wfs4; repeat step || rewrite Forall_forall in *; eauto ];
try solve [ apply_anywhere fv_close; steps ].
eapply reducibility_open_equivalent; eauto;
repeat step || apply subst_erased_type || apply wf_subst || apply wf_close;
eauto with erased wf fv;
eauto using combine_equivalent_is_erased_term.
- rewrite substitute_open2;
repeat step || list_utils || list_utils2 ||
rewrite open_close by auto;
eauto using combine_wfs5.
apply IHxs with l0;
repeat step || apply subst_erased_type || apply wf_subst || t_pfv_in_subst;
eauto.
+ rewrite <- substitute_cons; steps.
+ clear_marked; apply pfv_in_subst2 in H6; steps.
instantiate_any; steps.
- apply wfs_monotone2.
apply combine_wfs4; repeat step || rewrite Forall_forall in *; eauto with wf.
- apply fv_nils2; repeat step || list_utils2 || unfold subset || apply_anywhere fv_close;
eauto using combine_closed_mapping.
apply_anywhere H12; steps.
- apply combine_wfs5; auto.
Qed.
Lemma reducibility_equivalent_substititions:
forall xs T ρ v ts1 ts2,
[ ρ ⊨ v : psubstitute T (combine xs ts1) term_var ]v ->
valid_interpretation ρ ->
length ts1 = length xs ->
length ts2 = length xs ->
is_erased_type T ->
wf T 0 ->
(forall t1 t2, (t1, t2) ∈ combine ts1 ts2 -> [ t1 ≡ t2 ]) ->
(forall x, x ∈ fv T -> x ∈ xs) ->
[ ρ ⊨ v : psubstitute T (combine xs ts2) term_var ]v.
Proof.
intros; eapply reducibility_equivalent_substititions_helper; try eassumption;
repeat step || rewrite Forall_forall || find_fst || find_snd;
eauto using combine_equivalent_wfs1;
try solve [ instantiate_any; t_closer ].
Qed.
Lemma erased_terms_combine:
forall xs f ys,
is_erased_term f ->
erased_terms (combine xs (List.map (fun y : nat => app f (fvar y term_var)) ys)).
Proof.
induction xs; destruct ys; steps.
Qed.
Lemma wfs_combine7:
forall xs keys m,
Forall (fun key => [ key : T_key ]v) keys ->
length keys = length xs ->
wfs (combine xs (List.map (fun key : tree => select key (fvar m term_var)) keys)) 0.
Proof.
induction xs; destruct keys;
repeat step || apply wf_select;
eauto using reducible_val_wf with step_tactic.
Qed.
Lemma list_map_subst3:
forall keys m v,
Forall (fun key => [ key : T_key ]v) keys ->
List.map (fun x => psubstitute (select x (fvar m term_var)) ((m, v) :: nil) term_var) keys =
List.map (fun x => select x v) keys.
Proof.
induction keys;
repeat step || rewrite psubstitute_select || t_substitutions.
rewrite substitute_nothing5; eauto using reducible_val_fv with step_tactic.
apply f_equal; eauto.
Qed.
Lemma wfs_combine8:
forall xs ys,
length ys = length xs ->
wfs (combine xs (List.map (fun y : nat => fvar y term_var) ys)) 0.
Proof.
induction xs; destruct ys; intros;
repeat step; eauto.
Qed.
Lemma erased_terms_combine2:
forall xs ys,
length ys = length xs ->
erased_terms (combine xs (List.map (fun y => fvar y term_var) ys)).
Proof.
induction xs; destruct ys; intros;
repeat step; eauto.
Qed.
Lemma erased_terms_combine3:
forall xs keys m,
length keys = length xs ->
Forall (fun key => [ key : T_key ]v) keys ->
erased_terms (combine xs (List.map (fun key => select key (fvar m term_var)) keys)).
Proof.
induction xs; destruct keys; intros;
repeat step || apply is_erased_term_select;
try solve [ eapply reducible_values_erased; eauto; steps ];
eauto.
Qed.
Lemma forall_select_type:
forall keys tr,
Forall (fun key => [ key : T_key ]v) keys ->
[ tr : T_tree ]v ->
Forall (fun t => [ t : T_tree ]v) (List.map (fun key => select key tr) keys).
Proof.
induction keys; repeat step || constructor; eauto using select_type.
Qed.
Lemma list_map_subst4:
forall keys tr l,
Forall (fun key => [ key : T_key ]v) keys ->
[ tr : T_tree ]v ->
List.map (fun key => psubstitute (select key tr) l term_var) keys =
List.map (fun key => select key tr) keys.
Proof.
induction keys; repeat step || t_substitutions || rewrite psubstitute_select.
repeat rewrite substitute_nothing5 by eauto using reducible_val_fv with step_tactic.
apply f_equal; eauto.
Qed.
Lemma list_map_subst5:
forall ys l,
(forall y, y ∈ ys -> y ∈ support l -> False) ->
List.map (fun x =>
match lookup PeanoNat.Nat.eq_dec l x with
| Some e => e
| None => fvar x term_var
end) ys =
List.map (fun x => fvar x term_var) ys.
Proof.
induction ys; repeat step || t_lookup || apply f_equal; eauto with exfalso.
Qed.
Lemma list_map_change_list:
forall A B C (l1: list A) (l2: list B) (f: A -> C) (g: B -> C),
(forall a b, (a, b) ∈ combine l1 l2 -> f a = g b) ->
length l1 = length l2 ->
List.map f l1 = List.map g l2.
Proof.
induction l1; destruct l2; repeat step || f_equal.
Qed.
Lemma lookup_combine:
forall A B (l1: list nat) (l2: list A) x a (f: A -> B),
length l1 = length l2 ->
functional (combine l1 l2) ->
(x, a) ∈ combine l1 l2 ->
lookup Nat.eq_dec (combine l1 (List.map f l2)) x = Some (f a).
Proof.
induction l1; destruct l2; repeat step || step_inversion NoDup;
eauto using in_combine_l with exfalso;
try solve [ eapply_anywhere functional_head; eauto; steps ];
eauto using functional_tail.
Qed.
Lemma list_map_subst7:
forall ys keys a,
length ys = length keys ->
functional (combine ys keys) ->
List.map
(fun y =>
match
lookup PeanoNat.Nat.eq_dec
(combine ys (List.map (fun key => select key a) keys)) y
with
| Some e1 => e1
| None => fvar y term_var
end) ys =
List.map (fun key => select key a) keys.
Proof.
intros; apply list_map_change_list; repeat step || step_inversion NoDup;
eauto using in_combine_l with exfalso;
try solve [ erewrite_anywhere lookup_combine; eauto; steps ].
Qed.
Lemma lookup_combine2:
forall A B (l1: list nat) (l2: list A) x a (f: A -> B),
length l1 = length l2 ->
functional (combine l1 l2) ->
(x, a) ∈ combine l1 l2 ->
lookup Nat.eq_dec (combine l1 l2) x = Some a.
Proof.
induction l1; destruct l2; repeat step || step_inversion NoDup;
eauto using in_combine_l with exfalso;
try solve [ eapply_anywhere functional_head; eauto; steps ];
eauto using functional_tail.
Qed.
Lemma list_map_subst8:
forall ys vs l,
length vs = length ys ->
functional (combine ys vs) ->
(forall y, y ∈ ys -> y ∈ support l -> False) ->
List.map
(fun x =>
psubstitute
match lookup Nat.eq_dec l x with
| Some e => e
| None => fvar x term_var
end (combine ys vs) term_var) ys = vs.
Proof.
intros.
rewrite <- map_id.
apply list_map_change_list;
repeat step || step_inversion NoDup || t_lookup || list_utils2;
eauto using in_combine_l with exfalso;
try solve [ erewrite_anywhere lookup_combine2; eauto; steps ].
Qed.
Lemma is_erased_term_global_tree':
forall keys vs acc0,
is_erased_term acc0 ->
Forall is_erased_term keys ->
Forall is_erased_term vs ->
is_erased_term (fold_left (fun acc p => update acc (fst p) (snd p)) (combine keys vs) acc0).
Proof.
induction keys; repeat step || apply_any; eauto with erased.
Qed.
Lemma wfs_global_tree':
forall keys vs acc0,
wf acc0 0 ->
Forall (fun v => wf v 0) keys ->
Forall (fun v => wf v 0) vs ->
wf (fold_left (fun acc p => update acc (fst p) (snd p)) (combine keys vs) acc0) 0.
Proof.
induction keys; repeat step || apply_any; eauto with wf.
Qed.
Lemma fvs_global_tree':
forall keys vs acc0 tag,
pfv acc0 tag = nil ->
Forall (fun v => pfv v tag = nil) keys ->
Forall (fun v => pfv v tag = nil) vs ->
pfv (fold_left (fun acc p => update acc (fst p) (snd p)) (combine keys vs) acc0) tag = nil.
Proof.
induction keys; repeat step || apply_any || rewrite pfv_update || list_utils.
Qed.
Lemma global_tree_is_tree':
forall keys vs acc0,
[ acc0 : T_tree ]v ->
Forall (fun key => [ key : T_key ]v) keys ->
Forall (fun tree => [ tree : T_tree ]v) vs ->
[ fold_left (fun acc p => update acc (fst p) (snd p)) (combine keys vs) acc0 : T_tree ]v.
Proof.
induction keys; repeat step || apply_any; eauto using update_type.
Qed.
Definition global_tree keys vs :=
fold_left (fun acc p => update acc (fst p) (snd p)) (combine keys vs) empty_tree.
Lemma is_erased_term_global_tree:
forall keys vs,
Forall is_erased_term keys ->
Forall is_erased_term vs ->
is_erased_term (global_tree keys vs).
Proof.
intros; apply is_erased_term_global_tree'; steps;
try solve [ eapply reducible_values_erased; eauto using empty_tree_type; steps ].
Qed.
Lemma wfs_global_tree:
forall keys vs,
Forall (fun v => wf v 0) keys ->
Forall (fun v => wf v 0) vs ->
wf (global_tree keys vs) 0.
Proof.
intros; apply wfs_global_tree'; steps;
try solve [ eapply reducible_val_wf; eauto using empty_tree_type; steps ].
Qed.
Lemma fvs_global_tree:
forall keys vs tag,
Forall (fun v => pfv v tag = nil) keys ->
Forall (fun v => pfv v tag = nil) vs ->
pfv (global_tree keys vs) tag = nil.
Proof.
intros; apply fvs_global_tree'; steps;
try solve [ eapply reducible_val_fv; eauto using empty_tree_type; steps ].
Qed.
Lemma global_tree_is_tree:
forall keys vs,
Forall (fun key => [ key : T_key ]v) keys ->
Forall (fun tr => [ tr : T_tree ]v) vs ->
[ global_tree keys vs : T_tree ]v.
Proof.
intros; apply global_tree_is_tree'; steps; eauto using empty_tree_type.
Qed.
Lemma typed_erased_terms:
forall ρ T l,
valid_interpretation ρ ->
Forall (fun v => [ ρ ⊨ v : T ]v) l ->
Forall is_erased_term l.
Proof.
induction l; repeat step || constructor;
try solve [ eapply reducible_values_erased; eauto using empty_tree_type; steps ].
Qed.
Lemma typed_erased_terms':
forall T l,
Forall (fun v => [ v : T ]v) l ->
Forall is_erased_term l.
Proof.
intros; eapply typed_erased_terms; eauto; steps.
Qed.
Lemma typed_wfs:
forall ρ T l,
valid_interpretation ρ ->
Forall (fun v => [ ρ ⊨ v : T ]v) l ->
Forall (fun v => wf v 0) l.
Proof.
induction l; repeat step || constructor;
try solve [ eapply reducible_val_wf; eauto using empty_tree_type; steps ].
Qed.
Lemma typed_wfs':
forall T l,
Forall (fun v => [ v : T ]v) l ->
Forall (fun v => wf v 0) l.
Proof.
intros; eapply typed_wfs; eauto; steps.
Qed.
Lemma typed_fv:
forall ρ T l tag,
valid_interpretation ρ ->
Forall (fun v => [ ρ ⊨ v : T ]v) l ->
Forall (fun v => pfv v tag = nil) l.
Proof.
induction l; repeat step || constructor;
try solve [ eapply reducible_val_fv; eauto using empty_tree_type; steps ].
Qed.
Lemma typed_fv':
forall T l tag,
Forall (fun v => [ v : T ]v) l ->
Forall (fun v => pfv v tag = nil) l.
Proof.
intros; eapply typed_fv; eauto; steps.
Qed.
Lemma fvs_global_tree2:
forall keys vs tag x,
Forall (fun key => [ key : T_key ]v) keys ->
Forall (fun tr => [ tr : T_tree ]v) vs ->
x ∈ pfv (global_tree keys vs) tag ->
False.
Proof.
intros; rewrite fvs_global_tree in *; steps; eauto using typed_fv'.
Qed.
Notation "'υ'" := (fun (acc : tree) (p : tree * tree) => update acc (fst p) (snd p))
(at level 0).
Lemma fold_left_update_move:
forall keys trees old_tree key0 tree0,
[ old_tree : T_tree ]v ->
[ tree0 : T_tree ]v ->
[ key0 : T_key ]v ->
Forall (fun tr => [ tr : T_tree ]v) trees ->
Forall (fun k => [ k : T_key ]v) keys ->
functional (combine (key0 :: keys) (tree0 :: trees)) ->
incomparable_keys (key0 :: keys) ->
fold_left υ (combine keys trees) (update old_tree key0 tree0) =
update (fold_left υ (combine keys trees) old_tree) key0 tree0.
Proof.
unfold incomparable_keys; induction keys; destruct trees; repeat step.
repeat rewrite IHkeys by (steps; eauto using update_type, functional_tail, functional_tail2).
unshelve epose proof (H5 a key0 _ _); steps; eauto.
- unfold functional in *; steps.
unshelve epose proof (H4 key0 tree0 t _ _); steps.
- apply update_commutative; repeat step || apply global_tree_is_tree'.
Qed.
Lemma global_tree_good_tree':
forall keys trees key0 acc tree0,
length keys = length trees ->
Forall (fun tr => [ tr : T_tree ]v) trees ->
Forall (fun k => [ k : T_key ]v) keys ->
[ acc : T_tree ]v ->
(key0, tree0) ∈ combine keys trees ->
functional (combine keys trees) ->
incomparable_keys keys ->
tree0 = select key0 (fold_left υ (combine keys trees) acc).
Proof.
unfold incomparable_keys; induction keys; destruct trees; repeat step;
try solve [ apply_any; steps; eauto using update_type, functional_tail ].
rewrite fold_left_update_move; steps; eauto using functional_tail.
rewrite select_update; steps; eauto using global_tree_is_tree'.
Qed.
Lemma global_tree_good_tree:
forall keys trees key0 tree0,
length keys = length trees ->
Forall (fun tr => [ tr : T_tree ]v) trees ->
Forall (fun k => [ k : T_key ]v) keys ->
functional (combine keys trees) ->
incomparable_keys keys ->
(key0, tree0) ∈ combine keys trees ->
tree0 = select key0 (global_tree keys trees).
Proof.
intros; apply global_tree_good_tree'; steps; eauto using empty_tree_type.
Qed.
Opaque global_tree.
Lemma in_combine_equivalent:
forall keys trees tr0,
length keys = length trees ->
(forall key tr, (key, tr) ∈ combine keys trees -> tr = select key tr0) ->
List.map (fun key => select key tr0) keys = trees.
Proof.
induction keys; destruct trees; steps; eauto.
rewrite (IHkeys trees); steps.
rewrite (H0 a t); steps.
Qed.
Lemma in_combine_equivalent':
forall keys trees,
length keys = length trees ->
Forall (fun tr => [ tr : T_tree ]v) trees ->
Forall (fun k => [ k : T_key ]v) keys ->
functional (combine keys trees) ->
incomparable_keys keys ->
List.map (fun key => select key (global_tree keys trees)) keys = trees.
Proof.
intros; apply in_combine_equivalent;
repeat step || apply global_tree_good_tree.
Qed.
Opaque T_tree.
Lemma equal_equivalent:
forall t1 t2,
closed_term t1 ->
t1 = t2 ->
[ t1 ≡ t2 ].
Proof. repeat step || equivalent_refl; t_closer. Qed.
Lemma untangle_freshen:
forall Γ T T' template xs ys keys m,
is_erased_type template ->
wf template 0 ->
Forall (fun key => [ key : T_key ]v) keys ->
functional (combine ys keys) ->
functional (combine keys ys) ->
incomparable_keys keys ->
~ m ∈ fv template ->
length keys = length xs ->
length ys = length xs ->
(forall y, y ∈ ys -> y ∈ support Γ -> False) ->
(forall y, y ∈ ys -> y ∈ fv template -> False) ->
(forall x, x ∈ xs -> x ∈ support Γ -> False) ->
(forall x, x ∈ fv template -> x ∈ xs \/ x ∈ support Γ) ->
T = substitute template
(List.combine xs (List.map (fun key => select key (fvar m term_var)) keys)) ->
T' = substitute template
(List.combine xs (List.map (fun y => fvar y term_var) ys)) ->
[ Γ ⊫ T_exists T_tree (close 0 T m) = T_exists_vars ys T_tree T' ].
Proof.
unfold open_equivalent_types, equivalent_types; intros;
repeat step || list_utils || list_utils2 || simp_red_top_level_hyp || rewrite substitute_tree in *.
- rewrite substitute_open2 in *; repeat step || list_utils; eauto with wf.
rewrite open_close in *; repeat step || apply wf_subst || apply wfs_combine7.
rewrite (subst_subst template) in * |-;
repeat step || t_substitutions ||
(rewrite substitute_nothing6 in * by auto) ||
(rewrite list_map_apps in * by repeat step || list_utils2) ||
rewrite List.map_map in *.
rewrite list_map_subst3 in *; steps; eauto.
rewrite psubstitute_texists_vars;
repeat step || rewrite substitute_tree || rewrite <- satisfies_same_support in *;
eauto with fv;
eauto using var_in_support.
apply reducible_exists_vars with (List.map (fun key => select key a) keys);
repeat step || apply wf_subst || apply subst_erased_type || list_utils || list_utils2 ||
Forall_inst || (erewrite reducible_val_fv in * by eauto) ||
apply wfs_combine8 || apply erased_terms_combine2 || rewrite pfv_select in *;
eauto 3 with wf step_tactic;
eauto with erased;
try solve [ eapply satisfies_erased_terms; eauto; steps ];
eauto 2 using forall_select_type.
rewrite (subst_subst2 template) in * |-;
repeat step || list_utils2 || rewrite list_map_subst4 in * ||
(rewrite length_apps by (repeat step || list_utils2)) ||
(rewrite list_map_apps in * by repeat step || list_utils2);
eauto using var_in_support;
eauto with fv.
rewrite (subst_subst2 template);
repeat step || t_substitutions || list_utils2 ||
(rewrite length_apps by (repeat step || list_utils2)) ||
(rewrite substitute_nothing6 in * by auto) ||
(rewrite list_map_apps in * by repeat step || list_utils2) ||
(rewrite list_map_subst5 by (steps; eauto using var_in_support));
eauto using var_in_support;
eauto with fv.
rewrite (subst_subst (psubstitute template l term_var));
repeat step || t_substitutions || list_utils2 ||
(rewrite length_apps by (repeat step || list_utils2)) ||
(rewrite substitute_nothing6 in * by auto) ||
(rewrite list_map_apps in * by repeat step || list_utils2);
eauto using var_in_support;
eauto with fv;
try solve [ t_pfv_in_subst; eauto with fv ].
rewrite list_map_subst7; repeat step || erewrite satisfies_same_support in * by eauto;
eauto with fv.
- rewrite psubstitute_texists_vars in *;
repeat step || rewrite substitute_tree in * || rewrite <- satisfies_same_support in *;
eauto with fv;
eauto using var_in_support.
apply_anywhere reducible_exists_vars2;
repeat step || apply subst_erased_type || apply wf_subst;
eauto using wfs_combine8, erased_terms_combine2 with wf fv erased;
try solve [ eapply satisfies_erased_terms; eauto; steps ].
rewrite (subst_subst2 template) in *;
repeat step || t_substitutions || list_utils2 ||
(rewrite length_apps by (repeat step || list_utils2)) ||
(rewrite substitute_nothing6 in * by auto) ||
(rewrite list_map_apps in * by repeat step || list_utils2) ||
(rewrite list_map_subst5 by (steps; eauto using var_in_support));
eauto using var_in_support;
eauto with fv.
rewrite (subst_subst (psubstitute template l term_var)) in *;
repeat step || t_substitutions || list_utils2 ||
(rewrite length_apps by (repeat step || list_utils2)) ||
(rewrite substitute_nothing6 in * by auto) ||
(rewrite list_map_apps in * by repeat step || list_utils2);
eauto using var_in_support;
eauto with fv;
try solve [ t_pfv_in_subst; eauto with fv ].
rewrite list_map_subst8 in *; repeat step || erewrite satisfies_same_support in * by eauto;
eauto with fv.
simp_red_goal; repeat step || apply subst_erased_type || apply is_erased_type_close;
eauto 3 with erased step_tactic;
eauto 3 using wfs_combine8, erased_terms_combine3 with wf fv erased;
try solve [ eapply satisfies_erased_terms; eauto; steps ];
try solve [ eapply reducible_values_closed; eauto; steps ].
exists (global_tree keys vs); repeat step;
eauto using typed_erased_terms', is_erased_term_global_tree;
eauto using typed_fv', fvs_global_tree;
eauto using typed_wfs', wfs_global_tree;
eauto using global_tree_is_tree.
rewrite substitute_open2 in *; repeat step || list_utils; eauto with wf;
eauto using fvs_global_tree2.
rewrite open_close in *; steps; eauto using wfs_combine7 with wf.
rewrite (subst_subst template);
repeat step || t_substitutions ||
(rewrite substitute_nothing6 in * by auto) ||
(rewrite list_map_apps in * by repeat step || list_utils2) ||
rewrite List.map_map in *.
rewrite list_map_subst3 in *; steps; eauto.
rewrite (subst_subst2 template);
repeat step || list_utils2 || rewrite list_map_subst4 in * ||
(rewrite length_apps by (repeat step || list_utils2)) ||
(rewrite list_map_apps in * by repeat step || list_utils2);
eauto using var_in_support;
eauto with fv;
eauto using global_tree_is_tree.
rewrite in_combine_equivalent'; steps.
apply functional_trans with _ ys; steps.
Qed.
Lemma in_pfv_range:
forall l x tag,
x ∈ pfv_range l tag ->
exists t, t ∈ range l /\ x ∈ pfv t tag.
Proof.
induction l; repeat step || list_utils || instantiate_any; eauto.
Qed.
Lemma untangle_freshen2:
forall Γ T0 T T' template xs ys keys m x,
is_erased_type template ->
is_erased_type T0 ->
wf template 0 ->
wf T0 1 ->
subset (fv T0) (support Γ) ->
~ x ∈ fv_context Γ ->
Forall (fun key => [ key : T_key ]v) keys ->
functional (combine ys keys) ->
functional (combine keys ys) ->
incomparable_keys keys ->
~ m ∈ fv template ->
length keys = length xs ->
length ys = length xs ->
(forall y, y ∈ ys -> y ∈ support Γ -> False) ->
(forall y, y ∈ ys -> y ∈ fv template -> False) ->
(forall x, x ∈ xs -> x ∈ support Γ -> False) ->
(forall x, x ∈ fv template -> x ∈ xs \/ x ∈ support Γ) ->
T = substitute template
(List.combine xs (List.map (fun key => select key (fvar m term_var)) keys)) ->
T' = substitute template
(List.combine xs (List.map (fun y => fvar y term_var) ys)) ->
[ (x, T_tree) :: Γ ⊫
open 0 T0 (fvar x term_var) =
open 0 (close 0 T m) (fvar x term_var) ] ->
[ Γ ⊫ T_exists T_tree T0 = T_exists_vars ys T_tree T' ].
Proof.
intros; eapply open_equivalent_types_trans; eauto using untangle_freshen.
apply open_nexists_2 with x;
repeat step || apply is_erased_type_open || apply wf_close ||
apply subst_erased_type || apply wf_subst ||
apply wfs_combine7 || rewrite tree_fv in * ||
apply is_erased_type_close || apply erased_terms_combine3;
eauto with erased wf;
eauto using open_equivalent_types_refl.
unfold subset; intros; apply_anywhere fv_close; steps.
unshelve epose proof (fv_subst2 _ _ _ _ H19);
repeat step || list_utils || list_utils2 || instantiate_any || apply_anywhere in_pfv_range ||
rewrite pfv_select in * ||
unshelve erewrite reducible_val_fv in * by (eauto; steps).
Qed.
Lemma untangle_abstract:
forall Γ T A,
is_erased_type A ->
is_erased_type T ->
wf T 1 ->
wf A 0 ->
subset (fv A) (support Γ) ->
subset (fv T) (support Γ) ->
[ Γ ⊫ tnil : A ] ->
[ Γ ⊫ T_exists T_tree (shift_open 0 T (tlookup A (lvar 0 term_var))) = T_exists A T ].
Proof.
unfold open_equivalent_types, equivalent_types; intros;
repeat step || list_utils || list_utils2 || simp_red_top_level_hyp || rewrite substitute_tree in *.
- rewrite substitute_open2 in *; repeat step || list_utils; eauto with wf.
rewrite open_shift_open4 in *; repeat step || rewrite open_lookup in * || open_none.
rewrite no_shift_open in H13;
repeat step || apply subst_erased_type;
eauto with wf;
try solve [ eapply satisfies_erased_terms; eauto; steps ].
apply reducible_expr_value;
try solve [ eapply reducible_values_closed; eauto; steps ].
apply reducible_exists with (tlookup (psubstitute A l term_var) a); steps;
repeat step || rewrite lookup_fv || list_utils ||
apply subst_erased_type || t_substitutions ||
(rewrite (substitute_nothing5 a) in * by auto) ||
rewrite substitute_lookup in * || apply lookup_type ||
apply is_erased_term_lookup;
eauto with erased wf fv;
try solve [ eapply satisfies_erased_terms; eauto; steps ];
try solve [ apply reducible_value_expr; steps ].
unfold open_reducible in *; repeat step.
unshelve epose proof (H5 nil l _ _ _); steps;
eauto using reducible_expr_value with values.
- unshelve epose proof (lookup_onto _ _ H11);
repeat step || simp_red_goal || apply subst_erased_type;
try solve [ eapply satisfies_erased_terms; eauto; steps ];
eauto 3 with erased.
exists tree; steps; eauto with erased fv wf.
rewrite substitute_open2;
repeat step || list_utils ||
(unshelve erewrite reducible_val_fv in * by (eauto; steps));
eauto with wf.
rewrite open_shift_open4; repeat step || rewrite open_lookup in * || open_none; eauto with wf.
rewrite no_shift_open;
repeat step || apply subst_erased_type || t_substitutions;
eauto with wf;
try solve [ eapply satisfies_erased_terms; eauto; steps ].
eapply reducibility_open_equivalent; eauto;
repeat step || rewrite substitute_lookup in *;
eauto using equivalent_sym with wf fv.
rewrite (substitute_nothing5 tree); eauto with fv; eauto using equivalent_sym.
Qed.
Lemma untangle_abstract2:
forall Γ T A x T0,
is_erased_type A ->
is_erased_type T ->
is_erased_type T0 ->
wf T0 1 ->
wf T 1 ->
wf A 0 ->
subset (fv A) (support Γ) ->
subset (fv T) (support Γ) ->
subset (fv T0) (support Γ) ->
~ x ∈ fv_context Γ ->
[ Γ ⊫ tnil : A ] ->
[ (x, T_tree) :: Γ ⊫
open 0 T0 (fvar x term_var) =
open 0 (shift_open 0 T (tlookup A (lvar 0 term_var))) (fvar x term_var) ] ->
[ Γ ⊫ T_exists T_tree T0 = T_exists A T ].
Proof.
intros; eapply open_equivalent_types_trans; eauto using untangle_abstract.
apply open_nexists_2 with x;
repeat step || apply is_erased_type_open || apply wf_close || apply wf_lookup ||
apply subst_erased_type || apply wf_subst || apply wf_shift_open ||
apply is_erased_type_shift_open ||
apply is_erased_term_lookup ||
rewrite tree_fv in * ||
apply is_erased_type_close || apply erased_terms_combine3;
eauto with erased wf;
eauto using open_equivalent_types_refl.
eapply subset_transitive; eauto using pfv_shift_open2;
repeat step || sets || rewrite lookup_fv; eauto with sets.
Qed.
Lemma untangle_singleton:
forall Θ Γ T T' t,
[ Θ; Γ ⊨ T = T' ] ->
[ Θ; Γ ⊨ T_singleton T t = T_singleton T' t ].
Proof.
unfold open_equivalent_types, equivalent_types;
repeat step || simp_red || t_instantiate_sat3;
eauto with eapply_any.
Qed.
Opaque List.
Lemma untangle_list_match_1:
forall Γ T1 T2 T1' T2' t x y,
wf T2' 2 ->
is_erased_type T2' ->
subset (fv T2') (support Γ) ->
wf t 0 ->