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 "Fsub/defn.ma".
18 (*** Lemma A.1 (Reflexivity) ***)
20 theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴ T.
22 [apply (SA_Refl_TVar l n H2 H1);
23 |apply (SA_Top l Top H1 (WFT_Top l));
24 |apply (SA_Arrow l t t1 t t1 (H2 H5) (H4 H5))
25 |apply (SA_All ? ? ? ? ? (H2 H5));intros;apply (H4 X H6)
26 [intro;apply H6;apply (fv_WFT (Forall t t1) X l)
27 [apply (WFT_Forall ? ? ? H1 H3)
33 * A slightly more general variant to lemma A.2.2, where weakening isn't
34 * defined as concatenation of any two disjoint environments, but as
38 lemma JS_weakening : \forall G,T,U.(JSubtype G T U) \to
39 \forall H.(WFEnv H) \to (incl ? G H) \to (JSubtype H T U).
41 [apply (SA_Top ? ? H4);lapply (incl_bound_fv ? ? H5);
42 apply (WFT_env_incl ? ? H2 ? Hletin)
43 |apply (SA_Refl_TVar ? ? H4);lapply (incl_bound_fv ? ? H5);
45 |lapply (H3 ? H5 H6);lapply (H6 ? H1);
46 apply (SA_Trans_TVar ? ? ? ? Hletin1 Hletin)
47 |lapply (H2 ? H6 H7);lapply (H4 ? H6 H7);
48 apply (SA_Arrow ? ? ? ? ? Hletin Hletin1)
49 |lapply (H2 ? H6 H7);apply (SA_All ? ? ? ? ? Hletin);intros;apply H4
50 [unfold;intro;apply H8;lapply (incl_bound_fv ? ? H7);apply (Hletin1 ? H9)
53 |apply (JS_to_WFT1 ? ? ? Hletin)]
54 |unfold;intros;elim (in_cons_case ? ? ? ? H9)
55 [rewrite > H10;apply in_Base
56 |elim H10;apply (in_Skip ? ? ? ? ? H11);apply (H7 ? H12)]]]
59 lemma decidable_eq_Typ : \forall S,T:Typ.(S = T) ∨ (S ≠ T).
62 [elim (decidable_eq_nat n n1)
63 [rewrite > H;left;reflexivity
64 |right;intro;destruct H1;apply (H Hcut)]
65 |2,3:right;intro;destruct H
66 |*:right;intro;destruct H2]
68 [2:elim (decidable_eq_nat n n1)
69 [rewrite > H;left;reflexivity
70 |right;intro;destruct H1;apply (H Hcut)]
71 |1,3:right;intro;destruct H
72 |*:right;intro;destruct H2]
75 |1,2:right;intro;destruct H
76 |*:right;intro;destruct H2]
78 [1,2,3:right;intro;destruct H2
80 [rewrite > H4;elim (H1 t3)
81 [rewrite > H5;left;reflexivity
82 |right;intro;apply H5;destruct H6;assumption]
83 |right;intro;apply H4;destruct H5;assumption]
84 |right;intro;destruct H4]
86 [1,2,3:right;intro;destruct H2
87 |right;intro;destruct H4
89 [rewrite > H4;elim (H1 t3)
90 [rewrite > H5;left;reflexivity
91 |right;intro;apply H5;destruct H6;assumption]
92 |right;intro;apply H4;destruct H5;assumption]]]
95 lemma decidable_eq_bound: ∀b1,b2:bound.(b1 = b2) ∨ (b1 ≠ b2).
96 intros;elim b1;elim b2;elim (decidable_eq_nat n n1)
97 [rewrite < H;elim (decidable_eq_Typ t t1)
98 [rewrite < H1;elim (bool_to_decidable_eq b b3)
99 [rewrite > H2;left;reflexivity
100 |right;intro;destruct H3;apply (H2 Hcut)]
101 |right;intro;destruct H2;apply (H1 Hcut1)]
102 |right;intro;destruct H1;apply (H Hcut1)]
105 (* Lemma A.3 (Transitivity and Narrowing) *)
107 lemma JS_trans_narrow : \forall Q.
109 (JSubtype G T Q) \to (JSubtype G Q U) \to
110 (JSubtype G T U)) \land
111 (\forall G,H,X,P,M,N.
112 (JSubtype (H @ ((mk_bound true X Q) :: G)) M N) \to
114 (JSubtype (H @ ((mk_bound true X P) :: G)) M N)).
115 apply Typ_len_ind;intros 2;
122 |cut (\forall G,M,N.(JSubtype G M N) \to
124 (G = G2 @ ((mk_bound true X U) :: G1)) \to
125 (JSubtype G1 P U) \to
126 (JSubtype (G2 @ ((mk_bound true X P) :: G1)) M N))
127 [intros;apply (Hcut1 ? ? ? H2 ? ? ? ? ? H3);reflexivity
128 |intros;cut (incl ? (fv_env (G2 @ ((mk_bound true X U)::G1)))
129 (fv_env (G2 @ ((mk_bound true X P)::G1))))
130 [intros;generalize in match H2;generalize in match Hcut1;
131 generalize in match Hcut;generalize in match G2;elim H1
133 [rewrite > H8 in H4;lapply (JS_to_WFT1 ? ? ? H3);
134 apply (WFE_Typ_subst ? ? ? ? ? ? ? H4 Hletin)
135 |rewrite > H8 in H5;apply (WFT_env_incl ? ? H5 ? H7)]
137 [rewrite > H8 in H4;apply (WFE_Typ_subst ? ? ? ? ? ? ? H4);
138 apply (JS_to_WFT1 ? ? ? H3)
139 |rewrite > H8 in H5;apply (H7 ? H5)]
140 |elim (decidable_eq_nat X n)
141 [apply (SA_Trans_TVar ? ? ? P)
142 [rewrite < H10;elim l1
143 [simplify;constructor 1
144 |simplify;elim (decidable_eq_bound (mk_bound true X P) t2)
145 [rewrite < H12;apply in_Base
146 |apply (in_Skip ? ? ? ? ? H12);assumption]]
148 [lapply (H6 ? H7 H8 H9);lapply (JS_to_WFE ? ? ? Hletin);
149 apply (JS_weakening ? ? ? H3 ? Hletin1);unfold;intros;
152 elim (decidable_eq_bound x (mk_bound true X P))
153 [rewrite < H12;apply in_Base
154 |apply (in_Skip ? ? ? ? ? H12);assumption]
155 |simplify;elim (decidable_eq_bound x t2)
156 [rewrite < H13;apply in_Base
157 |apply (in_Skip ? ? ? ? ? H13);assumption]]
158 |lapply (WFE_bound_bound true n t1 U ? ? H4)
159 [apply (JS_to_WFE ? ? ? H5)
160 |rewrite < Hletin;apply (H6 ? H7 H8 H9)
161 |rewrite > H9;rewrite > H10;elim l1;simplify
163 |elim (decidable_eq_bound (mk_bound true n U) t2)
164 [rewrite > H12;apply in_Base
165 |apply (in_Skip ? ? ? ? ? H12);assumption]]]]]
166 |apply (SA_Trans_TVar ? ? ? t1)
168 apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H4);
169 unfold;intro;apply H10;symmetry;assumption
170 |apply (H6 ? H7 H8 H9)]]
172 [apply (H5 ? H8 H9 H10)
173 |apply (H7 ? H8 H9 H10)]
175 [apply (H5 ? H8 H9 H10)
176 |intros;apply (H7 ? ? (mk_bound true X1 t2::l1) H8)
177 [rewrite > H10;cut ((fv_env (l1@(mk_bound true X P::G1))) =
178 (fv_env (l1@(mk_bound true X U::G1))))
179 [unfold;intro;apply H11;rewrite > Hcut2;assumption
181 [simplify;reflexivity
182 |elim t4;simplify;rewrite > H12;reflexivity]]
183 |simplify;apply (incl_nat_cons ? ? ? H9)
184 |simplify;rewrite < H10;reflexivity]]]
185 |cut ((fv_env (G2@(mk_bound true X U::G1))) =
186 (fv_env (G2@(mk_bound true X P::G1))))
187 [rewrite > Hcut1;unfold;intros;assumption
189 [simplify;reflexivity
190 |elim t;simplify;rewrite > H4;reflexivity]]]]]
191 |intros 4;generalize in match H;elim H1
193 [intros;rewrite < H8;apply (SA_Top ? ? H2 H3)
196 |*:intros;destruct H11]
198 |apply (SA_Trans_TVar ? ? ? ? H2);apply (H4 H5 H6)
200 [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Arrow
201 [apply (JS_to_WFT2 ? ? ? H2)
202 |apply (JS_to_WFT1 ? ? ? H4)]
205 |intros;destruct H13;apply SA_Arrow
206 [rewrite > H12 in H2;rewrite < Hcut in H8;
208 [elim Hletin;apply (H15 ? ? ? H8 H2)
209 |apply (t_len_arrow1 t2 t3)]
210 |rewrite > H12 in H4;rewrite < Hcut1 in H10;
212 [elim Hletin;apply (H15 ? ? ? H4 H10)
213 |apply (t_len_arrow2 t2 t3)]]
214 |intros;destruct H13]
216 [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Forall
217 [apply (JS_to_WFT2 ? ? ? H2)
218 |intros;lapply (H4 ? H13);lapply (JS_to_WFT1 ? ? ? Hletin);
219 apply (WFT_env_incl ? ? Hletin1);simplify;unfold;intros;
224 |intros;destruct H13;subst;apply SA_All
226 [elim Hletin;apply (H12 ? ? ? H8 H2)
227 |apply t_len_forall1]
228 |intros;(*destruct H12;*)subst;
229 lapply (H6 (subst_type_nat t5 (TFree X) O))
230 [elim Hletin;apply H13
232 [elim Hletin1;apply (H16 l1 [] X t6);
233 [simplify;apply H4;assumption
235 |apply t_len_forall1]
237 |rewrite < eq_t_len_TFree_subst;
238 apply t_len_forall2]]]]]
241 theorem JS_trans : \forall G,T,U,V.(JSubtype G T U) \to
244 intros;elim JS_trans_narrow;autobatch;
247 theorem JS_narrow : \forall G1,G2,X,P,Q,T,U.
248 (JSubtype (G2 @ (mk_bound true X Q :: G1)) T U) \to
249 (JSubtype G1 P Q) \to
250 (JSubtype (G2 @ (mk_bound true X P :: G1)) T U).
251 intros;elim JS_trans_narrow;autobatch;