2 (**************************************************************************)
5 (* ||A|| A project by Andrea Asperti *)
7 (* ||I|| Developers: *)
8 (* ||T|| The HELM team. *)
9 (* ||A|| http://helm.cs.unibo.it *)
11 (* \ / This file is distributed under the terms of the *)
12 (* v GNU General Public License Version 2 *)
14 (**************************************************************************)
16 include "logic/equality.ma".
18 include "datatypes/bool.ma".
19 include "list/list.ma".
20 include "nat/compare.ma".
21 include "Fsub/util.ma".
22 include "Fsub/defn2.ma".
24 inductive NTyp : Set \def
25 | TName : nat \to NTyp
27 | NArrow : NTyp \to NTyp \to NTyp
28 | NForall : nat \to NTyp \to NTyp \to NTyp.
30 (*inductive NTerm : Set \def
31 | Name : nat \to NTerm
32 | NAbs : nat \to NTyp \to NTerm \to NTerm
33 | NApp : NTerm \to NTerm \to NTerm
34 | NTAbs : nat \to NTyp \to NTerm \to NTerm
35 | NTApp : NTerm \to NTyp \to NTerm.*)
37 (*inductive LNTyp: nat \to Set \def
38 | LNTVar : \forall m,n.(m < n) \to LNTyp n
39 | LNTFree : \forall n.nat \to LNTyp n
40 | LNTop : \forall n.LNTyp n
41 | LNArrow : \forall n.(LNTyp n) \to (LNTyp n) \to (LNTyp n)
42 | LNForall : \forall n.(LNTyp n) \to (LNTyp (S n)) \to (LNTyp n).
44 inductive LNTerm : nat \to Set \def
45 | LNVar : \forall m,n.(m < n) \to LNTerm n
46 | LNFree : \forall n.nat \to LNTerm n
47 | LNAbs : \forall n.(LNTyp n) \to (LNTerm (S n)) \to (LNTerm n)
48 | LNApp : \forall n.(LNTerm n) \to (LNTerm n) \to (LNTerm n)
49 | LNTAbs : \forall n.(LNTyp n) \to (LNTerm (S n)) \to (LNTerm n)
50 | LNTApp : \forall n.(LNTerm n) \to (LNTyp n) \to (LNTerm n).*)
52 record nbound : Set \def {
58 (*record lnbound (n:nat) : Set \def {
64 inductive option (A:Type) : Set \def
65 | Some : A \to option A
68 (*definition S_opt : (option nat) \to (option nat) \def
69 \lambda n.match n with
70 [ (Some n) \Rightarrow (Some nat (S n))
71 | None \Rightarrow None nat].*)
73 (* position of the first occurrence of nat x in list l
74 returns (length l) when x not in l *)
76 definition swap : nat \to nat \to nat \to nat \def
77 \lambda u,v,x.match (eqb x u) with
79 |false \Rightarrow match (eqb x v) with
81 |false \Rightarrow x]].
83 axiom swap_left : \forall x,y.(swap x y x) = y.
84 (*intros;unfold swap;rewrite > eqb_n_n;simplify;reflexivity;
87 axiom swap_right : \forall x,y.(swap x y y) = x.
88 (*intros;unfold swap;elim (eq_eqb_case y x)
89 [elim H;rewrite > H2;simplify;rewrite > H1;reflexivity
90 |elim H;rewrite > H2;simplify;rewrite > eqb_n_n;simplify;reflexivity]
93 axiom swap_other : \forall x,y,z.(z \neq x) \to (z \neq y) \to (swap x y z) = z.
94 (*intros;unfold swap;elim (eq_eqb_case z x)
95 [elim H2;lapply (H H3);elim Hletin
96 |elim H2;rewrite > H4;simplify;elim (eq_eqb_case z y)
97 [elim H5;lapply (H1 H6);elim Hletin
98 |elim H5;rewrite > H7;simplify;reflexivity]]
101 axiom swap_inv : \forall u,v,x.(swap u v (swap u v x)) = x.
102 (*intros;unfold in match (swap u v x);elim (eq_eqb_case x u)
103 [elim H;rewrite > H2;simplify;rewrite > H1;apply swap_right
104 |elim H;rewrite > H2;simplify;elim (eq_eqb_case x v)
105 [elim H3;rewrite > H5;simplify;rewrite > H4;apply swap_left
106 |elim H3;rewrite > H5;simplify;apply (swap_other ? ? ? H1 H4)]]
109 axiom swap_inj : \forall u,v,x,y.(swap u v x) = (swap u v y) \to x = y.
110 (*intros;unfold swap in H;elim (eq_eqb_case x u)
111 [elim H1;elim (eq_eqb_case y u)
112 [elim H4;rewrite > H5;assumption
113 |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
114 elim (eq_eqb_case y v)
115 [elim H7;rewrite > H9 in H;simplify in H;rewrite > H in H8;
116 lapply (H5 H8);elim Hletin
117 |elim H7;rewrite > H9 in H;simplify in H;elim H8;symmetry;assumption]]
118 |elim H1;elim (eq_eqb_case y u)
119 [elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
120 elim (eq_eqb_case x v)
121 [elim H7;rewrite > H9 in H;simplify in H;rewrite < H in H8;
123 |elim H7;rewrite > H9 in H;simplify in H;elim H8;assumption]
124 |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
125 elim (eq_eqb_case x v)
126 [elim H7;rewrite > H9 in H;elim (eq_eqb_case y v)
127 [elim H10;rewrite > H11;assumption
128 |elim H10;rewrite > H12 in H;simplify in H;elim H5;symmetry;
130 |elim H7;rewrite > H9 in H;elim (eq_eqb_case y v)
131 [elim H10;rewrite > H12 in H;simplify in H;elim H2;assumption
132 |elim H10;rewrite > H12 in H;simplify in H;assumption]]]]
135 let rec swap_NTyp u v T on T \def
137 [(TName X) \Rightarrow (TName (swap u v X))
138 |NTop \Rightarrow NTop
139 |(NArrow T1 T2) \Rightarrow (NArrow (swap_NTyp u v T1) (swap_NTyp u v T2))
140 |(NForall X T1 T2) \Rightarrow
141 (NForall (swap u v X) (swap_NTyp u v T1) (swap_NTyp u v T2))].
143 let rec swap_Typ u v T on T \def
145 [(TVar n) \Rightarrow (TVar n)
146 |(TFree X) \Rightarrow (TFree (swap u v X))
148 |(Arrow T1 T2) \Rightarrow (Arrow (swap_Typ u v T1) (swap_Typ u v T2))
149 |(Forall T1 T2) \Rightarrow (Forall (swap_Typ u v T1) (swap_Typ u v T2))].
151 definition swap_list : nat \to nat \to (list nat) \to (list nat) ≝
152 \lambda u,v,l.(map ? ? (swap u v) l).
154 let rec var_NTyp (T:NTyp):list nat\def
158 |NArrow U V ⇒ (var_NTyp U)@(var_NTyp V)
159 |NForall X U V ⇒ X::(var_NTyp U)@(var_NTyp V)].
161 inductive alpha_eq : NTyp \to NTyp \to Prop \def
162 | A_refl : \forall T.(alpha_eq T T)
163 | A_arrow : \forall T1,T2,U1,U2.(alpha_eq T1 U1) \to (alpha_eq T2 U2) \to
164 (alpha_eq (NArrow T1 T2) (NArrow U1 U2))
165 | A_forall : \forall T1,T2,U1,U2,X,Y.
168 \lnot (in_list nat Z (X::Y::((var_NTyp T2)@(var_NTyp U2))))
169 \to (alpha_eq (swap_NTyp Z X T2) (swap_NTyp Z Y U2))) \to
170 (alpha_eq (NForall X T1 T2) (NForall Y U1 U2)).
172 let rec posn l x on l \def
175 | (cons (y:nat) l2) \Rightarrow
178 | false \Rightarrow S (posn l2 x)]].
180 let rec length A l on l \def
183 | (cons (y:A) l2) \Rightarrow S (length A l2)].
185 let rec lookup n l on l \def
188 | cons (x:nat) l1 \rArr match (eqb n x) with
190 |false \rArr (lookup n l1)]].
192 let rec encodetype T vars on T \def
194 [ (TName n) ⇒ match (lookup n vars) with
195 [ true ⇒ (TVar (posn vars n))
198 | (NArrow T1 T2) ⇒ Arrow (encodetype T1 vars) (encodetype T2 vars)
199 | (NForall n2 T1 T2) ⇒ Forall (encodetype T1 vars)
200 (encodetype T2 (n2::vars))].
202 let rec head (A:Type) l on l \def
204 [ nil \Rightarrow None A
205 | (cons (x:A) l2) \Rightarrow Some A x].
207 (*let rec tail (A:Type) l \def
209 [ nil \Rightarrow nil A
210 | (cons (x:A) l2) \Rightarrow l2].*)
212 let rec nth n l on n \def
214 [ O \Rightarrow match l with
217 | (S n2) \Rightarrow (nth n2 (tail ? l))].
219 definition max_list : (list nat) \to nat \def
220 \lambda l.let rec aux l0 m on l0 \def
223 | (cons n l2) ⇒ (aux l2 (max m n))]
226 let rec decodetype T vars C on T \def
228 [ (TVar n) ⇒ (TName (nth n vars))
229 | (TFree x) ⇒ (TName x)
230 | Top \Rightarrow NTop
231 | (Arrow T1 T2) ⇒ (NArrow (decodetype T1 vars C) (decodetype T2 vars C))
232 | (Forall T1 T2) ⇒ (NForall (S (max_list (vars@C))) (decodetype T1 vars C)
233 (decodetype T2 ((S (max_list (vars@C)))::vars) C))].
235 definition sublist: \forall A:Type.(list A) \to (list A) \to Prop \def
236 \lambda A,l1,l2.\forall x.(in_list ? x l1) \to (in_list ? x l2).
238 let rec remove_nat (x:nat) (l:list nat) on l \def
241 | (cons y l2) ⇒ match (eqb x y) with
242 [ true ⇒ (remove_nat x l2)
243 | false ⇒ (y :: (remove_nat x l2)) ]].
245 let rec fv_NTyp (T:NTyp):list nat\def
249 |NArrow U V ⇒ (fv_NTyp U)@(fv_NTyp V)
250 |NForall X U V ⇒ (fv_NTyp U)@(remove_nat X (fv_NTyp V))].
253 let rec subst_NTyp_var T X Y \def
255 [TName Z ⇒ match (eqb X Z) with
256 [ true \rArr (TName Y)
257 | false \rArr (TName Z) ]
259 |NArrow U V ⇒ (NArrow (subst_NTyp_var U X Y) (subst_NTyp_var V X Y))
260 |NForall Z U V ⇒ match (eqb X Z) with
261 [ true ⇒ (NForall Z (subst_NTyp_var U X Y) V)
262 | false ⇒ (NForall Z (subst_NTyp_var U X Y)
263 (subst_NTyp_var V X Y))]].
265 definition fv_Nenv : list nbound → list nat ≝
268 [mk_nbound (B:bool) (X:nat) (T:NTyp) ⇒ X]).
270 inductive NWFType : (list nbound) → NTyp → Prop ≝
271 | NWFT_TName : ∀X,G.(in_list ? X (fv_Nenv G))
272 → (NWFType G (TName X))
273 | NWFT_Top : ∀G.(NWFType G NTop)
274 | NWFT_Arrow : ∀G,T,U.(NWFType G T) → (NWFType G U) →
275 (NWFType G (NArrow T U))
276 | NWFT_Forall : ∀G,X,T,U.(NWFType G T) →
277 (∀Y.¬(Y ∈ (fv_Nenv G)) →
278 (Y = X ∨ ¬(Y ∈ (fv_NTyp U))) →
279 (NWFType ((mk_nbound true Y T) :: G) (swap_NTyp Y X U))) →
280 (NWFType G (NForall X T U)).
281 (*NWFT_alpha : ∀G,T,U.(NWFType G T) → (alpha_eq T U) → (NWFType G U).*)
283 inductive NWFEnv : (list nbound) → Prop ≝
284 | NWFE_Empty : (NWFEnv (nil ?))
285 | NWFE_cons : ∀B,X,T,G.(NWFEnv G) →
286 ¬(in_list ? X (fv_Nenv G)) →
287 (NWFType G T) → (NWFEnv ((mk_nbound B X T) :: G)).
289 inductive NJSubtype : (list nbound) → NTyp → NTyp → Prop ≝
290 | NSA_Top : ∀G,T.(NWFEnv G) → (NWFType G T) → (NJSubtype G T NTop)
291 | NSA_Refl_TVar : ∀G,X.(NWFEnv G)
292 → (in_list ? X (fv_Nenv G))
293 → (NJSubtype G (TName X) (TName X))
294 | NSA_Trans_TVar : ∀G,X,T,U.
295 (in_list ? (mk_nbound true X U) G) →
296 (NJSubtype G U T) → (NJSubtype G (TName X) T)
297 | NSA_Arrow : ∀G,S1,S2,T1,T2.
298 (NJSubtype G T1 S1) → (NJSubtype G S2 T2) →
299 (NJSubtype G (NArrow S1 S2) (NArrow T1 T2))
300 | NSA_All : ∀G,X,Y,S1,S2,T1,T2.
301 (NWFType G (NForall X S1 S2)) \to
302 (NWFType G (NForall Y T1 T2)) \to
303 (NJSubtype G T1 S1) →
304 (∀Z.¬(Z ∈ fv_Nenv G) →
305 (Z = X \lor \lnot in_list ? Z (fv_NTyp S2)) \to
306 (Z = Y \lor \lnot in_list ? Z (fv_NTyp T2)) \to
307 (NJSubtype ((mk_nbound true Z T1) :: G)
308 (swap_NTyp Z X S2) (swap_NTyp Z Y T2))) →
309 (NJSubtype G (NForall X S1 S2) (NForall Y T1 T2))
310 | NSA_alpha : ∀G,T1,T2,U1,U2.(NJSubtype G T1 U1) →
315 let rec nt_len T \def
319 | NArrow T1 T2 ⇒ S (max (nt_len T1) (nt_len T2))
320 | NForall X T1 T2 ⇒ S (max (nt_len T1) (nt_len T2)) ].
322 definition encodeenv : list nbound → list bound ≝
325 [ mk_nbound b x T ⇒ mk_bound b x (encodetype T []) ]).
327 axiom append_associative : ∀A.∀l1,l2,l3:(list A).((l1@l2)@l3) = (l1@l2@l3).
329 lemma eq_fv_Nenv_fv_env : ∀G. fv_Nenv G = fv_env (encodeenv G).
331 [simplify;reflexivity
332 |simplify;rewrite < H;elim t;simplify;reflexivity]
336 axiom decidable_eq_bound : \forall b,c:bound.decidable (b = c).
338 lemma in_Nenv_to_in_env: ∀l,n,n2.mk_nbound true n n2 ∈ l →
339 mk_bound true n (encodetype n2 []) ∈ encodeenv l.
341 [elim (not_in_list_nil ? ? H)
343 [destruct;simplify;apply in_list_head
344 |destruct;elim t;simplify;apply in_list_cons;apply H;assumption]]
347 lemma in_lookup : \forall x,l.(in_list ? x l) \to (lookup x l = true).
349 [simplify;rewrite > eqb_n_n;reflexivity
350 |simplify;rewrite > H2;elim (eqb a a1);reflexivity]
353 lemma lookup_in : \forall x,l.(lookup x l = true) \to (in_list ? x l).
355 [simplify in H;destruct H
356 |generalize in match H1;simplify;elim (decidable_eq_nat x t)
357 [rewrite > H2;apply in_list_head
358 |rewrite > (not_eq_to_eqb_false ? ? H2) in H3;simplify in H3;
359 apply in_list_cons;apply H;assumption]]
362 lemma posn_length : \forall x,vars.(in_list ? x vars) \to
363 (posn vars x) < (length ? vars).
365 [elim (not_in_list_nil ? ? H)
367 [intros;destruct;simplify;rewrite > eqb_n_n;simplify;
369 |intros;destruct;simplify;elim (eqb x t);simplify
371 |apply le_S_S;apply H;assumption]]]
374 lemma in_remove : \forall a,b,l.(a \neq b) \to (in_list ? a l) \to
375 (in_list ? a (remove_nat b l)).
377 [elim (not_in_list_nil ? ? H1)
378 |inversion H2;intros;
379 [destruct;simplify;rewrite > not_eq_to_eqb_false
380 [simplify;apply in_list_head
381 |intro;apply H;symmetry;assumption]
382 |destruct;simplify;elim (eqb b t)
383 [simplify;apply H1;assumption
384 |simplify;apply in_list_cons;apply H1;assumption]]]
387 axiom NTyp_len_ind : \forall P:NTyp \to Prop.
388 (\forall U.(\forall V.((nt_len V) < (nt_len U)) \to (P V))
392 axiom ntlen_arrow1 : ∀T1,T2.(nt_len T1) < (nt_len (NArrow T1 T2)).
393 axiom ntlen_arrow2 : ∀T1,T2.(nt_len T2) < (nt_len (NArrow T1 T2)).
394 axiom ntlen_forall1 : ∀X,T1,T2.(nt_len T1) < (nt_len (NForall X T1 T2)).
395 axiom ntlen_forall2 : ∀X,T1,T2.(nt_len T2) < (nt_len (NForall X T1 T2)).
396 axiom eq_ntlen_swap : ∀X,Y,T.nt_len T = nt_len (swap_NTyp X Y T).
398 axiom nat_in_list_case :\forall G:list nat
400 .\forall n:nat.in_list nat n (H@G)\rarr in_list nat n G\lor in_list nat n H.
402 lemma swap_same : \forall x,y.swap x x y = y.
403 intros;elim (decidable_eq_nat y x)
404 [autobatch paramodulation
405 |rewrite > swap_other;autobatch]
408 lemma not_nat_in_to_lookup_false : ∀l,X.¬(X ∈ l) → lookup X l = false.
410 [simplify;reflexivity
411 |simplify;elim (decidable_eq_nat X t)
412 [elim H1;rewrite > H2;apply in_list_head
413 |rewrite > (not_eq_to_eqb_false ? ? H2);simplify;apply H;intro;apply H1;
414 apply (in_list_cons ? ? ? ? H3);]]
417 lemma fv_encode : ∀T,l1,l2.
418 (∀x.(in_list ? x (fv_NTyp T)) →
419 (lookup x l1 = lookup x l2 ∧
420 (lookup x l1 = true → posn l1 x = posn l2 x))) →
421 (encodetype T l1 = encodetype T l2).
423 [simplify in H;elim (H n)
424 [simplify;rewrite < H1;generalize in match H2;elim (lookup n l1)
425 [simplify;rewrite > H3;autobatch
426 |simplify;reflexivity]
428 |simplify;reflexivity
429 |simplify;rewrite > (H l1 l2)
430 [rewrite > (H1 l1 l2)
432 |intros;apply H2;simplify;apply in_list_to_in_list_append_r;autobatch]
433 |intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]
434 |simplify;rewrite > (H l1 l2)
435 [rewrite > (H1 (n::l1) (n::l2))
437 |intros;elim (decidable_eq_nat x n)
438 [simplify;rewrite > (eq_to_eqb_true ? ? H4);simplify;split
439 [reflexivity|intro;reflexivity]
442 [simplify;rewrite < H5;reflexivity
443 |simplify;elim (eqb x n);
444 [simplify;reflexivity
445 |simplify in H7;rewrite < (H6 H7);reflexivity]]
446 |simplify;apply in_list_to_in_list_append_r;
447 apply (in_remove ? ? ? H4);assumption]]]
448 |intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]]
451 lemma lookup_swap : \forall a,b,x,vars.
452 (lookup (swap a b x) (swap_list a b vars) =
455 [simplify;reflexivity
456 |simplify;elim (decidable_eq_nat x t)
457 [rewrite > H1;rewrite > eqb_n_n;rewrite > eqb_n_n;simplify;reflexivity
458 |rewrite > (not_eq_to_eqb_false ? ? H1);elim (decidable_eq_nat x a)
459 [rewrite > H;rewrite > H2;rewrite > swap_left;
460 elim (decidable_eq_nat b t)
461 [rewrite < H3;rewrite > swap_right;
462 rewrite > (not_eq_to_eqb_false b a)
465 |rewrite > (swap_other a b t)
466 [rewrite > (not_eq_to_eqb_false ? ? H3);simplify;reflexivity
469 |elim (decidable_eq_nat x b)
470 [rewrite > H;rewrite > H3;rewrite > swap_right;
471 elim (decidable_eq_nat t a)
472 [rewrite > H4;rewrite > swap_left;
473 rewrite > (not_eq_to_eqb_false a b)
476 |rewrite > (swap_other a b t)
477 [rewrite > (not_eq_to_eqb_false a t)
482 |rewrite > H;rewrite > (swap_other a b x)
483 [elim (decidable_eq_nat a t)
484 [rewrite > H4;rewrite > swap_left;
485 rewrite > (not_eq_to_eqb_false ? ? H3);reflexivity
486 |elim (decidable_eq_nat b t)
487 [rewrite > H5;rewrite > swap_right;
488 rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity
489 |rewrite > (swap_other a b t)
490 [rewrite > (not_eq_to_eqb_false ? ? H1);reflexivity
497 lemma posn_swap : \forall a,b,x,vars.
498 (posn vars x = posn (swap_list a b vars) (swap a b x)).
500 [simplify;reflexivity
501 |simplify;rewrite < H;elim (decidable_eq_nat x t)
502 [rewrite > H1;do 2 rewrite > eqb_n_n;reflexivity
503 |elim (decidable_eq_nat (swap a b x) (swap a b t))
505 |rewrite > (not_eq_to_eqb_false ? ? H1);
506 rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity]]]
509 theorem encode_swap : ∀a,x,T,vars.
510 ((in_list ? a (fv_NTyp T)) → (in_list ? a vars)) →
513 encodetype (swap_NTyp a x T) (swap_list a x vars).
515 [elim (decidable_eq_nat n x)
516 [rewrite > H2;simplify in match (swap_NTyp ? ? ?);rewrite > swap_right;
517 simplify;lapply (lookup_swap a x x vars);rewrite > swap_right in Hletin;
518 rewrite > Hletin;cut ((in_list ? x vars) \to (lookup x vars = true))
519 [rewrite > (Hcut H1);simplify;lapply (posn_swap a x x vars);
520 rewrite > swap_right in Hletin1;rewrite < Hletin1;reflexivity
521 |generalize in match x;elim vars
522 [elim (not_in_list_nil ? ? H3)
524 [intros;simplify;rewrite > eqb_n_n;reflexivity
525 |intros;simplify;destruct;rewrite > (H3 ? H5);
526 elim (eqb n1 t);reflexivity]]]
527 |elim (decidable_eq_nat n a);
528 [rewrite < H3;simplify;rewrite < posn_swap;rewrite > lookup_swap;
529 rewrite < H3 in H;simplify in H;rewrite > in_lookup;
530 [simplify;reflexivity
531 |apply H;apply in_list_head]
532 |simplify in ⊢ (? ? ? (? % ?));rewrite > swap_other;
533 [apply (fv_encode ? vars (swap_list a x vars));intros;
534 simplify in H4;cut (x1 = n)
535 [rewrite > Hcut;elim vars
536 [simplify;split [reflexivity|intro;reflexivity]
537 |simplify;elim H5;cut
538 (t = a ∨t = x ∨ (t ≠ a ∧ t ≠ x))
539 [|elim (decidable_eq_nat t a)
540 [left;left;assumption
541 |elim (decidable_eq_nat t x)
542 [left;right;assumption
543 |right;split;assumption]]]
546 [rewrite > H9;rewrite > swap_left;
547 rewrite > (not_eq_to_eqb_false ? ? H2);
548 rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
551 |intro;rewrite < (H7 H10);reflexivity]
552 |rewrite > H9;rewrite > swap_right;
553 rewrite > (not_eq_to_eqb_false ? ? H2);
554 rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
557 |intro;rewrite < (H7 H10);reflexivity]]
558 |elim H8;rewrite > (swap_other a x t)
562 [simplify;reflexivity
563 |simplify in H11;rewrite < (H7 H11);reflexivity]]
566 [intros;destruct;reflexivity
567 |intros;destruct;elim (not_in_list_nil ? ? H5)]]
569 |simplify;reflexivity
570 |simplify;simplify in H2;rewrite < H
573 |intro;apply H2;apply in_list_to_in_list_append_r;autobatch
575 |intro;apply H2;apply in_list_to_in_list_append_l;autobatch
577 |simplify;simplify in H2;rewrite < H
578 [elim (decidable_eq_nat a n)
579 [rewrite < (H1 (n::vars));
581 |intro;rewrite > H4;apply in_list_head
582 |apply in_list_cons;assumption]
583 |rewrite < (H1 (n::vars));
585 |intro;apply in_list_cons;apply H2;apply in_list_to_in_list_append_r;
586 apply (in_remove ? ? ? H4 H5)
587 |apply in_list_cons;assumption]]
588 |intro;apply H2;apply in_list_to_in_list_append_l;assumption
592 lemma encode_swap2 : ∀a:nat.∀x:nat.∀T:NTyp.
594 \forall vars.x ∈ vars
595 →encodetype T vars=encodetype (swap_NTyp a x T) (swap_list a x vars).
596 intros;apply (encode_swap ? ? ? ? ? H1);intro;elim (H H2);
599 lemma remove_inlist : \forall x,y,l.(in_list ? x (remove_nat y l)) \to
600 (in_list ? x l) \land x \neq y.
602 [simplify;intro;elim (not_in_list_nil ? ? H)
603 |simplify;intro;elim (decidable_eq_nat y t)
604 [rewrite > H in H2;rewrite > eqb_n_n in H2;simplify in H2;
605 rewrite > H in H1;elim (H1 H2);rewrite > H;split
606 [apply in_list_cons;assumption
608 |rewrite > (not_eq_to_eqb_false ? ? H) in H2;simplify in H2;
610 [intros;destruct;split
615 [apply in_list_cons;assumption
619 lemma inlist_remove : \forall x,y,l.(in_list ? x l \to x \neq y \to
620 (in_list ? x (remove_nat y l))).
622 [elim (not_in_list_nil ? ? H);
623 |simplify;elim (decidable_eq_nat y t)
624 [rewrite > (eq_to_eqb_true ? ? H3);simplify;apply H
625 [(*FIXME*)generalize in match H1;intro;inversion H1
626 [intros;destruct;elim H2;reflexivity
627 |intros;destruct;assumption]
629 |rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
630 (*FIXME*)generalize in match H1;intro;inversion H4
631 [intros;destruct;apply in_list_head
632 |intros;destruct;apply in_list_cons;apply (H H5 H2)
636 lemma incl_fv_var : \forall T.(incl ? (fv_NTyp T) (var_NTyp T)).
638 [simplify;unfold;intros;assumption
639 |simplify;unfold;intros;assumption
640 |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
641 [apply in_list_to_in_list_append_l;apply (H ? H3)
642 |apply in_list_to_in_list_append_r;apply (H1 ? H3)]
643 |simplify;unfold;intros;elim (decidable_eq_nat x n)
644 [rewrite > H3;apply in_list_head
645 |apply in_list_cons;elim (in_list_append_to_or_in_list ? ? ? ? H2)
646 [apply in_list_to_in_list_append_l;apply (H ? H4)
647 |apply in_list_to_in_list_append_r;elim (remove_inlist ? ? ? H4);
651 lemma fv_encode2 : ∀T,l1,l2.
652 (∀x.(in_list ? x (fv_NTyp T)) →
653 (lookup x l1 = lookup x l2 ∧
654 posn l1 x = posn l2 x)) →
655 (encodetype T l1 = encodetype T l2).
656 intros;apply fv_encode;intros;elim (H ? H1);split
657 [assumption|intro;assumption]
660 lemma alpha_sym : \forall S,T.(alpha_eq S T) \to (alpha_eq T S).
663 |apply A_arrow;assumption
666 |intros;apply H4;intro;apply H5;elim (decidable_eq_nat Z n5)
667 [rewrite > H7;apply in_list_head
668 |apply in_list_cons;(*FIXME*)generalize in match H6;intro;
670 [intros;destruct;apply in_list_head
671 |intros;destruct;apply in_list_cons;inversion H9
672 [intros;destruct;elim H7;reflexivity
674 elim (in_list_append_to_or_in_list ? ? ? ? H11)
675 [apply in_list_to_in_list_append_r;assumption
676 |apply in_list_to_in_list_append_l;assumption]]]]]]
679 lemma inlist_fv_swap : \forall x,y,b,T.
680 (\lnot (in_list ? b (y::var_NTyp T))) \to
681 (in_list ? x (fv_NTyp (swap_NTyp b y T))) \to
682 (x \neq y \land (x = b \lor (in_list ? x (fv_NTyp T)))).
684 [simplify in H;simplify;simplify in H1;elim (decidable_eq_nat y n)
685 [rewrite > H2 in H1;rewrite > swap_right in H1;
687 [intros;destruct;split
688 [unfold;intro;apply H;rewrite > H2;apply in_list_head
690 |intros;destruct;elim (not_in_list_nil ? ? H3)]
691 |elim (decidable_eq_nat b n)
692 [rewrite > H3 in H;elim H;apply in_list_cons;apply in_list_head
693 |rewrite > swap_other in H1
696 [intros;destruct;intro;apply H2;
699 elim (not_in_list_nil ? ? H4)]
703 |simplify in H1;elim (not_in_list_nil ? ? H1)
704 |simplify;simplify in H3;simplify in H2;elim (nat_in_list_case ? ? ? H3)
710 |right;apply in_list_to_in_list_append_r;assumption]]
711 |intro;apply H2;elim (nat_in_list_case (var_NTyp n1) [y] ? H5)
712 [apply (in_list_to_in_list_append_r ? ? (y::var_NTyp n) (var_NTyp n1));
715 [intros;destruct;apply in_list_head
717 elim (not_in_list_nil ? ? H7)]]
724 |right;apply in_list_to_in_list_append_l;assumption]]
725 |intro;apply H2;inversion H5
726 [intros;destruct;apply in_list_head
727 |intros;destruct;apply in_list_cons;
728 apply in_list_to_in_list_append_l;assumption]
730 |simplify;simplify in H3;simplify in H2;elim (nat_in_list_case ? ? ? H3)
736 |right;apply in_list_to_in_list_append_r;apply inlist_remove
738 |intro;elim (remove_inlist ? ? ? H4);apply H10;
741 |intro;rewrite > H8 in H7;rewrite > H11 in H7;apply H2;
742 destruct;apply in_list_cons;apply in_list_head
743 |destruct;assumption]]]]
744 |intro;apply H2;inversion H5
745 [intros;destruct;apply in_list_head
748 cut ((n::var_NTyp n1)@(var_NTyp n2) = n::var_NTyp n1@var_NTyp n2)
749 [rewrite < Hcut;elim (n::var_NTyp n1)
751 |simplify;elim (decidable_eq_nat b t)
752 [rewrite > H9;apply in_list_head
753 |apply in_list_cons;assumption]]
754 |simplify;reflexivity]]
755 |elim(remove_inlist ? ? ? H4);assumption]
761 |right;apply in_list_to_in_list_append_l;
763 |intro;apply H2;inversion H5
764 [intros;destruct;apply in_list_head
765 |intros;destruct;apply in_list_cons;
766 elim (decidable_eq_nat b n)
767 [rewrite > H8;apply in_list_head
768 |apply in_list_cons;apply in_list_to_in_list_append_l;
773 lemma inlist_fv_swap_r : \forall x,y,b,T.
774 (\lnot (in_list ? b (y::var_NTyp T))) \to
775 ((x = b \land (in_list ? y (fv_NTyp T))) \lor
776 (x \neq y \land (in_list ? x (fv_NTyp T)))) \to
777 (in_list ? x (fv_NTyp (swap_NTyp b y T))).
779 [simplify;simplify in H;simplify in H1;cut (b \neq n)
782 [rewrite > Hcut1;rewrite > swap_right;rewrite > H3;apply in_list_head
784 [intros;destruct;autobatch
785 |intros;destruct;elim (not_in_list_nil ? ? H5)]]
786 |elim H2;inversion H4
787 [intros;destruct;rewrite > (swap_other b y x)
791 |intros;destruct;elim (not_in_list_nil ? ? H5)]]
792 |intro;apply H;apply (in_list_to_in_list_append_r ? ? [y] [n]);
793 rewrite > H2;apply in_list_head]
794 |simplify in H1;elim H1;elim H2;elim (not_in_list_nil ? ? H4)
795 |simplify;simplify in H3;cut (\lnot (in_list ? b (y::var_NTyp n1)))
796 [cut (\lnot (in_list ? b (y::var_NTyp n)))
798 [elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
799 [apply in_list_to_in_list_append_l;apply H
801 |left;split;assumption]
802 |apply in_list_to_in_list_append_r;apply H1
804 |left;split;assumption]]
805 |elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
806 [apply in_list_to_in_list_append_l;apply H;
808 |right;split;assumption]
809 |apply in_list_to_in_list_append_r;apply H1
811 |right;split;assumption]]]
812 |intro;apply H2;inversion H4
813 [intros;destruct;apply in_list_head
814 |intros;destruct;apply in_list_cons;
815 simplify;apply in_list_to_in_list_append_l;
817 |intro;apply H2;inversion H4
818 [intros;destruct;apply in_list_head
819 |intros;destruct;apply in_list_cons;
820 simplify;apply in_list_to_in_list_append_r;
822 |simplify;simplify in H3;cut (\lnot (in_list ? b (y::var_NTyp n1)))
823 [cut (\lnot (in_list ? b (y::var_NTyp n2)))
825 [elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
826 [apply in_list_to_in_list_append_l;apply H
828 |left;split;assumption]
829 |apply in_list_to_in_list_append_r;apply inlist_remove
833 [assumption|elim (remove_inlist ? ? ? H7);assumption]]
834 |elim (remove_inlist ? ? ? H7);elim (decidable_eq_nat b n)
835 [rewrite > H10;rewrite > swap_left;intro;apply H9;
836 rewrite < H11;rewrite < H10;assumption
837 |rewrite > swap_other
838 [rewrite > H5;assumption
839 |intro;apply H10;symmetry;assumption
840 |intro;apply H9;symmetry;assumption]]]]
841 |elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
842 [apply in_list_to_in_list_append_l;apply H
844 |right;split;assumption]
845 |apply in_list_to_in_list_append_r;apply inlist_remove
849 [assumption|elim (remove_inlist ? ? ? H7);assumption]]
850 |elim (decidable_eq_nat b n)
851 [rewrite > H8;rewrite > swap_left;assumption
852 |elim (decidable_eq_nat y n)
853 [rewrite > H9;rewrite > swap_right;intro;apply Hcut1;
854 rewrite > H9;apply in_list_cons;
855 apply incl_fv_var;elim (remove_inlist ? ? ? H7);
856 rewrite < H10;assumption
857 |rewrite > (swap_other b y n)
858 [elim (remove_inlist ? ? ? H7);assumption
860 |intro;autobatch]]]]]]
861 |intro;apply H2;inversion H4
862 [intros;destruct;apply in_list_head
863 |simplify;intros;destruct;
865 apply (in_list_to_in_list_append_r ? ? (n::var_NTyp n1) (var_NTyp n2));
867 |intro;apply H2;inversion H4
868 [intros;destruct;apply in_list_head
869 |simplify;intros;destruct;
871 apply (in_list_to_in_list_append_l ? ? (n::var_NTyp n1) (var_NTyp n2));
872 apply in_list_cons;assumption]]]
875 lemma fv_alpha : \forall S,T.(alpha_eq S T) \to
876 (incl ? (fv_NTyp S) (fv_NTyp T)).
878 [unfold;intros;assumption
879 |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
880 [apply in_list_to_in_list_append_l;autobatch
881 |apply in_list_to_in_list_append_r;autobatch]
882 |simplify;unfold;intros;
883 elim (in_list_append_to_or_in_list ? ? ? ? H5)
884 [apply in_list_to_in_list_append_l;apply (H2 ? H6)
885 |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
886 apply in_list_to_in_list_append_r;
888 elim (remove_inlist ? ? ? H6);apply inlist_remove
889 [lapply (inlist_fv_swap_r x n4 a n1)
890 [elim (inlist_fv_swap x n5 a n3)
892 [rewrite < H12 in H7;elim H7;
893 do 2 apply in_list_cons;
894 apply in_list_to_in_list_append_l;
895 apply (incl_fv_var n1 ? H8);
897 |intro;apply H7;inversion H10;intros;destruct;
898 [apply in_list_cons;apply in_list_head
899 |do 2 apply in_list_cons;apply in_list_to_in_list_append_r;
901 |apply (Hletin ? Hletin1)]
902 |intro;apply H7;inversion H10
903 [intros;destruct;apply in_list_head
904 |intros;destruct;do 2 apply in_list_cons;
905 apply in_list_to_in_list_append_l;assumption]
906 |right;split;assumption]
907 |intros;intro;lapply (inlist_fv_swap_r x n4 a n1)
908 [lapply (Hletin ? Hletin1);
909 elim (inlist_fv_swap x n5 a n3 ? Hletin2)
911 |intro;apply H7;elim (decidable_eq_nat a n4)
912 [rewrite > H12;apply in_list_head
913 |apply in_list_cons;inversion H11;intros;destruct;
915 |apply in_list_cons;apply in_list_to_in_list_append_r;
917 |intro;apply H7;inversion H11
918 [intros;destruct;apply in_list_head
919 |intros;destruct;do 2 apply in_list_cons;
920 apply in_list_to_in_list_append_l;assumption]
921 |right;split;assumption]]]]
924 theorem alpha_to_encode : ∀S,T.(alpha_eq S T) →
925 ∀vars.(encodetype S vars) = (encodetype T vars).
928 |simplify;rewrite > H2;rewrite > H4;reflexivity
929 |simplify;rewrite > H2;
930 cut (encodetype n1 (n4::vars) = encodetype n3 (n5::vars))
931 [rewrite > Hcut;reflexivity
932 |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
933 lapply (encode_swap2 a n4 n1 ? (n4::vars))
934 [intro;apply H5;do 2 apply in_list_cons;
935 apply in_list_to_in_list_append_l;autobatch
936 |lapply (encode_swap2 a n5 n3 ? (n5::vars))
937 [intro;apply H5;do 2 apply in_list_cons;
938 apply in_list_to_in_list_append_r;autobatch
939 |rewrite > Hletin;rewrite > Hletin1;simplify;rewrite > swap_right;
940 rewrite > swap_right;rewrite > (H4 a H5 (a::swap_list a n4 vars));
941 rewrite > (fv_encode2 ? ? (a::swap_list a n5 vars))
943 |intros;elim (decidable_eq_nat n4 n5)
944 [rewrite > H7;autobatch
945 |cut ((x \neq n4) \land (x \neq n5))
946 [elim Hcut;elim (decidable_eq_nat x a)
947 [simplify;rewrite > (eq_to_eqb_true ? ? H10);simplify;
949 |simplify;rewrite > (not_eq_to_eqb_false ? ? H10);
952 |simplify;elim H11;rewrite < H12;
953 rewrite > H13;elim (decidable_eq_nat a t)
954 [rewrite > H14;rewrite > swap_left;
956 rewrite > (not_eq_to_eqb_false ? ? H8);
957 rewrite > (not_eq_to_eqb_false ? ? H9);
959 |elim (decidable_eq_nat n4 t)
960 [rewrite > H15;rewrite > swap_right;
961 rewrite > (swap_other a n5 t)
962 [rewrite > (not_eq_to_eqb_false ? ? H10);
964 rewrite > (not_eq_to_eqb_false ? ? H8);
967 |intro;apply H7;autobatch]
968 |rewrite > (swap_other a n4 t);
969 elim (decidable_eq_nat n5 t)
970 [rewrite < H16;rewrite > swap_right;
971 rewrite > (not_eq_to_eqb_false ? ? H9);
972 rewrite > (not_eq_to_eqb_false ? ? H10);
974 |rewrite > (swap_other a n5 t);try intro;
976 |*:intro;autobatch]]]]]
978 [lapply (H3 ? H5);lapply (alpha_sym ? ? Hletin2);
979 lapply (fv_alpha ? ? Hletin3);
980 lapply (Hletin4 ? H6);
981 elim (inlist_fv_swap ? ? ? ? ? Hletin5)
983 |intro;apply H5;inversion H8
987 do 2 apply in_list_cons;
988 apply in_list_to_in_list_append_l;assumption]]
989 |elim (inlist_fv_swap ? ? ? ? ? H6)
991 |intro;apply H5;elim (decidable_eq_nat a n4)
992 [rewrite > H9;apply in_list_head
994 inversion H8;intros;destruct;
997 apply in_list_to_in_list_append_r;
1000 |apply in_list_head]]]
1003 lemma encode_append : ∀T,U,n,l.length ? l ≤ n →
1004 subst_type_nat (encodetype T l) U n = encodetype T l.
1006 [simplify;elim (bool_to_decidable_eq (lookup n l) true)
1007 [rewrite > H1;simplify;lapply (lookup_in ? ? H1);
1008 lapply (posn_length ? ? Hletin);
1010 [rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;reflexivity
1011 |intro;rewrite > H2 in Hletin1;unfold in Hletin1;autobatch;]
1012 |cut (lookup n l = false)
1013 [rewrite > Hcut;reflexivity
1014 |generalize in match H1;elim (lookup n l);
1015 [elim H2;reflexivity|reflexivity]]]
1016 |simplify;reflexivity
1018 |simplify;rewrite > (H ? ? H2);rewrite > H1
1020 |simplify;autobatch]]
1023 lemma encode_subst_simple : ∀X,T,l.
1024 (encodetype T l = subst_type_nat (encodetype T (l@[X])) (TFree X) (length ? l)).
1026 [simplify;cut (lookup n l = true → posn l n = posn (l@[X]) n)
1027 [generalize in match Hcut;elim (bool_to_decidable_eq (lookup n l) true)
1028 [cut (lookup n (l@[X]) = true)
1029 [rewrite > H;rewrite > Hcut1;simplify;
1030 cut (eqb (posn (l@[X]) n) (length nat l) = false)
1031 [rewrite > Hcut2;simplify;rewrite < (H1 H);reflexivity
1032 |generalize in match H;elim l 0
1033 [simplify;intro;destruct H2
1034 |intros 2;simplify;elim (eqb n t)
1035 [simplify;reflexivity
1036 |simplify in H3;simplify;apply (H2 H3)]]]
1037 |generalize in match H;elim l
1038 [simplify in H2;destruct H2
1039 |generalize in match H3;simplify;elim (eqb n t) 0
1040 [simplify;intro;reflexivity
1041 |simplify;intro;apply (H2 H4)]]]
1042 |cut (lookup n l = false)
1043 [elim (decidable_eq_nat n X)
1044 [rewrite > Hcut1;rewrite > H2;cut (lookup X (l@[X]) = true)
1045 [rewrite > Hcut2;simplify;
1046 cut (eqb (posn (l@[X]) X) (length nat l) = true)
1047 [rewrite > Hcut3;simplify;reflexivity
1048 |generalize in match Hcut1;elim l 0
1049 [intros;simplify;rewrite > eqb_n_n;simplify;reflexivity
1050 |simplify;intros 2;rewrite > H2;elim (eqb X t)
1051 [simplify in H4;destruct H4
1052 |simplify;simplify in H4;apply (H3 H4)]]]
1054 [simplify;rewrite > eqb_n_n;reflexivity
1055 |simplify;elim (eqb X t)
1056 [simplify;reflexivity
1057 |simplify;assumption]]]
1058 |cut (lookup n l = lookup n (l@[X]))
1059 [rewrite < Hcut2;rewrite > Hcut1;simplify;reflexivity
1061 [simplify;rewrite > (not_eq_to_eqb_false ? ? H2);simplify;
1063 |simplify;elim (eqb n t)
1064 [simplify;reflexivity
1065 |simplify;assumption]]]]
1066 |generalize in match H;elim (lookup n l);
1067 [elim H2;reflexivity|reflexivity]]]
1069 [intro;simplify in H;destruct H
1070 |simplify;intros 2;elim (eqb n t)
1071 [simplify;reflexivity
1072 |simplify in H1;simplify;rewrite < (H H1);reflexivity]]]
1073 |simplify;reflexivity
1074 |simplify;rewrite < H;rewrite < H1;reflexivity
1075 |simplify;rewrite < H;rewrite < (append_associative ? [n] l [X]);
1076 rewrite < (H1 ([n]@l));reflexivity]
1079 lemma encode_subst : ∀T,X,Y,l.¬(X ∈ l) → ¬(Y ∈ l) →
1080 (X ∈ (fv_NTyp T) → X = Y) →
1081 encodetype (swap_NTyp X Y T) l =
1082 subst_type_nat (encodetype T (l@[Y])) (TFree X) (length ? l).
1083 apply NTyp_len_ind;intro;elim U
1084 [elim (decidable_eq_nat n X)
1085 [rewrite > H4 in H3;rewrite > H4;rewrite > H3
1086 [simplify in \vdash (? ? (? % ?) ?);rewrite > swap_same;
1087 cut (lookup Y (l@[Y]) = true)
1088 [simplify;rewrite > Hcut;rewrite > (not_nat_in_to_lookup_false ? ? H2);
1089 simplify;cut (posn (l@[Y]) Y = length ? l)
1090 [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
1091 |generalize in match H2;elim l;simplify
1092 [rewrite > eqb_n_n;reflexivity
1093 |elim (decidable_eq_nat Y t)
1094 [elim H6;rewrite > H7;apply in_list_head
1095 |rewrite > (not_eq_to_eqb_false ? ? H7);simplify;
1098 |intro;apply H6;apply in_list_cons;assumption]]]]
1100 [simplify;rewrite > eqb_n_n;reflexivity
1101 |simplify;rewrite > H5;elim (eqb Y t);reflexivity]]
1102 |simplify;apply in_list_head]
1103 |elim (decidable_eq_nat Y n);
1104 [rewrite < H5;simplify;rewrite > swap_right;
1105 rewrite > (not_nat_in_to_lookup_false ? ? H1);
1106 cut (lookup Y (l@[Y]) = true)
1107 [rewrite > Hcut;simplify;cut (posn (l@[Y]) Y = length ? l)
1108 [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
1109 |generalize in match H2;elim l;simplify
1110 [rewrite > eqb_n_n;reflexivity
1111 |elim (decidable_eq_nat Y t)
1112 [elim H7;rewrite > H8;apply in_list_head
1113 |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;
1116 |intro;apply H7;apply in_list_cons;assumption]]]]
1118 [rewrite > eqb_n_n;reflexivity
1119 |elim (eqb Y t);simplify;autobatch]]
1120 |simplify;rewrite > (swap_other X Y n)
1121 [cut (lookup n l = lookup n (l@[Y]) ∧
1122 (lookup n l = true → posn l n = posn (l@[Y]) n))
1123 [elim Hcut;rewrite > H6;generalize in match H7;
1124 generalize in match H6;elim (lookup n (l@[Y]))
1125 [simplify;rewrite < H9;generalize in match H8;elim l
1126 [simplify in H10;destruct H10
1127 |elim (decidable_eq_nat n t)
1128 [simplify;rewrite > (eq_to_eqb_true ? ? H12);simplify;
1130 |simplify;rewrite > (not_eq_to_eqb_false ? ? H12);
1131 simplify;generalize in match H10;
1132 elim (eqb (posn l1 n) (length nat l1))
1133 [simplify in H13;simplify in H11;
1134 rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
1135 simplify in H11;lapply (H13 H11);destruct Hletin
1136 |simplify;reflexivity]]
1139 |simplify;reflexivity]
1141 [simplify;cut (n ≠ Y)
1142 [rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;
1144 |intro;apply H5;symmetry;assumption]
1145 |intro;simplify in H6;destruct H6
1146 |elim H6;simplify;rewrite < H7;reflexivity
1147 |simplify;elim (eqb n t)
1148 [simplify;reflexivity
1149 |simplify;simplify in H7;elim H6;rewrite < (H9 H7);
1152 |intro;apply H5;symmetry;assumption]]]
1153 |simplify;reflexivity
1154 |simplify;rewrite < (H2 n ? ? ? ? H3 H4)
1155 [rewrite < (H2 n1 ? ? ? ? H3 H4);
1156 [autobatch|autobatch
1157 |intro;apply H5;simplify;apply in_list_to_in_list_append_r;assumption]
1159 |intro;apply H5;simplify;apply in_list_to_in_list_append_l;assumption]
1160 |simplify;rewrite < (H2 n1 ? ? ? ? H3 H4)
1161 [cut (l = swap_list X Y l)
1162 [|generalize in match H3;generalize in match H4;elim l
1163 [simplify;reflexivity
1164 |simplify;elim (decidable_eq_nat t X)
1165 [elim H8;rewrite > H9;apply in_list_head
1166 |elim (decidable_eq_nat t Y)
1167 [elim H7;rewrite > H10;apply in_list_head
1168 |rewrite > (swap_other X Y t)
1171 |intro;apply H7;apply in_list_cons;assumption
1172 |intro;apply H8;apply in_list_cons;assumption]
1174 elim (decidable_eq_nat n Y)
1175 [rewrite > H6;rewrite > (fv_encode (swap_NTyp X Y n2) (swap X Y Y::l)
1176 (swap_list X Y (Y::l)));
1177 [rewrite < (encode_swap X Y n2);
1178 [rewrite < (fv_encode ? (Y::l) (Y::l@[Y]))
1179 [rewrite > encode_append;
1180 [reflexivity(*rewrite < (fv_encode n2 (Y::l) (Y::l@[Y]));
1182 |intros;elim (decidable_eq_nat x Y)
1183 [rewrite > H8;simplify;rewrite > eqb_n_n;simplify;
1184 split [reflexivity|intro;reflexivity]
1185 |simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
1187 [simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
1188 simplify;split [reflexivity|intro;destruct H9]
1189 |elim H9;simplify;elim (eqb x t)
1190 [simplify;split [reflexivity|intro;reflexivity]
1191 |simplify;rewrite < H10;generalize in match H11;
1195 |intro;rewrite < (H12 H13);reflexivity]
1196 |split [reflexivity|intro;destruct H13]]]]]]*)
1197 |simplify;constructor 1]
1198 |intros;simplify;elim (decidable_eq_nat x Y)
1199 [rewrite > (eq_to_eqb_true ? ? H8);simplify;split
1200 [reflexivity|intro;reflexivity]
1201 |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;elim l
1202 [simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
1203 simplify;split [reflexivity|intro;destruct H9]
1204 |simplify;elim (eqb x t)
1205 [simplify;split [reflexivity|intro;reflexivity]
1206 |simplify;elim H9;split
1208 |intro;rewrite < (H11 H12);reflexivity]]]]]
1209 |intro;elim (decidable_eq_nat X Y)
1210 [rewrite > H8;apply in_list_head
1211 |elim H8;apply H5;simplify;apply in_list_to_in_list_append_r;
1212 rewrite > H6;apply (in_remove ? ? ? H8 H7)]
1213 |apply in_list_head]
1214 |intros;simplify;rewrite > swap_right;rewrite < Hcut;
1215 split [reflexivity|intro;reflexivity]]
1216 |(*rewrite < Hcut;*)elim (decidable_eq_nat n X)
1217 [rewrite > H7;rewrite > (fv_encode (swap_NTyp X Y n2) (swap X Y X::l)
1218 (swap_list X Y (X::l)))
1219 [rewrite > (encode_swap X Y n2);
1221 cut (swap X Y X::swap_list X Y (l@[Y]) =
1222 (swap X Y X::swap_list X Y l)@[X])
1223 [rewrite > Hcut1;cut (S (length ? l) = (length ? (swap X Y X::swap_list X Y l)))
1224 [rewrite > Hcut2;rewrite < (encode_subst_simple X
1225 (swap_NTyp X Y n2) (swap X Y X::swap_list X Y l));
1229 |simplify;rewrite < H8;reflexivity]]
1231 [simplify;rewrite > swap_right;reflexivity
1232 |simplify;destruct;rewrite > Hcut1;reflexivity]]
1233 |intro;apply in_list_head
1234 |apply in_list_cons;elim l
1235 [simplify;apply in_list_head
1236 |simplify;apply in_list_cons;assumption]]
1237 |intros;simplify;rewrite < Hcut;
1238 split [reflexivity|intro;reflexivity]]
1239 |rewrite > (swap_other X Y n)
1240 [rewrite < (append_associative ? [n] l [Y]);
1241 cut (S (length nat l) = length nat (n::l)) [|reflexivity]
1242 rewrite > Hcut1;rewrite < (H2 n2);
1245 |intro;apply H7;inversion H8;intros
1246 [destruct;reflexivity
1247 |destruct;elim (H3 H9)]
1248 |intro;apply H6;inversion H8;intros
1249 [destruct;reflexivity
1250 |destruct;elim (H4 H9)]
1251 |intro;apply H5;simplify;apply in_list_to_in_list_append_r;
1252 apply (in_remove ? ? ? ? H8);intro;apply H7;symmetry;assumption]
1255 |intro;apply H5;simplify;apply in_list_to_in_list_append_l;assumption]]
1258 lemma swap_case: ∀u,v,x.(swap u v x) = u ∨ (swap u v x) = v ∨ (swap u v x = x).
1259 intros.unfold in match swap.simplify.elim (eqb x u)
1261 |simplify;elim (eqb x v);simplify;autobatch]
1264 lemma in_fvNTyp_in_fvNenv : ∀G,T.(NWFType G T) → (incl ? (fv_NTyp T) (fv_Nenv G)).
1266 [simplify;unfold;intros;inversion H2;intros
1267 [destruct;assumption
1268 |destruct;elim (not_in_list_nil ? ? H3)]
1269 |simplify;unfold;intros;elim (not_in_list_nil ? ? H1)
1270 |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
1271 [apply (H2 ? H6)|apply (H4 ? H6)]
1272 |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
1273 [apply H2;assumption
1274 |elim (fresh_name (x::fv_Nenv l@var_NTyp n2));lapply (H4 a)
1275 [cut (a ≠ x ∧ x ≠ n)
1276 [elim Hcut;lapply (Hletin x)
1277 [simplify in Hletin1;inversion Hletin1;intros;
1278 [destruct;elim H8;reflexivity
1279 |destruct;assumption]
1280 |generalize in match H6;generalize in match H7;elim n2
1281 [simplify in H11;elim (decidable_eq_nat n n3)
1282 [rewrite > (eq_to_eqb_true ? ? H12) in H11;simplify in H11;
1283 elim (not_in_list_nil ? ? H11)
1284 |rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
1285 simplify in H11;inversion H11;intros
1287 rewrite > swap_other
1289 |intro;apply H8;rewrite > H13;reflexivity
1290 |intro;apply H9;rewrite > H13;reflexivity]
1291 |destruct;elim (not_in_list_nil ? ? H13)]]
1292 |simplify in H11;elim (not_in_list_nil ? ? H11)
1293 |simplify in H13;simplify;elim (remove_inlist ? ? ? H13);
1294 elim (in_list_append_to_or_in_list ? ? ? ? H14)
1295 [apply in_list_to_in_list_append_l;apply H10
1296 [intro;apply H12;simplify;
1297 rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4));
1298 elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3) H17);
1299 [apply in_list_to_in_list_append_l;assumption
1300 |apply in_list_to_in_list_append_r;
1301 apply in_list_to_in_list_append_l;assumption]
1302 |apply (in_remove ? ? ? H15 H16)]
1303 |apply in_list_to_in_list_append_r;apply H11
1304 [intro;apply H12;simplify;
1305 rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4));
1306 elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n4) H17);
1307 [apply in_list_to_in_list_append_l;assumption
1308 |apply in_list_to_in_list_append_r;
1309 apply in_list_to_in_list_append_r;assumption]
1310 |apply (in_remove ? ? ? H15 H16)]]
1311 |simplify;simplify in H13;elim (remove_inlist ? ? ? H13);
1312 elim (nat_in_list_case ? ? ? H14);
1313 [apply in_list_to_in_list_append_r;apply in_remove;
1314 [elim (remove_inlist ? ? ? H16);intro;apply H18;
1315 elim (swap_case a n n3)
1317 [elim H8;symmetry;rewrite < H21;assumption
1318 |elim H9;rewrite < H21;assumption]
1319 |rewrite < H20;assumption]
1321 [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n5));
1322 intro;apply H12;simplify;
1323 rewrite < (append_associative ? [x] (fv_Nenv l) (n3::var_NTyp n4 @ var_NTyp n5));
1324 elim (nat_in_list_case ? ? ? H17)
1325 [apply in_list_to_in_list_append_r;
1327 apply in_list_to_in_list_append_r;assumption
1328 |apply in_list_to_in_list_append_l;assumption]
1329 |elim (remove_inlist ? ? ? H16);apply in_remove
1332 |apply in_list_to_in_list_append_l;apply H10;
1333 [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n4));
1334 intro;apply H12;simplify;
1335 rewrite < (append_associative ? [x] (fv_Nenv l) (n3::var_NTyp n4@var_NTyp n5));
1336 elim (nat_in_list_case ? ? ? H17)
1337 [apply in_list_to_in_list_append_r;apply in_list_cons;
1338 apply in_list_to_in_list_append_l;assumption
1339 |apply in_list_to_in_list_append_l;assumption]
1340 |apply in_remove;assumption]]]]
1342 [intro;apply H7;rewrite > H8;apply in_list_head
1343 |elim (remove_inlist ? ? ? H6);assumption]]
1344 |intro;apply H7;apply in_list_cons;apply in_list_to_in_list_append_l;
1346 |right;intro;apply H7;apply in_list_cons;
1347 apply in_list_to_in_list_append_r;apply (incl_fv_var ? ? H8)]]]
1350 lemma fv_NTyp_fv_Typ : ∀T,X,l.(X ∈ (fv_NTyp T)) → ¬(X ∈ l) →
1351 (X ∈ (fv_type (encodetype T l))).
1353 [simplify;simplify in H;cut (X = n)
1354 [rewrite < Hcut;generalize in match (lookup_in X l);elim (lookup X l)
1355 [elim H1;apply H2;reflexivity
1356 |simplify;apply in_list_head]
1357 |(*FIXME*)generalize in match H;intro;inversion H;intros;
1358 [destruct;reflexivity
1359 |destruct;elim (not_in_list_nil ? ? H3)]]
1360 |simplify in H;elim (not_in_list_nil ? ? H)
1361 |simplify;simplify in H2;
1362 elim (in_list_append_to_or_in_list ? ? ? ? H2);
1363 [apply in_list_to_in_list_append_l;apply (H ? H4 H3)
1364 |apply in_list_to_in_list_append_r;apply (H1 ? H4 H3)]
1365 |simplify;simplify in H2;
1366 elim (in_list_append_to_or_in_list ? ? ? ? H2)
1367 [apply in_list_to_in_list_append_l;apply (H ? H4 H3)
1368 |apply in_list_to_in_list_append_r;
1369 elim (remove_inlist ? ? ? H4);apply (H1 ? H5);intro;apply H6;
1371 [destruct;reflexivity
1372 |destruct;elim (H3 H8)]]]
1375 lemma adeq_WFT : ∀G,T.NWFType G T → WFType (encodeenv G) (encodetype T []).
1377 [simplify;apply WFT_TFree;rewrite < eq_fv_Nenv_fv_env;assumption
1378 |simplify;apply WFT_Top;
1379 |simplify;apply WFT_Arrow;assumption
1380 |simplify;apply WFT_Forall
1382 |intros;rewrite < (encode_subst n2 X n []);
1383 [simplify in H4;apply H4
1384 [rewrite > (eq_fv_Nenv_fv_env l);assumption
1385 |elim (decidable_eq_nat X n)
1387 |right;intro;apply H6;apply (fv_NTyp_fv_Typ ? ? ? H8);intro;
1388 apply H7;inversion H9;intros
1389 [destruct;reflexivity
1391 elim (not_in_list_nil ? ? H10)]]]
1392 |4:intro;elim (decidable_eq_nat X n)
1394 |elim H6;cut (¬(X ∈ [n]))
1395 [generalize in match Hcut;generalize in match [n];
1396 generalize in match H7;elim n2
1397 [simplify in H9;generalize in match H9;intro;inversion H9;intros;
1399 generalize in match (lookup_in X l1);elim (lookup X l1)
1400 [elim H10;apply H12;reflexivity
1401 |simplify;apply in_list_head]
1403 elim (not_in_list_nil ? ? H12)]
1404 |simplify in H9;elim (not_in_list_nil ? ? H9)
1405 |simplify;simplify in H11;
1406 elim (in_list_append_to_or_in_list ? ? ? ? H11);autobatch
1407 |simplify;simplify in H11;
1408 elim (in_list_append_to_or_in_list ? ? ? ? H11);
1410 |elim (remove_inlist ? ? ? H13);
1411 apply in_list_to_in_list_append_r;
1413 intro;inversion H16;intros;
1414 [destruct;elim H15;reflexivity
1415 |destruct;elim H12;assumption]]]
1416 |intro;elim H8;inversion H9;intros
1418 |destruct;elim (not_in_list_nil ? ? H10)]]]
1419 |*:apply not_in_list_nil]]]
1422 lemma not_in_list_encodetype : \forall T,l,x.in_list ? x l \to
1423 \lnot (in_list ? x (fv_type (encodetype T l))).
1424 intro;elim T;simplify
1425 [apply (bool_elim ? (lookup n l));intro
1426 [simplify;apply not_in_list_nil
1427 |simplify;intro;inversion H2;intros
1429 rewrite > (in_lookup ? ? H) in H1;destruct H1
1430 |destruct;apply (not_in_list_nil ? ? H3)]]
1431 |apply not_in_list_nil
1432 |intro;elim (nat_in_list_case ? ? ? H3)
1433 [apply H1;assumption
1434 |apply H;assumption]
1435 |intro;elim (nat_in_list_case ? ? ? H3)
1436 [apply (H1 (n::l) x ? H4);apply in_list_cons;assumption
1437 |apply H;assumption]]
1440 lemma incl_fv_encode_fv : \forall T,l.incl ? (fv_type (encodetype T l)) (fv_NTyp T).
1441 intro;elim T;simplify;unfold;
1442 [intro;elim (lookup n l)
1443 [simplify in H;elim (not_in_list_nil ? ? H)
1444 |simplify in H;assumption]
1445 |intros;elim (not_in_list_nil ? ? H)
1446 |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
1447 [apply in_list_to_in_list_append_l;apply H;autobatch
1448 |apply in_list_to_in_list_append_r;apply H1;autobatch]
1449 |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
1450 [apply in_list_to_in_list_append_l;apply H;autobatch
1451 |apply in_list_to_in_list_append_r;apply in_remove
1452 [intro;apply (not_in_list_encodetype n2 (n::l) x)
1453 [rewrite > H4;apply in_list_head
1455 |apply (H1 (n::l));assumption]]]
1458 lemma adeq_WFT2 : ∀G1,T1.WFType G1 T1 →
1459 ∀G2,T2.G1 = encodeenv G2 → T1 = encodetype T2 [] →
1462 [rewrite > H2 in H1;rewrite < eq_fv_Nenv_fv_env in H1;
1464 [|generalize in match H3;elim T2
1465 [simplify in H4;destruct;reflexivity
1466 |simplify in H4;destruct H4
1467 |simplify in H6;destruct H6
1468 |simplify in H6;destruct H6]]
1469 rewrite > Hcut;apply NWFT_TName;assumption
1471 [|generalize in match H2;elim T2
1472 [simplify in H3;destruct H3
1474 |simplify in H5;destruct H5
1475 |simplify in H5;destruct H5]]
1476 rewrite > Hcut;apply NWFT_Top;
1477 |cut (∃U,V.T2 = (NArrow U V))
1478 [|generalize in match H6;elim T2
1479 [1,2:simplify in H7;destruct H7
1480 |apply (ex_intro ? ? n);apply (ex_intro ? ? n1);reflexivity
1481 |simplify in H9;destruct H9]]
1482 elim Hcut;elim H7;rewrite > H8 in H6;simplify in H6;destruct;
1483 apply NWFT_Arrow;autobatch
1484 |cut (\exists Z,U,V.T2 = NForall Z U V)
1485 [|generalize in match H6;elim T2
1486 [1,2:simplify in H7;destruct H7
1487 |simplify in H9;destruct H9
1488 |apply (ex_intro ? ? n);apply (ex_intro ? ? n1);
1489 apply (ex_intro ? ? n2);reflexivity]]
1490 elim Hcut;elim H7;elim H8;clear Hcut H7 H8;rewrite > H9;
1491 rewrite > H9 in H6;simplify in H6;destruct;apply NWFT_Forall
1494 [rewrite > H7;cut (swap_NTyp a a a2 = a2)
1496 [rewrite > swap_same;reflexivity
1498 |rewrite > H8;rewrite > H9;reflexivity
1499 |rewrite > swap_same;rewrite > H8;rewrite > H9;reflexivity]]
1500 rewrite > Hcut;apply (H4 Y)
1501 [rewrite < eq_fv_Nenv_fv_env;assumption
1502 |rewrite > H7;apply not_in_list_encodetype;
1504 |rewrite > H7;simplify;reflexivity
1505 |rewrite > H7;autobatch]
1507 [rewrite < eq_fv_Nenv_fv_env;assumption
1508 |intro;apply H7;apply incl_fv_encode_fv;autobatch
1509 |simplify;reflexivity
1510 |symmetry;apply (encode_subst a2 Y a []);
1511 [3:intro;elim (H7 H8)
1515 lemma adeq_WFE : ∀G.NWFEnv G → WFEnv (encodeenv G).
1517 [simplify;apply WFE_Empty
1518 |simplify;apply WFE_cons;
1519 [2:rewrite < eq_fv_Nenv_fv_env;]
1523 lemma NWFT_env_incl : ∀G,T.NWFType G T → ∀H.incl ? (fv_Nenv G) (fv_Nenv H)
1526 [apply NWFT_TName;apply (H3 ? H1)
1533 |intros;apply (H4 ? ? H8);
1534 [intro;apply H7;apply (H6 ? H9)
1535 |unfold;intros;simplify;simplify in H9;inversion H9;intros
1536 [destruct;apply in_list_head
1537 |destruct;apply in_list_cons;apply (H6 ? H10)]]]]
1540 (*lemma NWFT_subst :
1541 \forall T,U,a,X,Y,G.
1542 NWFType (mk_nbound true a U::G) (swap_NTyp a X T) \to
1543 \lnot (in_list ? a (Y::X::fv_NTyp T@fv_Nenv G)) \to
1544 \lnot (in_list ? Y (fv_Nenv G)) \to
1545 (Y = X \lor \lnot (in_list ? Y (fv_NTyp T))) \to
1546 NWFType (mk_nbound true Y U::G) (swap_NTyp Y X T).
1547 apply NTyp_len_ind;intro;cases U
1548 [4:simplify;intros;apply NWFT_Forall
1550 |intros;apply (H ? ? ? Y)
1551 [2:inversion H1;simplify;intros;destruct;
1555 [4:simplify;apply NWFT_Forall
1560 lemma NJSubtype_to_NWFT : ∀G,T,U.NJSubtype G T U → NWFType G T ∧ NWFType G U.
1562 [split [assumption|apply NWFT_Top]
1563 |split;apply NWFT_TName;assumption
1565 [apply NWFT_TName;generalize in match H1;elim l
1566 [elim (not_in_list_nil ? ? H6)
1567 |inversion H7;intros
1568 [rewrite < H8;simplify;apply in_list_head
1569 |destruct;elim t;simplify;apply in_list_cons;
1570 apply H6;assumption]]
1572 |elim H2;elim H4;split;apply NWFT_Arrow;assumption
1575 [lapply (adeq_WFT ? ? H5);apply (adeq_WFT2 ? ? Hletin);autobatch
1576 |lapply (adeq_WFT ? ? H6);apply (adeq_WFT2 ? ? Hletin);autobatch]]
1579 theorem adequacy : ∀G,T,U.NJSubtype G T U →
1580 JSubtype (encodeenv G) (encodetype T []) (encodetype U []).
1581 intros;elim H;simplify
1584 [apply (adeq_WFE ? H1)|rewrite < eq_fv_Nenv_fv_env;assumption]
1587 |intros;lapply (NSA_All ? ? ? ? ? ? ? H1 H2 H3 H5);
1588 rewrite < (encode_subst n3 X n [])
1589 [rewrite < (encode_subst n5 X n1 [])
1590 [rewrite < eq_fv_Nenv_fv_env in H7;
1591 elim (NJSubtype_to_NWFT ? ? ? Hletin);
1592 lapply (in_fvNTyp_in_fvNenv ? ? H8);
1593 lapply (in_fvNTyp_in_fvNenv ? ? H9);
1594 simplify in Hletin1;simplify in Hletin2;
1596 [elim (decidable_eq_nat X n)
1598 |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7;
1599 apply Hletin1;apply in_list_to_in_list_append_r;assumption]
1600 |elim (decidable_eq_nat X n1)
1602 |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7;
1603 apply Hletin2;apply in_list_to_in_list_append_r;assumption]]
1604 |2,3:apply not_in_list_nil
1605 |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);
1606 lapply (in_fvNTyp_in_fvNenv ? ? H10);simplify in Hletin1;
1607 elim (decidable_eq_nat X n1)
1609 |lapply (in_remove ? ? ? H11 H8);elim H7;rewrite < eq_fv_Nenv_fv_env;
1610 apply Hletin1;apply in_list_to_in_list_append_r;assumption]]
1611 |2,3:apply not_in_list_nil
1612 |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);lapply (in_fvNTyp_in_fvNenv ? ? H9);
1613 simplify in Hletin1;elim (decidable_eq_nat X n)
1615 |lapply (in_remove ? ? ? H11 H8);elim H7;rewrite < eq_fv_Nenv_fv_env;
1616 apply Hletin1;apply in_list_to_in_list_append_r;assumption]]]
1617 |rewrite < (alpha_to_encode ? ? H3);rewrite < (alpha_to_encode ? ? H4);
1621 let rec closed_type T n ≝
1626 | Arrow T1 T2 ⇒ closed_type T1 n ∧ closed_type T2 n
1627 | Forall T1 T2 ⇒ closed_type T1 n ∧ closed_type T2 (S n)].
1629 alias id "nth" = "cic:/matita/list/list/nth.con".
1630 alias id "length" = "cic:/matita/list/list/length.con".
1631 definition distinct_list ≝
1632 λl.∀n,m.n < length ? l → m < length ? l → n ≠ m → nth ? l O n ≠ nth ? l O m.
1634 lemma posn_nth: ∀l,n.distinct_list l → n < length ? l →
1635 posn l (nth ? l O n) = n.
1637 [simplify in H1;elim (not_le_Sn_O ? H1)
1638 |simplify in H2;generalize in match H2;elim n
1639 [simplify;rewrite > eqb_n_n;simplify;reflexivity
1640 |simplify;cut (nth ? (t::l1) O (S n1) ≠ nth ? (t::l1) O O)
1641 [simplify in Hcut;rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;
1644 |unfold;intros;unfold in H1;lapply (H1 (S n2) (S m));
1645 [simplify in Hletin;assumption
1646 |2,3:simplify;autobatch
1647 |intro;apply H7;destruct H8;reflexivity]
1656 lemma nth_in_list : ∀l,n. n < length ? l → nth ? l O n ∈ l.
1658 [simplify in H;elim (not_le_Sn_O ? H)
1659 |generalize in match H1;elim n
1660 [simplify;apply in_list_head
1661 |simplify;apply in_list_cons;apply H;simplify in H3;apply (le_S_S_to_le ? ? H3)]]
1664 lemma lookup_nth : \forall l,n.n < length ? l \to
1665 lookup (nth nat l O n) l = true.
1667 [elim (not_le_Sn_O ? H);
1668 |generalize in match H1;elim n
1669 [simplify;rewrite > eqb_n_n;reflexivity
1670 |simplify;elim (eqb (nth nat l1 O n1) t)
1672 |simplify;apply H;apply le_S_S_to_le;assumption]]]
1675 lemma decoder : ∀T,n.closed_type T n →
1676 ∀l.length ? l = n → distinct_list l →
1677 (\forall x. in_list ? x (fv_type T) \to \lnot in_list ? x l) \to
1678 ∃U.T = encodetype U l.
1680 [simplify in H;apply (ex_intro ? ? (TName (nth ? l O n)));simplify;
1681 rewrite > lookup_nth
1682 [simplify;rewrite > posn_nth;
1683 [reflexivity|assumption|rewrite > H1;assumption]
1684 |rewrite > H1;assumption]
1685 |apply (ex_intro ? ? (TName n));rewrite > (fv_encode (TName n) l []);
1686 [simplify;reflexivity
1687 |intros;simplify in H3;simplify in H4;lapply (H3 ? H4);
1688 cut (lookup x l = false)
1689 [rewrite > Hcut;simplify;split
1690 [reflexivity|intro;destruct H5]
1691 |elim (bool_to_decidable_eq (lookup x l) true)
1692 [lapply (lookup_in ? ? H5);elim (Hletin Hletin1)
1693 |generalize in match H5;elim (lookup x l);
1694 [elim H6;reflexivity|reflexivity]]]]
1695 |apply (ex_intro ? ? NTop);simplify;reflexivity
1696 |simplify in H2;elim H2;lapply (H ? H6 ? H3 H4);
1697 [lapply (H1 ? H7 ? H3 H4)
1698 [elim Hletin;elim Hletin1;
1699 apply (ex_intro ? ? (NArrow a a1));simplify;
1700 rewrite < H9;rewrite < H8;reflexivity
1701 |intros;apply H5;simplify;apply in_list_to_in_list_append_r;assumption]
1702 |intros;apply H5;simplify;apply in_list_to_in_list_append_l;assumption]
1703 |simplify in H2;elim H2;elim (H ? H6 ? H3 H4);elim (fresh_name (fv_type t1@l));
1704 [elim (H1 ? H7 (a1::l))
1705 [apply (ex_intro ? ? (NForall a1 a a2));simplify;rewrite < H8;rewrite < H10;
1707 |simplify;rewrite > H3;reflexivity
1708 |unfold;intros;intro;apply H12;generalize in match H13;generalize in match H10;
1709 generalize in match H11;generalize in match H9;
1710 generalize in match m;generalize in match n1;
1714 |simplify in H18;rewrite > H18 in H9;elim H9;simplify in H16;
1715 lapply (le_S_S_to_le ? ? H16);apply in_list_to_in_list_append_r;
1717 |intro;intros;change in H17:(? ? % ?) with (nth nat l O n2);
1718 simplify in H17:(? ? ? %);elim H9;rewrite < H17;
1719 apply in_list_to_in_list_append_r;apply nth_in_list;
1720 simplify in H16;apply (le_S_S_to_le ? ? H16)
1721 |intros;change in H18 with (nth nat l O n2 = nth nat l O m1);
1722 unfold in H4;elim (decidable_eq_nat n2 m1)
1723 [rewrite > H19;reflexivity
1724 |simplify in H17;simplify in H16;elim (H4 ? ? ? ? H19)
1726 |apply (le_S_S_to_le ? ? H17)
1727 |apply (le_S_S_to_le ? ? H16)]]]
1728 |intro;elim (in_list_cons_case ? ? ? ? H11)
1729 [apply H9;apply in_list_to_in_list_append_l;rewrite < H12;assumption
1731 [simplify;apply in_list_to_in_list_append_r;assumption
1733 |apply H5;simplify;apply in_list_to_in_list_append_l;assumption]]
1736 lemma closed_subst : \forall T,X,n.closed_type (subst_type_nat T (TFree X) n) n
1737 \to closed_type T (S n).
1738 intros 2;elim T 0;simplify;intros
1739 [elim (decidable_eq_nat n n1)
1740 [rewrite > H1;apply le_n
1741 |rewrite > (not_eq_to_eqb_false ? ? H1) in H;simplify in H;
1742 apply le_S;assumption]
1744 |elim H2;split;autobatch
1745 |elim H2;split;autobatch]
1748 lemma WFT_to_closed: ∀G,T.WFType G T → closed_type T O.
1749 intros;elim H;simplify
1755 |elim (fresh_name (fv_env l@fv_type t1));lapply (H4 a)
1757 |intro;apply H5;apply in_list_to_in_list_append_l;assumption
1758 |intro;apply H5;apply in_list_to_in_list_append_r;assumption]]]
1761 lemma adeq_WFE2 : ∀G1.WFEnv G1 → ∀G2.(G1 = encodeenv G2) → NWFEnv G2.
1765 |simplify in H2;destruct H2]
1767 [simplify in H5;destruct H5
1768 |generalize in match H6;elim t1;simplify in H7;destruct H7;apply NWFE_cons
1769 [apply H2;reflexivity
1770 |rewrite > eq_fv_Nenv_fv_env;assumption
1774 lemma xxx : \forall b,X,T,l.
1775 in_list ? (mk_bound b X (encodetype T [])) (encodeenv l) \to
1776 \exists U.encodetype U [] = encodetype T [] \land
1777 in_list ? (mk_nbound b X U) l.
1779 [simplify in H;elim (not_in_list_nil ? ? H)
1780 |simplify in H1;inversion H1;elim t 0;simplify;intros;destruct;
1781 [apply (ex_intro ? ? n1);split;autobatch
1782 |elim (H H2);elim H4;apply (ex_intro ? ? a);split;autobatch]]
1785 lemma eq_swap_NTyp_to_case :
1786 \forall X,Y,Z,T.\lnot in_list ? Y (X::var_NTyp T) \to
1787 swap_NTyp Z Y (swap_NTyp Y X T) = swap_NTyp Z X T \to
1788 Z = X \lor \lnot in_list ? Z (fv_NTyp T).
1790 [simplify in H;simplify in H1;elim (decidable_eq_nat X n)
1791 [rewrite > H2;simplify;elim (decidable_eq_nat Z n)
1793 |right;intro;apply H3;apply in_list_singleton_to_eq;assumption]
1794 |elim (decidable_eq_nat Y n)
1795 [elim H;rewrite > H3;apply in_list_cons;apply in_list_head
1796 |rewrite > (swap_other Y X n) in H1
1797 [elim (decidable_eq_nat Z n)
1798 [rewrite > H4 in H1;do 2 rewrite > swap_left in H1;
1799 destruct H1;elim H;apply in_list_head
1800 |elim (decidable_eq_nat Z X)
1802 |rewrite > (swap_other Z X n) in H1
1803 [right;intro;apply H3;simplify in H6;
1804 rewrite > (in_list_singleton_to_eq ? ? ? H6) in H1;
1805 rewrite > swap_left in H1;destruct H1;reflexivity
1806 |intro;apply H4;symmetry;assumption
1807 |intro;apply H2;symmetry;assumption]]]
1808 |intro;apply H3;symmetry;assumption
1809 |intro;apply H2;symmetry;assumption]]]
1810 |simplify;right;apply not_in_list_nil
1815 |right;simplify;intro;elim (in_list_append_to_or_in_list ? ? ? ? H6)
1818 |intro;apply H2;simplify;inversion H5;intros;destruct;
1820 |apply in_list_cons;apply in_list_to_in_list_append_r;assumption]
1821 |simplify in H3;destruct H3;assumption]
1822 |intro;apply H2;simplify;inversion H4;intros;destruct;
1824 |apply in_list_cons;apply in_list_to_in_list_append_l;assumption]
1825 |simplify in H3;destruct H3;assumption]
1830 |right;simplify;intro;elim (in_list_append_to_or_in_list ? ? ? ? H6)
1832 |elim H5;elim (remove_inlist ? ? ? H7);assumption]
1833 |intro;apply H2;simplify;inversion H5;intros;destruct;
1835 |do 2 apply in_list_cons;apply in_list_to_in_list_append_r;assumption]
1836 |simplify in H3;destruct H3;assumption]
1837 |intro;apply H2;simplify;inversion H4;intros;destruct;
1839 |do 2 apply in_list_cons;apply in_list_to_in_list_append_l;assumption]
1840 |simplify in H3;destruct H3;assumption]]
1844 theorem faithfulness : ∀G1,T1,U1.G1 ⊢ T1 ⊴ U1 →
1847 T1 = encodetype T2 [] →
1848 U1 = encodetype U2 [] →
1851 [intros;cut (U2 = NTop)
1852 [|generalize in match H5;elim U2 0;simplify;intros;destruct;reflexivity]
1853 rewrite > Hcut;apply NSA_Top;
1854 [apply (adeq_WFE2 ? H1);assumption
1855 |apply (adeq_WFT2 ? ? H2);assumption]
1856 |intros;cut (T2 = TName n ∧ U2 = TName n)
1858 [generalize in match H4;elim T2 0;simplify;intros;destruct;reflexivity
1859 |generalize in match H5;elim U2 0;simplify;intros;destruct;reflexivity]]
1861 rewrite > H6;rewrite > H7;apply NSA_Refl_TVar;
1862 [apply (adeq_WFE2 ? H1);assumption
1863 |rewrite > H3 in H2;rewrite < eq_fv_Nenv_fv_env in H2;assumption]
1864 |intros;cut (T2 = TName n)
1865 [|generalize in match H5;elim T2 0;simplify;intros;destruct;reflexivity]
1867 elim (decoder t1 O ? []);
1868 [rewrite > H4 in H1;rewrite > H7 in H1;elim (xxx ? ? ? ? H1);elim H8;
1869 apply NSA_Trans_TVar
1872 |apply H3;autobatch]
1873 |apply (WFT_to_closed l);apply (JS_to_WFT1 ? ? ? H2)
1874 |simplify;reflexivity
1875 |unfold;intros;simplify in H7;elim (not_le_Sn_O ? H7)
1876 |apply not_in_list_nil]
1877 |intros;cut (∃u,u1,u2,u3.T2 = NArrow u u1 ∧ U2 = NArrow u2 u3)
1878 [elim Hcut;elim H8;elim H9;elim H10;elim H11;clear Hcut H8 H9 H10 H11;
1879 rewrite > H12;rewrite > H13;rewrite > H13 in H7;simplify in H7;destruct;
1880 simplify in H6;destruct;apply NSA_Arrow
1881 [apply H2;reflexivity
1882 |apply H4;reflexivity]
1883 |generalize in match H6;elim T2 0;simplify;intros;destruct;
1884 generalize in match H7;elim U2 0;simplify;intros;destruct;
1885 autobatch depth=6 width=2 size=7]
1886 |intros;cut (∃n,u,u1,n1,u2,u3.T2 = NForall n u u1 ∧ U2 = NForall n1 u2 u3)
1887 [elim Hcut;elim H8;elim H9;elim H10;elim H11;elim H12;elim H13;
1888 clear Hcut H8 H9 H10 H11 H12 H13;rewrite > H14;rewrite > H15;
1889 rewrite > H14 in H6;rewrite > H15 in H7;simplify in H6;simplify in H7;
1890 destruct H6;destruct H7;lapply (SA_All ? ? ? ? ? H1 H3);destruct H5;
1891 lapply (JS_to_WFT1 ? ? ? Hletin);lapply (JS_to_WFT2 ? ? ? Hletin);
1893 [apply (adeq_WFT2 ? ? Hletin1);reflexivity
1894 |apply (adeq_WFT2 ? ? Hletin2);reflexivity
1895 |apply H2;reflexivity
1898 |rewrite < eq_fv_Nenv_fv_env;assumption
1899 |simplify;reflexivity
1900 |rewrite < (encode_subst a2 Z a []);
1902 |2,3:apply not_in_list_nil
1903 |lapply (SA_All ? ? ? ? ? H1 H3);lapply (JS_to_WFT1 ? ? ? Hletin);
1904 intro;elim (decidable_eq_nat Z a)
1906 |lapply (fv_WFT ? Z ? Hletin1)
1907 [elim H5;rewrite > eq_fv_Nenv_fv_env;assumption
1908 |simplify;apply in_list_to_in_list_append_r;
1909 apply fv_NTyp_fv_Typ
1911 |intro;apply H9;autobatch]]]]
1912 |rewrite < (encode_subst a5 Z a3 [])
1914 |2,3:apply not_in_list_nil
1918 |generalize in match H6;elim T2 0;simplify;intros;destruct;
1919 generalize in match H7;elim U2 0;simplify;intros;destruct;
1920 autobatch depth=8 width=2 size=9]]