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/util.ma".
21 include "Fsub/defn.ma".
23 (*** Lemma A.1 (Reflexivity) ***)
25 theorem JS_Refl : \forall T,G.(WFType G T) \to (WFEnv G) \to (JSubtype G T T).
26 apply Typ_len_ind;intro;elim U
27 [(* FIXME *) generalize in match H1;intro;inversion H1
30 |*:intros;destruct H9]
31 |apply (SA_Refl_TVar ? ? H2);(*FIXME*)generalize in match H1;intro;
33 [intros;destruct H6;rewrite > Hcut;assumption
35 |*:intros;destruct H9]
36 |apply (SA_Top ? ? H2 H1)
37 |cut ((WFType G t) \land (WFType G t1))
38 [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]]
52 [lapply (H2 t ? ? Hcut H4)
54 |apply (SA_All ? ? ? ? ? Hletin);intros;apply H2
55 [rewrite < eq_t_len_TFree_subst;
57 |generalize in match H3;intro;inversion H3
61 |intros;destruct H12;subst;apply H9
63 |unfold;intro;apply H5;
64 elim (fresh_name ((fv_env l)@(fv_type t3)));
65 cut ((\lnot (in_list ? a (fv_env l))) \land
66 (\lnot (in_list ? a (fv_type t3))))
67 [elim Hcut1;lapply (H9 ? H13 H14);
68 lapply (fv_WFT ? X ? Hletin1)
69 [simplify in Hletin2;inversion Hletin2
70 [intros;lapply (inj_head_nat ? ? ? ? H16);subst;
72 |intros;lapply (inj_tail ? ? ? ? ? H18);
73 rewrite < Hletin3 in H15;assumption]
74 |apply varinT_varinT_subst;
76 |split;unfold;intro;apply H12;apply natinG_or_inH_to_natinGH
79 |apply WFE_cons;assumption]]
80 |(*FIXME*)generalize in match H3;intro;inversion H3
84 |intros;destruct H11;subst;assumption]]]
88 * A slightly more general variant to lemma A.2.2, where weakening isn't
89 * defined as concatenation of any two disjoint environments, but as
93 lemma JS_weakening : \forall G,T,U.(JSubtype G T U) \to
94 \forall H.(WFEnv H) \to (incl ? G H) \to (JSubtype H T U).
96 [apply (SA_Top ? ? H4);lapply (incl_bound_fv ? ? H5);
97 apply (WFT_env_incl ? ? H2 ? Hletin)
98 |apply (SA_Refl_TVar ? ? H4);lapply (incl_bound_fv ? ? H5);
100 |lapply (H3 ? H5 H6);lapply (H6 ? H1);
101 apply (SA_Trans_TVar ? ? ? ? Hletin1 Hletin)
102 |lapply (H2 ? H6 H7);lapply (H4 ? H6 H7);
103 apply (SA_Arrow ? ? ? ? ? Hletin Hletin1)
104 |lapply (H2 ? H6 H7);apply (SA_All ? ? ? ? ? Hletin);intros;apply H4
105 [unfold;intro;apply H8;lapply (incl_bound_fv ? ? H7);apply (Hletin1 ? H9)
108 |apply (JS_to_WFT1 ? ? ? Hletin)]
109 |unfold;intros;inversion H9
110 [intros;lapply (inj_head ? ? ? ? H11);rewrite > Hletin1;apply in_Base
111 |intros;lapply (inj_tail ? ? ? ? ? H13);rewrite < Hletin1 in H10;
112 apply in_Skip;apply (H7 ? H10)]]]
115 (* Lemma A.3 (Transitivity and Narrowing) *)
117 lemma JS_trans_narrow : \forall Q.
119 (JSubtype G T Q) \to (JSubtype G Q U) \to
120 (JSubtype G T U)) \land
121 (\forall G,H,X,P,M,N.
122 (JSubtype (H @ ((mk_bound true X Q) :: G)) M N) \to
124 (JSubtype (H @ ((mk_bound true X P) :: G)) M N)).
125 apply Typ_len_ind;intros 2;
132 |cut (\forall G,M,N.(JSubtype G M N) \to
134 (G = G2 @ ((mk_bound true X U) :: G1)) \to
135 (JSubtype G1 P U) \to
136 (JSubtype (G2 @ ((mk_bound true X P) :: G1)) M N))
137 [intros;apply (Hcut1 ? ? ? H2 ? ? ? ? ? H3);reflexivity
138 |intros;cut (incl ? (fv_env (G2 @ ((mk_bound true X U)::G1)))
139 (fv_env (G2 @ ((mk_bound true X P)::G1))))
140 [intros;generalize in match H2;generalize in match Hcut1;
141 generalize in match Hcut;generalize in match G2;elim H1
143 [rewrite > H8 in H4;lapply (JS_to_WFT1 ? ? ? H3);
144 apply (WFE_Typ_subst ? ? ? ? ? ? ? H4 Hletin)
145 |rewrite > H8 in H5;apply (WFT_env_incl ? ? H5 ? H7)]
147 [rewrite > H8 in H4;apply (WFE_Typ_subst ? ? ? ? ? ? ? H4);
148 apply (JS_to_WFT1 ? ? ? H3)
149 |rewrite > H8 in H5;apply (H7 ? H5)]
150 |elim (decidable_eq_nat X n)
151 [apply (SA_Trans_TVar ? ? ? P)
152 [rewrite < H10;elim l1
153 [simplify;constructor 1
154 |simplify;constructor 2;assumption]
156 [lapply (H6 ? H7 H8 H9);lapply (JS_to_WFE ? ? ? Hletin);
157 apply (JS_weakening ? ? ? H3 ? Hletin1);unfold;intros;
158 elim l1;simplify;constructor 2;assumption
159 |lapply (WFE_bound_bound true n t1 U ? ? H4)
160 [apply (JS_to_WFE ? ? ? H5)
161 |rewrite < Hletin;apply (H6 ? H7 H8 H9)
162 |rewrite > H9;rewrite > H10;elim l1;simplify
164 |constructor 2;assumption]]]]
165 |apply (SA_Trans_TVar ? ? ? t1)
167 apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H4);
168 unfold;intro;apply H10;symmetry;assumption
169 |apply (H6 ? H7 H8 H9)]]
171 [apply (H5 ? H8 H9 H10)
172 |apply (H7 ? H8 H9 H10)]
174 [apply (H5 ? H8 H9 H10)
175 |intros;apply (H7 ? ? (mk_bound true X1 t2::l1) H8)
176 [rewrite > H10;cut ((fv_env (l1@(mk_bound true X P::G1))) =
177 (fv_env (l1@(mk_bound true X U::G1))))
178 [unfold;intro;apply H11;rewrite > Hcut2;assumption
180 [simplify;reflexivity
181 |elim t4;simplify;rewrite > H12;reflexivity]]
182 |simplify;apply (incl_nat_cons ? ? ? H9)
183 |simplify;rewrite < H10;reflexivity]]]
184 |cut ((fv_env (G2@(mk_bound true X U::G1))) =
185 (fv_env (G2@(mk_bound true X P::G1))))
186 [rewrite > Hcut1;unfold;intros;assumption
188 [simplify;reflexivity
189 |elim t;simplify;rewrite > H4;reflexivity]]]]]
190 |intros 4;generalize in match H;elim H1
192 [intros;rewrite < H8;apply (SA_Top ? ? H2 H3)
195 |*:intros;destruct H11]
197 |apply (SA_Trans_TVar ? ? ? ? H2);apply (H4 H5 H6)
199 [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Arrow
200 [apply (JS_to_WFT2 ? ? ? H2)
201 |apply (JS_to_WFT1 ? ? ? H4)]
204 |intros;destruct H13;apply SA_Arrow
205 [rewrite > H12 in H2;rewrite < Hcut in H8;
207 [elim Hletin;apply (H15 ? ? ? H8 H2)
208 |apply (t_len_arrow1 t2 t3)]
209 |rewrite > H12 in H4;rewrite < Hcut1 in H10;
211 [elim Hletin;apply (H15 ? ? ? H4 H10)
212 |apply (t_len_arrow2 t2 t3)]]
213 |intros;destruct H13]
215 [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Forall
216 [apply (JS_to_WFT2 ? ? ? H2)
217 |intros;lapply (H4 ? H13);lapply (JS_to_WFT1 ? ? ? Hletin);
218 apply (WFT_env_incl ? ? Hletin1);simplify;unfold;intros;
223 |intros;destruct H13;subst;apply SA_All
225 [elim Hletin;apply (H12 ? ? ? H8 H2)
226 |apply t_len_forall1]
227 |intros;(*destruct H12;*)subst;
228 lapply (H6 (subst_type_nat t5 (TFree X) O))
229 [elim Hletin;apply H13
231 [elim Hletin1;apply (H16 l1 [] X t6);
232 [simplify;apply H4;assumption
234 |apply t_len_forall1]
236 |rewrite < eq_t_len_TFree_subst;
237 apply t_len_forall2]]]]]
240 theorem JS_trans : \forall G,T,U,V.(JSubtype G T U) \to
243 intros;elim JS_trans_narrow;autobatch;
246 theorem JS_narrow : \forall G1,G2,X,P,Q,T,U.
247 (JSubtype (G2 @ (mk_bound true X Q :: G1)) T U) \to
248 (JSubtype G1 P Q) \to
249 (JSubtype (G2 @ (mk_bound true X P :: G1)) T U).
250 intros;elim JS_trans_narrow;autobatch;