-
Notifications
You must be signed in to change notification settings - Fork 1
/
ANF_Soundness.v
1592 lines (1493 loc) · 56.5 KB
/
ANF_Soundness.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
(** Type-safety proofs for Fsub.
Authors: Brian Aydemir and Arthur Charguéraud, with help from
Aaron Bohannon, Jeffrey Vaughan, and Dimitrios Vytiniotis.
In parentheses are given the label of the corresponding lemma in
the appendix (informal proofs) of the POPLmark Challenge.
Table of contents:
- #<a href="##subtyping">Properties of subtyping</a>#
- #<a href="##typing">Properties of typing</a>#
- #<a href="##preservation">Preservation</a>#
- #<a href="##progress">Progress</a># *)
Require Export ANF_Lemmas.
Require Import Coq.Logic.Eqdep_dec.
Require Import Coq.Program.Equality.
(* ********************************************************************** *)
(** * #<a name="subtyping"></a># Properties of subtyping *)
(* ********************************************************************** *)
(** ** Reflexivity (1) *)
Lemma sub_reflexivity : forall E T,
wf_env E ->
wf_typ E T ->
sub E T T.
Proof with eauto.
intros E T Ok Wf.
induction Wf; try constructor...
pick fresh Y and apply sub_all...
Qed.
(* ********************************************************************** *)
(** ** Weakening (2) *)
Lemma sub_weakening : forall E F G S T,
sub (G ++ E) S T ->
wf_env (G ++ F ++ E) ->
sub (G ++ F ++ E) S T.
Proof with simpl_env; auto using wf_typ_weakening.
intros E F G S T Sub Ok.
eremember (G ++ E) as H.
generalize dependent G.
induction Sub; intros G Ok EQ; subst...
Case "sub_trans_tvar".
apply (sub_trans_tvar U)...
Case "sub_all".
pick fresh Y and apply sub_all...
rewrite <- concat_assoc.
apply H0...
Case "sub_prod".
apply sub_prod...
Qed.
(* ********************************************************************** *)
(** ** Narrowing and transitivity (3) *)
Definition transitivity_on Q := forall E S T,
sub E S Q -> sub E Q T -> sub E S T.
Lemma sub_narrowing_aux : forall Q F E Z P S T,
transitivity_on Q ->
sub (F ++ [(Z, bind_sub Q)] ++ E) S T ->
sub E P Q ->
sub (F ++ [(Z, bind_sub P)] ++ E) S T.
Proof with simpl_env; eauto using wf_typ_narrowing, wf_env_narrowing.
intros Q F E Z P S T TransQ SsubT PsubQ.
eremember (F ++ [(Z, bind_sub Q)] ++ E) as G. generalize dependent F.
induction SsubT; intros F EQ; subst...
- Case "sub_top".
apply sub_top...
- Case "sub_refl_tvar".
apply sub_refl_tvar...
- Case "sub_trans_tvar".
destruct (X == Z); subst.
+ SCase "X = Z".
apply (sub_trans_tvar P)...
apply TransQ.
* SSCase "P <: Q".
rewrite_env (empty ++ (F ++ [(Z, bind_sub P)]) ++ E).
apply sub_weakening...
* SSCase "Q <: T".
binds_get H.
inversion H1; subst...
+ SCase "X <> Z".
apply (sub_trans_tvar U)...
- Case "sub_all".
pick fresh Y and apply sub_all...
rewrite <- concat_assoc.
apply H0...
- Case "sub_prod".
apply sub_prod...
Qed.
Lemma sub_transitivity : forall Q,
transitivity_on Q.
Proof with simpl_env; auto.
unfold transitivity_on.
intros Q E S T SsubQ QsubT.
assert (W : type Q) by auto.
generalize dependent T.
generalize dependent S.
generalize dependent E.
remember Q as Q' in |-.
generalize dependent Q'.
induction W;
intros Q' EQ E S SsubQ;
induction SsubQ; try discriminate; inversion EQ; subst;
intros T' QsubT;
inversion QsubT; subst. (* try eauto 4 using sub_trans_tvar. *)
1-14: eauto 4 using sub_trans_tvar.
- Case "sub_all / sub_top".
assert (sub E (typ_all S1 S2) (typ_all T1 T2)).
{ pick fresh y and apply sub_all... }
auto.
- Case "sub_all / sub_all".
pick fresh Y and apply sub_all.
+ SCase "bounds".
eauto.
+ SCase "bodies".
lapply (H0 Y); [ intros K | auto ].
apply (K (open_tt T2 Y))...
rewrite_env (empty ++ [(Y, bind_sub T0)] ++ E).
apply (sub_narrowing_aux T1)...
unfold transitivity_on.
auto using (IHW T1).
- Case "sub_prod / sub_top".
apply sub_top...
eapply wf_typ_var, H.
- Case "sub_prod / sub_prod".
apply sub_trans_tvar with (U := U)...
- Case "sum_top / sub_prod".
apply sub_top...
- Case "sub_prod / sub_prod".
apply sub_prod.
apply IHW1 with (Q' := T1)...
apply IHW2 with (Q' := T2)...
Qed.
Lemma sub_narrowing : forall Q E F Z P S T,
sub E P Q ->
sub (F ++ [(Z, bind_sub Q)] ++ E) S T ->
sub (F ++ [(Z, bind_sub P)] ++ E) S T.
Proof.
intros.
eapply sub_narrowing_aux; eauto.
apply sub_transitivity.
Qed.
(* ********************************************************************** *)
(** ** Type substitution preserves subtyping (10) *)
Lemma sub_through_subst_tt : forall Q E F Z S T P,
sub (F ++ [(Z, bind_sub Q)] ++ E) S T ->
sub E P Q ->
sub (map (subst_tb Z P) F ++ E) (subst_tt Z P S) (subst_tt Z P T).
Proof with
simpl_env;
eauto 4 using wf_typ_subst_tb, wf_env_subst_tb, wf_typ_weaken_head.
intros Q E F Z S T P SsubT PsubQ.
eremember (F ++ [(Z, bind_sub Q)] ++ E) as G.
generalize dependent F.
induction SsubT; intros G EQ; subst; simpl subst_tt...
- Case "sub_top".
apply sub_top...
- Case "sub_refl_tvar".
destruct (X == Z); subst.
+ SCase "X = Z".
apply sub_reflexivity...
+ SCase "X <> Z".
apply sub_reflexivity...
inversion H0; subst.
binds_cases H3...
apply (wf_typ_var (subst_tt Z P U))...
- Case "sub_trans_tvar".
destruct (X == Z); subst.
+ SCase "X = Z".
apply (sub_transitivity Q).
* SSCase "left branch".
rewrite_env (empty ++ map (subst_tb Z P) G ++ E).
apply sub_weakening...
* SSCase "right branch".
rewrite (subst_tt_fresh Z P Q).
-- binds_get H.
inversion H1; subst...
-- apply (notin_fv_wf E).
++ auto.
++ destruct (sub_regular (G ++ [(Z, bind_sub Q)] ++ E) U T SsubT) as [wf_G_Z_E _].
apply ok_from_wf_env in wf_G_Z_E as ok_G_Z_E.
apply fresh_mid_tail with (F := G) (a := bind_sub Q), ok_G_Z_E.
+ SCase "X <> Z".
apply (sub_trans_tvar (subst_tt Z P U))...
rewrite (map_subst_tb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ].
binds_cases H...
- Case "sub_all".
pick fresh X and apply sub_all...
rewrite subst_tt_open_tt_var...
rewrite subst_tt_open_tt_var...
rewrite_env (map (subst_tb Z P) ([(X, bind_sub T1)] ++ G) ++ E).
apply H0...
- Case "sub_prod".
apply sub_prod...
Qed.
(* ********************************************************************** *)
(** * #<a name="typing"></a># Properties of typing *)
(* ********************************************************************** *)
(** ** Weakening (5) *)
Lemma typing_weakening : forall E F G e T,
typing (G ++ E) e T ->
wf_env (G ++ F ++ E) ->
typing (G ++ F ++ E) e T.
Proof with simpl_env;
eauto using wf_typ_weakening,
wf_typ_from_wf_env_typ,
wf_typ_from_wf_env_sub,
sub_weakening.
intros E F G e T Typ.
eremember (G ++ E) as H.
generalize dependent G.
induction Typ; intros G EQ Ok; subst...
Case "typing_abs".
pick fresh x and apply typing_abs.
lapply (H x); [intros K | auto].
rewrite <- concat_assoc.
apply (H0 x)...
Case "typing_tabs".
pick fresh X and apply typing_tabs.
lapply (H X); [intros K | auto].
rewrite <- concat_assoc.
apply (H0 X)...
Case "typing_let".
eapply typing_let with (T1 := T1) (L := L `union` dom (G ++ F ++ E)).
apply IHTyp...
intros x x_fresh.
rewrite_env (([(x, bind_typ T1)] ++ G) ++ F ++ E).
apply H0...
Case "typing_pair".
apply typing_pair...
Case "typing_fst".
eapply typing_fst...
Case "typing_snd".
eapply typing_snd...
Qed.
Lemma eval_typing_weakening : forall E F G E' T U,
eval_typing (G ++ E) E' T U ->
wf_env (G ++ F ++ E) ->
eval_typing (G ++ F ++ E) E' T U.
Proof with eauto*.
intros E F G E' T U Typ.
induction Typ; intros wf.
- Case "typing_eval_nil".
apply typing_eval_nil...
apply sub_weakening...
- Case "typing_eval_cons".
apply typing_eval_cons with (L := L `union` dom (G ++ F ++ E)) (U := U)...
intros x x_fresh.
assert (c_typing : typing (([(x, bind_typ T)] ++ G) ++ E) (open_ve c x) U) by (apply (H x); eauto).
eapply typing_weakening with (F := F) in c_typing.
* SSCase "typing".
apply c_typing.
* SSCase "well formedness".
simpl_env.
apply wf_env_typ...
assert (wf_env_xTGE : wf_env (([(x, bind_typ T)] ++ G) ++ E)).
{ eapply typing_regular, c_typing. }
assert (wf_typ_xTGE_T : wf_typ (([(x, bind_typ T)] ++ G) ++ E) T).
{ apply (wf_typ_from_wf_env_typ x) in wf_env_xTGE.
simpl_env.
apply wf_typ_weaken_head... }
simpl_env in *.
apply wf_typ_weakening with (F := F)...
apply (wf_typ_from_wf_env_typ x)...
Qed.
(* ********************************************************************** *)
(** ** Strengthening (6) *)
Lemma sub_strengthening : forall x U E F S T,
sub (F ++ [(x, bind_typ U)] ++ E) S T ->
sub (F ++ E) S T.
Proof with eauto using wf_typ_strengthening, wf_env_strengthening.
intros x U E F S T SsubT.
eremember (F ++ [(x, bind_typ U)] ++ E) as E'.
generalize dependent F.
induction SsubT; intros F EQ; subst...
Case "sub_trans_tvar".
apply (sub_trans_tvar U0)...
binds_cases H...
Case "sub_all".
pick fresh X and apply sub_all...
rewrite <- concat_assoc.
apply H0...
Case "sub_prod".
apply sub_prod...
Qed.
Lemma wf_typ_tvar_comes_from_binds : forall Γ (X : atom),
wf_env Γ ->
wf_typ Γ X ->
exists S, binds X (bind_sub S) Γ /\ wf_typ Γ S.
Proof with eauto using wf_typ_from_binds_sub.
intros Γ X wf_Γ wf_X.
eremember (X : typ) as T.
induction wf_X; inversion HeqT; subst...
Qed.
Lemma notin_open_ve_rec : forall k y z e,
y `notin` (fv_ve e `union` singleton z) ->
y `notin` fv_ve (open_ve_rec k z e).
Proof with eauto*.
intros k y z e y_notin_e_z.
generalize dependent k.
induction e; intros k; simpl in *;
repeat match goal with
| v : var |- _ =>
destruct v; simpl in *; eauto*;
destruct (k === n); eauto*
| |- y `notin` (_ `union` _) => apply notin_union
| IH : y `notin` _ -> forall k, _ |- _ => apply IH; eauto*
end.
Qed.
Lemma open_te_preserves_fv_ve : forall k e X,
fv_ve (open_te_rec k X e) = fv_ve e.
Proof with eauto*.
intros k e X.
generalize dependent k.
induction e; simpl...
Qed.
Lemma typing_strengthening : forall Γ x S Δ e T,
typing (Γ ++ [(x, bind_typ S)] ++ Δ) e T ->
x `notin` fv_ve e ->
typing (Γ ++ Δ) e T.
Proof with eauto using wf_typ_strengthening, wf_env_strengthening.
intros Γ x S Δ e T typ x_notin_fv_e.
eremember (Γ ++ [(x, bind_typ S)] ++ Δ) as Γ'.
assert (e_expr : expr e) by apply (typing_regular _ _ _ typ).
generalize dependent Γ.
generalize dependent x.
induction typ; intros y y_notin_fv_e Γ EQ.
- Case "typing_var".
inversion e_expr; subst...
binds_cases H0...
contradict y_notin_fv_e.
apply AtomSetNotin.in_singleton.
- Case "typing_abs".
inversion e_expr; subst...
pick fresh z and apply typing_abs.
rewrite_env (([(z, bind_typ V)] ++ Γ) ++ Δ).
apply (H0 z ltac:(fsetdec) (H4 z ltac:(fsetdec)) y).
+ apply notin_open_ve_rec.
apply notin_union.
* fsetdec.
* assert (z_notin_y : z `notin` singleton y) by fsetdec.
assert (z_neq_y : z <> y) by apply AtomSetNotin.elim_notin_singleton, z_notin_y.
apply notin_singleton.
contradict z_neq_y.
symmetry.
apply z_neq_y.
+ rewrite concat_assoc.
reflexivity.
- Case "typing_app".
simpl in y_notin_fv_e.
apply typing_app with (T1 := T1).
+ apply IHtyp1 with (x := y)...
+ apply IHtyp2 with (x0 := y)...
- Case "typing_tabs".
inversion e_expr; subst...
pick fresh Z and apply typing_tabs.
rewrite_env (([(Z, bind_sub V)] ++ Γ) ++ Δ).
apply (H0 Z ltac:(fsetdec) (H4 Z ltac:(fsetdec)) y).
+ unfold open_te.
rewrite open_te_preserves_fv_ve.
fsetdec.
+ rewrite concat_assoc.
reflexivity.
- Case "typing_tapp".
inversion e_expr; subst...
simpl in y_notin_fv_e.
apply typing_tapp with (T1 := T1).
+ apply IHtyp with (x0 := y)...
+ apply sub_strengthening in H...
- Case "typing_let".
inversion e_expr; subst...
simpl in y_notin_fv_e.
pick fresh z and apply typing_let.
+ SCase "val".
eapply IHtyp with (x := y)...
+ SCase "cont".
rewrite_env (([(z, bind_typ T1)] ++ Γ) ++ Δ).
apply (H0 z ltac:(fsetdec) (H4 z ltac:(fsetdec)) y).
* apply notin_open_ve_rec.
apply notin_union.
-- fsetdec.
-- assert (z_notin_y : z `notin` singleton y) by fsetdec.
assert (z_neq_y : z <> y) by apply AtomSetNotin.elim_notin_singleton, z_notin_y.
apply notin_singleton.
contradict z_neq_y.
symmetry.
apply z_neq_y.
* rewrite concat_assoc.
reflexivity.
- Case "typing_pair".
simpl in y_notin_fv_e.
apply typing_pair.
+ apply IHtyp1 with (x := y)...
+ apply IHtyp2 with (x := y)...
- Case "typing_fst".
simpl in y_notin_fv_e.
apply typing_fst with (T2 := T2).
apply IHtyp with (x0 := y)...
- Case "typing_snd".
simpl in y_notin_fv_e.
apply typing_snd with (T1 := T1).
apply IHtyp with (x0 := y)...
- Case "typing_sub".
apply typing_sub with (S := S0); subst.
+ apply IHtyp with (x := y)...
+ apply sub_strengthening in H.
apply H.
Qed.
Lemma typing_strengthening_sub_head : forall X S Γ e T,
typing ([(X, bind_sub S)] ++ Γ) e T ->
X `notin` fv_te e ->
typing Γ e T.
Abort.
(************************************************************************ *)
(** ** Narrowing for typing (7) *)
Lemma typing_narrowing : forall Q E F X P e T,
sub E P Q ->
typing (F ++ [(X, bind_sub Q)] ++ E) e T ->
typing (F ++ [(X, bind_sub P)] ++ E) e T.
Proof with eauto 6 using wf_env_narrowing, wf_typ_narrowing, sub_narrowing.
intros Q E F X P e T PsubQ Typ.
eremember (F ++ [(X, bind_sub Q)] ++ E) as E'.
generalize dependent F.
induction Typ; intros F EQ; subst...
Case "typing_var".
binds_cases H0...
Case "typing_abs".
pick fresh y and apply typing_abs.
rewrite <- concat_assoc.
apply H0...
Case "typing_tabs".
pick fresh Y and apply typing_tabs.
rewrite <- concat_assoc.
apply H0...
Case "typing_let".
pick fresh y and apply typing_let...
rewrite <- concat_assoc.
apply H0...
Case "typing_pair".
apply typing_pair...
Case "typing_fst".
eapply typing_fst...
Case "typing_snd".
eapply typing_snd...
Qed.
Lemma sub_specializing : forall Q E F z P S T,
sub E P Q ->
sub (F ++ [(z, bind_typ Q)] ++ E) S T ->
sub (F ++ [(z, bind_typ P)] ++ E) S T.
Proof with eauto using sub_weakening, sub_strengthening.
intros Q E F z P S T PsubQ SsubT.
apply sub_weakening.
apply sub_strengthening in SsubT.
eauto.
destruct (sub_regular _ _ _ SsubT) as [wf_E _].
eapply wf_env_specializing with (V := Q)...
Qed.
Lemma typing_specializing : forall Q F E z P e T,
sub E P Q ->
typing (F ++ [(z, bind_typ Q)] ++ E) e T ->
typing (F ++ [(z, bind_typ P)] ++ E) e T.
Proof with simpl_env; eauto using wf_typ_specializing, wf_env_specializing.
intros Q F E z P e T PsubQ e_T.
eremember (F ++ [(z, bind_typ Q)] ++ E) as G. generalize dependent F.
induction e_T; intros F EQ; subst...
- Case "typing_var".
binds_cases H0.
+ apply typing_var.
* eauto using wf_env_specializing.
* apply binds_weaken_at_head.
apply binds_weaken_at_head.
eauto.
apply ok_from_wf_env, wf_env_strengthening_concat with (F := F)...
apply ok_from_wf_env...
+ inversion H1; subst.
apply typing_sub with (S := P)...
rewrite_env (empty ++ (F ++ [(x, bind_typ P)]) ++ E).
apply sub_weakening...
+ apply typing_var...
- Case "typing_abs".
pick fresh x and apply typing_abs.
rewrite_env (([(x, bind_typ V)] ++ F) ++ [(z, bind_typ P)] ++ E).
apply H0...
- Case "typing_tabs".
pick fresh X and apply typing_tabs.
rewrite_env (([(X, bind_sub V)] ++ F) ++ [(z, bind_typ P)] ++ E).
apply H0...
- Case "typing_tapp".
apply typing_tapp with (T1 := T1).
apply IHe_T...
apply sub_specializing with (Q := Q)...
- Case "typing_let".
pick fresh x and apply typing_let...
rewrite_env (([(x, bind_typ T1)] ++ F) ++ [(z, bind_typ P)] ++ E).
apply H0...
- Case "typing_pair".
apply typing_pair...
- Case "typing_fst".
apply typing_fst with (T2 := T2)...
- Case "typing_snd".
apply typing_snd with (T1 := T1)...
- Case "typing_sub".
apply typing_sub with (S := S)...
apply sub_specializing with (Q := Q)...
Qed.
Lemma eval_specializing : forall Γ E T U T',
sub Γ T' T ->
eval_typing Γ E T U ->
eval_typing Γ E T' U.
Proof with eauto*.
intros *.
intros subT eval_typ.
generalize dependent T'.
induction eval_typ; intros T' subT.
- apply typing_eval_nil...
apply sub_transitivity with (Q := T)...
- eapply typing_eval_cons with (L := L) (U := U)...
intros x x_fresh.
rewrite_env (empty ++ [(x, bind_typ T')] ++ Γ).
eapply typing_specializing...
Qed.
(************************************************************************ *)
(** ** Substitution preserves typing (8) *)
Lemma typing_through_subst_ve : forall U E F x T e u,
typing (F ++ [(x, bind_typ U)] ++ E) e T ->
binds u (bind_typ U) E ->
typing (F ++ E) (subst_ve x u e) T.
(* begin show *)
(** We provide detailed comments for the following proof, mainly to
point out several useful tactics and proof techniques.
Starting a proof with "Proof with <some tactic>" allows us to
specify a default tactic that should be used to solve goals. To
invoke this default tactic at the end of a proof step, we signal
the end of the step with three periods instead of a single one,
e.g., "apply typing_weakening...". *)
Proof with simpl_env;
eauto 4 using wf_typ_strengthening,
wf_env_strengthening,
sub_strengthening.
(** The proof proceeds by induction on the given typing derivation
for e. We use the remember tactic, along with generalize
dependent, to ensure that the goal is properly strengthened
before we use induction. *)
intros U E F x T e u TypT TypU.
eremember (F ++ [(x, bind_typ U)] ++ E) as E'.
generalize dependent F.
induction TypT; intros F EQ; subst; simpl subst_ve...
(** The typing_var case involves a case analysis on whether the
variable is the same as the one being substituted for. *)
Case "typing_var".
destruct (x0 == x); subst.
(** In the case where x0=x, we first observe that hypothesis H0
implies that T=U, since x can only be bound once in the
environment. The conclusion then follows from hypothesis TypU
and weakening. We can use the binds_get tactic, described in
the Environment library, with H0 to obtain the fact that
T=U. *)
SCase "x0 = x".
binds_get H0.
inversion H2; subst.
(** In order to apply typing_weakening, we need to rewrite the
environment so that it has the right shape. (We could
also prove a corollary of typing_weakening.) The
rewrite_env tactic, described in the Environment library,
is one way to perform this rewriting. *)
rewrite_env (empty ++ F ++ E).
apply typing_weakening...
apply typing_var...
apply wf_env_strengthening in H.
apply wf_env_strengthening_concat in H.
apply H.
(** In the case where x0<>x, the result follows by an exhaustive
case analysis on exactly where x0 is bound in the environment.
We perform this case analysis by using the binds_cases tactic,
described in the Environment library. *)
SCase "x0 <> x".
binds_cases H0.
eauto using wf_env_strengthening.
eauto using wf_env_strengthening.
(** Informally, the typing_abs case is a straightforward application
of the induction hypothesis, which is called H0 here. *)
Case "typing_abs".
(** We use the "pick fresh and apply" tactic to apply the rule
typing_abs without having to calculate the appropriate finite
set of atoms. *)
pick fresh y and apply typing_abs.
unfold open_ve.
(** We cannot apply H0 directly here. The first problem is that
the induction hypothesis has (subst_ee open_ee), whereas in
the goal we have (open_ee subst_ee). The lemma
subst_ee_open_ee_var lets us swap the order of these two
operations. *)
rewrite subst_ve_open_ve_var...
(** The second problem is how the concatenations are associated in
the environments. In the goal, we currently have
<< ([(y, bind_typ V)] ++ F ++ E),
>>
where concatenation associates to the right. In order to
apply the induction hypothesis, we need
<< (([(y, bind_typ V)] ++ F) ++ E).
>>
We can use the rewrite_env tactic to perform this rewriting,
or we can rewrite directly with an appropriate lemma from the
Environment library. *)
rewrite <- concat_assoc.
(** Now we can apply the induction hypothesis. *)
apply H0...
(** The remaining cases in this proof are straightforward, given
everything that we have pointed out above. *)
Case "typing_app".
rewrite (if_hoist (f == x) u f var_f).
rewrite (if_hoist (x0 == x) u x0 var_f).
apply typing_app with (T1 := T1).
SCase "callee".
rewrite <- (if_hoist (f == x) u f var_f).
apply IHTypT1...
SCase "argument".
rewrite <- (if_hoist (x0 == x) u x0 var_f).
apply IHTypT2...
Case "typing_tabs".
pick fresh Y and apply typing_tabs.
rewrite subst_ve_open_te_var...
rewrite <- concat_assoc.
apply H0...
Case "typing_tapp".
rewrite (if_hoist (x0 == x) u x0 var_f).
apply typing_tapp with (T1 := T1).
SCase "callee".
rewrite <- (if_hoist (x0 == x) u x0 var_f).
apply IHTypT...
SCase "type argument".
eauto using sub_strengthening.
Case "typing_let".
pick fresh y and apply typing_let...
unfold open_ve.
rewrite subst_ve_open_ve_var...
rewrite <- concat_assoc.
apply H0...
Case "typing_pair".
rewrite (if_hoist (x1 == x) u x1 var_f).
rewrite (if_hoist (x2 == x) u x2 var_f).
apply typing_pair.
SCase "first element".
rewrite <- (if_hoist (x1 == x) u x1 var_f).
apply IHTypT1...
SCase "second element".
rewrite <- (if_hoist (x2 == x) u x2 var_f).
apply IHTypT2...
Case "typing_fst".
rewrite (if_hoist (x0 == x) u x0 var_f).
apply typing_fst with (T2 := T2).
rewrite <- (if_hoist (x0 == x) u x0 var_f).
apply IHTypT...
Case "typing_snd".
rewrite (if_hoist (x0 == x) u x0 var_f).
apply typing_snd with (T1 := T1).
rewrite <- (if_hoist (x0 == x) u x0 var_f).
apply IHTypT...
Qed.
(* end show *)
(************************************************************************ *)
(** ** Type substitution preserves typing (11) *)
Lemma typing_through_subst_te : forall Q E F Z e T P,
typing (F ++ [(Z, bind_sub Q)] ++ E) e T ->
sub E P Q ->
typing (map (subst_tb Z P) F ++ E) (subst_te Z P e) (subst_tt Z P T).
Proof with simpl_env;
eauto 6 using wf_env_subst_tb,
wf_typ_subst_tb,
sub_through_subst_tt.
intros Q E F Z e T P Typ PsubQ.
eremember (F ++ [(Z, bind_sub Q)] ++ E) as G.
generalize dependent F.
induction Typ; intros F EQ; subst;
simpl subst_te in *; simpl subst_tt in *...
Case "typing_var".
apply typing_var...
rewrite (map_subst_tb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ].
binds_cases H0...
Case "typing_abs".
pick fresh y and apply typing_abs.
rewrite subst_te_open_ve_var...
rewrite_env (map (subst_tb Z P) ([(y, bind_typ V)] ++ F) ++ E).
apply H0...
Case "typing_tabs".
pick fresh Y and apply typing_tabs.
rewrite subst_te_open_te_var...
rewrite subst_tt_open_tt_var...
rewrite_env (map (subst_tb Z P) ([(Y, bind_sub V)] ++ F) ++ E).
apply H0...
Case "typing_tapp".
rewrite subst_tt_open_tt...
Case "typing_let".
pick fresh y and apply typing_let.
instantiate (1 := subst_tt Z P T1).
apply IHTyp...
rewrite subst_te_open_ve_var.
rewrite_env (map (subst_tb Z P) ([(y, bind_typ T1)] ++ F) ++ E).
apply H0...
Case "typing_pair".
apply typing_pair.
apply IHTyp1...
apply IHTyp2...
Case "typing_fst".
eapply typing_fst, IHTyp...
Case "typing_snd".
eapply typing_snd, IHTyp...
Qed.
(* ********************************************************************** *)
(** * #<a name="preservation"></a># Preservation *)
(* ********************************************************************** *)
(** ** Inversion of typing (13) *)
Lemma typing_inv_abs : forall E S1 e1 T,
typing E (exp_abs S1 e1) T ->
forall U1 U2, sub E T (typ_arrow U1 U2) ->
sub E U1 S1
/\ exists S2, exists L, forall x, x `notin` L ->
typing ([(x, bind_typ S1)] ++ E) (open_ve e1 x) S2 /\ sub E S2 U2.
Proof with auto.
intros E S1 e1 T Typ.
eremember (exp_abs S1 e1) as e.
generalize dependent e1.
generalize dependent S1.
induction Typ; intros S1 b1 EQ U1 U2 Sub; inversion EQ; subst.
Case "typing_abs".
inversion Sub; subst.
split...
exists T1. exists L...
Case "typing_sub".
auto using (sub_transitivity T).
Qed.
Lemma typing_inv_tabs : forall E S1 e1 T,
typing E (exp_tabs S1 e1) T ->
forall U1 U2, sub E T (typ_all U1 U2) ->
sub E U1 S1
/\ exists S2, exists L, forall X, X `notin` L ->
typing ([(X, bind_sub U1)] ++ E) (open_te e1 X) (open_tt S2 X)
/\ sub ([(X, bind_sub U1)] ++ E) (open_tt S2 X) (open_tt U2 X).
Proof with simpl_env; auto.
intros E S1 e1 T Typ.
eremember (exp_tabs S1 e1) as e.
generalize dependent e1.
generalize dependent S1.
induction Typ; intros S1 e0 EQ U1 U2 Sub; inversion EQ; subst.
Case "typing_tabs".
inversion Sub; subst.
split...
exists T1.
exists (L0 `union` L).
intros Y Fr.
split...
rewrite_env (empty ++ [(Y, bind_sub U1)] ++ E).
apply (typing_narrowing S1)...
Case "typing_sub".
auto using (sub_transitivity T).
Qed.
(* ********************************************************************** *)
(** ** Preservation (20) *)
Lemma typing_abs_typ_arrow_implies_sub_param : forall Γ U e T1 T2,
typing Γ (exp_abs U e) (typ_arrow T1 T2) ->
sub Γ T1 U.
Proof with eauto*.
intros *.
intros typ.
destruct (typing_regular _ _ _ typ) as [wf_Γ [_ wf_T1_arr_T2]].
inversion wf_T1_arr_T2; subst.
eremember (exp_abs U e) as abs.
eremember (typ_arrow T1 T2) as S.
rename wf_T1_arr_T2 into wf_S.
assert (S_sub_T1_arr_T2 : sub Γ S (typ_arrow T1 T2)) by (subst; apply sub_reflexivity; eauto).
clear HeqS.
induction typ; inversion Heqabs; subst.
- inversion S_sub_T1_arr_T2...
- eapply IHtyp...
apply sub_transitivity with (Q := T)...
Qed.
Lemma typing_tabs_typ_all_implies_sub_param : forall Γ U e T1 T2,
typing Γ (exp_tabs U e) (typ_all T1 T2) ->
sub Γ T1 U.
Proof with eauto*.
intros *.
intros typ.
destruct (typing_regular _ _ _ typ) as [wf_Γ [_ wf_all_T1_T2]].
inversion wf_all_T1_T2; subst.
eremember (exp_tabs U e) as tabs.
eremember (typ_all T1 T2) as S.
rename wf_all_T1_T2 into wf_S.
assert (S_sub_all_T1_T2 : sub Γ S (typ_all T1 T2)) by (subst; apply sub_reflexivity; eauto).
clear HeqS.
induction typ; inversion Heqtabs; subst.
- inversion S_sub_all_T1_T2...
- eapply IHtyp...
apply sub_transitivity with (Q := T)...
Qed.
Lemma typing_pair_typ_prod_implies_sub_components : forall Γ x1 x2 T1 T2,
typing Γ (exp_pair x1 x2) (typ_prod T1 T2) ->
typing Γ x1 T1 /\ typing Γ x2 T2.
Proof with eauto*.
intros *.
intros typ.
destruct (typing_regular _ _ _ typ) as [wf_Γ [_ wf_prod_T1_T2]].
inversion wf_prod_T1_T2; subst.
eremember (exp_pair x1 x2) as pair.
eremember (typ_prod T1 T2) as S.
rename wf_prod_T1_T2 into wf_S.
assert (S_sub_prod_T1_T2 : sub Γ S (typ_prod T1 T2)) by (subst; apply sub_reflexivity; eauto).
clear HeqS.
induction typ; inversion Heqpair; subst.
- inversion S_sub_prod_T1_T2; subst...
- eapply IHtyp...
apply sub_transitivity with (Q := T)...
Qed.
Ltac impossible_typing typ :=
clear - typ;
match type of typ with
| typing ?Γ ?e ?T =>
let S := fresh "S" in
eremember T as S eqn:HeqS;
assert (S_sub_T : sub Γ S T) by (subst; apply sub_reflexivity; eauto);
clear HeqS;
dependent induction typ;
[ inversion S_sub_T
| (* cannot name IH in the dependent induction tactic, so we need to match *)
match goal with
| H : sub ?Γ S ?T, IH : forall _ _, e = _ -> _ |- _ =>
eapply IH; [ eauto | eapply sub_transitivity with (Q := T); eauto ]; trivial
end ]
end.
Goal forall Γ U e T1 T2,
~ typing Γ (exp_tabs U e) (typ_arrow T1 T2).
Proof with eauto*.
intros Γ U e T1 T2 typ.
impossible_typing typ.
Qed.
Goal forall Γ x y T1 T2,
~ typing Γ (exp_pair x y) (typ_all T1 T2).
Proof with eauto*.
intros Γ x y T1 T2 typ.
impossible_typing typ.
Qed.
Lemma binds_sub_arrow_implies_store_abs : forall S Γ TFun T1 T2 f,
store_typing S Γ ->
binds f (bind_typ TFun) Γ ->
sub Γ TFun (typ_arrow T1 T2) ->
exists U e abs_value, stores S f (exp_abs U e) abs_value /\ sub Γ T1 U.
Proof with eauto*.
intros *.
intros store_typ Γ_binds_f TFun_sub_T1_arr_T2.
eremember (typ_arrow T1 T2) as T1_arr_T2.
induction store_typ; inversion Γ_binds_f; inversion HeqT1_arr_T2; subst.
destruct (f == x).
- inversion H2; subst...
unfold stores.
unfold binds.
simpl.
destruct (x == x); [ clear e | contradict n; reflexivity ].
inversion v_value; subst.
+ inversion H; subst.
* exists T, e1, v_value.
inversion TFun_sub_T1_arr_T2; subst.
split...
* exists T, e1, v_value.
split...
rewrite_env (empty ++ [(x, bind_typ TFun)] ++ Γ).
apply sub_weakening.
-- assert (abs_has_type_T1_arr_T2 : typing Γ (exp_abs T e1) (typ_arrow T1 T2)).
{ apply typing_sub with (S := TFun)...
rewrite_env (empty ++ [(x, bind_typ TFun)] ++ Γ) in TFun_sub_T1_arr_T2.
apply sub_strengthening in TFun_sub_T1_arr_T2... }
apply (typing_abs_typ_arrow_implies_sub_param _ _ _ _ _ abs_has_type_T1_arr_T2).
-- apply wf_env_typ...
+ assert (tabs_has_type_T1_arr_T2 : typing Γ (exp_tabs T e1) (typ_arrow T1 T2)).
{ apply typing_sub with (S := TFun)...
rewrite_env (empty ++ [(x, bind_typ TFun)] ++ Γ) in TFun_sub_T1_arr_T2.
apply sub_strengthening in TFun_sub_T1_arr_T2... }
exfalso; impossible_typing tabs_has_type_T1_arr_T2.
+ assert (pair_has_type_T1_arr_T2 : typing Γ (exp_pair x0 y) (typ_arrow T1 T2)).
{ apply typing_sub with (S := TFun)...
rewrite_env (empty ++ [(x, bind_typ TFun)] ++ Γ) in TFun_sub_T1_arr_T2.
apply sub_strengthening in TFun_sub_T1_arr_T2... }
exfalso; impossible_typing pair_has_type_T1_arr_T2.
- assert (TFun_sub_T1_arr_T2' : sub Γ TFun (typ_arrow T1 T2)).
{ rewrite_env (empty ++ [(x, bind_typ T)] ++ Γ) in TFun_sub_T1_arr_T2.
apply sub_strengthening in TFun_sub_T1_arr_T2... }
destruct IHstore_typ as [U [e [abs_value [xv_S_stores_f T1_sub_U]]]]...
exists U, e, abs_value.
split.
+ rewrite_env ([let' x v v_value] ++ S).
apply binds_tail.
* trivial.
* simpl; fsetdec.
+ rewrite_env (empty ++ [(x, bind_typ T)] ++ Γ).
apply sub_weakening...
Qed.
Lemma binds_sub_all_implies_store_tabs : forall S Γ TAll T1 T2 f,
store_typing S Γ ->
binds f (bind_typ TAll) Γ ->
sub Γ TAll (typ_all T1 T2) ->
exists U e tabs_value, stores S f (exp_tabs U e) tabs_value /\ sub Γ T1 U.
Proof with eauto*.
intros *.
intros store_typ Γ_binds_f TAll_sub_all_T1_T2.
induction store_typ; inversion Γ_binds_f; subst.
- destruct (f == x).
+ inversion H2; subst...
unfold stores.
unfold binds.
simpl.
destruct (x == x); [ clear e | contradict n; reflexivity ].
inversion v_value; subst.
* assert (abs_has_type_all_T1_T2 : typing Γ (exp_abs T e1) (typ_all T1 T2)).
{ apply typing_sub with (S := TAll)...
rewrite_env (empty ++ [(x, bind_typ TAll)] ++ Γ) in TAll_sub_all_T1_T2.
apply sub_strengthening in TAll_sub_all_T1_T2... }
exfalso; impossible_typing abs_has_type_all_T1_T2.
* inversion H; subst.
-- exists T, e1, v_value.
inversion TAll_sub_all_T1_T2; subst.
split...