-
Notifications
You must be signed in to change notification settings - Fork 2
/
ML_SP_Infrastructure.v
1151 lines (967 loc) · 31.7 KB
/
ML_SP_Infrastructure.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
(***************************************************************************
* Preservation and Progress for mini-ML (CBV) - Infrastructure *
* Arthur Chargueraud, March 2007, Coq v8.1 *
* Extension to structural polymorphism *
* Jacques Garrigue, October 2007 - May 2008 *
***************************************************************************)
Set Implicit Arguments.
Require Import List Omega Metatheory ML_SP_Definitions.
Require Import ProofIrrelevance.
(* ====================================================================== *)
(** * The infrastructure needs to be parameterized over definitions *)
Module MkInfra(Cstr:CstrIntf)(Const:CstIntf).
Module Defs := MkDefs(Cstr)(Const).
Import Defs.
(* These tactics needs definitions *)
Ltac length_hyps :=
instantiate_fail;
repeat match goal with
| H: fresh _ _ _ |- _ => puts (fresh_length _ _ _ H); clear H
| H: types _ _ |- _ => puts (proj1 H); clear H
| H: list_for_n _ _ _ |- _ => puts (proj1 H); clear H
| H: list_forall2 _ _ _ |- _ => puts (list_forall2_length H); clear H
| H: split _ = (_,_) |- _ => puts (split_length _ H); clear H
end;
repeat progress
(simpl in *; unfold typ_fvars, kinds_open_vars, kinds_open in *;
try rewrite map_length in *; try rewrite app_length in *).
Hint Extern 1 (_ = length _) => length_hyps; omega : core.
Hint Extern 1 (length _ = _) => length_hyps; omega : core.
Lemma dom_kinds_open_vars : forall Xs Ks,
length Ks = length Xs ->
dom (kinds_open_vars Ks Xs) = mkset Xs.
Proof.
intros. unfold kinds_open_vars; rewrite* dom_combine.
Qed.
Ltac disjoint_simpls :=
repeat match goal with
| H: fresh _ _ _ |- _ =>
let Hf := fresh "Hf" in poses Hf (fresh_disjoint _ _ H);
let Hn := fresh "Hn" in poses Hn (fresh_length _ _ _ H); clear H
| H: ok (_ & _) |- _ =>
let Ho := fresh "Ho" in poses Ho (ok_disjoint _ _ H); clear H
| H: kenv_ok (_ & _) |- _ =>
let Hk := fresh "Hk" in poses Hk (ok_disjoint _ _ (proj1 H)); clear H
| H: binds _ _ _ |- _ =>
let Hb := fresh "Hb" in poses Hb (binds_dom H); clear H
| H: get _ _ = None |- _ =>
let Hn := fresh "Hn" in poses Hn (get_none_notin _ H); clear H
| H: In _ _ |- _ =>
let Hi := fresh "Hi" in poses Hi (in_mkset H); clear H
| H: ~In _ _ |- _ =>
let Hn := fresh "Hn" in poses Hn (notin_mkset _ H); clear H
| x := ?y : env _ |- _ => subst x
end.
Ltac disjoint_solve :=
instantiate_fail;
disjoint_simpls;
fold kind in *; unfold env_fv in *;
repeat progress
(simpl dom in *; simpl fv_in in *; simpl typ_fv in *;
try rewrite dom_concat in *; try rewrite fv_in_concat in *;
try rewrite dom_map in *;
try (rewrite dom_combine in * by (length_hyps; omega));
try (rewrite dom_kinds_open_vars in * by (length_hyps; omega)));
sets_solve.
Hint Extern 1 (_ \in _) => solve [disjoint_solve] : core.
Hint Extern 1 (_ << _) => solve [disjoint_solve] : core.
Hint Extern 1 (_ \notin _) => solve [disjoint_solve] : core.
Hint Extern 1 (disjoint _ _) => solve [disjoint_solve] : core.
Lemma disjoint_fresh : forall n L1 Xs L2,
fresh L1 n Xs ->
disjoint L2 (mkset Xs) ->
fresh L2 n Xs.
Proof.
induction n; destruct Xs; simpl; intros; auto; try discriminate.
split2*.
Qed.
Ltac env_ok_hyps :=
repeat match goal with
| H: env_ok _ |- _ => destruct H
end.
Ltac kenv_ok_hyps :=
repeat match goal with
| H: kenv_ok _ |- _ => destruct H
end.
Ltac env_ok_solve :=
env_ok_hyps; split; [ok_solve | env_prop_solve].
Ltac kenv_ok_solve :=
kenv_ok_hyps; split; [ok_solve | env_prop_solve].
Hint Extern 2 (env_ok _) => solve [env_ok_solve] : core.
Hint Extern 2 (kenv_ok _) => solve [kenv_ok_solve] : core.
(* ====================================================================== *)
(** * Additional Definitions used in the Proofs *)
(* ********************************************************************** *)
(** ** Free Variables *)
(** Computing free variables of a term. *)
Fixpoint trm_fv (t : trm) {struct t} : vars :=
match t with
| trm_bvar i => {}
| trm_fvar x => {{x}}
| trm_abs t1 => (trm_fv t1)
| trm_let t1 t2 => (trm_fv t1) \u (trm_fv t2)
| trm_app t1 t2 => (trm_fv t1) \u (trm_fv t2)
| trm_cst c => {}
end.
(* ********************************************************************** *)
(** ** Substitution for free names *)
Definition subs := Env.env typ.
(** Substitution for names for types *)
Fixpoint typ_subst (S : subs) (T : typ) {struct T} : typ :=
match T with
| typ_bvar i => typ_bvar i
| typ_fvar X =>
match get X S with
| None => T
| Some T' => T'
end
| typ_arrow T1 T2 => typ_arrow (typ_subst S T1) (typ_subst S T2)
end.
(** Substitution for names for schemes. *)
Definition kind_subst S := kind_map (typ_subst S).
Definition sch_subst S M :=
Sch (typ_subst S (sch_type M)) (List.map (kind_subst S) (sch_kinds M)).
(** Substitution for name in a term. *)
Fixpoint trm_subst (z : var) (u : trm) (t : trm) {struct t} : trm :=
match t with
| trm_bvar i => trm_bvar i
| trm_fvar x => if x == z then u else (trm_fvar x)
| trm_abs t1 => trm_abs (trm_subst z u t1)
| trm_let t1 t2 => trm_let (trm_subst z u t1) (trm_subst z u t2)
| trm_app t1 t2 => trm_app (trm_subst z u t1) (trm_subst z u t2)
| trm_cst c => trm_cst c
end.
Notation "[ z ~> u ] t" := (trm_subst z u t) (at level 68).
(* ====================================================================== *)
(** * Tactics *)
(* ********************************************************************** *)
(** ** Instanciation of Tactics *)
Ltac gather_vars :=
let A := gather_vars_with (fun x : vars => x) in
let B := gather_vars_with (fun x : var => {{ x }}) in
let C := gather_vars_with (fun x : env => dom x) in
let D := gather_vars_with (fun x : trm => trm_fv x) in
let E := gather_vars_with (fun x : typ => typ_fv x) in
let F := gather_vars_with (fun x : list typ => typ_fv_list x) in
let G := gather_vars_with (fun x : env => env_fv x) in
let H := gather_vars_with (fun x : sch => sch_fv x) in
let I := gather_vars_with (fun x : kenv => dom x) in
let J := gather_vars_with (fun x : kenv => fv_in kind_fv x) in
let K := gather_vars_with (fun x : list kind => kind_fv_list x) in
constr:(A \u B \u C \u D \u E \u F \u G \u H \u I \u J \u K).
Tactic Notation "pick_fresh" ident(x) :=
let L := gather_vars in (pick_fresh_gen L x).
Tactic Notation "pick_freshes" constr(n) ident(x) :=
let L := gather_vars in (pick_freshes_gen L n x).
Tactic Notation "apply_fresh" constr(T) "as" ident(x) :=
apply_fresh_base T gather_vars x.
Tactic Notation "apply_fresh" "*" constr(T) "as" ident(x) :=
apply_fresh T as x; auto*.
(* ********************************************************************** *)
(** ** Automation *)
Hint Constructors type term well_kinded : core.
Lemma typ_def_fresh : typ_fv typ_def = {}.
Proof.
auto.
Qed.
Hint Extern 1 (_ \notin typ_fv typ_def) =>
rewrite typ_def_fresh : core.
Hint Extern 1 (types _ _) => split; auto : core.
(* ====================================================================== *)
(** ** Properties of fv *)
Lemma fv_list_map : forall ts1 ts2,
typ_fv_list (ts1 ++ ts2) = typ_fv_list ts1 \u typ_fv_list ts2.
Proof.
induction ts1; simpl; intros.
rewrite* union_empty_l.
rewrite IHts1. rewrite* union_assoc.
Qed.
(* ====================================================================== *)
(** * Properties of terms *)
(* begin hide *)
(** Substitution on indices is identity on well-formed terms. *)
Lemma trm_open_rec_core :forall t j v i u, i <> j ->
trm_open_rec j v t = trm_open_rec i u (trm_open_rec j v t) ->
t = trm_open_rec i u t.
Proof.
induction t; introv Neq Equ;
simpl in *; inversion* Equ; f_equal*.
case_nat*. case_nat*.
Qed.
Lemma trm_open_rec : forall t u,
term t -> forall k, t = trm_open_rec k u t.
Proof.
induction 1; intros; simpl; f_equal*.
unfolds trm_open. pick_fresh x.
apply* (@trm_open_rec_core t1 0 (trm_fvar x)).
unfolds trm_open. pick_fresh x.
apply* (@trm_open_rec_core t2 0 (trm_fvar x)).
Qed.
(* end hide *)
(** Substitution for a fresh name is identity. *)
Lemma trm_subst_fresh : forall x t u,
x \notin trm_fv t -> [x ~> u] t = t.
Proof.
intros. induction t; simpls; f_equal*.
case_var*. notin_contradiction.
Qed.
(** Substitution distributes on the open operation. *)
Lemma trm_subst_open : forall x u t1 t2, term u ->
[x ~> u] (t1 ^^ t2) = ([x ~> u]t1) ^^ ([x ~> u]t2).
Proof.
intros. unfold trm_open. generalize 0.
induction t1; intros; simpl; f_equal*.
case_nat*. case_var*. apply* trm_open_rec.
Qed.
(** Substitution and open_var for distinct names commute. *)
Lemma trm_subst_open_var : forall x y u e, y <> x -> term u ->
([x ~> u]e) ^ y = [x ~> u] (e ^ y).
Proof.
introv Neq Wu. rewrite* trm_subst_open.
simpl. case_var*.
Qed.
(** Opening up an abstraction of body t with a term u is the same as opening
up the abstraction with a fresh name x and then substituting u for x. *)
Lemma trm_subst_intro : forall x t u,
x \notin (trm_fv t) -> term u ->
t ^^ u = [x ~> u](t ^ x).
Proof.
introv Fr Wu. rewrite* trm_subst_open.
rewrite* trm_subst_fresh. simpl. case_var*.
Qed.
(** Terms are stable by substitution *)
Lemma trm_subst_term : forall t z u,
term u -> term t -> term ([z ~> u]t).
Proof.
induction 2; simpl*.
case_var*.
apply_fresh term_abs as y. rewrite* trm_subst_open_var.
apply_fresh* term_let as y. rewrite* trm_subst_open_var.
Qed.
Hint Resolve trm_subst_term : core.
(** Conversion from locally closed abstractions and bodies *)
Lemma term_abs_to_body : forall t1,
term (trm_abs t1) -> term_body t1.
Proof.
intros. unfold term_body. inversion* H.
Qed.
Lemma body_to_term_abs : forall t1,
term_body t1 -> term (trm_abs t1).
Proof.
intros. inversion* H.
Qed.
Lemma term_let_to_body : forall t1 t2,
term (trm_let t1 t2) -> term_body t2.
Proof.
intros. unfold term_body. inversion* H.
Qed.
Lemma body_to_term_let : forall t1 t2,
term_body t2 -> term t1 -> term (trm_let t1 t2).
Proof.
intros. inversion* H.
Qed.
Hint Resolve body_to_term_abs body_to_term_let : core.
Hint Extern 1 (term_body ?t) =>
match goal with
| H: context [trm_abs t] |- _ =>
apply term_abs_to_body
| H: context [trm_let ?t1 t] |- _ =>
apply (@term_let_to_body t1)
end : core.
(** ** Opening a body with a term gives a term *)
Lemma trm_open_term : forall t u,
term_body t -> term u -> term (t ^^ u).
Proof.
intros. destruct H. pick_fresh y. rewrite* (@trm_subst_intro y).
Qed.
Hint Resolve trm_open_term : core.
(* ====================================================================== *)
(** * Properties of types *)
(** Open on a type is the identity. *)
Lemma typ_open_type : forall T Us,
type T -> T = typ_open T Us.
Proof.
introv W. induction T; simpls; inversions W; f_equal*.
Qed.
(** Substitution for a fresh name is identity. *)
Lemma typ_subst_fresh : forall S T,
disjoint (dom S) (typ_fv T) ->
typ_subst S T = T.
Proof.
intros. induction T; simpls; f_equal*.
rewrite* get_notin_dom.
Qed.
Lemma ckind_pi : forall k k',
kind_cstr k = kind_cstr k' ->
kind_rel k = kind_rel k' ->
k = k'.
Proof.
intros [kc kv kr kh] [kc' kv' kr' kh']; simpl; intros.
subst.
rewrite (proof_irrelevance _ kv kv').
rewrite (proof_irrelevance _ kh kh').
auto.
Qed.
Lemma kind_pi : forall k k',
kind_cstr k = kind_cstr k' ->
kind_rel k = kind_rel k' ->
Some k = Some k'.
Proof.
intros. rewrite* (ckind_pi k k').
Qed.
Lemma kind_subst_fresh : forall S k,
disjoint (dom S) (kind_fv k) ->
kind_subst S k = k.
Proof.
unfold kind_subst, kind_fv, kind_types.
intros; destruct k as [[kc kv kr kh]|]; simpl*.
apply* kind_pi; simpl in *.
clear -H; induction* kr; intros.
destruct a; simpl.
rewrite* IHkr.
rewrite* typ_subst_fresh. simpl in H. auto.
simpl in *. auto.
Qed.
Lemma typ_subst_fresh_list : forall S ts,
disjoint (dom S) (typ_fv_list ts) ->
ts = List.map (typ_subst S) ts.
Proof.
induction ts; simpl; intros Fr.
auto. f_equal*. rewrite~ typ_subst_fresh.
Qed.
Lemma typ_subst_fresh_trm_fvars : forall S xs,
fresh (dom S) (length xs) xs ->
typ_fvars xs = List.map (typ_subst S) (typ_fvars xs).
Proof.
intros. apply typ_subst_fresh_list.
induction xs; intro v; simpls. auto.
destruct H.
destruct (fresh_union_r _ _ _ _ H0).
use (IHxs H1).
Qed.
(** Substitution distributes on the open operation. *)
Lemma typ_subst_open : forall S T1 T2, env_prop type S ->
typ_subst S (typ_open T1 T2) =
typ_open (typ_subst S T1) (List.map (typ_subst S) T2).
Proof.
intros. induction T1; intros; simpl; f_equal*.
apply list_map_nth. apply* typ_subst_fresh.
case_eq (get v S); intros. apply* typ_open_type.
auto.
Qed.
(** Substitution and open_var for distinct names commute. *)
Lemma typ_subst_open_vars : forall S Ys T,
fresh (dom S) (length Ys) Ys ->
env_prop type S ->
typ_open_vars (typ_subst S T) Ys
= typ_subst S (typ_open_vars T Ys).
Proof.
introv Fr Tu. unfold typ_open_vars.
rewrite* typ_subst_open. f_equal.
induction Ys; simpls. auto.
destruct Fr.
rewrite* get_notin_dom.
rewrite* <- IHYs.
Qed.
Lemma kind_subst_open_vars : forall S k Xs,
fresh (dom S) (length Xs) Xs ->
env_prop type S ->
kind_subst S (kind_open k (typ_fvars Xs)) =
kind_open (kind_subst S k) (typ_fvars Xs).
Proof.
intros.
destruct* k as [[kc kv kr kh]|].
simpl.
apply* kind_pi; simpl.
clear kh; induction* kr.
simpl. fold (typ_open_vars (snd a) Xs).
rewrite* <- typ_subst_open_vars.
rewrite* IHkr.
Qed.
Lemma map_combine : forall (A:Set) (f:A->A) Xs Ys,
map f (combine Xs Ys) = combine Xs (List.map f Ys).
Proof.
induction Xs; destruct Ys; simpl*.
rewrite* IHXs.
Qed.
Lemma kinds_subst_open_vars : forall S Ks Xs,
fresh (dom S) (length Xs) Xs ->
env_prop type S ->
map (kind_subst S) (kinds_open_vars Ks Xs) =
kinds_open_vars (List.map (kind_subst S) Ks) Xs.
Proof.
unfold kinds_open_vars.
intros.
rewrite map_combine.
apply (f_equal (combine Xs (B:=kind))).
unfold kinds_open.
induction* Ks.
simpls. rewrite IHKs.
rewrite* kind_subst_open_vars.
Qed.
(** Opening up an abstraction of body t with a term u is the same as opening
up the abstraction with a fresh name x and then substituting u for x. *)
Lemma typ_subst_nil : forall T,
typ_subst nil T = T.
Proof.
induction T; simpl; auto.
rewrite IHT1; rewrite* IHT2.
Qed.
Lemma typ_subst_nth : forall S1 n S Xs Us,
fresh (dom S) (length Xs) Xs ->
types (length Xs) Us ->
nth n Us typ_def =
typ_subst (S1 & combine Xs Us & S) (typ_open_vars (typ_bvar n) Xs).
Proof.
induction n; intros; destruct H0; destruct Xs; destruct Us;
rewrite concat_assoc; simpls; try discriminate; auto.
assert (Bv: binds v t ((v, t) :: combine Xs Us)).
unfold binds; simpl.
destruct* (eq_var_dec v v).
destruct H; assert (v # S) by auto.
rewrite* (binds_prepend S1 (binds_concat_fresh S Bv H3)).
destruct H.
unfold typ_open_vars in *; simpl in *.
rewrite* (IHn (S ++ (v,t)::nil) Xs).
fold (((v,t)::nil) & S).
repeat rewrite <- concat_assoc. simpl*.
fold (((v,t)::nil) & S).
rewrite* dom_concat.
Qed.
Lemma typ_subst_intro0 : forall S Xs Us T,
fresh (typ_fv T) (length Xs) Xs ->
types (length Xs) Us ->
env_prop type S ->
typ_open (typ_subst S T) Us =
typ_subst (S & combine Xs Us) (typ_open_vars T Xs).
Proof.
induction T; simpls; intros.
rewrite <- (concat_empty (combine Xs Us)).
rewrite <- concat_assoc.
apply* typ_subst_nth.
case_eq (get v S); intros.
rewrite* (binds_concat_fresh (combine Xs Us) H2).
rewrite* <- typ_open_type.
rewrite* get_notin_dom.
rewrite* IHT1. rewrite* IHT2.
Qed.
Lemma typ_subst_intro : forall Xs Us T,
fresh (typ_fv T) (length Xs) Xs ->
types (length Xs) Us ->
(typ_open T Us) = typ_subst (combine Xs Us) (typ_open_vars T Xs).
Proof.
intros.
rewrite (app_nil_end (combine Xs Us)).
fold (empty(A:=typ)).
pattern T at 1.
rewrite <- (typ_subst_fresh empty T).
apply* (typ_subst_intro0 (S:=empty) Xs T (Us:=Us) H).
intro; intros.
elim H1.
simpl; intro; auto.
Qed.
(** Types are stable by type substitution *)
Lemma typ_subst_type : forall S T,
env_prop type S -> type T -> type (typ_subst S T).
Proof.
induction 2; simpl*.
case_eq (get X S); intros; auto*.
Qed.
Hint Resolve typ_subst_type : core.
(** List of types are stable by type substitution *)
Lemma typ_subst_type_list : forall S Ts n,
env_prop type S -> types n Ts ->
types n (List.map (typ_subst S) Ts).
Proof.
unfold types, list_for_n.
induction Ts; destruct n; simpl; intros TU [EQ TT].
auto. auto. inversion EQ.
inversions TT. forward~ (IHTs n) as [K1 K2].
Qed.
(** ** Opening a body with a list of types gives a type *)
Lemma typ_open_types : forall T Us Ks,
typ_body T Ks ->
types (length Ks) Us ->
type (typ_open T Us).
Proof.
introv K WT. pick_freshes (length Ks) Xs.
rewrite* (@typ_subst_intro Xs).
apply* typ_subst_type. destruct* WT.
destruct* (K Xs).
rewrite* <- (fresh_length _ _ _ Fr).
Qed.
(* ====================================================================== *)
(** * Properties of schemes *)
(** Substitution for a fresh name is identity. *)
Lemma sch_subst_fresh : forall S M,
disjoint (dom S) (sch_fv M) ->
sch_subst S M = M.
Proof.
intros. destruct M as [T K]. unfold sch_subst.
unfold sch_fv in H; simpl in H.
rewrite* typ_subst_fresh.
simpl. apply (f_equal (Sch T)).
induction* K.
simpl in *; rewrite* IHK.
rewrite* kind_subst_fresh.
Qed.
(** Trivial lemma to unfolding definition of [sch_subst] by rewriting. *)
Lemma sch_subst_fold : forall S T K,
Sch (typ_subst S T) (List.map (kind_subst S) K) = sch_subst S (Sch T K).
Proof.
auto.
Qed.
(** Distributivity of type substitution on opening of scheme. *)
Lemma sch_subst_open : forall S M Us,
env_prop type S ->
typ_subst S (sch_open M Us)
= sch_open (sch_subst S M) (List.map (typ_subst S) Us).
Proof.
unfold sch_open. intros. destruct M. simpl.
rewrite* <- typ_subst_open.
Qed.
(** Distributivity of type substitution on opening of scheme with variables. *)
Lemma sch_subst_open_vars : forall S M Xs,
fresh (dom S) (length Xs) Xs ->
env_prop type S ->
typ_subst S (sch_open_vars M Xs)
= sch_open_vars (sch_subst S M) Xs.
Proof.
unfold sch_open_vars. intros. destruct M.
rewrite* <- typ_subst_open_vars.
Qed.
(** Distributivity of type substitution on opening of kinds. *)
Lemma kind_subst_open : forall S k Us,
env_prop type S ->
kind_subst S (kind_open k Us) =
kind_open (kind_subst S k) (List.map (typ_subst S) Us).
Proof.
intros.
destruct* k as [[kc kv kr kh]|]; simpl.
apply* kind_pi; simpl.
clear kh; induction* kr.
simpl. rewrite <- IHkr.
rewrite* typ_subst_open.
Qed.
Lemma kinds_subst_open : forall S Ks Us,
env_prop type S ->
List.map (kind_subst S) (kinds_open Ks Us) =
kinds_open (List.map (kind_subst S) Ks) (List.map (typ_subst S) Us).
Proof.
intros.
unfold kinds_open.
induction* Ks.
simpl; rewrite <- IHKs.
rewrite* kind_subst_open.
Qed.
(** Properties of entailment. *)
Lemma entails_refl : forall k, entails k k.
Proof.
intros. split2*.
Qed.
Hint Resolve entails_refl : core.
Lemma entails_trans : forall k1 k2 k3,
entails k1 k2 -> entails k2 k3 -> entails k1 k3.
Proof.
intros.
destruct H; destruct H0.
split.
apply* (Cstr.entails_trans H H0).
intros; auto.
Qed.
Lemma kind_subst_entails : forall S k k',
entails k' k ->
entails (ckind_map (typ_subst S) k') (ckind_map (typ_subst S) k).
Proof.
intros.
destruct H.
destruct k as [kc kr]; destruct k' as [kc' kr'].
split; simpl*.
intros; simpl in *.
destruct T.
destruct (map_snd_inv _ _ _ _ H1) as [T' [e i]].
rewrite <- e.
apply* in_map_snd.
Qed.
Hint Resolve kind_subst_entails : core.
(** Properties of well-kindedness *)
Lemma well_kinded_extend : forall K K' x T,
disjoint (dom K) (dom K') ->
well_kinded K x T -> well_kinded (K & K') x T.
Proof.
induction 2.
apply wk_any.
apply* wk_kind.
Qed.
Hint Resolve well_kinded_extend : core.
Lemma well_kinded_comm : forall K K' K'',
ok (K & K' & K'') ->
forall x T,
well_kinded (K & K'' & K') x T ->
well_kinded (K & K' & K'') x T.
Proof.
introv OK; introv WK. gen_eq (K & K'' & K') as H. gen K''.
induction WK; introv Ok EQ; subst.
apply wk_any.
apply* (@wk_kind k').
destruct* (binds_concat_inv H).
destruct H1.
destruct* (binds_concat_inv H2).
Qed.
Lemma well_kinded_weaken : forall K K' K'',
ok (K & K' & K'') ->
forall x T,
well_kinded (K & K'') x T ->
well_kinded (K & K' & K'') x T.
Proof.
intros. apply* well_kinded_comm.
Qed.
Hint Resolve well_kinded_weaken : core.
(** Well substitutions *)
(* Need to define typ_subst first *)
Definition well_subst K K' S :=
forall Z k,
binds Z k K ->
well_kinded K' (kind_subst S k) (typ_subst S (typ_fvar Z)).
Lemma well_kinded_subst: forall S K K' k T,
well_subst K K' S ->
well_kinded K k T ->
well_kinded K' (kind_subst S k) (typ_subst S T).
Proof.
intros.
induction H0.
constructor.
generalize (H x _ H0); intro HW.
inversions HW.
simpl typ_subst.
case_eq (get x S); intros; rewrite H2 in H3.
subst.
simpl. apply* wk_kind.
refine (entails_trans H6 _); auto.
simpl.
inversions H3.
apply* wk_kind.
refine (entails_trans H6 _); auto.
Qed.
Hint Resolve well_kinded_subst : core.
(** Properties of instantiation and constants *)
Lemma trm_inst_nil : forall t, trm_inst t nil = t.
Proof.
unfold trm_inst; intros.
generalize 0; induction t; intros; simpl*.
destruct* (Compare_dec.le_lt_dec n0 n).
destruct* (n-n0).
rewrite* IHt.
rewrite IHt1; rewrite* IHt2.
rewrite IHt1; rewrite* IHt2.
Qed.
Lemma const_app_app : forall c l l',
const_app c (l++l') = fold_left trm_app l' (const_app c l).
Proof.
intros. unfold const_app. apply fold_left_app.
Qed.
Lemma trm_inst_app : forall c tl pl,
trm_inst_rec 0 tl (const_app c pl) =
const_app c (List.map (trm_inst_rec 0 tl) pl).
Proof.
introv.
rewrite <- (rev_involutive pl).
induction (rev pl). simpl. auto.
simpl in *.
rewrite map_app.
repeat rewrite const_app_app.
simpl. congruence.
Qed.
Lemma const_app_inv : forall c pl,
pl = nil \/
exists t1, exists t2, const_app c pl = trm_app t1 t2.
Proof.
intros.
destruct* pl.
right*.
destruct* (exists_last (l:=t::pl)). intro; discriminate.
destruct s. rewrite e.
rewrite const_app_app. simpl.
esplit; esplit; reflexivity.
Qed.
Lemma trm_inst_app_inv : forall c pl tl,
pl = nil \/
exists t1, exists t2,
trm_inst (const_app c pl) tl = trm_app t1 t2.
Proof.
intros.
destruct* (const_app_inv c pl).
right*.
destruct H as [x1 [x2 e]].
rewrite e.
exists (trm_inst x1 tl).
exists* (trm_inst x2 tl).
Qed.
Lemma const_app_eq : forall c1 vl1 c2 vl2,
const_app c1 vl1 = const_app c2 vl2 -> c1 = c2 /\ vl1 = vl2.
Proof.
intros.
gen vl2.
induction vl1 using rev_ind; intros.
unfold const_app in H.
destruct vl2 using rev_ind; simpl in H.
inversions* H.
rewrite fold_left_app in H. simpl in H. discriminate.
destruct vl2 using rev_ind; repeat rewrite const_app_app in H.
discriminate.
inversions H; clear H.
destruct (IHvl1 _ H1).
subst*.
Qed.
(* Extra properties *)
Lemma All_kind_types_None : forall P, All_kind_types P None.
Proof.
unfold All_kind_types. simpl*.
Qed.
Hint Resolve All_kind_types_None : core.
Lemma All_kind_types_imp (P P' : typ -> Prop) k:
(forall x, P x -> P' x) ->
All_kind_types P k -> All_kind_types P' k.
Proof.
intros.
destruct* k as [[kc kv kr kh]|].
unfold All_kind_types, kind_types in *.
simpl in *.
clear -H H0; induction kr; simpl in *. auto.
inversions* H0.
Qed.
Lemma All_kind_types_map : forall P f a,
All_kind_types (fun x => P (f x)) a ->
All_kind_types P (kind_map f a).
Proof.
intros.
destruct a as [[kc kv kr kh]|]; simpl*.
unfold All_kind_types in *; simpl in *.
clear kv kh; induction kr. simpl*.
simpl in *. inversions* H.
Qed.
Lemma All_kind_types_inv: forall P f a,
All_kind_types P (kind_map f a) ->
All_kind_types (fun x => P (f x)) a.
Proof.
intros.
destruct a as [[kc kv kr kh]|]; simpl*.
unfold All_kind_types in *; simpl in *.
clear kv kh; induction kr. simpl*.
simpl in *. inversions* H.
Qed.
Lemma incr_subst_fresh : forall a t S Xs,
fresh {{a}} (length Xs) Xs ->
List.map (typ_subst ((a, t) :: S)) (typ_fvars Xs) =
List.map (typ_subst S) (typ_fvars Xs).
Proof.
induction Xs; simpl; intros. auto.
destruct* (eq_var_dec a0 a).
rewrite e in H. destruct* H. elim H. auto.
rewrite* IHXs.
Qed.
Lemma fresh_subst : forall L Xs Vs,
fresh L (length Vs) Xs ->
List.map (typ_subst (combine Xs Vs)) (typ_fvars Xs) = Vs.
Proof.
induction Xs; destruct Vs; intros; try contradiction; simpl*.
destruct* (eq_var_dec a a).
simpl in H.
rewrite incr_subst_fresh. rewrite* IHXs.
destruct* H.
Qed.
Lemma kind_fv_fresh : forall k Ks n Xs,
In k Ks ->
fresh (kind_fv_list Ks) n Xs ->
fresh (typ_fv_list (kind_types k)) n Xs.
Proof.
induction Ks; intros. elim H.
simpl in H; destruct H.
rewrite H in H0; destruct (fresh_union_r _ _ _ _ H0).
unfold kind_fv in H1. auto.
apply* IHKs.
simpls; auto*.
Qed.
Lemma typ_fv_typ_fvars : forall Ys,
typ_fv_list (typ_fvars Ys) = mkset Ys.
Proof.
induction Ys; simpl*.
rewrite* IHYs.
Qed.
Lemma typ_fvars_app : forall Xs Ys,
typ_fvars (Xs++Ys) = typ_fvars Xs ++ typ_fvars Ys.
Proof.
unfold typ_fvars; intros; apply map_app.
Qed.
Lemma types_typ_fvars : forall Xs,
types (length Xs) (typ_fvars Xs).
Proof.
unfold typ_fvars; intro; split.
rewrite* map_length.
induction Xs; simpl*.
Qed.
Hint Immediate types_typ_fvars : core.
(** Schemes are stable by type substitution. *)
Lemma typ_open_other_type : forall Us Vs T,
type (typ_open T Us) ->
types (length Us) Vs ->
type (typ_open T Vs).
Proof.
induction T; simpl; intros.
destruct H0.
gen Us Vs; induction n; destruct Us; destruct Vs;
simpl in *; intros; try discriminate;
inversion* H1.
simpl*.
inversion* H.
Qed.
Lemma typ_open_vars_type : forall Xs Ys T,
type (typ_open_vars T Xs) ->
length Ys = length Xs ->
type (typ_open_vars T Ys).
Proof.
intros.
unfold typ_open_vars.
apply (typ_open_other_type (typ_fvars Xs)). apply H.
replace (length (typ_fvars Xs)) with (length Ys).
apply types_typ_fvars.
unfold typ_fvars. rewrite* map_length.
Qed.
Lemma sch_subst_type : forall S M,
env_prop type S -> scheme M -> scheme (sch_subst S M).
Proof.
unfold scheme. intros S [T Ks] TU K.
simpls.
introv Len.
rewrite map_length in Len.
destruct (var_freshes (dom S) (length Ks)) as [Ys Fr].
destruct* (K Ys); clear K.
assert (LenYs: length Xs = length Ys) by rewrite* <- Len.
split.
apply* (typ_open_vars_type Ys).
rewrite* typ_subst_open_vars.
apply* list_forall_map.
clear H0; intros.
unfold kind_subst.
apply All_kind_types_map.