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 include "Fsub/util.ma".
17 (*** representation of Fsub types ***)
19 | TVar : nat → Typ (* type var *)
20 | TFree: nat → Typ (* free type name *)
21 | Top : Typ (* maximum type *)
22 | Arrow : Typ → Typ → Typ (* functions *)
23 | Forall : Typ → Typ → Typ. (* universal type *)
25 (* representation of bounds *)
27 record bound : Set ≝ {
28 istype : bool; (* is subtyping bound? *)
29 name : nat ; (* name *)
30 btype : Typ (* type to which the name is bound *)
33 (*** Various kinds of substitution, not all will be used probably ***)
35 (* substitutes i-th dangling index in type T with type U *)
36 let rec subst_type_nat T U i ≝
38 [ TVar n ⇒ match eqb n i with
43 | Arrow T1 T2 ⇒ Arrow (subst_type_nat T1 U i) (subst_type_nat T2 U i)
44 | Forall T1 T2 ⇒ Forall (subst_type_nat T1 U i) (subst_type_nat T2 U (S i)) ].
46 (*** definitions about lists ***)
48 definition fv_env : list bound → list nat ≝
49 λG.(map ? ? (λb.match b with [mk_bound B X T ⇒ X]) G).
56 |Arrow U V ⇒ fv_type U @ fv_type V
57 |Forall U V ⇒ fv_type U @ fv_type V].
59 (*** Type Well-Formedness judgement ***)
61 inductive WFType : list bound → Typ → Prop ≝
62 | WFT_TFree : ∀X,G.in_list ? X (fv_env G) → WFType G (TFree X)
63 | WFT_Top : ∀G.WFType G Top
64 | WFT_Arrow : ∀G,T,U.WFType G T → WFType G U → WFType G (Arrow T U)
65 | WFT_Forall : ∀G,T,U.WFType G T →
67 (¬ (in_list ? X (fv_env G))) →
68 (¬ (in_list ? X (fv_type U))) →
69 (WFType ((mk_bound true X T) :: G)
70 (subst_type_nat U (TFree X) O))) →
71 (WFType G (Forall T U)).
73 (*** Environment Well-Formedness judgement ***)
75 inductive WFEnv : list bound → Prop ≝
76 | WFE_Empty : WFEnv (nil ?)
77 | WFE_cons : ∀B,X,T,G.WFEnv G → ¬ (in_list ? X (fv_env G)) →
78 WFType G T → WFEnv ((mk_bound B X T) :: G).
80 (*** Subtyping judgement ***)
81 inductive JSubtype : list bound → Typ → Typ → Prop ≝
82 | SA_Top : ∀G,T.WFEnv G → WFType G T → JSubtype G T Top
83 | SA_Refl_TVar : ∀G,X.WFEnv G → in_list ? X (fv_env G)
84 → JSubtype G (TFree X) (TFree X)
85 | SA_Trans_TVar : ∀G,X,T,U.in_list ? (mk_bound true X U) G →
86 JSubtype G U T → JSubtype G (TFree X) T
87 | SA_Arrow : ∀G,S1,S2,T1,T2. JSubtype G T1 S1 → JSubtype G S2 T2 →
88 JSubtype G (Arrow S1 S2) (Arrow T1 T2)
89 | SA_All : ∀G,S1,S2,T1,T2. JSubtype G T1 S1 →
90 (∀X.¬ (in_list ? X (fv_env G)) →
91 JSubtype ((mk_bound true X T1) :: G)
92 (subst_type_nat S2 (TFree X) O) (subst_type_nat T2 (TFree X) O)) →
93 JSubtype G (Forall S1 S2) (Forall T1 T2).
95 notation "hvbox(e ⊢ break ta ⊴ break tb)"
96 non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.
97 interpretation "Fsub subtype judgement" 'subjudg e ta tb = (JSubtype e ta tb).
99 notation > "hvbox(\Forall S.T)"
100 non associative with precedence 60 for @{ 'forall $S $T}.
101 notation < "hvbox('All' \sub S. break T)"
102 non associative with precedence 60 for @{ 'forall $S $T}.
103 interpretation "universal type" 'forall S T = (Forall S T).
105 notation "#x" with precedence 79 for @{'tvar $x}.
106 interpretation "bound tvar" 'tvar x = (TVar x).
108 notation "!x" with precedence 79 for @{'tname $x}.
109 interpretation "bound tname" 'tname x = (TFree x).
111 notation "⊤" with precedence 90 for @{'toptype}.
112 interpretation "toptype" 'toptype = Top.
114 notation "hvbox(s break ⇛ t)"
115 right associative with precedence 55 for @{ 'arrow $s $t }.
116 interpretation "arrow type" 'arrow S T = (Arrow S T).
118 notation "hvbox(S [# n ↦ T])"
119 non associative with precedence 80 for @{ 'substvar $S $T $n }.
120 interpretation "subst bound var" 'substvar S T n = (subst_type_nat S T n).
122 notation "hvbox(!X ⊴ T)"
123 non associative with precedence 60 for @{ 'subtypebound $X $T }.
124 interpretation "subtyping bound" 'subtypebound X T = (mk_bound true X T).
126 (****** PROOFS ********)
128 (*** theorems about lists ***)
130 lemma boundinenv_natinfv : ∀x,G.(∃B,T.in_list ? (mk_bound B x T) G) →
131 in_list ? x (fv_env G).
132 intros 2;elim G;decompose
133 [elim (not_in_list_nil ? ? H)
134 |elim (in_list_cons_case ? ? ? ? H1)
135 [rewrite < H2;simplify;apply in_list_head
136 |simplify;apply in_list_cons;apply H;autobatch]]
139 lemma natinfv_boundinenv : ∀x,G.in_list ? x (fv_env G) →
140 ∃B,T.in_list ? (mk_bound B x T) G.
142 [simplify;intro;lapply (not_in_list_nil ? ? H);elim Hletin
144 elim a;simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
145 [rewrite < H2;autobatch
146 |elim (H H2);elim H3;apply ex_intro[apply a1];autobatch]]
149 lemma incl_bound_fv : ∀l1,l2.incl ? l1 l2 → incl ? (fv_env l1) (fv_env l2).
150 intros;unfold in H;unfold;intros;apply boundinenv_natinfv;
151 lapply (natinfv_boundinenv ? ? H1);decompose;autobatch depth=4;
154 lemma incl_cons : ∀x,l1,l2.incl ? l1 l2 → incl nat (x :: l1) (x :: l2).
155 intros.unfold in H.unfold.intros.elim (in_list_cons_case ? ? ? ? H1)
156 [applyS in_list_head|autobatch]
159 lemma WFT_env_incl : ∀G,T.WFType G T →
160 ∀H.incl ? (fv_env G) (fv_env H) → WFType H T.
162 [apply WFT_TFree;unfold in H3;apply (H3 ? H1)
164 |apply WFT_Arrow;autobatch
167 |intros;apply (H4 ? ? H8)
168 [unfold;intro;autobatch
169 |simplify;apply (incl_cons ? ? ? H6)]]]
172 lemma fv_env_extends : ∀H,x,B,C,T,U,G.
173 fv_env (H @ ((mk_bound B x T) :: G)) =
174 fv_env (H @ ((mk_bound C x U) :: G)).
176 [reflexivity|elim a;simplify;rewrite > H1;reflexivity]
179 lemma lookup_env_extends : ∀G,H,B,C,D,T,U,V,x,y.
180 in_list ? (mk_bound D y V) (H @ ((mk_bound C x U) :: G)) → y ≠ x →
181 in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G)).
183 [simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
184 [destruct H3;elim H2;reflexivity
185 |simplify;apply (in_list_cons ? ? ? ? H3);]
186 |simplify in H2;simplify;elim (in_list_cons_case ? ? ? ? H2)
187 [rewrite > H4;apply in_list_head
188 |apply (in_list_cons ? ? ? ? (H1 H4 H3))]]
191 lemma in_FV_subst : ∀x,T,U,n.in_list ? x (fv_type T) →
192 in_list ? x (fv_type (subst_type_nat T U n)).
194 [simplify in H;elim (not_in_list_nil ? ? H)
195 |2,3:simplify;simplify in H;assumption
196 |*:simplify in H2;simplify;elim (in_list_append_to_or_in_list ? ? ? ? H2);
200 (*** lemma on fresh names ***)
202 lemma fresh_name : ∀l:list nat.∃n.¬in_list ? n l.
203 cut (∀l:list nat.∃n.∀m.n ≤ m → ¬ in_list ? m l);intros
204 [lapply (Hcut l);elim Hletin;apply ex_intro;autobatch
206 [apply ex_intro[apply O];intros;unfold;intro;elim (not_in_list_nil ? ? H1)
207 |elim H;apply ex_intro[apply (S (max a1 a))];
209 elim (in_list_cons_case ? ? ? ? H3)
210 [rewrite > H4 in H2;autobatch
212 [apply (H1 m ? H4);autobatch
216 (*** lemmata on well-formedness ***)
218 lemma fv_WFT : ∀T,x,G.WFType G T → in_list ? x (fv_type T) →
219 in_list ? x (fv_env G).
221 [simplify in H2;elim (in_list_cons_case ? ? ? ? H2)
222 [applyS H1|elim (not_in_list_nil ? ? H3)]
223 |simplify in H1;elim (not_in_list_nil ? x H1)
224 |simplify in H5;elim (in_list_append_to_or_in_list ? ? ? ? H5);autobatch
225 |simplify in H5;elim (in_list_append_to_or_in_list ? ? ? ? H5)
227 |elim (fresh_name (fv_type t1 @ fv_env l));
228 cut (¬ in_list ? a (fv_type t1) ∧ ¬ in_list ? a (fv_env l))
229 [elim Hcut;lapply (H4 ? H9 H8)
231 [simplify in Hletin;elim (in_list_cons_case ? ? ? ? Hletin)
234 |intro;apply H8;applyS H6]
236 |split;intro;apply H7;autobatch]]]
239 (*** lemmata relating subtyping and well-formedness ***)
241 lemma JS_to_WFE : ∀G,T,U.G ⊢ T ⊴ U → WFEnv G.
242 intros;elim H;assumption.
245 lemma JS_to_WFT : ∀G,T,U.G ⊢ T ⊴ U → WFType G T ∧ WFType G U.
249 [apply WFT_TFree;(* FIXME! qui bastava autobatch, ma si e` rotto *) apply boundinenv_natinfv;autobatch
251 |decompose;autobatch size=7
253 [apply (WFT_Forall ? ? ? H6);intros;elim (H4 X H7);
254 apply (WFT_env_incl ? ? H9);simplify;unfold;intros;assumption
255 |apply (WFT_Forall ? ? ? H5);intros;elim (H4 X H7);
256 apply (WFT_env_incl ? ? H10);simplify;unfold;intros;assumption]]
259 lemma JS_to_WFT1 : ∀G,T,U.G ⊢ T ⊴ U → WFType G T.
260 intros;elim (JS_to_WFT ? ? ? H);assumption;
263 lemma JS_to_WFT2 : ∀G,T,U.G ⊢ T ⊴ U → WFType G U.
264 intros;elim (JS_to_WFT ? ? ? H);assumption;
267 lemma WFE_Typ_subst : ∀H,x,B,C,T,U,G.
268 WFEnv (H @ ((mk_bound B x T) :: G)) → WFType G U →
269 WFEnv (H @ ((mk_bound C x U) :: G)).
271 [simplify;intros;inversion H1;intros
272 [elim (nil_cons ? G (mk_bound B x T) H3)
273 |destruct H7;autobatch]
274 |intros;simplify;generalize in match H2;elim a;simplify in H4;
277 |destruct H9;apply WFE_cons
279 |rewrite < (fv_env_extends ? x B C T U); assumption
280 |apply (WFT_env_incl ? ? H8);
281 rewrite < (fv_env_extends ? x B C T U);unfold;intros;
285 lemma WFE_bound_bound : ∀B,x,T,U,G.WFEnv G → in_list ? (mk_bound B x T) G →
286 in_list ? (mk_bound B x U) G → T = U.
288 [lapply (not_in_list_nil ? ? H1);elim Hletin
289 |elim (in_list_cons_case ? ? ? ? H6)
290 [destruct H7;destruct;elim (in_list_cons_case ? ? ? ? H5)
291 [destruct H7;reflexivity
292 |elim H7;elim H3;apply boundinenv_natinfv;autobatch]
293 |elim (in_list_cons_case ? ? ? ? H5)
294 [destruct H8;elim H3;apply boundinenv_natinfv;autobatch
298 lemma WFT_to_incl: ∀G,T,U.(∀X.¬in_list ? X (fv_env G) → ¬in_list ? X (fv_type U) →
299 WFType (mk_bound true X T::G) (subst_type_nat U (TFree X) O))
300 → incl ? (fv_type U) (fv_env G).
301 intros;elim (fresh_name (fv_type U@fv_env G));lapply(H a)
302 [unfold;intros;lapply (fv_WFT ? x ? Hletin)
303 [simplify in Hletin1;inversion Hletin1;intros
304 [destruct H4;elim H1;autobatch
305 |destruct H6;assumption]
306 |apply in_FV_subst;assumption]
307 |*:intro;apply H1;autobatch]
310 lemma incl_fv_env: ∀X,G,G1,U,P.
311 incl ? (fv_env (G1@(mk_bound true X U::G)))
312 (fv_env (G1@(mk_bound true X P::G))).
313 intros.rewrite < fv_env_extends.apply incl_A_A.
316 lemma fv_append : ∀G,H.fv_env (G @ H) = fv_env G @ fv_env H.
317 intro;elim G;simplify;autobatch paramodulation;