1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/Fsub/part1a/".
16 include "logic/equality.ma".
18 include "datatypes/bool.ma".
19 include "nat/compare.ma".
20 include "Fsub/defn.ma".
22 theorem JS_Refl : \forall T,G.(WFType G T) \to (WFEnv G) \to (JSubtype G T T).
23 apply Typ_len_ind;intro;elim U
24 [(* FIXME *) generalize in match H1;intro;inversion H1
29 |apply (SA_Refl_TVar ? ? H2);(*FIXME*)generalize in match H1;intro;
31 [intros;destruct H6;rewrite > Hcut;assumption
35 |apply (SA_Top ? ? H2 H1)
36 |cut ((WFType G t) \land (WFType G t1))
37 [elim Hcut;apply SA_Arrow
46 |(*FIXME*)generalize in match H3;intro;inversion H3
49 |intros;destruct H11;rewrite > Hcut;rewrite > Hcut1;split;assumption
50 |intros;destruct H11]]
51 |elim (fresh_name ((fv_type t1) @ (fv_env G)));
52 cut ((\lnot (in_list ? a (fv_type t1))) \land
53 (\lnot (in_list ? a (fv_env G))))
54 [elim Hcut;cut (WFType G t)
55 [apply (SA_All2 ? ? ? ? ? a ? H7 H6 H6)
61 [rewrite > subst_O_nat;rewrite < eq_t_len_TFree_subst;
63 |(*FIXME*)generalize in match H3;intro;inversion H3
67 |intros;destruct H14;rewrite < Hcut2 in H11;
68 rewrite < Hcut3 in H11;rewrite < H13;rewrite < H13 in H11;
70 |apply WFE_cons;assumption]]
71 |(*FIXME*)generalize in match H3;intro;inversion H3
75 |intros;destruct H14;rewrite > Hcut1;assumption]]
76 |split;unfold;intro;apply H5;apply natinG_or_inH_to_natinGH;auto]]
79 lemma env_append_weaken : \forall G,H.(WFEnv (H @ G)) \to
82 [simplify;unfold;intros;assumption
83 |simplify in H2;simplify;unfold;intros;apply in_Skip;apply H1
84 [apply (WFE_consG_WFE_G ? ? H2)
88 lemma JS_weakening : \forall G,T,U.(JSubtype G T U) \to
89 \forall H.(WFEnv H) \to (incl ? G H) \to (JSubtype H T U).
91 [apply (SA_Top ? ? H4);lapply (incl_bound_fv ? ? H5);
92 apply (WFT_env_incl ? ? H2 ? Hletin)
93 |apply (SA_Refl_TVar ? ? H4);lapply (incl_bound_fv ? ? H5);
95 |lapply (H3 ? H5 H6);lapply (H6 ? H1);
96 apply (SA_Trans_TVar ? ? ? ? Hletin1 Hletin)
97 |lapply (H2 ? H6 H7);lapply (H4 ? H6 H7);
98 apply (SA_Arrow ? ? ? ? ? Hletin Hletin1)
99 |lapply (H2 ? H6 H7);apply (SA_All ? ? ? ? ? Hletin);intros;apply H4
100 [unfold;intro;apply H8;lapply (incl_bound_fv ? ? H7);apply (Hletin1 ? H9)
104 |lapply (incl_bound_fv ? ? H7);apply (WFT_env_incl ? ? ? ? Hletin1);
105 apply (JS_to_WFT1 ? ? ? H1)]
106 |unfold;intros;inversion H9
107 [intros;lapply (inj_head ? ? ? ? H11);rewrite > Hletin1;apply in_Base
108 |intros;lapply (inj_tail ? ? ? ? ? H13);rewrite < Hletin1 in H10;
109 apply in_Skip;apply (H7 ? H10)]]]
112 lemma fv_env_extends : \forall H,x,B,C,T,U,G.
113 (fv_env (H @ ((mk_bound B x T) :: G))) =
114 (fv_env (H @ ((mk_bound C x U) :: G))).
116 [simplify;reflexivity
117 |elim s;simplify;rewrite > H1;reflexivity]
120 lemma WFE_Typ_subst : \forall H,x,B,C,T,U,G.
121 (WFEnv (H @ ((mk_bound B x T) :: G))) \to (WFType G U) \to
122 (WFEnv (H @ ((mk_bound C x U) :: G))).
124 [simplify;intros;(*FIXME*)generalize in match H1;intro;inversion H1
125 [intros;lapply (nil_cons ? G (mk_bound B x T));lapply (Hletin H4);
127 |intros;lapply (inj_tail ? ? ? ? ? H8);lapply (inj_head ? ? ? ? H8);
128 destruct Hletin1;rewrite < Hletin in H6;rewrite < Hletin in H4;
129 rewrite < Hcut1 in H6;apply (WFE_cons ? ? ? ? H4 H6 H2)]
130 |intros;simplify;generalize in match H2;elim s;simplify in H4;
132 [intros;absurd (mk_bound b n t::l@(mk_bound B x T::G)=Empty)
135 |intros;lapply (inj_tail ? ? ? ? ? H9);lapply (inj_head ? ? ? ? H9);
136 destruct Hletin1;apply WFE_cons
138 [rewrite > Hletin;assumption
140 |rewrite > Hcut1;generalize in match H7;rewrite < Hletin;
141 rewrite > (fv_env_extends ? x B C T U);intro;assumption
142 |rewrite < Hletin in H8;rewrite > Hcut2;
143 apply (WFT_env_incl ? ? H8);rewrite > (fv_env_extends ? x B C T U);
144 unfold;intros;assumption]]]
147 lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y.
148 (in_list ? (mk_bound D y V) (H @ ((mk_bound C x U) :: G))) \to
150 (in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G))).
152 [simplify in H1;(*FIXME*)generalize in match H1;intro;inversion H1
153 [intros;lapply (inj_head ? ? ? ? H5);rewrite < H4 in Hletin;
154 destruct Hletin;absurd (y = x) [symmetry;assumption|assumption]
155 |intros;simplify;lapply (inj_tail ? ? ? ? ? H7);rewrite > Hletin;
156 apply in_Skip;assumption]
157 |(*FIXME*)generalize in match H2;intro;inversion H2
158 [intros;simplify in H6;lapply (inj_head ? ? ? ? H6);rewrite > Hletin;
159 simplify;apply in_Base
160 |simplify;intros;lapply (inj_tail ? ? ? ? ? H8);rewrite > Hletin in H1;
161 rewrite > H7 in H1;apply in_Skip;apply (H1 H5 H3)]]
164 lemma t_len_pred: \forall T,m.(S (t_len T)) \leq m \to (t_len T) \leq (pred m).
166 [elim (not_le_Sn_O ? H)
167 |simplify;apply (le_S_S_to_le ? ? H1)]
170 lemma pred_m_lt_m : \forall m,T.(t_len T) \leq m \to (pred m) < m.
173 [simplify in H;elim (not_le_Sn_n ? H)
174 |simplify in H;elim (not_le_Sn_n ? H)
175 |simplify in H;elim (not_le_Sn_n ? H)
176 |simplify in H2;elim (not_le_Sn_O ? H2)
177 |simplify in H2;elim (not_le_Sn_O ? H2)]
178 |intros;simplify;unfold;constructor 1]
181 lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to
182 (in_list ? (mk_bound B x T) G) \to
183 (in_list ? (mk_bound B x U) G) \to T = U.
185 [lapply (in_list_nil ? ? H1);elim Hletin
187 [intros;rewrite < H7 in H8;lapply (inj_head ? ? ? ? H8);
188 rewrite > Hletin in H5;inversion H5
189 [intros;rewrite < H9 in H10;lapply (inj_head ? ? ? ? H10);
190 destruct Hletin1;symmetry;assumption
191 |intros;lapply (inj_tail ? ? ? ? ? H12);rewrite < Hletin1 in H9;
192 rewrite < H11 in H9;lapply (boundinenv_natinfv x e)
193 [destruct Hletin;rewrite < Hcut1 in Hletin2;lapply (H3 Hletin2);
196 [apply B|apply ex_intro [apply T|assumption]]]]
197 |intros;lapply (inj_tail ? ? ? ? ? H10);rewrite < H9 in H7;
198 rewrite < Hletin in H7;(*FIXME*)generalize in match H5;intro;inversion H5
199 [intros;rewrite < H12 in H13;lapply (inj_head ? ? ? ? H13);
200 destruct Hletin1;rewrite < Hcut1 in H7;
201 lapply (boundinenv_natinfv n e)
202 [lapply (H3 Hletin2);elim Hletin3
204 [apply B|apply ex_intro [apply U|assumption]]]
205 |intros;apply (H2 ? H7);rewrite > H14;lapply (inj_tail ? ? ? ? ? H15);
206 rewrite > Hletin1;assumption]]]
209 lemma JS_trans_narrow : \forall n.
211 (t_len Q) \leq n \to (JSubtype G T Q) \to (JSubtype G Q U) \to
212 (JSubtype G T U)) \land
213 (\forall G,H,X,P,Q,M,N.
215 (JSubtype (H @ ((mk_bound true X Q) :: G)) M N) \to
217 (JSubtype (H @ ((mk_bound true X P) :: G)) M N)).
218 intro;apply (nat_elim1 n);intros 2;
219 cut (\forall G,T,Q.(JSubtype G T Q) \to
220 \forall U.(t_len Q \leq m) \to (JSubtype G Q U) \to (JSubtype G T U))
221 [cut (\forall G,M,N.(JSubtype G M N) \to
223 (G = G2 @ ((mk_bound true X Q) :: G1)) \to (t_len Q) \leq m \to
224 (JSubtype G1 P Q) \to
225 (JSubtype (G2 @ ((mk_bound true X P) :: G1)) M N))
227 [intros;apply (Hcut ? ? ? H2 ? H1 H3)
228 |intros;apply (Hcut1 ? ? ? H3 ? ? ? ? ? ? H2 H4);reflexivity]
229 |intros 9;cut (incl ? (fv_env (G2 @ ((mk_bound true X Q)::G1)))
230 (fv_env (G2 @ ((mk_bound true X P)::G1))))
232 (* [rewrite > H6 in H2;lapply (JS_to_WFT1 ? ? ? H8);
233 apply (WFE_Typ_subst ? ? ? ? ? ? ? H2 Hletin) *)
234 generalize in match Hcut1;generalize in match H2;
235 generalize in match H1;generalize in match H4;
236 generalize in match G1;generalize in match G2;elim H1
238 [rewrite > H9 in H5;lapply (JS_to_WFT1 ? ? ? H7);
239 apply (WFE_Typ_subst ? ? ? ? ? ? ? H5 Hletin)
240 |rewrite > H9 in H6;apply (WFT_env_incl ? ? H6);elim l
241 [simplify;unfold;intros;assumption
242 |simplify;apply (incl_nat_cons ? ? ? H11)]]
244 [rewrite > H9 in H5;lapply (JS_to_WFT1 ? ? ? H7);
245 apply (WFE_Typ_subst ? ? ? ? ? ? ? H5 Hletin)
246 |apply H10;rewrite < H9;assumption]
247 |elim (decidable_eq_nat X n1)
248 [apply (SA_Trans_TVar ? ? ? P)
249 [rewrite < H12;elim l
250 [simplify;apply in_Base
251 |simplify;apply in_Skip;assumption]
252 |lapply (JS_to_WFE ? ? ? H9);rewrite > H10 in Hletin;
254 lapply (WFE_bound_bound ? ? ? Q ? Hletin H5)
255 [lapply (H7 ? ? H8 H6 H10 H11);rewrite > Hletin1 in Hletin2;
256 apply (Hcut ? ? ? ? ? H3 Hletin2);
257 lapply (JS_to_WFE ? ? ? Hletin2);
258 apply (JS_weakening ? ? ? H8 ? Hletin3);unfold;intros;
259 elim l;simplify;apply in_Skip;assumption
260 |rewrite > H12;elim l
261 [simplify;apply in_Base
262 |simplify;apply in_Skip;assumption]]]
263 |rewrite > H10 in H5;apply (SA_Trans_TVar ? ? ? t1)
264 [apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H5);unfold;
265 intro;apply H12;symmetry;assumption
266 |apply (H7 ? ? H8 H6 H10 H11)]]
268 [apply (H6 ? ? H9 H5 H11 H12)
269 |apply (H8 ? ? H9 H7 H11 H12)]
271 [apply (H6 ? ? H9 H5 H11 H12)
272 |intros;apply (H8 ? ? (mk_bound true X1 t2::l) l1)
273 [unfold;intro;apply H13;rewrite > H11 in H14;apply (H12 ? H14)
275 |apply H7;rewrite > H11;unfold;intro;apply H13;apply (H12 ? H14)
276 |simplify;rewrite < H11;reflexivity
277 |simplify;apply incl_nat_cons;assumption]]]
279 [simplify;unfold;intros;assumption
280 |intro;elim s 0;simplify;intros;apply incl_nat_cons;assumption]]]
281 |intros 4;(*generalize in match H1;*)elim H1
283 [intros;rewrite < H8;apply (SA_Top ? ? H2 H3)
287 |intros;destruct H11]
289 |apply (SA_Trans_TVar ? ? ? ? H2);apply (H4 ? H5 H6)
291 [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Arrow
292 [apply (JS_to_WFT2 ? ? ? H2)
293 |apply (JS_to_WFT1 ? ? ? H4)]
296 |intros;destruct H13;elim (H (pred m))
298 [rewrite > H12 in H2;rewrite < Hcut in H8;
299 apply (H15 ? ? ? ? ? H8 H2);lapply (t_len_arrow1 t2 t3);
300 unfold in Hletin;lapply (trans_le ? ? ? Hletin H6);
301 apply (t_len_pred ? ? Hletin1)
302 |rewrite > H12 in H4;rewrite < Hcut1 in H10;
303 apply (H15 ? ? ? ? ? H4 H10);lapply (t_len_arrow2 t2 t3);
304 unfold in Hletin;lapply (trans_le ? ? ? Hletin H6);
305 apply (t_len_pred ? ? Hletin1)]
306 |apply (pred_m_lt_m ? ? H6)]
307 |intros;destruct H13]
309 [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Forall
310 [apply (JS_to_WFT2 ? ? ? H2)
311 |intros;lapply (H4 ? H13);lapply (JS_to_WFT1 ? ? ? Hletin);
312 apply (WFT_env_incl ? ? Hletin1);simplify;unfold;intros;
317 |intros;destruct H13;elim (H (pred m))
318 [elim (fresh_name ((fv_env e1) @ (fv_type t1) @ (fv_type t7)));
319 cut ((\lnot (in_list ? a (fv_env e1))) \land
320 (\lnot (in_list ? a (fv_type t1))) \land
321 (\lnot (in_list ? a (fv_type t7))))
322 [elim Hcut2;elim H18;clear Hcut2 H18;apply (SA_All2 ? ? ? ? ? a)
323 [rewrite < Hcut in H8;rewrite > H12 in H2;
324 apply (H15 ? ? ? ? ? H8 H2);lapply (t_len_forall1 t2 t3);
325 unfold in Hletin;lapply (trans_le ? ? ? Hletin H6);
326 apply (t_len_pred ? ? Hletin1)
330 |lapply (H10 ? H20);rewrite > H12 in H5;
331 lapply (H5 ? H20 (subst_type_O t5 (TFree a)))
332 [apply (H15 ? ? ? ? ? ? Hletin)
333 [rewrite < Hcut1;rewrite > subst_O_nat;
334 rewrite < eq_t_len_TFree_subst;
335 lapply (t_len_forall2 t2 t3);unfold in Hletin2;
336 lapply (trans_le ? ? ? Hletin2 H6);
337 apply (t_len_pred ? ? Hletin3)
338 |rewrite < Hcut in H8;
339 apply (H16 e1 (nil ?) a t6 t2 ? ? ? Hletin1 H8);
340 lapply (t_len_forall1 t2 t3);unfold in Hletin2;
341 lapply (trans_le ? ? ? Hletin2 H6);
342 apply (t_len_pred ? ? Hletin3)]
343 |rewrite > subst_O_nat;rewrite < eq_t_len_TFree_subst;
344 lapply (t_len_forall2 t2 t3);unfold in Hletin1;
345 lapply (trans_le ? ? ? Hletin1 H6);
346 apply (trans_le ? ? ? ? Hletin2);constructor 2;
348 |rewrite > Hcut1;rewrite > H12 in H4;
349 lapply (H4 ? H20);rewrite < Hcut1;apply JS_Refl
350 [apply (JS_to_WFT2 ? ? ? Hletin1)
351 |apply (JS_to_WFE ? ? ? Hletin1)]]]
354 [unfold;intro;apply H17;
355 apply (natinG_or_inH_to_natinGH ? (fv_env e1));right;
357 |unfold;intro;apply H17;
358 apply (natinG_or_inH_to_natinGH
359 ((fv_type t1) @ (fv_type t7)));left;
360 apply natinG_or_inH_to_natinGH;right;assumption]
361 |unfold;intro;apply H17;
362 apply (natinG_or_inH_to_natinGH
363 ((fv_type t1) @ (fv_type t7)));left;
364 apply natinG_or_inH_to_natinGH;left;assumption]]
365 |apply (pred_m_lt_m ? ? H6)]]]]
368 theorem JS_trans : \forall G,T,U,V.(JSubtype G T U) \to
371 intros;elim (JS_trans_narrow (t_len U));apply (H2 ? ? ? ? ? H H1);constructor 1;
374 theorem JS_narrow : \forall G1,G2,X,P,Q,T,U.
375 (JSubtype (G2 @ (mk_bound true X Q :: G1)) T U) \to
376 (JSubtype G1 P Q) \to
377 (JSubtype (G2 @ (mk_bound true X P :: G1)) T U).
378 intros;elim (JS_trans_narrow (t_len Q));apply (H3 ? ? ? ? ? ? ? ? H H1);