2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "finite_lambda/finite_lambda.ma".
15 (****************************************************************)
17 inductive TJ (O: Type[0]) (D:O → FinSet): list (FType O) → T O D → FType O → Prop ≝
18 | tval: ∀G,o,a. TJ O D G (Val O D o a) (atom O o)
19 | trel: ∀G1,ty,G2,n. length ? G1 = n → TJ O D (G1@ty::G2) (Rel O D n) ty
20 | tapp: ∀G,M,N,ty1,ty2. TJ O D G M (arrow O ty1 ty2) → TJ O D G N ty1 →
21 TJ O D G (App O D M N) ty2
22 | tlambda: ∀G,M,ty1,ty2. TJ O D (ty1::G) M ty2 →
23 TJ O D G (Lambda O D ty1 M) (arrow O ty1 ty2)
25 (|v| = |enum (FinSet_of_FType O D ty1)|) →
26 (∀M. mem ? M v → TJ O D G M ty2) →
27 TJ O D G (Vec O D ty1 v) (arrow O ty1 ty2).
29 lemma wt_to_T: ∀O,D,G,ty,a.TJ O D G (to_T O D ty a) ty.
31 [#o #a normalize @tval
32 |#ty1 #ty2 #Hind1 #Hind2 normalize * #v #Hv @tvec
33 [<Hv >length_map >length_map //
35 [normalize @False_ind |#a #v1 #Hind3 * [#eqM >eqM @Hind2 |@Hind3]]
40 lemma inv_rel: ∀O,D,G,n,ty.
41 TJ O D G (Rel O D n) ty → ∃G1,G2.|G1|=n∧G=G1@ty::G2.
42 #O #D #G #n #ty #Hrel inversion Hrel
43 [#G1 #o #a #_ #H destruct
44 |#G1 #ty1 #G2 #n1 #H1 #H2 #H3 #H4 destruct %{G1} %{G2} /2/
45 |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
46 |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct
47 |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct
51 lemma inv_tlambda: ∀O,D,G,M,ty1,ty2,ty3.
52 TJ O D G (Lambda O D ty1 M) (arrow O ty2 ty3) →
53 ty1 = ty2 ∧ TJ O D (ty2::G) M ty3.
54 #O #D #G #M #ty1 #ty2 #ty3 #Hlam inversion Hlam
55 [#G1 #o #a #_ #H destruct
56 |#G1 #ty #G2 #n #_ #_ #H destruct
57 |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
58 |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct % //
59 |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct
63 lemma inv_tvec: ∀O,D,G,v,ty1,ty2,ty3.
64 TJ O D G (Vec O D ty1 v) (arrow O ty2 ty3) →
65 (|v| = |enum (FinSet_of_FType O D ty1)|) ∧
66 (∀M. mem ? M v → TJ O D G M ty3).
67 #O #D #G #v #ty1 #ty2 #ty3 #Hvec inversion Hvec
68 [#G #o #a #_ #H destruct
69 |#G1 #ty #G2 #n #_ #_ #H destruct
70 |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
71 |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct
72 |#G1 #v1 #ty4 #ty5 #Hv #Hmem #_ #_ #H #H1 destruct % // @Hmem
76 (* could be generalized *)
77 lemma weak_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n →
78 TJ O D (G1@G2) (Rel O D n) ty1 →
79 TJ O D (G1@ty2::G2) (Rel O D (S n)) ty1.
80 #O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel)
81 * #G3 * #G4 * #H1 #H2 lapply (compare_append … H2)
83 [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4
84 @(absurd … H4) @le_to_not_lt //
85 |* #H3 #H4 >H4 >append_cons <associative_append @trel
86 >length_append >length_append <H1 >H3 >length_append normalize
87 >plus_n_Sm >associative_plus @eq_f //
91 lemma strength_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n →
92 TJ O D (G1@ty2::G2) (Rel O D n) ty1 →
93 TJ O D (G1@G2) (Rel O D (n-1)) ty1.
94 #O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel)
95 * #G3 * #G4 * #H1 #H2 lapply (compare_append … H2)
97 [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4
98 @(absurd … H4) @le_to_not_lt //
100 [>append_nil normalize * #H3 #H4 destruct @False_ind @(absurd … HG1)
102 |#ty3 #G5 * #H3 normalize #H4 destruct (H4) <associative_append @trel
103 <H1 >H3 >length_append >length_append normalize <plus_minus_associative //
108 lemma weakening: ∀O,D,G,N,tyN.
109 TJ O D G N tyN → ∀G1,G2,G3.G=G1@G2 →
110 TJ O D (G1@G3@G2) (lift O D N (|G1|) (|G3|)) tyN.
111 #O #D #G #N #tyN #HN elim HN -HN -tyN -N -G
112 [#G #o #a #G1 #G2 #G3 #_ @tval
113 |#G #ty #G2 #n #HG #G3 #G4 #G5 #H normalize
114 cases (true_or_false (leb (|G3|) n)) #Hcase >Hcase normalize
115 [lapply (compare_append … H) * #G6 *
116 [* #H1 #H2 >H2 <associative_append <associative_append @trel
117 <HG >H1 >length_append >length_append >length_append //
119 [* >append_nil normalize #H1 #H2 <H2 <associative_append @trel
120 <HG >H1 >length_append //
121 |#ty1 #G7 * #H @False_ind @(absurd … (leb_true_to_le … Hcase))
122 @lt_to_not_le <HG >H >length_append normalize //
125 |lapply (compare_append … H) * #G6 *
126 [* #H1 @False_ind @(absurd ?? (leb_false_to_not_le … Hcase)) <HG >H1
127 >length_append normalize //
129 [>append_nil normalize #H1 @False_ind
130 @(absurd ?? (leb_false_to_not_le … Hcase)) <HG >H1 //
131 |#ty1 #G7 #H1 normalize #H2 destruct >associative_append @trel //
135 |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #G3
136 #Heq @(tapp … (HindM … Heq) (HindN … Heq))
137 |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #G3 #Heq @tlambda @(HindM (ty1::G1))
139 |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #G3 #H1 @tvec
141 |#M #Hmem lapply (mem_map ????? Hmem) * #M1 * #memM1 #eqM <eqM @Hind //
146 lemma nth_spec: ∀A,a,d,l1,l2,n. |l1| = n → nth n A (l1@a::l2) d = a.
147 #A #a #d #l1 elim l1 normalize
149 |#b #tl #Hind #l2 #m #Hm <Hm normalize @Hind //
153 lemma wt_subst_gen: ∀O,D,G,M,tyM.
155 ∀G1,G2,N,tyN.G=(G1@tyN::G2) →
157 TJ O D (G1@G2) (subst O D M (|G1|) N) tyM.
158 #O #D #G #M #tyM #HM elim HM -HM -tyM -M -G
159 [#G #o #a #G1 #G2 #N #tyN #HG #_ normalize @tval
160 |#G #ty #G2 #n #Hlen #G21 #G22 #N #tyN #HG #HN
161 normalize cases (true_or_false (leb (|G21|) n))
162 [#H >H cases (le_to_or_lt_eq … (leb_true_to_le … H))
163 [#ltn >(not_eq_to_eqb_false … (lt_to_not_eq … ltn)) normalize
164 lapply (compare_append … HG) * #G3 *
165 [* #HG1 #HG2 @(strength_rel … tyN … ltn) <HG @trel @Hlen
166 |* #HG >HG in ltn; >length_append #ltn @False_ind
167 @(absurd … ltn) @le_to_not_lt >Hlen //
169 |#HG21 >(eq_to_eqb_true … HG21)
171 [<(nth_spec ? ty ty ? G2 … Hlen) >HG @nth_spec @HG21] #Hty >Hty
172 normalize <HG21 @(weakening ????? HN [ ]) //
174 |#H >H normalize lapply (compare_append … HG) * #G3 *
175 [* #H1 @False_ind @(absurd ? Hlen) @sym_not_eq @lt_to_not_eq >H1
176 >length_append @(lt_to_le_to_lt n (|G21|)) // @not_le_to_lt
177 @(leb_false_to_not_le … H)
179 [>append_nil * #H1 @False_ind @(absurd ? Hlen) <H1 @sym_not_eq
180 @lt_to_not_eq @not_le_to_lt @(leb_false_to_not_le … H)
181 |#ty2 #G4 * #H1 normalize #H2 destruct >associative_append @trel //
185 |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #N0 #tyN0 #eqG
186 #HN0 normalize @(tapp … ty1) [@(HindM … eqG HN0) |@(HindN … eqG HN0)]
187 |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #N0 #tyN0 #eqG
188 #HN0 normalize @(tlambda … ty1) @(HindM (ty1::G1) … HN0) >eqG //
189 |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #N0 #tyN0 #eqG
190 #HN0 normalize @(tvec … ty1)
192 |#M #Hmem lapply (mem_map ????? Hmem) * #a * -Hmem #Hmem #eqM <eqM
193 @(Hind … Hmem … eqG HN0)
198 lemma wt_subst: ∀O,D,M,N,G,ty1,ty2.
199 TJ O D (ty1::G) M ty2 →
201 TJ O D G (subst O D M 0 N) ty2.
202 #O #D #M #N #G #ty1 #ty2 #HM #HN @(wt_subst_gen …(ty1::G) … [ ] … HN) //
205 lemma subject_reduction: ∀O,D,M,M1,G,ty.
206 TJ O D G M ty → red O D M M1 → TJ O D G M1 ty.
207 #O #D #M #M1 #G #ty #HM lapply M1 -M1 elim HM -HM -ty -G -M
208 [#G #o #a #M1 #Hval elim (red_val ????? Hval)
209 |#G #ty #G1 #n #_ #M1 #Hrel elim (red_rel ???? Hrel)
210 |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #M1 #Hred inversion Hred
211 [#P #M0 #N0 #H1 destruct (H1) #HM1 @(wt_subst … HN)
212 @(proj2 … (inv_tlambda … HM))
213 |#ty #v #a #M0 #Ha #H1 #H2 destruct @(proj2 … (inv_tvec … HM))
215 |#M2 #M3 #N0 #Hredl #_ #H1 destruct (H1) #eqM1 @(tapp … HN) @HindM @Hredl
216 |#M2 #M3 #N0 #Hredr #_ #H1 destruct (H1) #eqM1 @(tapp … HM) @HindN @Hredr
217 |#ty #M0 #H1 destruct (H1)
218 |#ty #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1)
220 |#G #P #ty1 #ty2 #HP #Hind #M1 #Hred lapply(red_lambda ????? Hred) #HM1 >HM1
221 @tvec // #N #HN lapply(mem_map ????? HN) * #a * #mema #eqN <eqN -eqN
222 @(wt_subst …HP) @wt_to_T
223 |#G #v #ty1 #ty2 #Hlen #Hv #Hind #M1 #Hred lapply(red_vec ????? Hred)
224 * #N * #N1 * #v1 * #v2 * * #H1 #H2 #H3 >H3 @tvec
225 [<Hlen >H2 >length_append >length_append @eq_f //
226 |#M2 #Hmem cases (mem_append ???? Hmem) -Hmem #Hmem
227 [@Hv >H2 @mem_append_l1 //
229 [#HM2 >HM2 -HM2 @(Hind N … H1) >H2 @mem_append_l2 %1 //
230 |-Hmem #Hmem @Hv >H2 @mem_append_l2 %2 //