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/part1a.ma".
17 inductive NTyp : Set \def
18 | TName : nat \to NTyp
20 | NArrow : NTyp \to NTyp \to NTyp
21 | NForall : nat \to NTyp \to NTyp \to NTyp.
23 record nbound : Set \def {
29 let rec encodetype T vars on T ≝
31 [ (TName n) ⇒ match (lookup n vars) with
32 [ true ⇒ (TVar (posn vars n))
35 | (NArrow T1 T2) ⇒ Arrow (encodetype T1 vars) (encodetype T2 vars)
36 | (NForall n2 T1 T2) ⇒ Forall (encodetype T1 vars)
37 (encodetype T2 (n2::vars))].
39 let rec swap_NTyp u v T on T ≝
41 [(TName X) ⇒ (TName (swap u v X))
43 |(NArrow T1 T2) ⇒ (NArrow (swap_NTyp u v T1) (swap_NTyp u v T2))
45 (NForall (swap u v X) (swap_NTyp u v T1) (swap_NTyp u v T2))].
47 let rec swap_Typ u v T on T \def
50 |(TFree X) ⇒ (TFree (swap u v X))
52 |(Arrow T1 T2) ⇒ (Arrow (swap_Typ u v T1) (swap_Typ u v T2))
53 |(Forall T1 T2) ⇒ (Forall (swap_Typ u v T1) (swap_Typ u v T2))].
55 let rec var_NTyp (T:NTyp):list nat\def
59 |NArrow U V ⇒ (var_NTyp U)@(var_NTyp V)
60 |NForall X U V ⇒ X::(var_NTyp U)@(var_NTyp V)].
63 let rec fv_NTyp (T:NTyp):list nat\def
67 |NArrow U V ⇒ (fv_NTyp U)@(fv_NTyp V)
68 |NForall X U V ⇒ (fv_NTyp U)@(remove_nat X (fv_NTyp V))].
71 let rec subst_NTyp_var T X Y \def
73 [TName Z ⇒ match (eqb X Z) with
74 [ true \rArr (TName Y)
75 | false \rArr (TName Z) ]
77 |NArrow U V ⇒ (NArrow (subst_NTyp_var U X Y) (subst_NTyp_var V X Y))
78 |NForall Z U V ⇒ match (eqb X Z) with
79 [ true ⇒ (NForall Z (subst_NTyp_var U X Y) V)
80 | false ⇒ (NForall Z (subst_NTyp_var U X Y)
81 (subst_NTyp_var V X Y))]].
83 definition filter_ntypes : list nbound → list nbound ≝
84 λG.(filter ? G (λB.match B with [mk_nbound B X T ⇒ B])).
86 definition fv_Nenv : list nbound → list nat ≝
89 [mk_nbound (B:bool) (X:nat) (T:NTyp) ⇒ X]) (filter_ntypes G).
91 inductive NWFType : (list nbound) → NTyp → Prop ≝
92 | NWFT_TName : ∀X,G.(X ∈ (fv_Nenv G))
93 → (NWFType G (TName X))
94 | NWFT_Top : ∀G.(NWFType G NTop)
95 | NWFT_Arrow : ∀G,T,U.(NWFType G T) → (NWFType G U) →
96 (NWFType G (NArrow T U))
97 | NWFT_Forall : ∀G,X,T,U.(NWFType G T) →
99 (Y = X ∨ Y ∉ (fv_NTyp U)) →
100 (NWFType ((mk_nbound true Y T) :: G) (swap_NTyp Y X U))) →
101 (NWFType G (NForall X T U)).
103 inductive NWFEnv : (list nbound) → Prop ≝
104 | NWFE_Empty : (NWFEnv (nil ?))
105 | NWFE_cons : ∀B,X,T,G.(NWFEnv G) →
107 (NWFType G T) → (NWFEnv ((mk_nbound B X T) :: G)).
109 inductive NJSubtype : (list nbound) → NTyp → NTyp → Prop ≝
110 | NSA_Top : ∀G,T.(NWFEnv G) → (NWFType G T) → (NJSubtype G T NTop)
111 | NSA_Refl_TVar : ∀G,X.(NWFEnv G)
113 → (NJSubtype G (TName X) (TName X))
114 | NSA_Trans_TVar : ∀G,X,T,U.
115 (mk_nbound true X U) ∈ G →
116 (NJSubtype G U T) → (NJSubtype G (TName X) T)
117 | NSA_Arrow : ∀G,S1,S2,T1,T2.
118 (NJSubtype G T1 S1) → (NJSubtype G S2 T2) →
119 (NJSubtype G (NArrow S1 S2) (NArrow T1 T2))
120 | NSA_All : ∀G,X,Y,S1,S2,T1,T2.
121 (NWFType G (NForall X S1 S2)) →
122 (NWFType G (NForall Y T1 T2)) →
123 (NJSubtype G T1 S1) →
124 (∀Z.Z ∉ (fv_Nenv G) →
125 (Z = X ∨ Z ∉ (fv_NTyp S2)) →
126 (Z = Y ∨ Z ∉ (fv_NTyp T2)) →
127 (NJSubtype ((mk_nbound true Z T1) :: G)
128 (swap_NTyp Z X S2) (swap_NTyp Z Y T2))) →
129 (NJSubtype G (NForall X S1 S2) (NForall Y T1 T2)).
135 | NArrow T1 T2 ⇒ S (max (nt_len T1) (nt_len T2))
136 | NForall X T1 T2 ⇒ S (max (nt_len T1) (nt_len T2)) ].
138 definition encodeenv : list nbound → list bound ≝
141 [ mk_nbound b x T ⇒ mk_bound b x (encodetype T []) ]).
143 lemma eq_fv_Nenv_fv_env : ∀G. fv_Nenv G = fv_env (encodeenv G).
144 intro;elim G;simplify
146 |elim a;elim b;simplify;rewrite < H;reflexivity]
149 lemma decidable_eq_Typ : ∀T,U:Typ.decidable (T = U).
152 [cases (decidable_eq_nat n n1)
154 |right;intro;apply H;destruct H1;reflexivity]
155 |*:right;intro;destruct]
157 [2:cases (decidable_eq_nat n n1)
159 |right;intro;apply H;destruct H1;reflexivity]
160 |*:right;intro;destruct]
163 |*:right;intro;destruct]
168 |right;intro;destruct H4;elim H3;reflexivity]
169 |right;intro;destruct H3;elim H2;reflexivity]
170 |*:right;intro;destruct]
175 |right;intro;destruct H4;elim H3;reflexivity]
176 |right;intro;destruct H3;elim H2;reflexivity]
177 |*:right;intro;destruct]]
180 lemma decidable_eq_bound : ∀b,c:bound.decidable (b = c).
181 intros;cases b;cases c;cases (bool_to_decidable_eq b1 b2)
182 [cases (decidable_eq_nat n n1)
183 [cases (decidable_eq_Typ t t1)
185 |right;intro;destruct H3;elim H2;reflexivity]
186 |right;intro;destruct H2;elim H1;reflexivity]
187 |right;intro;destruct H1;elim H;reflexivity]
190 lemma in_Nenv_to_in_env: ∀l,n,n2.(mk_nbound true n n2) ∈ l →
191 (mk_bound true n (encodetype n2 [])) ∈ (encodeenv l).
193 [elim (not_in_list_nil ? ? H)
194 |inversion H1;intros;destruct;
195 [simplify;apply in_list_head
196 |elim a;simplify;apply in_list_cons;apply H;assumption]]
199 lemma NTyp_len_ind : \forall P:NTyp \to Prop.
200 (\forall U.(\forall V.((nt_len V) < (nt_len U)) \to (P V))
204 cut (∀m,n.max m n = m ∨ max m n = n) as Hmax
205 [|intros;unfold max;cases (leb m n);simplify
208 cut (∀S.nt_len S ≤ nt_len T → P S)
210 [1,2:simplify in H1;apply H;intros;lapply (trans_le ??? H2 H1);
211 elim (not_le_Sn_O ? Hletin)
212 |simplify in H3;apply H;intros;lapply (trans_le ??? H4 H3);
213 lapply (le_S_S_to_le ?? Hletin) as H5;clear Hletin;
214 cases (Hmax (nt_len n) (nt_len n1));rewrite > H6 in H5
216 |apply H2;assumption]
217 |simplify in H3;apply H;intros;lapply (trans_le ??? H4 H3);
218 lapply (le_S_S_to_le ?? Hletin) as H5;clear Hletin;
219 cases (Hmax (nt_len n1) (nt_len n2));rewrite > H6 in H5
221 |apply H2;assumption]]]
222 apply Hcut;apply le_n;
225 (*** even with this lemma, the following autobatch doesn't work properly
226 lemma aaa : ∀x,y.S x ≤ y → x < y.
231 lemma ntlen_arrow1 : ∀T1,T2.(nt_len T1) < (nt_len (NArrow T1 T2)).
233 [1,2:simplify;(*** autobatch *)apply le_S_S;autobatch
234 |*:whd in ⊢ (??%);apply le_S_S;apply le_m_max_m_n]
237 lemma ntlen_arrow2 : ∀T1,T2.(nt_len T2) < (nt_len (NArrow T1 T2)).
239 [1,2:simplify;autobatch
240 |*:whd in ⊢ (??%);apply le_S_S;apply le_n_max_m_n]
243 lemma ntlen_forall1 : ∀X,T1,T2.(nt_len T1) < (nt_len (NForall X T1 T2)).
245 [1,2:simplify;(*** autobatch *)apply le_S_S;autobatch
246 |*:whd in ⊢ (??%);apply le_S_S;apply le_m_max_m_n]
249 lemma ntlen_forall2 : ∀X,T1,T2.(nt_len T2) < (nt_len (NForall X T1 T2)).
251 [1,2:simplify;autobatch
252 |*:whd in ⊢ (??%);apply le_S_S;apply le_n_max_m_n]
255 lemma eq_ntlen_swap : ∀X,Y,T.nt_len T = nt_len (swap_NTyp X Y T).
256 intros;elim T;simplify
258 |*:autobatch paramodulation]
261 lemma fv_encode : ∀T,l1,l2.
262 (∀x.x ∈ (fv_NTyp T) →
263 (lookup x l1 = lookup x l2 ∧
264 (lookup x l1 = true → posn l1 x = posn l2 x))) →
265 (encodetype T l1 = encodetype T l2).
267 [simplify in H;elim (H n)
268 [simplify;rewrite < H1;elim (lookup n l1) in H2;simplify
269 [rewrite > H2;autobatch
272 |simplify;reflexivity
273 |simplify;rewrite > (H l1 l2)
274 [rewrite > (H1 l1 l2)
276 |intros;apply H2;simplify;apply in_list_to_in_list_append_r;autobatch]
277 |intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]
278 |simplify;rewrite > (H l1 l2)
279 [rewrite > (H1 (n::l1) (n::l2))
281 |intros;elim (decidable_eq_nat x n)
282 [simplify;rewrite > (eq_to_eqb_true ? ? H4);simplify;split
283 [reflexivity|intro;reflexivity]
284 |elim (H2 x);simplify
286 [rewrite < H5;reflexivity
288 [simplify;reflexivity
289 |simplify in H7;rewrite < (H6 H7);reflexivity]]
290 |apply in_list_to_in_list_append_r;
291 apply (in_remove ? ? ? H4);assumption]]]
292 |intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]]
295 theorem encode_swap : ∀a,x,T,vars.
296 (a ∈ (fv_NTyp T) → a ∈ vars) →
299 encodetype (swap_NTyp a x T) (swap_list a x vars).
301 [elim (decidable_eq_nat n x)
302 [rewrite > H2;simplify in match (swap_NTyp ? ? ?);rewrite > swap_right;
303 simplify;lapply (lookup_swap a x x vars);rewrite > swap_right in Hletin;
305 rewrite > (in_lookup ?? H1);simplify;lapply (posn_swap a x x vars);
306 rewrite > swap_right in Hletin1;rewrite < Hletin1;reflexivity
307 |elim (decidable_eq_nat n a);
308 [rewrite < H3;simplify;rewrite < posn_swap;rewrite > lookup_swap;
309 rewrite < H3 in H;simplify in H;rewrite > in_lookup;
310 [simplify;reflexivity
311 |apply H;apply in_list_head]
312 |simplify in ⊢ (? ? ? (? % ?));rewrite > swap_other;
313 [apply (fv_encode ? vars (swap_list a x vars));intros;
314 simplify in H4;cut (x1 = n)
315 [rewrite > Hcut;elim vars;simplify
316 [split [reflexivity|intro;reflexivity]
318 (a1 = a ∨a1 = x ∨ (a1 ≠ a ∧ a1 ≠ x))
319 [|elim (decidable_eq_nat a1 a)
320 [left;left;assumption
321 |elim (decidable_eq_nat a1 x)
322 [left;right;assumption
323 |right;split;assumption]]]
325 [rewrite > H10;rewrite > swap_left;
326 rewrite > (not_eq_to_eqb_false ? ? H2);
327 rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
330 |intro;rewrite < (H7 H5);reflexivity]
331 |rewrite > H10;rewrite > swap_right;
332 rewrite > (not_eq_to_eqb_false ? ? H2);
333 rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
336 |intro;rewrite < (H7 H5);reflexivity]
337 |rewrite > (swap_other a x a1)
341 [simplify;reflexivity
342 |simplify in H5;rewrite < (H7 H5);reflexivity]]
344 |inversion H4;intros;destruct;
346 |elim (not_in_list_nil ? ? H5)]]
348 |simplify;reflexivity
349 |simplify;simplify in H2;rewrite < H
352 |intro;apply H2;apply in_list_to_in_list_append_r;autobatch
354 |intro;apply H2;apply in_list_to_in_list_append_l;autobatch
356 |simplify;simplify in H2;rewrite < H
357 [elim (decidable_eq_nat a n)
358 [rewrite < (H1 (n::vars));
360 |intro;rewrite > H4;apply in_list_head
362 |rewrite < (H1 (n::vars));
364 |intro;apply in_list_cons;apply H2;apply in_list_to_in_list_append_r;
365 apply (in_remove ? ? ? H4 H5)
367 |intro;apply H2;apply in_list_to_in_list_append_l;assumption
371 lemma encode_swap2 : ∀a:nat.∀x:nat.∀T:NTyp.
374 → encodetype T vars=encodetype (swap_NTyp a x T) (swap_list a x vars).
375 intros;apply (encode_swap ? ? ? ? ? H1);intro;elim (H H2);
378 lemma incl_fv_var : \forall T.(fv_NTyp T) ⊆ (var_NTyp T).
379 intro;elim T;simplify;unfold;intros
381 |elim (in_list_append_to_or_in_list ? ? ? ? H2);autobatch
382 |elim (decidable_eq_nat x n)
383 [rewrite > H3;apply in_list_head
384 |apply in_list_cons;elim (in_list_append_to_or_in_list ? ? ? ? H2)
386 |apply in_list_to_in_list_append_r;elim (remove_inlist ? ? ? H4);
390 lemma fv_encode2 : ∀T,l1,l2.
391 (∀x.x ∈ (fv_NTyp T) →
392 (lookup x l1 = lookup x l2 ∧
393 posn l1 x = posn l2 x)) →
394 (encodetype T l1 = encodetype T l2).
395 intros;apply fv_encode;intros;elim (H ? H1);split
396 [assumption|intro;assumption]
399 lemma inlist_fv_swap : ∀x,y,b,T.
400 b ∉ (y::var_NTyp T) →
401 x ∈ (fv_NTyp (swap_NTyp b y T)) →
402 x ≠ y ∧ (x = b ∨ x ∈ (fv_NTyp T)).
404 [simplify in H;simplify;simplify in H1;elim (decidable_eq_nat y n)
405 [rewrite > H2 in H1;rewrite > swap_right in H1;inversion H1;intros;destruct;
407 [unfold;intro;apply H;rewrite > H2;apply in_list_head
409 |elim (not_in_list_nil ? ? H3)]
410 |elim (decidable_eq_nat b n)
411 [rewrite > H3 in H;elim H;autobatch
412 |rewrite > swap_other in H1
414 [inversion H1;intros;destruct;
415 [intro;apply H2;symmetry;assumption
416 |elim (not_in_list_nil ? ? H4)]
418 |*:intro;autobatch]]]
419 |simplify in H1;elim (not_in_list_nil ? ? H1)
420 |simplify;simplify in H3;simplify in H2;elim (in_list_append_to_or_in_list ? ? ? ? H3)
426 |right;apply in_list_to_in_list_append_l;assumption]]
427 |intro;apply H2;inversion H5;intros;destruct;
429 |apply in_list_cons;apply in_list_to_in_list_append_l;assumption]
436 |right;apply in_list_to_in_list_append_r;assumption]]
437 |intro;apply H2;elim (in_list_append_to_or_in_list ?? [y] (var_NTyp n1) H5)
438 [lapply (in_list_singleton_to_eq ??? H6);applyS in_list_head
441 |simplify;simplify in H3;simplify in H2;elim (in_list_append_to_or_in_list ? ? ? ? H3)
448 |intro;apply H2;inversion H5;intros;destruct;
450 |apply in_list_cons;elim (decidable_eq_nat b n);autobatch]
457 |right;apply in_list_to_in_list_append_r;apply inlist_remove
459 |intro;elim (remove_inlist ? ? ? H4);apply H10;rewrite > swap_other
461 |intro;rewrite > H8 in H7;rewrite > H11 in H7;apply H2;destruct;autobatch
462 |destruct;assumption]]]]
463 |intro;apply H2;inversion H5;intros;destruct;
465 |apply in_list_cons;change in ⊢ (???%) with ((n::var_NTyp n1)@var_NTyp n2);
466 elim (n::var_NTyp n1);simplify
468 |elim (decidable_eq_nat b a);autobatch]]
469 |elim(remove_inlist ? ? ? H4);assumption]]]
472 lemma inlist_fv_swap_r : ∀x,y,b,T.
473 (b ∉ (y::var_NTyp T)) →
474 ((x = b ∧ y ∈ (fv_NTyp T)) ∨
475 (x ≠ y ∧ x ∈ (fv_NTyp T))) →
476 x ∈ (fv_NTyp (swap_NTyp b y T)).
478 [simplify;simplify in H;simplify in H1;cut (b ≠ n)
481 [rewrite > Hcut1;rewrite > swap_right;rewrite > H3;apply in_list_head
482 |inversion H4;intros;destruct;
484 |elim (not_in_list_nil ? ? H5)]]
485 |elim H2;inversion H4;intros;destruct;
486 [rewrite > (swap_other b y x)
490 |elim (not_in_list_nil ? ? H5)]]
491 |intro;apply H;autobatch]
492 |simplify in H1;decompose;elim (not_in_list_nil ? ? H3)
493 |simplify;simplify in H3;cut (\lnot (in_list ? b (y::var_NTyp n1)))
494 [cut (¬(in_list ? b (y::var_NTyp n)))
496 [elim (in_list_append_to_or_in_list ? ? ? ? H5)
497 [apply in_list_to_in_list_append_l;apply H
499 |left;split;assumption]
500 |apply in_list_to_in_list_append_r;apply H1
502 |left;split;assumption]]
503 |elim (in_list_append_to_or_in_list ? ? ? ? H5)
504 [apply in_list_to_in_list_append_l;apply H;
506 |right;split;assumption]
507 |apply in_list_to_in_list_append_r;apply H1
509 |right;split;assumption]]]
510 |intro;apply H2;inversion H4;intros;destruct;simplify;autobatch]
511 |intro;apply H2;inversion H4;intros;destruct;simplify;autobatch]
512 |simplify;simplify in H3;cut (¬(in_list ? b (y::var_NTyp n1)))
513 [cut (¬(in_list ? b (y::var_NTyp n2)))
515 [elim (in_list_append_to_or_in_list ? ? ? ? H5)
516 [apply in_list_to_in_list_append_l;apply H
518 |left;split;assumption]
519 |apply in_list_to_in_list_append_r;apply inlist_remove
523 [assumption|elim (remove_inlist ? ? ? H4);assumption]]
524 |elim (remove_inlist ? ? ? H4);elim (decidable_eq_nat b n)
525 [rewrite > H8;rewrite > swap_left;intro;apply H7;autobatch paramodulation
526 |rewrite > swap_other
527 [rewrite > H3;assumption
528 |intro;apply H8;symmetry;assumption
529 |intro;apply H7;symmetry;assumption]]]]
530 |elim (in_list_append_to_or_in_list ? ? ? ? H5)
531 [apply in_list_to_in_list_append_l;apply H
533 |right;split;assumption]
534 |apply in_list_to_in_list_append_r;apply inlist_remove
538 [assumption|elim (remove_inlist ? ? ? H4);assumption]]
539 |elim (decidable_eq_nat b n)
540 [rewrite > H6;rewrite > swap_left;assumption
541 |elim (decidable_eq_nat y n)
542 [rewrite > H7;rewrite > swap_right;intro;apply Hcut1;
543 apply in_list_cons;apply incl_fv_var;elim (remove_inlist ? ? ? H4);
544 rewrite < H8;assumption
545 |rewrite > (swap_other b y n)
546 [elim (remove_inlist ? ? ? H4);assumption
547 |intro;apply H6;symmetry;assumption
548 |intro;apply H7;symmetry;assumption]]]]]]
549 |intro;apply H2;inversion H4;simplify;intros;destruct;
551 |change in ⊢ (???%) with ((y::n::var_NTyp n1)@var_NTyp n2);autobatch]]
552 |intro;apply H2;inversion H4;simplify;intros;destruct;autobatch depth=4]]
555 lemma encode_append : ∀T,U,n,l.length ? l ≤ n →
556 subst_type_nat (encodetype T l) U n = encodetype T l.
557 intros 2;elim T;simplify
558 [elim (bool_to_decidable_eq (lookup n l) true)
559 [rewrite > H1;simplify;lapply (lookup_in ? ? H1);
560 lapply (posn_length ? ? Hletin);cut (posn l n ≠ n1)
561 [rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;reflexivity
562 |intro;rewrite > H2 in Hletin1;unfold in Hletin1;autobatch]
563 |cut (lookup n l = false)
564 [rewrite > Hcut;reflexivity
565 |elim (lookup n l) in H1;
566 [elim H1;reflexivity|reflexivity]]]
569 |rewrite > (H ? ? H2);rewrite > H1;
571 |simplify;autobatch]]
574 lemma encode_subst_simple : ∀X,T,l.
575 encodetype T l = subst_type_nat (encodetype T (l@[X])) (TFree X) (length ? l).
576 intros 2;elim T;simplify
577 [cut (lookup n l = true → posn l n = posn (l@[X]) n)
578 [elim (bool_to_decidable_eq (lookup n l) true) in Hcut
579 [cut (lookup n (l@[X]) = true)
580 [rewrite > H;rewrite > Hcut;simplify;
581 cut (eqb (posn (l@[X]) n) (length nat l) = false)
582 [rewrite > Hcut1;simplify;rewrite < (H1 H);reflexivity
584 [simplify;intro;destruct
585 |intros 2;simplify;elim (eqb n a);simplify
587 |simplify in H3;apply (H H2)]]]
589 [simplify in H;destruct
590 |generalize in match H2;simplify;elim (eqb n a) 0;simplify;intro
593 |cut (lookup n l = false)
594 [elim (decidable_eq_nat n X)
595 [rewrite > Hcut;rewrite > H2;cut (lookup X (l@[X]) = true)
596 [rewrite > Hcut1;simplify;cut (eqb (posn (l@[X]) X) (length nat l) = true)
597 [rewrite > Hcut2;simplify;reflexivity
599 [intros;simplify;rewrite > eqb_n_n;simplify;reflexivity
600 |simplify;intros 2;rewrite > H2;elim (eqb X a);simplify in H4
604 [rewrite > eqb_n_n;reflexivity
605 |elim (eqb X a);simplify
608 |cut (lookup n l = lookup n (l@[X]))
609 [rewrite < Hcut1;rewrite > Hcut;simplify;reflexivity
611 [rewrite > (not_eq_to_eqb_false ? ? H2);simplify;reflexivity
612 |elim (eqb n a);simplify
615 |elim (lookup n l) in H
616 [elim H;reflexivity|reflexivity]]]
618 [intro;simplify in H;destruct
619 |simplify;intros 2;elim (eqb n a);simplify
621 |simplify in H1;rewrite < (H H1);reflexivity]]]
623 |rewrite < H;rewrite < H1;reflexivity
624 |rewrite < H;rewrite < (associative_append ? [n] l [X]);
625 rewrite < (H1 ([n]@l));reflexivity]
628 lemma encode_subst : ∀T,X,Y,l.X ∉ l → Y ∉ l →
629 (X ∈ (fv_NTyp T) → X = Y) →
630 encodetype (swap_NTyp X Y T) l =
631 subst_type_nat (encodetype T (l@[Y])) (TFree X) (length ? l).
632 apply NTyp_len_ind;intro;elim U
633 [elim (decidable_eq_nat n X)
634 [rewrite > H4 in H3;rewrite > H4;rewrite > H3
635 [simplify in ⊢ (?? (?%?) ?);rewrite > swap_same;
636 cut (lookup Y (l@[Y]) = true)
637 [simplify;rewrite > Hcut;rewrite > (not_nat_in_to_lookup_false ? ? H2);
638 simplify;cut (posn (l@[Y]) Y = length ? l)
639 [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
640 |elim l in H2;simplify
641 [rewrite > eqb_n_n;reflexivity
642 |elim (decidable_eq_nat Y a)
643 [elim H5;rewrite > H6;apply in_list_head
644 |rewrite > (not_eq_to_eqb_false ? ? H6);simplify;rewrite < H2
648 [rewrite > eqb_n_n;reflexivity
649 |rewrite > H5;elim (eqb Y a);reflexivity]]
650 |simplify;apply in_list_head]
651 |elim (decidable_eq_nat Y n);
652 [rewrite < H5;simplify;rewrite > swap_right;
653 rewrite > (not_nat_in_to_lookup_false ? ? H1);
654 cut (lookup Y (l@[Y]) = true)
655 [rewrite > Hcut;simplify;cut (posn (l@[Y]) Y = length ? l)
656 [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
657 |elim l in H2;simplify
658 [rewrite > eqb_n_n;reflexivity
659 |elim (decidable_eq_nat Y a)
660 [elim H6;applyS in_list_head
661 |rewrite > (not_eq_to_eqb_false ? ? H7);simplify;rewrite < H2
665 [rewrite > eqb_n_n;reflexivity
666 |elim (eqb Y a);simplify;autobatch]]
667 |simplify;rewrite > (swap_other X Y n)
668 [cut (lookup n l = lookup n (l@[Y]) ∧
669 (lookup n l = true → posn l n = posn (l@[Y]) n))
670 [elim Hcut;rewrite > H6;elim (lookup n (l@[Y])) in H7 H6;simplify;
671 [rewrite < H7;elim l in H6
672 [simplify in H6;destruct
673 |elim (decidable_eq_nat n a);simplify
674 [rewrite > (eq_to_eqb_true ? ? H9);reflexivity
675 |rewrite > (not_eq_to_eqb_false ? ? H9);
676 simplify;elim (eqb (posn l1 n) (length nat l1)) in H6
677 [simplify in H8;simplify in H6;
678 rewrite > (not_eq_to_eqb_false ? ? H9) in H8;
679 simplify in H8;lapply (H6 H8);destruct
684 [simplify;cut (n ≠ Y)
685 [rewrite > (not_eq_to_eqb_false ? ? Hcut);reflexivity
686 |intro;apply H5;symmetry;assumption]
687 |intro;simplify in H6;destruct H6
688 |elim H6;simplify;rewrite < H7;reflexivity
689 |simplify;elim (eqb n a);simplify
691 |simplify in H7;elim H6;rewrite < (H9 H7);reflexivity]]]
693 |intro;apply H5;symmetry;assumption]]]
695 |simplify;rewrite < (H2 n ? ? ? ? H3 H4)
696 [rewrite < (H2 n1 ? ? ? ? H3 H4);
698 |intro;apply H5;simplify;autobatch]
700 |intro;apply H5;simplify;autobatch]
701 |simplify;rewrite < (H2 n1 ? ? ? ? H3 H4)
702 [cut (l = swap_list X Y l)
703 [|elim l in H3 H4;simplify
705 |elim (decidable_eq_nat a X)
706 [elim H4;applyS in_list_head
707 |elim (decidable_eq_nat a Y)
708 [elim H6;applyS in_list_head
709 |rewrite > (swap_other X Y a)
714 elim (decidable_eq_nat n Y)
716 rewrite > (fv_encode (swap_NTyp X Y n2) (swap X Y Y::l) (swap_list X Y (Y::l)));
717 [rewrite < (encode_swap X Y n2);
718 [rewrite < (fv_encode ? (Y::l) (Y::l@[Y]))
719 [rewrite > encode_append;
721 |simplify;constructor 1]
722 |intros;simplify;elim (decidable_eq_nat x Y)
723 [rewrite > (eq_to_eqb_true ? ? H8);simplify;split
724 [reflexivity|intro;reflexivity]
725 |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;elim l;simplify
726 [rewrite > (not_eq_to_eqb_false ? ? H8);simplify;split
727 [reflexivity|intro;destruct H9]
728 |elim (eqb x a);simplify
729 [split [reflexivity|intro;reflexivity]
732 |intro;rewrite < (H11 H12);reflexivity]]]]]
733 |intro;elim (decidable_eq_nat X Y)
734 [rewrite > H8;apply in_list_head
735 |elim H8;apply H5;simplify;apply in_list_to_in_list_append_r;
736 rewrite > H6;apply (in_remove ? ? ? H8 H7)]
738 |intros;simplify;rewrite > swap_right;rewrite < Hcut;
739 split [reflexivity|intro;reflexivity]]
740 |elim (decidable_eq_nat n X)
742 rewrite > (fv_encode (swap_NTyp X Y n2) (swap X Y X::l) (swap_list X Y (X::l)))
743 [rewrite > (encode_swap X Y n2);
745 cut (swap X Y X::swap_list X Y (l@[Y]) =
746 (swap X Y X::swap_list X Y l)@[X])
747 [rewrite > Hcut1;cut (S (length ? l) = (length ? (swap X Y X::swap_list X Y l)))
749 rewrite < (encode_subst_simple X (swap_NTyp X Y n2) (swap X Y X::swap_list X Y l));
753 |simplify;rewrite < H8;reflexivity]]
754 |simplify;elim l;simplify
755 [rewrite > swap_right;reflexivity
756 |destruct;rewrite > Hcut1;reflexivity]]
757 |intro;apply in_list_head
758 |apply in_list_cons;elim l;simplify;autobatch]
759 |intros;simplify;rewrite < Hcut;
760 split [reflexivity|intro;reflexivity]]
761 |rewrite > (swap_other X Y n)
762 [rewrite < (associative_append ? [n] l [Y]);
763 cut (S (length nat l) = length nat (n::l)) [|reflexivity]
764 rewrite > Hcut1;rewrite < (H2 n2);
767 |intro;apply H7;inversion H8;intros;destruct;
770 |intro;apply H6;inversion H8;intros;destruct;
773 |intro;apply H5;simplify;apply in_list_to_in_list_append_r;
774 apply (in_remove ? ? ? ? H8);intro;apply H7;symmetry;assumption]
777 |intro;apply H5;simplify;autobatch]]
780 lemma in_fvNTyp_in_fvNenv : ∀G,T.(NWFType G T) → (fv_NTyp T) ⊆ (fv_Nenv G).
781 intros;elim H;simplify;unfold;intros;
782 [inversion H2;intros;destruct;
784 |elim (not_in_list_nil ? ? H3)]
785 |elim (not_in_list_nil ? ? H1)
786 |elim (in_list_append_to_or_in_list ? ? ? ? H5)
787 [apply (H2 ? H6)|apply (H4 ? H6)]
788 |elim (in_list_append_to_or_in_list ? ? ? ? H5)
790 |elim (fresh_name (x::fv_Nenv l@var_NTyp n2));lapply (H4 a)
792 [elim Hcut;lapply (Hletin x)
793 [simplify in Hletin1;inversion Hletin1;intros;destruct;
796 |generalize in match H6;generalize in match H7;elim n2
797 [simplify in H11;elim (decidable_eq_nat n n3)
798 [rewrite > (eq_to_eqb_true ? ? H12) in H11;simplify in H11;
799 elim (not_in_list_nil ? ? H11)
800 |rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
801 simplify in H11;inversion H11;intros
802 [destruct;simplify;rewrite > swap_other
804 |intro;apply H8;rewrite > H13;reflexivity
805 |intro;apply H9;rewrite > H13;reflexivity]
806 |destruct;elim (not_in_list_nil ? ? H13)]]
807 |simplify in H11;elim (not_in_list_nil ? ? H11)
808 |simplify in H13;simplify;elim (remove_inlist ? ? ? H13);
809 elim (in_list_append_to_or_in_list ? ? ? ? H14)
810 [apply in_list_to_in_list_append_l;apply H10
811 [intro;apply H12;simplify;
812 rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4));
813 elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3) H17);
815 |apply (in_remove ? ? ? H15 H16)]
816 |apply in_list_to_in_list_append_r;apply H11
817 [intro;apply H12;simplify;
818 rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4));
819 elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n4) H17);
821 |apply (in_remove ? ? ? H15 H16)]]
822 |simplify;simplify in H13;elim (remove_inlist ? ? ? H13);
823 elim (in_list_append_to_or_in_list ???? H14)
824 [apply in_list_to_in_list_append_l;apply H10;
825 [rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n4));
826 intro;apply H12;simplify;
827 rewrite < (associative_append ? [x] (fv_Nenv l) (n3::var_NTyp n4@var_NTyp n5));
828 elim (in_list_append_to_or_in_list ???? H17);autobatch depth=4
830 |apply in_list_to_in_list_append_r;apply in_remove;
831 [elim (remove_inlist ? ? ? H16);intro;apply H18;
832 elim (swap_case a n n3)
834 [elim H8;symmetry;rewrite < H21;assumption
835 |elim H9;rewrite < H21;assumption]
836 |rewrite < H20;assumption]
838 [rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n5));
839 intro;apply H12;simplify;
840 rewrite < (associative_append ? [x] (fv_Nenv l) (n3::var_NTyp n4 @ var_NTyp n5));
841 elim (in_list_append_to_or_in_list ???? H17);autobatch depth=4
842 |elim (remove_inlist ? ? ? H16);autobatch]]]]]
844 [intro;apply H7;rewrite > H8;apply in_list_head
845 |elim (remove_inlist ? ? ? H6);assumption]]
846 |intro;autobatch depth=4
847 |right;intro;autobatch depth=5]]]
850 lemma fv_NTyp_fv_Typ : ∀T,X,l.X ∈ (fv_NTyp T) → X ∉ l →
851 X ∈ (fv_type (encodetype T l)).
852 intros 2;elim T;simplify
853 [simplify in H;cut (X = n)
854 [rewrite < Hcut;generalize in match (lookup_in X l);elim (lookup X l)
855 [elim H1;apply H2;reflexivity
856 |simplify;apply in_list_head]
857 |inversion H;intros;destruct;
859 |elim (not_in_list_nil ? ? H2)]]
860 |simplify in H;elim (not_in_list_nil ? ? H)
861 |simplify in H2;elim (in_list_append_to_or_in_list ? ? ? ? H2);autobatch
863 elim (in_list_append_to_or_in_list ? ? ? ? H2)
865 |apply in_list_to_in_list_append_r;
866 elim (remove_inlist ? ? ? H4);apply (H1 ? H5);intro;apply H6;
867 inversion H7;intros;destruct;
872 lemma adeq_WFT : ∀G,T.NWFType G T → WFType (encodeenv G) (encodetype T []).
873 intros;elim H;simplify
874 [apply WFT_TFree;rewrite < eq_fv_Nenv_fv_env;assumption
878 |intros;rewrite < (encode_subst n2 X n []);
879 [simplify in H4;apply H4
880 [rewrite > (eq_fv_Nenv_fv_env l);assumption
881 |elim (decidable_eq_nat X n)
883 |right;intro;apply H6;apply (fv_NTyp_fv_Typ ? ? ? H8);intro;
884 apply H7;inversion H9;intros;destruct;
886 |elim (not_in_list_nil ? ? H10)]]]
887 |4:intro;elim (decidable_eq_nat X n)
889 |elim H6;cut (¬(in_list ? X [n]))
890 [generalize in match Hcut;generalize in match [n];
891 generalize in match H7;elim n2
892 [simplify in H9;generalize in match H9;intro;inversion H9;intros;destruct;
893 [simplify;generalize in match (lookup_in X l1);elim (lookup X l1)
894 [elim H10;apply H12;reflexivity
895 |simplify;apply in_list_head]
896 |elim (not_in_list_nil ? ? H12)]
897 |simplify in H9;elim (not_in_list_nil ? ? H9)
898 |simplify;simplify in H11;
899 elim (in_list_append_to_or_in_list ? ? ? ? H11);autobatch
900 |simplify;simplify in H11;elim (in_list_append_to_or_in_list ? ? ? ? H11);
902 |elim (remove_inlist ? ? ? H13);apply in_list_to_in_list_append_r;
903 apply (H10 H14);intro;inversion H16;intros;destruct;
904 [elim H15;reflexivity
905 |elim H12;assumption]]]
906 |intro;elim H8;inversion H9;intros;destruct;
908 |elim (not_in_list_nil ? ? H10)]]]
909 |*:apply not_in_list_nil]]]
912 lemma not_in_list_encodetype : \forall T,l,x.x ∈ l \to
913 \lnot x ∈ (fv_type (encodetype T l)).
914 intro;elim T;simplify
915 [apply (bool_elim ? (lookup n l));intro;simplify
916 [apply not_in_list_nil
917 |intro;inversion H2;intros;destruct;
918 [rewrite > (in_lookup ? ? H) in H1;destruct H1
919 |apply (not_in_list_nil ? ? H3)]]
920 |apply not_in_list_nil
921 |intro;elim (in_list_append_to_or_in_list ???? H3);autobatch
922 |intro;elim (in_list_append_to_or_in_list ???? H3);
924 |apply (H1 (n::l) x ? H4);apply in_list_cons;assumption]]
927 lemma incl_fv_encode_fv : \forall T,l.(fv_type (encodetype T l)) ⊆ (fv_NTyp T).
928 intro;elim T;simplify;unfold;
929 [intro;elim (lookup n l);simplify in H
930 [elim (not_in_list_nil ? ? H)
932 |intros;elim (not_in_list_nil ? ? H)
933 |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2);autobatch
934 |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
936 |apply in_list_to_in_list_append_r;apply in_remove
937 [intro;apply (not_in_list_encodetype n2 (n::l) x);autobatch;
941 lemma adeq_WFT2 : ∀G1,T1.WFType G1 T1 →
942 ∀G2,T2.G1 = encodeenv G2 → T1 = encodetype T2 [] →
945 [rewrite > H2 in H1;rewrite < eq_fv_Nenv_fv_env in H1;
948 [simplify in H3;destruct;reflexivity
949 |simplify in H3;destruct H3
950 |simplify in H5;destruct H5
951 |simplify in H5;destruct H5]]
952 rewrite > Hcut;apply NWFT_TName;assumption
955 [simplify in H2;destruct H2
957 |simplify in H4;destruct H4
958 |simplify in H4;destruct H4]]
959 rewrite > Hcut;apply NWFT_Top;
960 |cut (∃U,V.T2 = (NArrow U V))
962 [1,2:simplify in H6;destruct H6
964 |simplify in H8;destruct H8]]
965 elim Hcut;elim H7;rewrite > H8 in H6;simplify in H6;destruct;autobatch size=7
966 |cut (\exists Z,U,V.T2 = NForall Z U V)
968 [1,2:simplify in H6;destruct
969 |simplify in H8;destruct
970 |autobatch depth=4]]]
971 elim Hcut;elim H7;elim H8;clear Hcut H7 H8;rewrite > H9;
972 rewrite > H9 in H6;simplify in H6;destruct;apply NWFT_Forall
975 [rewrite > H7;cut (swap_NTyp a a a2 = a2)
976 [|elim a2;simplify;autobatch]
977 rewrite > Hcut;apply (H4 Y)
978 [4:rewrite > H7;(*** autobatch *)
979 change in ⊢ (? ? (? (? ? %) ? ?) ?) with ([]@[a]);
980 symmetry;rewrite < Hcut in ⊢ (??%?);
981 change in ⊢ (? ? ? (? ? ? %)) with (length nat []);autobatch
986 |symmetry;apply (encode_subst a2 Y a []);
987 [3:intro;elim (H7 H8)
991 lemma adeq_WFE : ∀G.NWFEnv G → WFEnv (encodeenv G).
992 intros;elim H;simplify;autobatch;
995 lemma NWFT_env_incl : ∀G,T.NWFType G T → ∀H.(fv_Nenv G) ⊆ (fv_Nenv H)
1000 |intros;apply (H4 ? ? H8);
1001 [intro;apply H7;apply (H6 ? H9)
1002 |unfold;intros;simplify;simplify in H9;inversion H9;intros;
1005 |apply in_list_cons;apply H6;apply H10]]]
1009 lemma NJSubtype_to_NWFT : ∀G,T,U.NJSubtype G T U → NWFType G T ∧ NWFType G U.
1011 [1,2:split;autobatch
1013 [apply NWFT_TName;elim l in H1
1014 [elim (not_in_list_nil ? ? H1)
1015 |inversion H6;intros;destruct;
1017 |elim a;simplify;elim b;simplify;try apply in_list_cons;
1020 |elim H2;elim H4;split;autobatch
1024 theorem adequacy : ∀G,T,U.NJSubtype G T U →
1025 JSubtype (encodeenv G) (encodetype T []) (encodetype U []).
1026 intros;elim H;simplify
1030 |intros;lapply (NSA_All ? ? ? ? ? ? ? H1 H2 H3 H5);
1031 rewrite < (encode_subst n3 X n [])
1032 [rewrite < (encode_subst n5 X n1 [])
1033 [rewrite < eq_fv_Nenv_fv_env in H7;
1034 elim (NJSubtype_to_NWFT ? ? ? Hletin);
1035 lapply (in_fvNTyp_in_fvNenv ? ? H8);
1036 lapply (in_fvNTyp_in_fvNenv ? ? H9);
1037 simplify in Hletin1;simplify in Hletin2;
1039 [elim (decidable_eq_nat X n)
1041 |right;intro;autobatch depth=5]
1042 |elim (decidable_eq_nat X n1)
1044 |right;intro;autobatch depth=5]]
1046 |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);
1047 lapply (in_fvNTyp_in_fvNenv ? ? H10);simplify in Hletin1;
1048 elim (decidable_eq_nat X n1)
1050 |elim H7;autobatch depth=4]]
1052 |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);lapply (in_fvNTyp_in_fvNenv ? ? H9);
1053 simplify in Hletin1;elim (decidable_eq_nat X n)
1055 |elim H7;autobatch depth=4]]]]
1058 let rec closed_type T n ≝
1063 | Arrow T1 T2 ⇒ closed_type T1 n ∧ closed_type T2 n
1064 | Forall T1 T2 ⇒ closed_type T1 n ∧ closed_type T2 (S n)].
1066 lemma decoder : ∀T,n.closed_type T n →
1067 ∀l.length ? l = n → distinct_list l →
1068 (\forall x. x ∈ (fv_type T) \to x ∉ l) \to
1069 ∃U.T = encodetype U l.
1071 [simplify in H;apply (ex_intro ? ? (TName (nth ? l O n)));simplify;
1072 rewrite > lookup_nth;simplify;autobatch;
1073 |apply (ex_intro ? ? (TName n));rewrite > (fv_encode (TName n) l []);
1074 [simplify;reflexivity
1075 |intros;simplify in H3;simplify in H4;lapply (H3 ? H4);
1076 cut (lookup x l = false)
1077 [rewrite > Hcut;simplify;split
1078 [reflexivity|intro;destruct H5]
1079 |elim (bool_to_decidable_eq (lookup x l) true)
1080 [lapply (lookup_in ? ? H5);elim (Hletin Hletin1)
1081 |generalize in match H5;elim (lookup x l);
1082 [elim H6;reflexivity|reflexivity]]]]
1083 |apply (ex_intro ? ? NTop);simplify;reflexivity
1084 |simplify in H2;elim H2;lapply (H ? H6 ? H3 H4);
1085 [lapply (H1 ? H7 ? H3 H4)
1086 [elim Hletin;elim Hletin1;
1087 apply (ex_intro ? ? (NArrow a a1));autobatch;
1088 |intros;apply H5;simplify;autobatch]
1089 |intros;apply H5;simplify;autobatch]
1090 |simplify in H2;elim H2;elim (H ? H6 ? H3 H4);elim (fresh_name (fv_type t1@l));
1091 [elim (H1 ? H7 (a1::l))
1092 [apply (ex_intro ? ? (NForall a1 a a2));simplify;autobatch
1094 |unfold;intros;intro;apply H12;generalize in match H13;generalize in match H10;
1095 generalize in match H11;generalize in match H9;
1096 generalize in match m;generalize in match n1;
1100 |simplify in H18;rewrite > H18 in H9;elim H9;simplify in H16;
1101 lapply (le_S_S_to_le ? ? H16);autobatch depth=4]
1102 |intro;intros;change in H17:(? ? % ?) with (nth nat l O n2);
1103 simplify in H17:(? ? ? %);elim H9;rewrite < H17;
1104 apply in_list_to_in_list_append_r;apply nth_in_list;
1105 simplify in H16;autobatch
1106 |intros;change in H18 with (nth nat l O n2 = nth nat l O m1);
1107 unfold in H4;elim (decidable_eq_nat n2 m1)
1109 |simplify in H17;simplify in H16;elim (H4 ? ? ? ? H19);autobatch]]
1110 |intro;elim (in_list_cons_case ? ? ? ? H11)
1111 [apply H9;apply in_list_to_in_list_append_l;rewrite < H12;assumption
1112 |apply (H5 x);simplify;autobatch]]
1113 |apply H5;simplify;autobatch]]
1116 lemma closed_subst : \forall T,X,n.closed_type (subst_type_nat T (TFree X) n) n
1117 \to closed_type T (S n).
1118 intros 2;elim T 0;simplify;intros
1119 [elim (decidable_eq_nat n n1)
1120 [rewrite > H1;apply le_n
1121 |rewrite > (not_eq_to_eqb_false ? ? H1) in H;simplify in H;
1122 apply le_S;assumption]
1124 |elim H2;split;autobatch
1125 |elim H2;split;autobatch]
1128 lemma WFT_to_closed: ∀G,T.WFType G T → closed_type T O.
1129 intros;elim H;simplify
1134 |elim (fresh_name (fv_env l@fv_type t1));lapply (H4 a)
1136 |*:intro;autobatch]]]
1139 lemma adeq_WFE2 : ∀G1.WFEnv G1 → ∀G2.(G1 = encodeenv G2) → NWFEnv G2.
1143 |simplify in H2;destruct H2]
1145 [simplify in H5;destruct H5
1146 |elim a in H6;simplify in H6;destruct H6;apply NWFE_cons;autobatch]]
1149 lemma in_list_encodeenv : \forall b,X,T,l.
1150 in_list ? (mk_bound b X (encodetype T [])) (encodeenv l) \to
1151 \exists U.encodetype U [] = encodetype T [] \land
1152 (mk_nbound b X U) ∈ l.
1154 [simplify in H;elim (not_in_list_nil ? ? H)
1155 |simplify in H1;inversion H1;elim a 0;simplify;intros;destruct;
1156 [apply (ex_intro ? ? n1);split;autobatch
1157 |elim (H H2);elim H4;apply (ex_intro ? ? a1);split;autobatch]]
1160 lemma eq_swap_NTyp_to_case :
1161 \forall X,Y,Z,T. Y ∉ (X::var_NTyp T) \to
1162 swap_NTyp Z Y (swap_NTyp Y X T) = swap_NTyp Z X T \to
1163 Z = X \lor Z ∉ (fv_NTyp T).
1165 [simplify in H;simplify in H1;elim (decidable_eq_nat X n)
1166 [rewrite > H2;simplify;elim (decidable_eq_nat Z n)
1168 |right;intro;apply H3;apply in_list_singleton_to_eq;assumption]
1169 |elim (decidable_eq_nat Y n)
1171 |rewrite > (swap_other Y X n) in H1
1172 [elim (decidable_eq_nat Z n)
1173 [rewrite > H4 in H1;do 2 rewrite > swap_left in H1;
1174 destruct H1;elim H;apply in_list_head
1175 |elim (decidable_eq_nat Z X)
1177 |rewrite > (swap_other Z X n) in H1
1178 [right;intro;apply H3;simplify in H6;
1179 rewrite > (in_list_singleton_to_eq ? ? ? H6) in H1;
1180 rewrite > swap_left in H1;destruct H1;reflexivity
1181 |*:intro;autobatch]]]
1182 |*:intro;autobatch]]]
1183 |simplify;right;apply not_in_list_nil
1188 |right;simplify;intro;elim (in_list_append_to_or_in_list ? ? ? ? H6)
1191 |intro;apply H2;simplify;inversion H5;intros;destruct;autobatch;
1192 |simplify in H3;destruct H3;assumption]
1193 |intro;apply H2;simplify;inversion H4;intros;destruct;autobatch
1194 |simplify in H3;destruct H3;assumption]
1199 |right;simplify;intro;elim (in_list_append_to_or_in_list ? ? ? ? H6)
1201 |elim H5;elim (remove_inlist ? ? ? H7);assumption]
1202 |intro;apply H2;simplify;inversion H5;intros;destruct;autobatch
1203 |simplify in H3;destruct H3;assumption]
1204 |intro;apply H2;simplify;inversion H4;intros;destruct;autobatch depth=4;
1205 |simplify in H3;destruct H3;assumption]]
1209 theorem faithfulness : ∀G1,T1,U1.G1 ⊢ T1 ⊴ U1 →
1212 T1 = encodetype T2 [] →
1213 U1 = encodetype U2 [] →
1216 [intros;cut (U2 = NTop)
1217 [|generalize in match H5;elim U2 0;simplify;intros;destruct;reflexivity]
1218 rewrite > Hcut;apply NSA_Top;autobatch;
1219 |intros;cut (T2 = TName n ∧ U2 = TName n)
1221 [elim T2 in H4 0;simplify;intros;destruct;reflexivity
1222 |elim U2 in H5 0;simplify;intros;destruct;reflexivity]]
1224 rewrite > H6;rewrite > H7;apply NSA_Refl_TVar;
1226 |rewrite > H3 in H2;rewrite < eq_fv_Nenv_fv_env in H2;assumption]
1227 |intros;cut (T2 = TName n)
1228 [|elim T2 in H5 0;simplify;intros;destruct;reflexivity]
1229 rewrite > Hcut;elim (decoder t1 O ? []);
1230 [rewrite > H4 in H1;rewrite > H7 in H1;elim (in_list_encodeenv ???? H1);
1232 |4:unfold;intros;simplify in H7;elim (not_le_Sn_O ? H7)
1234 |intros;cut (∃u,u1,u2,u3.T2 = NArrow u u1 ∧ U2 = NArrow u2 u3)
1235 [decompose;rewrite > H8;rewrite > H10;rewrite > H10 in H7;simplify in H7;destruct;
1236 simplify in H6;destruct;autobatch width=4 size=9
1237 |generalize in match H6;elim T2 0;simplify;intros;destruct;
1238 generalize in match H7;elim U2 0;simplify;intros;destruct;
1239 autobatch depth=6 width=2 size=7]
1240 |intros;cut (∃n,u,u1,n1,u2,u3.T2 = NForall n u u1 ∧ U2 = NForall n1 u2 u3)
1241 [decompose;rewrite > H8;rewrite > H10;
1242 rewrite > H8 in H6;rewrite > H10 in H7;simplify in H6;simplify in H7;
1243 destruct;lapply (SA_All ? ? ? ? ? H1 H3);
1244 lapply (JS_to_WFT1 ? ? ? Hletin);lapply (JS_to_WFT2 ? ? ? Hletin);
1250 |rewrite < (encode_subst a2 Z a []);
1252 |lapply (SA_All ? ? ? ? ? H1 H3);lapply (JS_to_WFT1 ? ? ? Hletin);
1253 intro;elim (decidable_eq_nat Z a)
1255 |lapply (fv_WFT ? Z ? Hletin1)
1257 |simplify;apply in_list_to_in_list_append_r;
1258 apply fv_NTyp_fv_Typ
1260 |intro;autobatch]]]]
1261 |rewrite < (encode_subst a5 Z a3 [])
1266 |generalize in match H6;elim T2 0;simplify;intros;destruct;
1267 generalize in match H7;elim U2 0;simplify;intros;destruct;
1268 autobatch depth=8 width=2 size=9]]
1271 theorem NJS_trans : ∀G,T,U,V.NJSubtype G T U → NJSubtype G U V → NJSubtype G T V.
1272 intros;apply faithfulness [5,6,7:autobatch|4:autobatch|*:skip]