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/defn.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,S1,S2,T1,T2.
301 (NJSubtype G T1 S1) →
302 (∀Y.¬(Y ∈ fv_Nenv G) →
303 (NJSubtype ((mk_nbound true Y T1) :: G)
304 (swap_NTyp Y X S2) (swap_NTyp Y X T2))) →
305 (NJSubtype G (NForall X S1 S2) (NForall X T1 T2))
306 | NSA_alpha : ∀G,T1,T2,U1,U2.(NJSubtype G T1 U1) →
311 let rec nt_len T \def
315 | NArrow T1 T2 ⇒ S (max (nt_len T1) (nt_len T2))
316 | NForall X T1 T2 ⇒ S (max (nt_len T1) (nt_len T2)) ].
318 definition encodeenv : list nbound → list bound ≝
321 [ mk_nbound b x T ⇒ mk_bound b x (encodetype T []) ]).
323 axiom append_associative : ∀A.∀l1,l2,l3:(list A).((l1@l2)@l3) = (l1@l2@l3).
325 lemma eq_fv_Nenv_fv_env : ∀G. fv_Nenv G = fv_env (encodeenv G).
327 [simplify;reflexivity
328 |simplify;rewrite < H;elim t;simplify;reflexivity]
332 axiom decidable_eq_bound : \forall b,c:bound.decidable (b = c).
334 lemma in_Nenv_to_in_env: ∀l,n,n2.mk_nbound true n n2 ∈ l →
335 mk_bound true n (encodetype n2 []) ∈ encodeenv l.
337 [elim (not_in_list_nil ? ? H)
339 [destruct H3;destruct;simplify;apply in_list_head
340 |destruct H5;elim t;simplify;apply in_list_cons;apply H;assumption]]
343 lemma in_lookup : \forall x,l.(in_list ? x l) \to (lookup x l = true).
345 [simplify;rewrite > eqb_n_n;reflexivity
346 |simplify;rewrite > H2;elim (eqb a a1);reflexivity]
349 lemma lookup_in : \forall x,l.(lookup x l = true) \to (in_list ? x l).
351 [simplify in H;destruct H
352 |generalize in match H1;simplify;elim (decidable_eq_nat x t)
353 [rewrite > H2;apply in_list_head
354 |rewrite > (not_eq_to_eqb_false ? ? H2) in H3;simplify in H3;
355 apply in_list_cons;apply H;assumption]]
358 lemma posn_length : \forall x,vars.(in_list ? x vars) \to
359 (posn vars x) < (length ? vars).
361 [elim (not_in_list_nil ? ? H)
363 [intros;destruct H3;destruct;simplify;rewrite > eqb_n_n;simplify;
365 |intros;destruct H5;simplify;elim (eqb x t);simplify
367 |apply le_S_S;apply H;assumption]]]
370 lemma in_remove : \forall a,b,l.(a \neq b) \to (in_list ? a l) \to
371 (in_list ? a (remove_nat b l)).
373 [elim (not_in_list_nil ? ? H1)
374 |inversion H2;intros;
375 [destruct H4;destruct;simplify;rewrite > not_eq_to_eqb_false
376 [simplify;apply in_list_head
377 |intro;apply H;symmetry;assumption]
378 |destruct H6;simplify;elim (eqb b t)
379 [simplify;apply H1;assumption
380 |simplify;apply in_list_cons;apply H1;assumption]]]
383 axiom NTyp_len_ind : \forall P:NTyp \to Prop.
384 (\forall U.(\forall V.((nt_len V) < (nt_len U)) \to (P V))
388 axiom ntlen_arrow1 : ∀T1,T2.(nt_len T1) < (nt_len (NArrow T1 T2)).
389 axiom ntlen_arrow2 : ∀T1,T2.(nt_len T2) < (nt_len (NArrow T1 T2)).
390 axiom ntlen_forall1 : ∀X,T1,T2.(nt_len T1) < (nt_len (NForall X T1 T2)).
391 axiom ntlen_forall2 : ∀X,T1,T2.(nt_len T2) < (nt_len (NForall X T1 T2)).
392 axiom eq_ntlen_swap : ∀X,Y,T.nt_len T = nt_len (swap_NTyp X Y T).
394 axiom nat_in_list_case :\forall G:list nat
396 .\forall n:nat.in_list nat n (H@G)\rarr in_list nat n G\lor in_list nat n H.
398 lemma swap_same : \forall x,y.swap x x y = y.
399 intros;elim (decidable_eq_nat y x)
400 [autobatch paramodulation
401 |rewrite > swap_other;autobatch]
404 lemma not_nat_in_to_lookup_false : ∀l,X.¬(X ∈ l) → lookup X l = false.
406 [simplify;reflexivity
407 |simplify;elim (decidable_eq_nat X t)
408 [elim H1;rewrite > H2;apply in_list_head
409 |rewrite > (not_eq_to_eqb_false ? ? H2);simplify;apply H;intro;apply H1;
410 apply (in_list_cons ? ? ? ? H3);]]
413 lemma fv_encode : ∀T,l1,l2.
414 (∀x.(in_list ? x (fv_NTyp T)) →
415 (lookup x l1 = lookup x l2 ∧
416 (lookup x l1 = true → posn l1 x = posn l2 x))) →
417 (encodetype T l1 = encodetype T l2).
419 [simplify in H;elim (H n)
420 [simplify;rewrite < H1;generalize in match H2;elim (lookup n l1)
421 [simplify;rewrite > H3;autobatch
422 |simplify;reflexivity]
424 |simplify;reflexivity
425 |simplify;rewrite > (H l1 l2)
426 [rewrite > (H1 l1 l2)
428 |intros;apply H2;simplify;apply in_list_to_in_list_append_r;autobatch]
429 |intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]
430 |simplify;rewrite > (H l1 l2)
431 [rewrite > (H1 (n::l1) (n::l2))
433 |intros;elim (decidable_eq_nat x n)
434 [simplify;rewrite > (eq_to_eqb_true ? ? H4);simplify;split
435 [reflexivity|intro;reflexivity]
438 [simplify;rewrite < H5;reflexivity
439 |simplify;elim (eqb x n);
440 [simplify;reflexivity
441 |simplify in H7;rewrite < (H6 H7);reflexivity]]
442 |simplify;apply in_list_to_in_list_append_r;
443 apply (in_remove ? ? ? H4);assumption]]]
444 |intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]]
447 lemma lookup_swap : \forall a,b,x,vars.
448 (lookup (swap a b x) (swap_list a b vars) =
451 [simplify;reflexivity
452 |simplify;elim (decidable_eq_nat x t)
453 [rewrite > H1;rewrite > eqb_n_n;rewrite > eqb_n_n;simplify;reflexivity
454 |rewrite > (not_eq_to_eqb_false ? ? H1);elim (decidable_eq_nat x a)
455 [rewrite > H;rewrite > H2;rewrite > swap_left;
456 elim (decidable_eq_nat b t)
457 [rewrite < H3;rewrite > swap_right;
458 rewrite > (not_eq_to_eqb_false b a)
461 |rewrite > (swap_other a b t)
462 [rewrite > (not_eq_to_eqb_false ? ? H3);simplify;reflexivity
465 |elim (decidable_eq_nat x b)
466 [rewrite > H;rewrite > H3;rewrite > swap_right;
467 elim (decidable_eq_nat t a)
468 [rewrite > H4;rewrite > swap_left;
469 rewrite > (not_eq_to_eqb_false a b)
472 |rewrite > (swap_other a b t)
473 [rewrite > (not_eq_to_eqb_false a t)
478 |rewrite > H;rewrite > (swap_other a b x)
479 [elim (decidable_eq_nat a t)
480 [rewrite > H4;rewrite > swap_left;
481 rewrite > (not_eq_to_eqb_false ? ? H3);reflexivity
482 |elim (decidable_eq_nat b t)
483 [rewrite > H5;rewrite > swap_right;
484 rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity
485 |rewrite > (swap_other a b t)
486 [rewrite > (not_eq_to_eqb_false ? ? H1);reflexivity
493 lemma posn_swap : \forall a,b,x,vars.
494 (posn vars x = posn (swap_list a b vars) (swap a b x)).
496 [simplify;reflexivity
497 |simplify;rewrite < H;elim (decidable_eq_nat x t)
498 [rewrite > H1;do 2 rewrite > eqb_n_n;reflexivity
499 |elim (decidable_eq_nat (swap a b x) (swap a b t))
501 |rewrite > (not_eq_to_eqb_false ? ? H1);
502 rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity]]]
505 theorem encode_swap : ∀a,x,T,vars.
506 ((in_list ? a (fv_NTyp T)) → (in_list ? a vars)) →
509 encodetype (swap_NTyp a x T) (swap_list a x vars).
511 [elim (decidable_eq_nat n x)
512 [rewrite > H2;simplify in match (swap_NTyp ? ? ?);rewrite > swap_right;
513 simplify;lapply (lookup_swap a x x vars);rewrite > swap_right in Hletin;
514 rewrite > Hletin;cut ((in_list ? x vars) \to (lookup x vars = true))
515 [rewrite > (Hcut H1);simplify;lapply (posn_swap a x x vars);
516 rewrite > swap_right in Hletin1;rewrite < Hletin1;reflexivity
517 |generalize in match x;elim vars
518 [elim (not_in_list_nil ? ? H3)
520 [intros;simplify;rewrite > eqb_n_n;reflexivity
521 |intros;simplify;destruct H8;rewrite > (H3 ? H5);
522 elim (eqb n1 t);reflexivity]]]
523 |elim (decidable_eq_nat n a);
524 [rewrite < H3;simplify;rewrite < posn_swap;rewrite > lookup_swap;
525 rewrite < H3 in H;simplify in H;rewrite > in_lookup;
526 [simplify;reflexivity
527 |apply H;apply in_list_head]
528 |simplify in ⊢ (? ? ? (? % ?));rewrite > swap_other;
529 [apply (fv_encode ? vars (swap_list a x vars));intros;
530 simplify in H4;cut (x1 = n)
531 [rewrite > Hcut;elim vars
532 [simplify;split [reflexivity|intro;reflexivity]
533 |simplify;elim H5;cut
534 (t = a ∨t = x ∨ (t ≠ a ∧ t ≠ x))
535 [|elim (decidable_eq_nat t a)
536 [left;left;assumption
537 |elim (decidable_eq_nat t x)
538 [left;right;assumption
539 |right;split;assumption]]]
542 [rewrite > H9;rewrite > swap_left;
543 rewrite > (not_eq_to_eqb_false ? ? H2);
544 rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
547 |intro;rewrite < (H7 H10);reflexivity]
548 |rewrite > H9;rewrite > swap_right;
549 rewrite > (not_eq_to_eqb_false ? ? H2);
550 rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
553 |intro;rewrite < (H7 H10);reflexivity]]
554 |elim H8;rewrite > (swap_other a x t)
558 [simplify;reflexivity
559 |simplify in H11;rewrite < (H7 H11);reflexivity]]
562 [intros;destruct H6;destruct;reflexivity
563 |intros;destruct H8;elim (not_in_list_nil ? ? H5)]]
565 |simplify;reflexivity
566 |simplify;simplify in H2;rewrite < H
569 |intro;apply H2;apply in_list_to_in_list_append_r;autobatch
571 |intro;apply H2;apply in_list_to_in_list_append_l;autobatch
573 |simplify;simplify in H2;rewrite < H
574 [elim (decidable_eq_nat a n)
575 [rewrite < (H1 (n::vars));
577 |intro;rewrite > H4;apply in_list_head
578 |apply in_list_cons;assumption]
579 |rewrite < (H1 (n::vars));
581 |intro;apply in_list_cons;apply H2;apply in_list_to_in_list_append_r;
582 apply (in_remove ? ? ? H4 H5)
583 |apply in_list_cons;assumption]]
584 |intro;apply H2;apply in_list_to_in_list_append_l;assumption
588 lemma encode_swap2 : ∀a:nat.∀x:nat.∀T:NTyp.
590 \forall vars.x ∈ vars
591 →encodetype T vars=encodetype (swap_NTyp a x T) (swap_list a x vars).
592 intros;apply (encode_swap ? ? ? ? ? H1);intro;elim (H H2);
595 lemma remove_inlist : \forall x,y,l.(in_list ? x (remove_nat y l)) \to
596 (in_list ? x l) \land x \neq y.
598 [simplify;intro;elim (not_in_list_nil ? ? H)
599 |simplify;intro;elim (decidable_eq_nat y t)
600 [rewrite > H in H2;rewrite > eqb_n_n in H2;simplify in H2;
601 rewrite > H in H1;elim (H1 H2);rewrite > H;split
602 [apply in_list_cons;assumption
604 |rewrite > (not_eq_to_eqb_false ? ? H) in H2;simplify in H2;
606 [intros;destruct H4;split
611 [apply in_list_cons;assumption
615 lemma inlist_remove : \forall x,y,l.(in_list ? x l \to x \neq y \to
616 (in_list ? x (remove_nat y l))).
618 [elim (not_in_list_nil ? ? H);
619 |simplify;elim (decidable_eq_nat y t)
620 [rewrite > (eq_to_eqb_true ? ? H3);simplify;apply H
621 [(*FIXME*)generalize in match H1;intro;inversion H1
622 [intros;destruct H6;destruct;elim H2;reflexivity
623 |intros;destruct H8;assumption]
625 |rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
626 (*FIXME*)generalize in match H1;intro;inversion H4
627 [intros;destruct H6;destruct;apply in_list_head
628 |intros;destruct H8;destruct;apply in_list_cons;apply (H H5 H2)
632 lemma incl_fv_var : \forall T.(incl ? (fv_NTyp T) (var_NTyp T)).
634 [simplify;unfold;intros;assumption
635 |simplify;unfold;intros;assumption
636 |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
637 [apply in_list_to_in_list_append_l;apply (H ? H3)
638 |apply in_list_to_in_list_append_r;apply (H1 ? H3)]
639 |simplify;unfold;intros;elim (decidable_eq_nat x n)
640 [rewrite > H3;apply in_list_head
641 |apply in_list_cons;elim (in_list_append_to_or_in_list ? ? ? ? H2)
642 [apply in_list_to_in_list_append_l;apply (H ? H4)
643 |apply in_list_to_in_list_append_r;elim (remove_inlist ? ? ? H4);
647 lemma fv_encode2 : ∀T,l1,l2.
648 (∀x.(in_list ? x (fv_NTyp T)) →
649 (lookup x l1 = lookup x l2 ∧
650 posn l1 x = posn l2 x)) →
651 (encodetype T l1 = encodetype T l2).
652 intros;apply fv_encode;intros;elim (H ? H1);split
653 [assumption|intro;assumption]
656 lemma alpha_sym : \forall S,T.(alpha_eq S T) \to (alpha_eq T S).
659 |apply A_arrow;assumption
662 |intros;apply H4;intro;apply H5;elim (decidable_eq_nat Z n5)
663 [rewrite > H7;apply in_list_head
664 |apply in_list_cons;(*FIXME*)generalize in match H6;intro;
666 [intros;destruct H10;destruct;apply in_list_head
667 |intros;destruct H12;apply in_list_cons;inversion H9
668 [intros;destruct H12;elim H7;reflexivity
669 |intros;destruct H14;
670 elim (in_list_append_to_or_in_list ? ? ? ? H11)
671 [apply in_list_to_in_list_append_r;assumption
672 |apply in_list_to_in_list_append_l;assumption]]]]]]
675 lemma inlist_fv_swap : \forall x,y,b,T.
676 (\lnot (in_list ? b (y::var_NTyp T))) \to
677 (in_list ? x (fv_NTyp (swap_NTyp b y T))) \to
678 (x \neq y \land (x = b \lor (in_list ? x (fv_NTyp T)))).
680 [simplify in H;simplify;simplify in H1;elim (decidable_eq_nat y n)
681 [rewrite > H2 in H1;rewrite > swap_right in H1;
683 [intros;destruct H4;split
684 [unfold;intro;apply H;rewrite > H2;apply in_list_head
686 |intros;destruct H6;elim (not_in_list_nil ? ? H3)]
687 |elim (decidable_eq_nat b n)
688 [rewrite > H3 in H;elim H;apply in_list_cons;apply in_list_head
689 |rewrite > swap_other in H1
692 [intros;destruct H5;intro;apply H2;
695 elim (not_in_list_nil ? ? H4)]
699 |simplify in H1;elim (not_in_list_nil ? ? H1)
700 |simplify;simplify in H3;simplify in H2;elim (nat_in_list_case ? ? ? H3)
706 |right;apply in_list_to_in_list_append_r;assumption]]
707 |intro;apply H2;elim (nat_in_list_case (var_NTyp n1) [y] ? H5)
708 [apply (in_list_to_in_list_append_r ? ? (y::var_NTyp n) (var_NTyp n1));
711 [intros;destruct H8;apply in_list_head
712 |intros;destruct H10;
713 elim (not_in_list_nil ? ? H7)]]
720 |right;apply in_list_to_in_list_append_l;assumption]]
721 |intro;apply H2;inversion H5
722 [intros;destruct H7;apply in_list_head
723 |intros;destruct H9;apply in_list_cons;
724 apply in_list_to_in_list_append_l;assumption]
726 |simplify;simplify in H3;simplify in H2;elim (nat_in_list_case ? ? ? H3)
732 |right;apply in_list_to_in_list_append_r;apply inlist_remove
734 |intro;elim (remove_inlist ? ? ? H4);apply H10;
737 |intro;rewrite > H8 in H7;rewrite > H11 in H7;apply H2;
738 destruct;apply in_list_cons;apply in_list_head
739 |destruct;assumption]]]]
740 |intro;apply H2;inversion H5
741 [intros;destruct H7;apply in_list_head
744 cut ((n::var_NTyp n1)@(var_NTyp n2) = n::var_NTyp n1@var_NTyp n2)
745 [rewrite < Hcut;elim (n::var_NTyp n1)
747 |simplify;elim (decidable_eq_nat b t)
748 [rewrite > H9;apply in_list_head
749 |apply in_list_cons;assumption]]
750 |simplify;reflexivity]]
751 |elim(remove_inlist ? ? ? H4);assumption]
757 |right;apply in_list_to_in_list_append_l;
759 |intro;apply H2;inversion H5
760 [intros;destruct H7;apply in_list_head
761 |intros;destruct H9;apply in_list_cons;
762 elim (decidable_eq_nat b n)
763 [rewrite > H8;apply in_list_head
764 |apply in_list_cons;apply in_list_to_in_list_append_l;
769 lemma inlist_fv_swap_r : \forall x,y,b,T.
770 (\lnot (in_list ? b (y::var_NTyp T))) \to
771 ((x = b \land (in_list ? y (fv_NTyp T))) \lor
772 (x \neq y \land (in_list ? x (fv_NTyp T)))) \to
773 (in_list ? x (fv_NTyp (swap_NTyp b y T))).
775 [simplify;simplify in H;simplify in H1;cut (b \neq n)
778 [rewrite > Hcut1;rewrite > swap_right;rewrite > H3;apply in_list_head
780 [intros;destruct H6;autobatch
781 |intros;destruct H8;elim (not_in_list_nil ? ? H5)]]
782 |elim H2;inversion H4
783 [intros;destruct H6;destruct;rewrite > (swap_other b y x)
787 |intros;destruct H8;elim (not_in_list_nil ? ? H5)]]
788 |intro;apply H;apply (in_list_to_in_list_append_r ? ? [y] [n]);
789 rewrite > H2;apply in_list_head]
790 |simplify in H1;elim H1;elim H2;elim (not_in_list_nil ? ? H4)
791 |simplify;simplify in H3;cut (\lnot (in_list ? b (y::var_NTyp n1)))
792 [cut (\lnot (in_list ? b (y::var_NTyp n)))
794 [elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
795 [apply in_list_to_in_list_append_l;apply H
797 |left;split;assumption]
798 |apply in_list_to_in_list_append_r;apply H1
800 |left;split;assumption]]
801 |elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
802 [apply in_list_to_in_list_append_l;apply H;
804 |right;split;assumption]
805 |apply in_list_to_in_list_append_r;apply H1
807 |right;split;assumption]]]
808 |intro;apply H2;inversion H4
809 [intros;destruct H6;apply in_list_head
810 |intros;destruct H8;apply in_list_cons;
811 simplify;apply in_list_to_in_list_append_l;
813 |intro;apply H2;inversion H4
814 [intros;destruct H6;apply in_list_head
815 |intros;destruct H8;apply in_list_cons;
816 simplify;apply in_list_to_in_list_append_r;
818 |simplify;simplify in H3;cut (\lnot (in_list ? b (y::var_NTyp n1)))
819 [cut (\lnot (in_list ? b (y::var_NTyp n2)))
821 [elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
822 [apply in_list_to_in_list_append_l;apply H
824 |left;split;assumption]
825 |apply in_list_to_in_list_append_r;apply inlist_remove
829 [assumption|elim (remove_inlist ? ? ? H7);assumption]]
830 |elim (remove_inlist ? ? ? H7);elim (decidable_eq_nat b n)
831 [rewrite > H10;rewrite > swap_left;intro;apply H9;
832 rewrite < H11;rewrite < H10;assumption
833 |rewrite > swap_other
834 [rewrite > H5;assumption
835 |intro;apply H10;symmetry;assumption
836 |intro;apply H9;symmetry;assumption]]]]
837 |elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
838 [apply in_list_to_in_list_append_l;apply H
840 |right;split;assumption]
841 |apply in_list_to_in_list_append_r;apply inlist_remove
845 [assumption|elim (remove_inlist ? ? ? H7);assumption]]
846 |elim (decidable_eq_nat b n)
847 [rewrite > H8;rewrite > swap_left;assumption
848 |elim (decidable_eq_nat y n)
849 [rewrite > H9;rewrite > swap_right;intro;apply Hcut1;
850 rewrite > H9;apply in_list_cons;
851 apply incl_fv_var;elim (remove_inlist ? ? ? H7);
852 rewrite < H10;assumption
853 |rewrite > (swap_other b y n)
854 [elim (remove_inlist ? ? ? H7);assumption
856 |intro;autobatch]]]]]]
857 |intro;apply H2;inversion H4
858 [intros;destruct H6;apply in_list_head
859 |simplify;intros;destruct H8;
861 apply (in_list_to_in_list_append_r ? ? (n::var_NTyp n1) (var_NTyp n2));
863 |intro;apply H2;inversion H4
864 [intros;destruct H6;apply in_list_head
865 |simplify;intros;destruct H8;
867 apply (in_list_to_in_list_append_l ? ? (n::var_NTyp n1) (var_NTyp n2));
868 apply in_list_cons;assumption]]]
871 lemma fv_alpha : \forall S,T.(alpha_eq S T) \to
872 (incl ? (fv_NTyp S) (fv_NTyp T)).
874 [unfold;intros;assumption
875 |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
876 [apply in_list_to_in_list_append_l;autobatch
877 |apply in_list_to_in_list_append_r;autobatch]
878 |simplify;unfold;intros;
879 elim (in_list_append_to_or_in_list ? ? ? ? H5)
880 [apply in_list_to_in_list_append_l;apply (H2 ? H6)
881 |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
882 apply in_list_to_in_list_append_r;
884 elim (remove_inlist ? ? ? H6);apply inlist_remove
885 [lapply (inlist_fv_swap_r x n4 a n1)
886 [elim (inlist_fv_swap x n5 a n3)
888 [rewrite < H12 in H7;elim H7;
889 do 2 apply in_list_cons;
890 apply in_list_to_in_list_append_l;
891 apply (incl_fv_var n1 ? H8);
893 |intro;apply H7;inversion H10;intros;destruct;
894 [apply in_list_cons;apply in_list_head
895 |do 2 apply in_list_cons;apply in_list_to_in_list_append_r;
897 |apply (Hletin ? Hletin1)]
898 |intro;apply H7;inversion H10
899 [intros;destruct H12;apply in_list_head
900 |intros;destruct H14;do 2 apply in_list_cons;
901 apply in_list_to_in_list_append_l;assumption]
902 |right;split;assumption]
903 |intros;intro;lapply (inlist_fv_swap_r x n4 a n1)
904 [lapply (Hletin ? Hletin1);
905 elim (inlist_fv_swap x n5 a n3 ? Hletin2)
907 |intro;apply H7;elim (decidable_eq_nat a n4)
908 [rewrite > H12;apply in_list_head
909 |apply in_list_cons;inversion H11;intros;destruct;
911 |apply in_list_cons;apply in_list_to_in_list_append_r;
913 |intro;apply H7;inversion H11
914 [intros;destruct H13;apply in_list_head
915 |intros;destruct H15;do 2 apply in_list_cons;
916 apply in_list_to_in_list_append_l;assumption]
917 |right;split;assumption]]]]
920 theorem alpha_to_encode : ∀S,T.(alpha_eq S T) →
921 ∀vars.(encodetype S vars) = (encodetype T vars).
924 |simplify;rewrite > H2;rewrite > H4;reflexivity
925 |simplify;rewrite > H2;
926 cut (encodetype n1 (n4::vars) = encodetype n3 (n5::vars))
927 [rewrite > Hcut;reflexivity
928 |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
929 lapply (encode_swap2 a n4 n1 ? (n4::vars))
930 [intro;apply H5;do 2 apply in_list_cons;
931 apply in_list_to_in_list_append_l;autobatch
932 |lapply (encode_swap2 a n5 n3 ? (n5::vars))
933 [intro;apply H5;do 2 apply in_list_cons;
934 apply in_list_to_in_list_append_r;autobatch
935 |rewrite > Hletin;rewrite > Hletin1;simplify;rewrite > swap_right;
936 rewrite > swap_right;rewrite > (H4 a H5 (a::swap_list a n4 vars));
937 rewrite > (fv_encode2 ? ? (a::swap_list a n5 vars))
939 |intros;elim (decidable_eq_nat n4 n5)
940 [rewrite > H7;autobatch
941 |cut ((x \neq n4) \land (x \neq n5))
942 [elim Hcut;elim (decidable_eq_nat x a)
943 [simplify;rewrite > (eq_to_eqb_true ? ? H10);simplify;
945 |simplify;rewrite > (not_eq_to_eqb_false ? ? H10);
948 |simplify;elim H11;rewrite < H12;
949 rewrite > H13;elim (decidable_eq_nat a t)
950 [rewrite > H14;rewrite > swap_left;
952 rewrite > (not_eq_to_eqb_false ? ? H8);
953 rewrite > (not_eq_to_eqb_false ? ? H9);
955 |elim (decidable_eq_nat n4 t)
956 [rewrite > H15;rewrite > swap_right;
957 rewrite > (swap_other a n5 t)
958 [rewrite > (not_eq_to_eqb_false ? ? H10);
960 rewrite > (not_eq_to_eqb_false ? ? H8);
963 |intro;apply H7;autobatch]
964 |rewrite > (swap_other a n4 t);
965 elim (decidable_eq_nat n5 t)
966 [rewrite < H16;rewrite > swap_right;
967 rewrite > (not_eq_to_eqb_false ? ? H9);
968 rewrite > (not_eq_to_eqb_false ? ? H10);
970 |rewrite > (swap_other a n5 t);try intro;
972 |*:intro;autobatch]]]]]
974 [lapply (H3 ? H5);lapply (alpha_sym ? ? Hletin2);
975 lapply (fv_alpha ? ? Hletin3);
976 lapply (Hletin4 ? H6);
977 elim (inlist_fv_swap ? ? ? ? ? Hletin5)
979 |intro;apply H5;inversion H8
980 [intros;destruct H10;
982 |intros;destruct H12;
983 do 2 apply in_list_cons;
984 apply in_list_to_in_list_append_l;assumption]]
985 |elim (inlist_fv_swap ? ? ? ? ? H6)
987 |intro;apply H5;elim (decidable_eq_nat a n4)
988 [rewrite > H9;apply in_list_head
990 inversion H8;intros;destruct;
993 apply in_list_to_in_list_append_r;
996 |apply in_list_head]]]
999 lemma encode_append : ∀T,U,n,l.length ? l ≤ n →
1000 subst_type_nat (encodetype T l) U n = encodetype T l.
1002 [simplify;elim (bool_to_decidable_eq (lookup n l) true)
1003 [rewrite > H1;simplify;lapply (lookup_in ? ? H1);
1004 lapply (posn_length ? ? Hletin);
1006 [rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;reflexivity
1007 |intro;rewrite > H2 in Hletin1;unfold in Hletin1;autobatch;]
1008 |cut (lookup n l = false)
1009 [rewrite > Hcut;reflexivity
1010 |generalize in match H1;elim (lookup n l);
1011 [elim H2;reflexivity|reflexivity]]]
1012 |simplify;reflexivity
1014 |simplify;rewrite > (H ? ? H2);rewrite > H1
1016 |simplify;autobatch]]
1019 lemma encode_subst_simple : ∀X,T,l.
1020 (encodetype T l = subst_type_nat (encodetype T (l@[X])) (TFree X) (length ? l)).
1022 [simplify;cut (lookup n l = true → posn l n = posn (l@[X]) n)
1023 [generalize in match Hcut;elim (bool_to_decidable_eq (lookup n l) true)
1024 [cut (lookup n (l@[X]) = true)
1025 [rewrite > H;rewrite > Hcut1;simplify;
1026 cut (eqb (posn (l@[X]) n) (length nat l) = false)
1027 [rewrite > Hcut2;simplify;rewrite < (H1 H);reflexivity
1028 |generalize in match H;elim l 0
1029 [simplify;intro;destruct H2
1030 |intros 2;simplify;elim (eqb n t)
1031 [simplify;reflexivity
1032 |simplify in H3;simplify;apply (H2 H3)]]]
1033 |generalize in match H;elim l
1034 [simplify in H2;destruct H2
1035 |generalize in match H3;simplify;elim (eqb n t) 0
1036 [simplify;intro;reflexivity
1037 |simplify;intro;apply (H2 H4)]]]
1038 |cut (lookup n l = false)
1039 [elim (decidable_eq_nat n X)
1040 [rewrite > Hcut1;rewrite > H2;cut (lookup X (l@[X]) = true)
1041 [rewrite > Hcut2;simplify;
1042 cut (eqb (posn (l@[X]) X) (length nat l) = true)
1043 [rewrite > Hcut3;simplify;reflexivity
1044 |generalize in match Hcut1;elim l 0
1045 [intros;simplify;rewrite > eqb_n_n;simplify;reflexivity
1046 |simplify;intros 2;rewrite > H2;elim (eqb X t)
1047 [simplify in H4;destruct H4
1048 |simplify;simplify in H4;apply (H3 H4)]]]
1050 [simplify;rewrite > eqb_n_n;reflexivity
1051 |simplify;elim (eqb X t)
1052 [simplify;reflexivity
1053 |simplify;assumption]]]
1054 |cut (lookup n l = lookup n (l@[X]))
1055 [rewrite < Hcut2;rewrite > Hcut1;simplify;reflexivity
1057 [simplify;rewrite > (not_eq_to_eqb_false ? ? H2);simplify;
1059 |simplify;elim (eqb n t)
1060 [simplify;reflexivity
1061 |simplify;assumption]]]]
1062 |generalize in match H;elim (lookup n l);
1063 [elim H2;reflexivity|reflexivity]]]
1065 [intro;simplify in H;destruct H
1066 |simplify;intros 2;elim (eqb n t)
1067 [simplify;reflexivity
1068 |simplify in H1;simplify;rewrite < (H H1);reflexivity]]]
1069 |simplify;reflexivity
1070 |simplify;rewrite < H;rewrite < H1;reflexivity
1071 |simplify;rewrite < H;rewrite < (append_associative ? [n] l [X]);
1072 rewrite < (H1 ([n]@l));reflexivity]
1075 lemma encode_subst : ∀T,X,Y,l.¬(X ∈ l) → ¬(Y ∈ l) →
1076 (X ∈ (fv_NTyp T) → X = Y) →
1077 encodetype (swap_NTyp X Y T) l =
1078 subst_type_nat (encodetype T (l@[Y])) (TFree X) (length ? l).
1079 apply NTyp_len_ind;intro;elim U
1080 [elim (decidable_eq_nat n X)
1081 [rewrite > H4 in H3;rewrite > H4;rewrite > H3
1082 [simplify in \vdash (? ? (? % ?) ?);rewrite > swap_same;
1083 cut (lookup Y (l@[Y]) = true)
1084 [simplify;rewrite > Hcut;rewrite > (not_nat_in_to_lookup_false ? ? H2);
1085 simplify;cut (posn (l@[Y]) Y = length ? l)
1086 [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
1087 |generalize in match H2;elim l;simplify
1088 [rewrite > eqb_n_n;reflexivity
1089 |elim (decidable_eq_nat Y t)
1090 [elim H6;rewrite > H7;apply in_list_head
1091 |rewrite > (not_eq_to_eqb_false ? ? H7);simplify;
1094 |intro;apply H6;apply in_list_cons;assumption]]]]
1096 [simplify;rewrite > eqb_n_n;reflexivity
1097 |simplify;rewrite > H5;elim (eqb Y t);reflexivity]]
1098 |simplify;apply in_list_head]
1099 |elim (decidable_eq_nat Y n);
1100 [rewrite < H5;simplify;rewrite > swap_right;
1101 rewrite > (not_nat_in_to_lookup_false ? ? H1);
1102 cut (lookup Y (l@[Y]) = true)
1103 [rewrite > Hcut;simplify;cut (posn (l@[Y]) Y = length ? l)
1104 [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
1105 |generalize in match H2;elim l;simplify
1106 [rewrite > eqb_n_n;reflexivity
1107 |elim (decidable_eq_nat Y t)
1108 [elim H7;rewrite > H8;apply in_list_head
1109 |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;
1112 |intro;apply H7;apply in_list_cons;assumption]]]]
1114 [rewrite > eqb_n_n;reflexivity
1115 |elim (eqb Y t);simplify;autobatch]]
1116 |simplify;rewrite > (swap_other X Y n)
1117 [cut (lookup n l = lookup n (l@[Y]) ∧
1118 (lookup n l = true → posn l n = posn (l@[Y]) n))
1119 [elim Hcut;rewrite > H6;generalize in match H7;
1120 generalize in match H6;elim (lookup n (l@[Y]))
1121 [simplify;rewrite < H9;generalize in match H8;elim l
1122 [simplify in H10;destruct H10
1123 |elim (decidable_eq_nat n t)
1124 [simplify;rewrite > (eq_to_eqb_true ? ? H12);simplify;
1126 |simplify;rewrite > (not_eq_to_eqb_false ? ? H12);
1127 simplify;generalize in match H10;
1128 elim (eqb (posn l1 n) (length nat l1))
1129 [simplify in H13;simplify in H11;
1130 rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
1131 simplify in H11;lapply (H13 H11);destruct Hletin
1132 |simplify;reflexivity]]
1135 |simplify;reflexivity]
1137 [simplify;cut (n ≠ Y)
1138 [rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;
1140 |intro;apply H5;symmetry;assumption]
1141 |intro;simplify in H6;destruct H6
1142 |elim H6;simplify;rewrite < H7;reflexivity
1143 |simplify;elim (eqb n t)
1144 [simplify;reflexivity
1145 |simplify;simplify in H7;elim H6;rewrite < (H9 H7);
1148 |intro;apply H5;symmetry;assumption]]]
1149 |simplify;reflexivity
1150 |simplify;rewrite < (H2 n ? ? ? ? H3 H4)
1151 [rewrite < (H2 n1 ? ? ? ? H3 H4);
1152 [autobatch|autobatch
1153 |intro;apply H5;simplify;apply in_list_to_in_list_append_r;assumption]
1155 |intro;apply H5;simplify;apply in_list_to_in_list_append_l;assumption]
1156 |simplify;rewrite < (H2 n1 ? ? ? ? H3 H4)
1157 [cut (l = swap_list X Y l)
1158 [|generalize in match H3;generalize in match H4;elim l
1159 [simplify;reflexivity
1160 |simplify;elim (decidable_eq_nat t X)
1161 [elim H8;rewrite > H9;apply in_list_head
1162 |elim (decidable_eq_nat t Y)
1163 [elim H7;rewrite > H10;apply in_list_head
1164 |rewrite > (swap_other X Y t)
1167 |intro;apply H7;apply in_list_cons;assumption
1168 |intro;apply H8;apply in_list_cons;assumption]
1170 elim (decidable_eq_nat n Y)
1171 [rewrite > H6;rewrite > (fv_encode (swap_NTyp X Y n2) (swap X Y Y::l)
1172 (swap_list X Y (Y::l)));
1173 [rewrite < (encode_swap X Y n2);
1174 [rewrite < (fv_encode ? (Y::l) (Y::l@[Y]))
1175 [rewrite > encode_append;
1176 [rewrite < (fv_encode n2 (Y::l) (Y::l@[Y]));
1178 |intros;elim (decidable_eq_nat x Y)
1179 [rewrite > H8;simplify;rewrite > eqb_n_n;simplify;
1180 split [reflexivity|intro;reflexivity]
1181 |simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
1183 [simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
1184 simplify;split [reflexivity|intro;destruct H9]
1185 |elim H9;simplify;elim (eqb x t)
1186 [simplify;split [reflexivity|intro;reflexivity]
1187 |simplify;rewrite < H10;generalize in match H11;
1191 |intro;rewrite < (H12 H13);reflexivity]
1192 |split [reflexivity|intro;destruct H13]]]]]]
1193 |simplify;constructor 1]
1194 |intros;simplify;elim (decidable_eq_nat x Y)
1195 [rewrite > (eq_to_eqb_true ? ? H8);simplify;split
1196 [reflexivity|intro;reflexivity]
1197 |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;elim l
1198 [simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
1199 simplify;split [reflexivity|intro;destruct H9]
1200 |simplify;elim (eqb x t)
1201 [simplify;split [reflexivity|intro;reflexivity]
1202 |simplify;elim H9;split
1204 |intro;rewrite < (H11 H12);reflexivity]]]]]
1205 |intro;elim (decidable_eq_nat X Y)
1206 [rewrite > H8;apply in_list_head
1207 |elim H8;apply H5;simplify;apply in_list_to_in_list_append_r;
1208 rewrite > H6;apply (in_remove ? ? ? H8 H7)]
1209 |apply in_list_head]
1210 |intros;simplify;rewrite > swap_right;rewrite < Hcut;
1211 split [reflexivity|intro;reflexivity]]
1212 |rewrite < Hcut;elim (decidable_eq_nat n X)
1213 [rewrite > H7;rewrite > (fv_encode (swap_NTyp X Y n2) (swap X Y X::l)
1214 (swap_list X Y (X::l)))
1215 [rewrite > (encode_swap X Y n2);
1217 cut (swap X Y X::swap_list X Y (l@[Y]) =
1218 (swap X Y X::swap_list X Y l)@[X])
1219 [rewrite > Hcut1;cut (S (length ? l) = (length ? (swap X Y X::swap_list X Y l)))
1220 [rewrite > Hcut2;rewrite < (encode_subst_simple X
1221 (swap_NTyp X Y n2) (swap X Y X::swap_list X Y l));
1225 |simplify;rewrite < H8;reflexivity]]
1227 [simplify;rewrite > swap_right;reflexivity
1228 |simplify;destruct H8;rewrite > Hcut1;reflexivity]]
1229 |intro;apply in_list_head
1230 |apply in_list_cons;elim l
1231 [simplify;apply in_list_head
1232 |simplify;apply in_list_cons;assumption]]
1233 |intros;simplify;rewrite < Hcut;
1234 split [reflexivity|intro;reflexivity]]
1235 |rewrite > (swap_other X Y n)
1236 [rewrite < (append_associative ? [n] l [Y]);
1237 cut (S (length nat l) = length nat (n::l)) [|reflexivity]
1238 rewrite > Hcut1;rewrite < (H2 n2);
1241 |intro;apply H7;inversion H8;intros
1242 [destruct H10;reflexivity
1243 |destruct H12;destruct;elim (H3 H9)]
1244 |intro;apply H6;inversion H8;intros
1245 [destruct H10;reflexivity
1246 |destruct H12;destruct;elim (H4 H9)]
1247 |intro;apply H5;simplify;apply in_list_to_in_list_append_r;
1248 apply (in_remove ? ? ? ? H8);intro;apply H7;symmetry;assumption]
1251 |intro;apply H5;simplify;apply in_list_to_in_list_append_l;assumption]]
1254 lemma swap_case: ∀u,v,x.(swap u v x) = u ∨ (swap u v x) = v ∨ (swap u v x = x).
1255 intros.unfold in match swap.simplify.elim (eqb x u)
1257 |simplify;elim (eqb x v);simplify;autobatch]
1260 lemma in_fvNTyp_in_fvNenv : ∀G,T.(NWFType G T) → (incl ? (fv_NTyp T) (fv_Nenv G)).
1262 [simplify;unfold;intros;inversion H2;intros
1263 [destruct H4;assumption
1264 |destruct H6;elim (not_in_list_nil ? ? H3)]
1265 |simplify;unfold;intros;elim (not_in_list_nil ? ? H1)
1266 |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
1267 [apply (H2 ? H6)|apply (H4 ? H6)]
1268 |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
1269 [apply H2;assumption
1270 |elim (fresh_name (x::fv_Nenv l@var_NTyp n2));lapply (H4 a)
1271 [cut (a ≠ x ∧ x ≠ n)
1272 [elim Hcut;lapply (Hletin x)
1273 [simplify in Hletin1;inversion Hletin1;intros;
1274 [destruct H11;elim H8;reflexivity
1275 |destruct H13;assumption]
1276 |generalize in match H6;generalize in match H7;elim n2
1277 [simplify in H11;elim (decidable_eq_nat n n3)
1278 [rewrite > (eq_to_eqb_true ? ? H12) in H11;simplify in H11;
1279 elim (not_in_list_nil ? ? H11)
1280 |rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
1281 simplify in H11;inversion H11;intros
1282 [destruct H14;simplify;
1283 rewrite > swap_other
1285 |intro;apply H8;rewrite > H13;reflexivity
1286 |intro;apply H9;rewrite > H13;reflexivity]
1287 |destruct H16;elim (not_in_list_nil ? ? H13)]]
1288 |simplify in H11;elim (not_in_list_nil ? ? H11)
1289 |simplify in H13;simplify;elim (remove_inlist ? ? ? H13);
1290 elim (in_list_append_to_or_in_list ? ? ? ? H14)
1291 [apply in_list_to_in_list_append_l;apply H10
1292 [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n4));
1293 intro;apply H12;simplify;
1294 rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4));
1295 elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3) H17);
1296 [apply in_list_to_in_list_append_l;assumption
1297 |apply in_list_to_in_list_append_r;
1298 apply in_list_to_in_list_append_l;assumption]
1299 |apply (in_remove ? ? ? H15 H16)]
1300 |apply in_list_to_in_list_append_r;apply H11
1301 [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3));
1302 intro;apply H12;simplify;
1303 rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4));
1304 elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n4) H17);
1305 [apply in_list_to_in_list_append_l;assumption
1306 |apply in_list_to_in_list_append_r;
1307 apply in_list_to_in_list_append_r;assumption]
1308 |apply (in_remove ? ? ? H15 H16)]]
1309 |simplify;simplify in H13;elim (remove_inlist ? ? ? H13);
1310 elim (nat_in_list_case ? ? ? H14);
1311 [apply in_list_to_in_list_append_r;apply in_remove;
1312 [elim (remove_inlist ? ? ? H16);intro;apply H18;
1313 elim (swap_case a n n3)
1315 [elim H8;symmetry;rewrite < H21;assumption
1316 |elim H9;rewrite < H21;assumption]
1317 |rewrite < H20;assumption]
1319 [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n5));
1320 intro;apply H12;simplify;
1321 rewrite < (append_associative ? [x] (fv_Nenv l) (n3::var_NTyp n4 @ var_NTyp n5));
1322 elim (nat_in_list_case ? ? ? H17)
1323 [apply in_list_to_in_list_append_r;
1325 apply in_list_to_in_list_append_r;assumption
1326 |apply in_list_to_in_list_append_l;assumption]
1327 |elim (remove_inlist ? ? ? H16);apply in_remove
1330 |apply in_list_to_in_list_append_l;apply H10;
1331 [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n4));
1332 intro;apply H12;simplify;
1333 rewrite < (append_associative ? [x] (fv_Nenv l) (n3::var_NTyp n4@var_NTyp n5));
1334 elim (nat_in_list_case ? ? ? H17)
1335 [apply in_list_to_in_list_append_r;apply in_list_cons;
1336 apply in_list_to_in_list_append_l;assumption
1337 |apply in_list_to_in_list_append_l;assumption]
1338 |apply in_remove;assumption]]]]
1340 [intro;apply H7;rewrite > H8;apply in_list_head
1341 |elim (remove_inlist ? ? ? H6);assumption]]
1342 |intro;apply H7;apply in_list_cons;apply in_list_to_in_list_append_l;
1344 |right;intro;apply H7;apply in_list_cons;
1345 apply in_list_to_in_list_append_r;apply (incl_fv_var ? ? H8)]]]
1348 lemma fv_NTyp_fv_Typ : ∀T,X,l.(X ∈ (fv_NTyp T)) → ¬(X ∈ l) →
1349 (X ∈ (fv_type (encodetype T l))).
1351 [simplify;simplify in H;cut (X = n)
1352 [rewrite < Hcut;generalize in match (lookup_in X l);elim (lookup X l)
1353 [elim H1;apply H2;reflexivity
1354 |simplify;apply in_list_head]
1355 |(*FIXME*)generalize in match H;intro;inversion H;intros;
1356 [destruct H4;reflexivity
1357 |destruct H6;elim (not_in_list_nil ? ? H3)]]
1358 |simplify in H;elim (not_in_list_nil ? ? H)
1359 |simplify;simplify in H2;
1360 elim (in_list_append_to_or_in_list ? ? ? ? H2);
1361 [apply in_list_to_in_list_append_l;apply (H ? H4 H3)
1362 |apply in_list_to_in_list_append_r;apply (H1 ? H4 H3)]
1363 |simplify;simplify in H2;
1364 elim (in_list_append_to_or_in_list ? ? ? ? H2)
1365 [apply in_list_to_in_list_append_l;apply (H ? H4 H3)
1366 |apply in_list_to_in_list_append_r;
1367 elim (remove_inlist ? ? ? H4);apply (H1 ? H5);intro;apply H6;
1369 [destruct H9;reflexivity
1370 |destruct H11;elim (H3 H8)]]]
1373 lemma adeq_WFT : ∀G,T.NWFType G T → WFType (encodeenv G) (encodetype T []).
1375 [simplify;apply WFT_TFree;rewrite < eq_fv_Nenv_fv_env;assumption
1376 |simplify;apply WFT_Top;
1377 |simplify;apply WFT_Arrow;assumption
1378 |simplify;apply WFT_Forall
1380 |intros;rewrite < (encode_subst n2 X n []);
1381 [simplify in H4;apply H4
1382 [rewrite > (eq_fv_Nenv_fv_env l);assumption
1383 |elim (decidable_eq_nat X n)
1385 |right;intro;apply H6;apply (fv_NTyp_fv_Typ ? ? ? H8);intro;
1386 apply H7;inversion H9;intros
1387 [destruct H11;reflexivity
1389 elim (not_in_list_nil ? ? H10)]]]
1390 |4:intro;elim (decidable_eq_nat X n)
1392 |elim H6;cut (¬(X ∈ [n]))
1393 [generalize in match Hcut;generalize in match [n];
1394 generalize in match H7;elim n2
1395 [simplify in H9;generalize in match H9;intro;inversion H9;intros;
1396 [destruct H13;destruct;simplify;
1397 generalize in match (lookup_in X l1);elim (lookup X l1)
1398 [elim H10;apply H12;reflexivity
1399 |simplify;apply in_list_head]
1401 elim (not_in_list_nil ? ? H12)]
1402 |simplify in H9;elim (not_in_list_nil ? ? H9)
1403 |simplify;simplify in H11;
1404 elim (in_list_append_to_or_in_list ? ? ? ? H11);autobatch
1405 |simplify;simplify in H11;
1406 elim (in_list_append_to_or_in_list ? ? ? ? H11);
1408 |elim (remove_inlist ? ? ? H13);
1409 apply in_list_to_in_list_append_r;
1411 intro;inversion H16;intros;
1412 [destruct H18;destruct;elim H15;reflexivity
1413 |destruct H20;elim H12;assumption]]]
1414 |intro;elim H8;inversion H9;intros
1415 [destruct H11;autobatch
1416 |destruct H13;elim (not_in_list_nil ? ? H10)]]]
1417 |*:apply not_in_list_nil]]]
1420 lemma not_in_list_encodetype : \forall T,l,x.in_list ? x l \to
1421 \lnot (in_list ? x (fv_type (encodetype T l))).
1422 intro;elim T;simplify
1423 [apply (bool_elim ? (lookup n l));intro
1424 [simplify;apply not_in_list_nil
1425 |simplify;intro;inversion H2;intros
1427 rewrite > (in_lookup ? ? H) in H1;destruct H1
1428 |destruct H6;apply (not_in_list_nil ? ? H3)]]
1429 |apply not_in_list_nil
1430 |intro;elim (nat_in_list_case ? ? ? H3)
1431 [apply H1;assumption
1432 |apply H;assumption]
1433 |intro;elim (nat_in_list_case ? ? ? H3)
1434 [apply (H1 (n::l) x ? H4);apply in_list_cons;assumption
1435 |apply H;assumption]]
1438 lemma incl_fv_encode_fv : \forall T,l.incl ? (fv_type (encodetype T l)) (fv_NTyp T).
1439 intro;elim T;simplify;unfold;
1440 [intro;elim (lookup n l)
1441 [simplify in H;elim (not_in_list_nil ? ? H)
1442 |simplify in H;assumption]
1443 |intros;elim (not_in_list_nil ? ? H)
1444 |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
1445 [apply in_list_to_in_list_append_l;apply H;autobatch
1446 |apply in_list_to_in_list_append_r;apply H1;autobatch]
1447 |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
1448 [apply in_list_to_in_list_append_l;apply H;autobatch
1449 |apply in_list_to_in_list_append_r;apply in_remove
1450 [intro;apply (not_in_list_encodetype n2 (n::l) x)
1451 [rewrite > H4;apply in_list_head
1453 |apply (H1 (n::l));assumption]]]
1456 lemma adeq_WFT2 : ∀G1,T1.WFType G1 T1 →
1457 ∀G2,T2.G1 = encodeenv G2 → T1 = encodetype T2 [] →
1460 [rewrite > H2 in H1;rewrite < eq_fv_Nenv_fv_env in H1;
1462 [|generalize in match H3;elim T2
1463 [simplify in H4;destruct H4;reflexivity
1464 |simplify in H4;destruct H4
1465 |simplify in H6;destruct H6
1466 |simplify in H6;destruct H6]]
1467 rewrite > Hcut;apply NWFT_TName;assumption
1469 [|generalize in match H2;elim T2
1470 [simplify in H3;destruct H3
1472 |simplify in H5;destruct H5
1473 |simplify in H5;destruct H5]]
1474 rewrite > Hcut;apply NWFT_Top;
1475 |cut (∃U,V.T2 = (NArrow U V))
1476 [|generalize in match H6;elim T2
1477 [1,2:simplify in H7;destruct H7
1478 |apply (ex_intro ? ? n);apply (ex_intro ? ? n1);reflexivity
1479 |simplify in H9;destruct H9]]
1480 elim Hcut;elim H7;rewrite > H8 in H6;simplify in H6;destruct H6;
1481 apply NWFT_Arrow;autobatch
1482 |cut (\exists Z,U,V.T2 = NForall Z U V)
1483 [|generalize in match H6;elim T2
1484 [1,2:simplify in H7;destruct H7
1485 |simplify in H9;destruct H9
1486 |apply (ex_intro ? ? n);apply (ex_intro ? ? n1);
1487 apply (ex_intro ? ? n2);reflexivity]]
1488 elim Hcut;elim H7;elim H8;clear Hcut H7 H8;rewrite > H9;
1489 rewrite > H9 in H6;simplify in H6;destruct H6;apply NWFT_Forall
1492 [rewrite > H7;cut (swap_NTyp a a a2 = a2)
1494 [rewrite > swap_same;reflexivity
1496 |rewrite > H8;rewrite > H9;reflexivity
1497 |rewrite > swap_same;rewrite > H8;rewrite > H9;reflexivity]]
1498 rewrite > Hcut;apply (H4 Y)
1499 [rewrite < eq_fv_Nenv_fv_env;assumption
1500 |rewrite > H7;apply not_in_list_encodetype;
1502 |rewrite > H7;simplify;rewrite < Hcut;reflexivity
1503 |rewrite > H7;autobatch]
1505 [rewrite < eq_fv_Nenv_fv_env;assumption
1506 |intro;apply H7;apply incl_fv_encode_fv;autobatch
1507 |simplify;reflexivity
1508 |symmetry;apply (encode_subst a2 Y a []);
1509 [3:intro;elim (H7 H8)
1513 lemma adeq_WFE : ∀G.NWFEnv G → WFEnv (encodeenv G).
1515 [simplify;apply WFE_Empty
1516 |simplify;apply WFE_cons;
1517 [2:rewrite < eq_fv_Nenv_fv_env;]
1521 lemma NWFT_env_incl : ∀G,T.NWFType G T → ∀H.incl ? (fv_Nenv G) (fv_Nenv H)
1524 [apply NWFT_TName;apply (H3 ? H1)
1531 |intros;apply (H4 ? ? H8);
1532 [intro;apply H7;apply (H6 ? H9)
1533 |unfold;intros;simplify;simplify in H9;inversion H9;intros
1534 [destruct H11;apply in_list_head
1535 |destruct H13;apply in_list_cons;apply (H6 ? H10)]]]]
1538 lemma NJSubtype_to_NWFT : ∀G,T,U.NJSubtype G T U → NWFType G T ∧ NWFType G U.
1540 [split [assumption|apply NWFT_Top]
1541 |split;apply NWFT_TName;assumption
1543 [apply NWFT_TName;generalize in match H1;elim l
1544 [elim (not_in_list_nil ? ? H6)
1545 |inversion H7;intros
1546 [rewrite < H8;simplify;apply in_list_head
1547 |destruct H11;elim t;simplify;apply in_list_cons;
1548 apply H6;assumption]]
1550 |elim H2;elim H4;split;apply NWFT_Arrow;assumption
1551 |elim H2;split;apply NWFT_Forall
1553 |*:intros;elim (H4 Y H7);
1554 [apply (NWFT_env_incl ? ? H9);unfold;simplify;intros;inversion H11;intros
1555 [destruct H13;apply in_list_head
1556 |destruct H15;apply in_list_cons;assumption]
1559 [lapply (adeq_WFT ? ? H5);apply (adeq_WFT2 ? ? Hletin);autobatch
1560 |lapply (adeq_WFT ? ? H6);apply (adeq_WFT2 ? ? Hletin);autobatch]]
1563 theorem adequacy : ∀G,T,U.NJSubtype G T U →
1564 JSubtype (encodeenv G) (encodetype T []) (encodetype U []).
1565 intros;elim H;simplify
1568 [apply (adeq_WFE ? H1)|rewrite < eq_fv_Nenv_fv_env;assumption]
1571 |intros;lapply (NSA_All ? ? ? ? ? ? H1 H3);rewrite < (encode_subst n2 X n [])
1572 [rewrite < (encode_subst n4 X n [])
1573 [rewrite < eq_fv_Nenv_fv_env in H5;apply (H4 ? H5)
1574 |2,3:apply not_in_list_nil
1575 |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);
1576 lapply (in_fvNTyp_in_fvNenv ? ? H8);simplify in Hletin1;
1577 elim (decidable_eq_nat X n)
1579 |lapply (in_remove ? ? ? H9 H6);elim H5;rewrite < eq_fv_Nenv_fv_env;
1580 apply Hletin1;apply in_list_to_in_list_append_r;assumption]]
1581 |2,3:apply not_in_list_nil
1582 |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);lapply (in_fvNTyp_in_fvNenv ? ? H7);
1583 simplify in Hletin1;elim (decidable_eq_nat X n)
1585 |lapply (in_remove ? ? ? H9 H6);elim H5;rewrite < eq_fv_Nenv_fv_env;
1586 apply Hletin1;apply in_list_to_in_list_append_r;assumption]]]
1587 |rewrite < (alpha_to_encode ? ? H3);rewrite < (alpha_to_encode ? ? H4);