--- /dev/null
+
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "logic/equality.ma".
+include "nat/nat.ma".
+include "datatypes/bool.ma".
+include "list/list.ma".
+include "nat/compare.ma".
+include "Fsub/util.ma".
+include "Fsub/defn.ma".
+
+inductive NTyp : Set \def
+| TName : nat \to NTyp
+| NTop : NTyp
+| NArrow : NTyp \to NTyp \to NTyp
+| NForall : nat \to NTyp \to NTyp \to NTyp.
+
+(*inductive NTerm : Set \def
+| Name : nat \to NTerm
+| NAbs : nat \to NTyp \to NTerm \to NTerm
+| NApp : NTerm \to NTerm \to NTerm
+| NTAbs : nat \to NTyp \to NTerm \to NTerm
+| NTApp : NTerm \to NTyp \to NTerm.*)
+
+(*inductive LNTyp: nat \to Set \def
+| LNTVar : \forall m,n.(m < n) \to LNTyp n
+| LNTFree : \forall n.nat \to LNTyp n
+| LNTop : \forall n.LNTyp n
+| LNArrow : \forall n.(LNTyp n) \to (LNTyp n) \to (LNTyp n)
+| LNForall : \forall n.(LNTyp n) \to (LNTyp (S n)) \to (LNTyp n).
+
+inductive LNTerm : nat \to Set \def
+| LNVar : \forall m,n.(m < n) \to LNTerm n
+| LNFree : \forall n.nat \to LNTerm n
+| LNAbs : \forall n.(LNTyp n) \to (LNTerm (S n)) \to (LNTerm n)
+| LNApp : \forall n.(LNTerm n) \to (LNTerm n) \to (LNTerm n)
+| LNTAbs : \forall n.(LNTyp n) \to (LNTerm (S n)) \to (LNTerm n)
+| LNTApp : \forall n.(LNTerm n) \to (LNTyp n) \to (LNTerm n).*)
+
+record nbound : Set \def {
+ nistype : bool;
+ nname : nat;
+ nbtype : NTyp
+ }.
+
+(*record lnbound (n:nat) : Set \def {
+ lnistype : bool;
+ lnname : nat;
+ lnbtype : LNTyp n
+ }.*)
+
+inductive option (A:Type) : Set \def
+| Some : A \to option A
+| None : option A.
+
+(*definition S_opt : (option nat) \to (option nat) \def
+ \lambda n.match n with
+ [ (Some n) \Rightarrow (Some nat (S n))
+ | None \Rightarrow None nat].*)
+
+(* position of the first occurrence of nat x in list l
+ returns (length l) when x not in l *)
+
+definition swap : nat \to nat \to nat \to nat \def
+ \lambda u,v,x.match (eqb x u) with
+ [true \Rightarrow v
+ |false \Rightarrow match (eqb x v) with
+ [true \Rightarrow u
+ |false \Rightarrow x]].
+
+axiom swap_left : \forall x,y.(swap x y x) = y.
+(*intros;unfold swap;rewrite > eqb_n_n;simplify;reflexivity;
+qed.*)
+
+axiom swap_right : \forall x,y.(swap x y y) = x.
+(*intros;unfold swap;elim (eq_eqb_case y x)
+ [elim H;rewrite > H2;simplify;rewrite > H1;reflexivity
+ |elim H;rewrite > H2;simplify;rewrite > eqb_n_n;simplify;reflexivity]
+qed.*)
+
+axiom swap_other : \forall x,y,z.(z \neq x) \to (z \neq y) \to (swap x y z) = z.
+(*intros;unfold swap;elim (eq_eqb_case z x)
+ [elim H2;lapply (H H3);elim Hletin
+ |elim H2;rewrite > H4;simplify;elim (eq_eqb_case z y)
+ [elim H5;lapply (H1 H6);elim Hletin
+ |elim H5;rewrite > H7;simplify;reflexivity]]
+qed.*)
+
+axiom swap_inv : \forall u,v,x.(swap u v (swap u v x)) = x.
+(*intros;unfold in match (swap u v x);elim (eq_eqb_case x u)
+ [elim H;rewrite > H2;simplify;rewrite > H1;apply swap_right
+ |elim H;rewrite > H2;simplify;elim (eq_eqb_case x v)
+ [elim H3;rewrite > H5;simplify;rewrite > H4;apply swap_left
+ |elim H3;rewrite > H5;simplify;apply (swap_other ? ? ? H1 H4)]]
+qed.*)
+
+axiom swap_inj : \forall u,v,x,y.(swap u v x) = (swap u v y) \to x = y.
+(*intros;unfold swap in H;elim (eq_eqb_case x u)
+ [elim H1;elim (eq_eqb_case y u)
+ [elim H4;rewrite > H5;assumption
+ |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
+ elim (eq_eqb_case y v)
+ [elim H7;rewrite > H9 in H;simplify in H;rewrite > H in H8;
+ lapply (H5 H8);elim Hletin
+ |elim H7;rewrite > H9 in H;simplify in H;elim H8;symmetry;assumption]]
+ |elim H1;elim (eq_eqb_case y u)
+ [elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
+ elim (eq_eqb_case x v)
+ [elim H7;rewrite > H9 in H;simplify in H;rewrite < H in H8;
+ elim H2;assumption
+ |elim H7;rewrite > H9 in H;simplify in H;elim H8;assumption]
+ |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
+ elim (eq_eqb_case x v)
+ [elim H7;rewrite > H9 in H;elim (eq_eqb_case y v)
+ [elim H10;rewrite > H11;assumption
+ |elim H10;rewrite > H12 in H;simplify in H;elim H5;symmetry;
+ assumption]
+ |elim H7;rewrite > H9 in H;elim (eq_eqb_case y v)
+ [elim H10;rewrite > H12 in H;simplify in H;elim H2;assumption
+ |elim H10;rewrite > H12 in H;simplify in H;assumption]]]]
+qed.*)
+
+let rec swap_NTyp u v T on T \def
+ match T with
+ [(TName X) \Rightarrow (TName (swap u v X))
+ |NTop \Rightarrow NTop
+ |(NArrow T1 T2) \Rightarrow (NArrow (swap_NTyp u v T1) (swap_NTyp u v T2))
+ |(NForall X T1 T2) \Rightarrow
+ (NForall (swap u v X) (swap_NTyp u v T1) (swap_NTyp u v T2))].
+
+let rec swap_Typ u v T on T \def
+ match T with
+ [(TVar n) \Rightarrow (TVar n)
+ |(TFree X) \Rightarrow (TFree (swap u v X))
+ |Top \Rightarrow Top
+ |(Arrow T1 T2) \Rightarrow (Arrow (swap_Typ u v T1) (swap_Typ u v T2))
+ |(Forall T1 T2) \Rightarrow (Forall (swap_Typ u v T1) (swap_Typ u v T2))].
+
+definition swap_list : nat \to nat \to (list nat) \to (list nat) ≝
+ \lambda u,v,l.(map ? ? (swap u v) l).
+
+let rec var_NTyp (T:NTyp):list nat\def
+ match T with
+ [TName x ⇒ [x]
+ |NTop ⇒ []
+ |NArrow U V ⇒ (var_NTyp U)@(var_NTyp V)
+ |NForall X U V ⇒ X::(var_NTyp U)@(var_NTyp V)].
+
+inductive alpha_eq : NTyp \to NTyp \to Prop \def
+| A_refl : \forall T.(alpha_eq T T)
+| A_arrow : \forall T1,T2,U1,U2.(alpha_eq T1 U1) \to (alpha_eq T2 U2) \to
+ (alpha_eq (NArrow T1 T2) (NArrow U1 U2))
+| A_forall : \forall T1,T2,U1,U2,X,Y.
+ (alpha_eq T1 U1) \to
+ (\forall Z.
+ \lnot (in_list nat Z (X::Y::((var_NTyp T2)@(var_NTyp U2))))
+ \to (alpha_eq (swap_NTyp Z X T2) (swap_NTyp Z Y U2))) \to
+ (alpha_eq (NForall X T1 T2) (NForall Y U1 U2)).
+
+let rec posn l x on l \def
+ match l with
+ [ nil \Rightarrow O
+ | (cons (y:nat) l2) \Rightarrow
+ match (eqb x y) with
+ [ true \Rightarrow O
+ | false \Rightarrow S (posn l2 x)]].
+
+let rec length A l on l \def
+ match l with
+ [ nil \Rightarrow O
+ | (cons (y:A) l2) \Rightarrow S (length A l2)].
+
+let rec lookup n l on l \def
+ match l with
+ [ nil ⇒ false
+ | cons (x:nat) l1 \rArr match (eqb n x) with
+ [true \rArr true
+ |false \rArr (lookup n l1)]].
+
+let rec encodetype T vars on T \def
+ match T with
+ [ (TName n) ⇒ match (lookup n vars) with
+ [ true ⇒ (TVar (posn vars n))
+ | false ⇒ (TFree n)]
+ | NTop ⇒ Top
+ | (NArrow T1 T2) ⇒ Arrow (encodetype T1 vars) (encodetype T2 vars)
+ | (NForall n2 T1 T2) ⇒ Forall (encodetype T1 vars)
+ (encodetype T2 (n2::vars))].
+
+let rec head (A:Type) l on l \def
+ match l with
+ [ nil \Rightarrow None A
+ | (cons (x:A) l2) \Rightarrow Some A x].
+
+let rec tail (A:Type) l \def
+ match l with
+ [ nil \Rightarrow nil A
+ | (cons (x:A) l2) \Rightarrow l2].
+
+let rec nth n l on n \def
+ match n with
+ [ O \Rightarrow match l with
+ [ nil ⇒ O
+ | (cons x l2) ⇒ x]
+ | (S n2) \Rightarrow (nth n2 (tail ? l))].
+
+definition max_list : (list nat) \to nat \def
+ \lambda l.let rec aux l0 m on l0 \def
+ match l0 with
+ [ nil ⇒ m
+ | (cons n l2) ⇒ (aux l2 (max m n))]
+ in aux l O.
+
+let rec decodetype T vars C on T \def
+ match T with
+ [ (TVar n) ⇒ (TName (nth n vars))
+ | (TFree x) ⇒ (TName x)
+ | Top \Rightarrow NTop
+ | (Arrow T1 T2) ⇒ (NArrow (decodetype T1 vars C) (decodetype T2 vars C))
+ | (Forall T1 T2) ⇒ (NForall (S (max_list (vars@C))) (decodetype T1 vars C)
+ (decodetype T2 ((S (max_list (vars@C)))::vars) C))].
+
+definition sublist: \forall A:Type.(list A) \to (list A) \to Prop \def
+ \lambda A,l1,l2.\forall x.(in_list ? x l1) \to (in_list ? x l2).
+
+let rec remove_nat (x:nat) (l:list nat) on l \def
+ match l with
+ [ nil ⇒ (nil nat)
+ | (cons y l2) ⇒ match (eqb x y) with
+ [ true ⇒ (remove_nat x l2)
+ | false ⇒ (y :: (remove_nat x l2)) ]].
+
+let rec fv_NTyp (T:NTyp):list nat\def
+ match T with
+ [TName x ⇒ [x]
+ |NTop ⇒ []
+ |NArrow U V ⇒ (fv_NTyp U)@(fv_NTyp V)
+ |NForall X U V ⇒ (fv_NTyp U)@(remove_nat X (fv_NTyp V))].
+
+
+let rec subst_NTyp_var T X Y \def
+ match T with
+ [TName Z ⇒ match (eqb X Z) with
+ [ true \rArr (TName Y)
+ | false \rArr (TName Z) ]
+ |NTop ⇒ NTop
+ |NArrow U V ⇒ (NArrow (subst_NTyp_var U X Y) (subst_NTyp_var V X Y))
+ |NForall Z U V ⇒ match (eqb X Z) with
+ [ true ⇒ (NForall Z (subst_NTyp_var U X Y) V)
+ | false ⇒ (NForall Z (subst_NTyp_var U X Y)
+ (subst_NTyp_var V X Y))]].
+
+definition fv_Nenv : list nbound → list nat ≝
+ map nbound nat
+ (λb.match b with
+ [mk_nbound (B:bool) (X:nat) (T:NTyp) ⇒ X]).
+
+inductive NWFType : (list nbound) → NTyp → Prop ≝
+ | NWFT_TName : ∀X,G.(in_list ? X (fv_Nenv G))
+ → (NWFType G (TName X))
+ | NWFT_Top : ∀G.(NWFType G NTop)
+ | NWFT_Arrow : ∀G,T,U.(NWFType G T) → (NWFType G U) →
+ (NWFType G (NArrow T U))
+ | NWFT_Forall : ∀G,X,T,U.(NWFType G T) →
+ (∀Y.¬(Y ∈ (fv_Nenv G)) →
+ (Y = X ∨ ¬(Y ∈ (fv_NTyp U))) →
+ (NWFType ((mk_nbound true Y T) :: G) (swap_NTyp Y X U))) →
+ (NWFType G (NForall X T U)).
+ (*NWFT_alpha : ∀G,T,U.(NWFType G T) → (alpha_eq T U) → (NWFType G U).*)
+
+inductive NWFEnv : (list nbound) → Prop ≝
+ | NWFE_Empty : (NWFEnv (nil ?))
+ | NWFE_cons : ∀B,X,T,G.(NWFEnv G) →
+ ¬(in_list ? X (fv_Nenv G)) →
+ (NWFType G T) → (NWFEnv ((mk_nbound B X T) :: G)).
+
+inductive NJSubtype : (list nbound) → NTyp → NTyp → Prop ≝
+ | NSA_Top : ∀G,T.(NWFEnv G) → (NWFType G T) → (NJSubtype G T NTop)
+ | NSA_Refl_TVar : ∀G,X.(NWFEnv G)
+ → (in_list ? X (fv_Nenv G))
+ → (NJSubtype G (TName X) (TName X))
+ | NSA_Trans_TVar : ∀G,X,T,U.
+ (in_list ? (mk_nbound true X U) G) →
+ (NJSubtype G U T) → (NJSubtype G (TName X) T)
+ | NSA_Arrow : ∀G,S1,S2,T1,T2.
+ (NJSubtype G T1 S1) → (NJSubtype G S2 T2) →
+ (NJSubtype G (NArrow S1 S2) (NArrow T1 T2))
+ | NSA_All : ∀G,X,S1,S2,T1,T2.
+ (NJSubtype G T1 S1) →
+ (∀Y.¬(Y ∈ fv_Nenv G) →
+ (NJSubtype ((mk_nbound true Y T1) :: G)
+ (swap_NTyp Y X S2) (swap_NTyp Y X T2))) →
+ (NJSubtype G (NForall X S1 S2) (NForall X T1 T2))
+ | NSA_alpha : ∀G,T1,T2,U1,U2.(NJSubtype G T1 U1) →
+ (alpha_eq T1 T2) →
+ (alpha_eq U1 U2) →
+ (NJSubtype G T2 U2).
+
+let rec nt_len T \def
+ match T with
+ [ TName X ⇒ O
+ | NTop ⇒ O
+ | NArrow T1 T2 ⇒ S (max (nt_len T1) (nt_len T2))
+ | NForall X T1 T2 ⇒ S (max (nt_len T1) (nt_len T2)) ].
+
+definition encodeenv : list nbound → list bound ≝
+ map nbound bound
+ (λb.match b with
+ [ mk_nbound b x T ⇒ mk_bound b x (encodetype T []) ]).
+
+axiom append_associative : ∀A.∀l1,l2,l3:(list A).((l1@l2)@l3) = (l1@l2@l3).
+
+lemma eq_fv_Nenv_fv_env : ∀G. fv_Nenv G = fv_env (encodeenv G).
+intro;elim G
+ [simplify;reflexivity
+ |simplify;rewrite < H;elim t;simplify;reflexivity]
+qed.
+
+(* palloso *)
+axiom decidable_eq_bound : \forall b,c:bound.decidable (b = c).
+
+lemma in_Nenv_to_in_env: ∀l,n,n2.mk_nbound true n n2 ∈ l →
+ mk_bound true n (encodetype n2 []) ∈ encodeenv l.
+intros 3;elim l
+ [elim (not_in_list_nil ? ? H)
+ |inversion H1;intros
+ [destruct H3;destruct;simplify;apply in_list_head
+ |destruct H5;elim t;simplify;apply in_list_cons;apply H;assumption]]
+qed.
+
+lemma in_lookup : \forall x,l.(in_list ? x l) \to (lookup x l = true).
+intros;elim H
+ [simplify;rewrite > eqb_n_n;reflexivity
+ |simplify;rewrite > H2;elim (eqb a a1);reflexivity]
+qed.
+
+lemma lookup_in : \forall x,l.(lookup x l = true) \to (in_list ? x l).
+intros 2;elim l
+ [simplify in H;destruct H
+ |generalize in match H1;simplify;elim (decidable_eq_nat x t)
+ [rewrite > H2;apply in_list_head
+ |rewrite > (not_eq_to_eqb_false ? ? H2) in H3;simplify in H3;
+ apply in_list_cons;apply H;assumption]]
+qed.
+
+lemma posn_length : \forall x,vars.(in_list ? x vars) \to
+ (posn vars x) < (length ? vars).
+intros 2;elim vars
+ [elim (not_in_list_nil ? ? H)
+ |inversion H1
+ [intros;destruct H3;destruct;simplify;rewrite > eqb_n_n;simplify;
+ apply lt_O_S
+ |intros;destruct H5;simplify;elim (eqb x t);simplify
+ [apply lt_O_S
+ |apply le_S_S;apply H;assumption]]]
+qed.
+
+lemma in_remove : \forall a,b,l.(a \neq b) \to (in_list ? a l) \to
+ (in_list ? a (remove_nat b l)).
+intros 4;elim l
+ [elim (not_in_list_nil ? ? H1)
+ |inversion H2;intros;
+ [destruct H4;destruct;simplify;rewrite > not_eq_to_eqb_false
+ [simplify;apply in_list_head
+ |intro;apply H;symmetry;assumption]
+ |destruct H6;simplify;elim (eqb b t)
+ [simplify;apply H1;assumption
+ |simplify;apply in_list_cons;apply H1;assumption]]]
+qed.
+
+axiom NTyp_len_ind : \forall P:NTyp \to Prop.
+ (\forall U.(\forall V.((nt_len V) < (nt_len U)) \to (P V))
+ \to (P U))
+ \to \forall T.(P T).
+
+axiom ntlen_arrow1 : ∀T1,T2.(nt_len T1) < (nt_len (NArrow T1 T2)).
+axiom ntlen_arrow2 : ∀T1,T2.(nt_len T2) < (nt_len (NArrow T1 T2)).
+axiom ntlen_forall1 : ∀X,T1,T2.(nt_len T1) < (nt_len (NForall X T1 T2)).
+axiom ntlen_forall2 : ∀X,T1,T2.(nt_len T2) < (nt_len (NForall X T1 T2)).
+axiom eq_ntlen_swap : ∀X,Y,T.nt_len T = nt_len (swap_NTyp X Y T).
+
+axiom nat_in_list_case :\forall G:list nat
+.\forall H:list nat
+ .\forall n:nat.in_list nat n (H@G)\rarr in_list nat n G\lor in_list nat n H.
+
+lemma swap_same : \forall x,y.swap x x y = y.
+intros;elim (decidable_eq_nat y x)
+ [autobatch paramodulation
+ |rewrite > swap_other;autobatch]
+qed.
+
+lemma not_nat_in_to_lookup_false : ∀l,X.¬(X ∈ l) → lookup X l = false.
+intros 2;elim l
+ [simplify;reflexivity
+ |simplify;elim (decidable_eq_nat X t)
+ [elim H1;rewrite > H2;apply in_list_head
+ |rewrite > (not_eq_to_eqb_false ? ? H2);simplify;apply H;intro;apply H1;
+ apply (in_list_cons ? ? ? ? H3);]]
+qed.
+
+lemma fv_encode : ∀T,l1,l2.
+ (∀x.(in_list ? x (fv_NTyp T)) →
+ (lookup x l1 = lookup x l2 ∧
+ (lookup x l1 = true → posn l1 x = posn l2 x))) →
+ (encodetype T l1 = encodetype T l2).
+intro;elim T
+ [simplify in H;elim (H n)
+ [simplify;rewrite < H1;generalize in match H2;elim (lookup n l1)
+ [simplify;rewrite > H3;autobatch
+ |simplify;reflexivity]
+ |apply in_list_head]
+ |simplify;reflexivity
+ |simplify;rewrite > (H l1 l2)
+ [rewrite > (H1 l1 l2)
+ [reflexivity
+ |intros;apply H2;simplify;apply in_list_to_in_list_append_r;autobatch]
+ |intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]
+ |simplify;rewrite > (H l1 l2)
+ [rewrite > (H1 (n::l1) (n::l2))
+ [reflexivity
+ |intros;elim (decidable_eq_nat x n)
+ [simplify;rewrite > (eq_to_eqb_true ? ? H4);simplify;split
+ [reflexivity|intro;reflexivity]
+ |elim (H2 x)
+ [split
+ [simplify;rewrite < H5;reflexivity
+ |simplify;elim (eqb x n);
+ [simplify;reflexivity
+ |simplify in H7;rewrite < (H6 H7);reflexivity]]
+ |simplify;apply in_list_to_in_list_append_r;
+ apply (in_remove ? ? ? H4);assumption]]]
+ |intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]]
+qed.
+
+lemma lookup_swap : \forall a,b,x,vars.
+ (lookup (swap a b x) (swap_list a b vars) =
+ lookup x vars).
+intros 4;elim vars
+ [simplify;reflexivity
+ |simplify;elim (decidable_eq_nat x t)
+ [rewrite > H1;rewrite > eqb_n_n;rewrite > eqb_n_n;simplify;reflexivity
+ |rewrite > (not_eq_to_eqb_false ? ? H1);elim (decidable_eq_nat x a)
+ [rewrite > H;rewrite > H2;rewrite > swap_left;
+ elim (decidable_eq_nat b t)
+ [rewrite < H3;rewrite > swap_right;
+ rewrite > (not_eq_to_eqb_false b a)
+ [reflexivity
+ |intro;autobatch]
+ |rewrite > (swap_other a b t)
+ [rewrite > (not_eq_to_eqb_false ? ? H3);simplify;reflexivity
+ |intro;autobatch
+ |intro;autobatch]]
+ |elim (decidable_eq_nat x b)
+ [rewrite > H;rewrite > H3;rewrite > swap_right;
+ elim (decidable_eq_nat t a)
+ [rewrite > H4;rewrite > swap_left;
+ rewrite > (not_eq_to_eqb_false a b)
+ [reflexivity
+ |intro;autobatch]
+ |rewrite > (swap_other a b t)
+ [rewrite > (not_eq_to_eqb_false a t)
+ [reflexivity
+ |intro;autobatch]
+ |assumption
+ |intro;autobatch]]
+ |rewrite > H;rewrite > (swap_other a b x)
+ [elim (decidable_eq_nat a t)
+ [rewrite > H4;rewrite > swap_left;
+ rewrite > (not_eq_to_eqb_false ? ? H3);reflexivity
+ |elim (decidable_eq_nat b t)
+ [rewrite > H5;rewrite > swap_right;
+ rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity
+ |rewrite > (swap_other a b t)
+ [rewrite > (not_eq_to_eqb_false ? ? H1);reflexivity
+ |intro;autobatch
+ |intro;autobatch]]]
+ |assumption
+ |assumption]]]]]
+qed.
+
+lemma posn_swap : \forall a,b,x,vars.
+ (posn vars x = posn (swap_list a b vars) (swap a b x)).
+intros 4;elim vars
+ [simplify;reflexivity
+ |simplify;rewrite < H;elim (decidable_eq_nat x t)
+ [rewrite > H1;do 2 rewrite > eqb_n_n;reflexivity
+ |elim (decidable_eq_nat (swap a b x) (swap a b t))
+ [elim H1;autobatch
+ |rewrite > (not_eq_to_eqb_false ? ? H1);
+ rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity]]]
+qed.
+
+theorem encode_swap : ∀a,x,T,vars.
+ ((in_list ? a (fv_NTyp T)) → (in_list ? a vars)) →
+ (in_list ? x vars) →
+ encodetype T vars =
+ encodetype (swap_NTyp a x T) (swap_list a x vars).
+intros 3;elim T
+ [elim (decidable_eq_nat n x)
+ [rewrite > H2;simplify in match (swap_NTyp ? ? ?);rewrite > swap_right;
+ simplify;lapply (lookup_swap a x x vars);rewrite > swap_right in Hletin;
+ rewrite > Hletin;cut ((in_list ? x vars) \to (lookup x vars = true))
+ [rewrite > (Hcut H1);simplify;lapply (posn_swap a x x vars);
+ rewrite > swap_right in Hletin1;rewrite < Hletin1;reflexivity
+ |generalize in match x;elim vars
+ [elim (not_in_list_nil ? ? H3)
+ |inversion H4
+ [intros;simplify;rewrite > eqb_n_n;reflexivity
+ |intros;simplify;destruct H8;rewrite > (H3 ? H5);
+ elim (eqb n1 t);reflexivity]]]
+ |elim (decidable_eq_nat n a);
+ [rewrite < H3;simplify;rewrite < posn_swap;rewrite > lookup_swap;
+ rewrite < H3 in H;simplify in H;rewrite > in_lookup;
+ [simplify;reflexivity
+ |apply H;apply in_list_head]
+ |simplify in ⊢ (? ? ? (? % ?));rewrite > swap_other;
+ [apply (fv_encode ? vars (swap_list a x vars));intros;
+ simplify in H4;cut (x1 = n)
+ [rewrite > Hcut;elim vars
+ [simplify;split [reflexivity|intro;reflexivity]
+ |simplify;elim H5;cut
+ (t = a ∨t = x ∨ (t ≠ a ∧ t ≠ x))
+ [|elim (decidable_eq_nat t a)
+ [left;left;assumption
+ |elim (decidable_eq_nat t x)
+ [left;right;assumption
+ |right;split;assumption]]]
+ elim Hcut1
+ [elim H8
+ [rewrite > H9;rewrite > swap_left;
+ rewrite > (not_eq_to_eqb_false ? ? H2);
+ rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
+ split
+ [assumption
+ |intro;rewrite < (H7 H10);reflexivity]
+ |rewrite > H9;rewrite > swap_right;
+ rewrite > (not_eq_to_eqb_false ? ? H2);
+ rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
+ split
+ [assumption
+ |intro;rewrite < (H7 H10);reflexivity]]
+ |elim H8;rewrite > (swap_other a x t)
+ [rewrite < H6;split
+ [reflexivity
+ |elim (eqb n t)
+ [simplify;reflexivity
+ |simplify in H11;rewrite < (H7 H11);reflexivity]]
+ |*:assumption]]]
+ |inversion H4
+ [intros;destruct H6;destruct;reflexivity
+ |intros;destruct H8;elim (not_in_list_nil ? ? H5)]]
+ |*:assumption]]]
+ |simplify;reflexivity
+ |simplify;simplify in H2;rewrite < H
+ [rewrite < H1
+ [reflexivity
+ |intro;apply H2;apply in_list_to_in_list_append_r;autobatch
+ |assumption]
+ |intro;apply H2;apply in_list_to_in_list_append_l;autobatch
+ |assumption]
+ |simplify;simplify in H2;rewrite < H
+ [elim (decidable_eq_nat a n)
+ [rewrite < (H1 (n::vars));
+ [reflexivity
+ |intro;rewrite > H4;apply in_list_head
+ |apply in_list_cons;assumption]
+ |rewrite < (H1 (n::vars));
+ [reflexivity
+ |intro;apply in_list_cons;apply H2;apply in_list_to_in_list_append_r;
+ apply (in_remove ? ? ? H4 H5)
+ |apply in_list_cons;assumption]]
+ |intro;apply H2;apply in_list_to_in_list_append_l;assumption
+ |assumption]]
+qed.
+
+lemma encode_swap2 : ∀a:nat.∀x:nat.∀T:NTyp.
+ ¬(a ∈ (fv_NTyp T)) →
+ \forall vars.x ∈ vars
+ →encodetype T vars=encodetype (swap_NTyp a x T) (swap_list a x vars).
+intros;apply (encode_swap ? ? ? ? ? H1);intro;elim (H H2);
+qed.
+
+lemma remove_inlist : \forall x,y,l.(in_list ? x (remove_nat y l)) \to
+ (in_list ? x l) \land x \neq y.
+intros 3;elim l 0
+ [simplify;intro;elim (not_in_list_nil ? ? H)
+ |simplify;intro;elim (decidable_eq_nat y t)
+ [rewrite > H in H2;rewrite > eqb_n_n in H2;simplify in H2;
+ rewrite > H in H1;elim (H1 H2);rewrite > H;split
+ [apply in_list_cons;assumption
+ |assumption]
+ |rewrite > (not_eq_to_eqb_false ? ? H) in H2;simplify in H2;
+ inversion H2
+ [intros;destruct H4;split
+ [apply in_list_head
+ |intro;autobatch]
+ |intros;destruct H6;
+ elim (H1 H3);split
+ [apply in_list_cons;assumption
+ |assumption]]]]
+qed.
+
+lemma inlist_remove : \forall x,y,l.(in_list ? x l \to x \neq y \to
+ (in_list ? x (remove_nat y l))).
+intros 3;elim l
+ [elim (not_in_list_nil ? ? H);
+ |simplify;elim (decidable_eq_nat y t)
+ [rewrite > (eq_to_eqb_true ? ? H3);simplify;apply H
+ [(*FIXME*)generalize in match H1;intro;inversion H1
+ [intros;destruct H6;destruct;elim H2;reflexivity
+ |intros;destruct H8;assumption]
+ |assumption]
+ |rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
+ (*FIXME*)generalize in match H1;intro;inversion H4
+ [intros;destruct H6;destruct;apply in_list_head
+ |intros;destruct H8;destruct;apply in_list_cons;apply (H H5 H2)
+ ]]]
+qed.
+
+lemma incl_fv_var : \forall T.(incl ? (fv_NTyp T) (var_NTyp T)).
+intro;elim T
+ [simplify;unfold;intros;assumption
+ |simplify;unfold;intros;assumption
+ |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
+ [apply in_list_to_in_list_append_l;apply (H ? H3)
+ |apply in_list_to_in_list_append_r;apply (H1 ? H3)]
+ |simplify;unfold;intros;elim (decidable_eq_nat x n)
+ [rewrite > H3;apply in_list_head
+ |apply in_list_cons;elim (in_list_append_to_or_in_list ? ? ? ? H2)
+ [apply in_list_to_in_list_append_l;apply (H ? H4)
+ |apply in_list_to_in_list_append_r;elim (remove_inlist ? ? ? H4);
+ apply (H1 ? H5)]]]
+qed.
+
+lemma fv_encode2 : ∀T,l1,l2.
+ (∀x.(in_list ? x (fv_NTyp T)) →
+ (lookup x l1 = lookup x l2 ∧
+ posn l1 x = posn l2 x)) →
+ (encodetype T l1 = encodetype T l2).
+intros;apply fv_encode;intros;elim (H ? H1);split
+ [assumption|intro;assumption]
+qed.
+
+lemma alpha_sym : \forall S,T.(alpha_eq S T) \to (alpha_eq T S).
+intros;elim H
+ [apply A_refl
+ |apply A_arrow;assumption
+ |apply A_forall
+ [assumption
+ |intros;apply H4;intro;apply H5;elim (decidable_eq_nat Z n5)
+ [rewrite > H7;apply in_list_head
+ |apply in_list_cons;(*FIXME*)generalize in match H6;intro;
+ inversion H6
+ [intros;destruct H10;destruct;apply in_list_head
+ |intros;destruct H12;apply in_list_cons;inversion H9
+ [intros;destruct H12;elim H7;reflexivity
+ |intros;destruct H14;
+ elim (in_list_append_to_or_in_list ? ? ? ? H11)
+ [apply in_list_to_in_list_append_r;assumption
+ |apply in_list_to_in_list_append_l;assumption]]]]]]
+qed.
+
+lemma inlist_fv_swap : \forall x,y,b,T.
+ (\lnot (in_list ? b (y::var_NTyp T))) \to
+ (in_list ? x (fv_NTyp (swap_NTyp b y T))) \to
+ (x \neq y \land (x = b \lor (in_list ? x (fv_NTyp T)))).
+intros 4;elim T
+ [simplify in H;simplify;simplify in H1;elim (decidable_eq_nat y n)
+ [rewrite > H2 in H1;rewrite > swap_right in H1;
+ inversion H1
+ [intros;destruct H4;split
+ [unfold;intro;apply H;rewrite > H2;apply in_list_head
+ |left;reflexivity]
+ |intros;destruct H6;elim (not_in_list_nil ? ? H3)]
+ |elim (decidable_eq_nat b n)
+ [rewrite > H3 in H;elim H;apply in_list_cons;apply in_list_head
+ |rewrite > swap_other in H1
+ [split
+ [inversion H1
+ [intros;destruct H5;intro;apply H2;
+ symmetry;assumption
+ |intros;destruct H7;
+ elim (not_in_list_nil ? ? H4)]
+ |autobatch]
+ |intro;autobatch
+ |intro;autobatch]]]
+ |simplify in H1;elim (not_in_list_nil ? ? H1)
+ |simplify;simplify in H3;simplify in H2;elim (nat_in_list_case ? ? ? H3)
+ [elim H1
+ [split
+ [assumption
+ |elim H6
+ [left;assumption
+ |right;apply in_list_to_in_list_append_r;assumption]]
+ |intro;apply H2;elim (nat_in_list_case (var_NTyp n1) [y] ? H5)
+ [apply (in_list_to_in_list_append_r ? ? (y::var_NTyp n) (var_NTyp n1));
+ assumption
+ |inversion H6
+ [intros;destruct H8;apply in_list_head
+ |intros;destruct H10;
+ elim (not_in_list_nil ? ? H7)]]
+ |assumption]
+ |elim H
+ [split
+ [assumption
+ |elim H6
+ [left;assumption
+ |right;apply in_list_to_in_list_append_l;assumption]]
+ |intro;apply H2;inversion H5
+ [intros;destruct H7;apply in_list_head
+ |intros;destruct H9;apply in_list_cons;
+ apply in_list_to_in_list_append_l;assumption]
+ |assumption]]
+ |simplify;simplify in H3;simplify in H2;elim (nat_in_list_case ? ? ? H3)
+ [elim H1
+ [split
+ [assumption
+ |elim H6
+ [left;assumption
+ |right;apply in_list_to_in_list_append_r;apply inlist_remove
+ [assumption
+ |intro;elim (remove_inlist ? ? ? H4);apply H10;
+ rewrite > swap_other
+ [assumption
+ |intro;rewrite > H8 in H7;rewrite > H11 in H7;apply H2;
+ destruct;apply in_list_cons;apply in_list_head
+ |destruct;assumption]]]]
+ |intro;apply H2;inversion H5
+ [intros;destruct H7;apply in_list_head
+ |intros;destruct H9;
+ apply in_list_cons;
+ cut ((n::var_NTyp n1)@(var_NTyp n2) = n::var_NTyp n1@var_NTyp n2)
+ [rewrite < Hcut;elim (n::var_NTyp n1)
+ [simplify;assumption
+ |simplify;elim (decidable_eq_nat b t)
+ [rewrite > H9;apply in_list_head
+ |apply in_list_cons;assumption]]
+ |simplify;reflexivity]]
+ |elim(remove_inlist ? ? ? H4);assumption]
+ |elim H
+ [split
+ [assumption
+ |elim H6
+ [left;assumption
+ |right;apply in_list_to_in_list_append_l;
+ assumption]]
+ |intro;apply H2;inversion H5
+ [intros;destruct H7;apply in_list_head
+ |intros;destruct H9;apply in_list_cons;
+ elim (decidable_eq_nat b n)
+ [rewrite > H8;apply in_list_head
+ |apply in_list_cons;apply in_list_to_in_list_append_l;
+ assumption]]
+ |assumption]]]
+qed.
+
+lemma inlist_fv_swap_r : \forall x,y,b,T.
+ (\lnot (in_list ? b (y::var_NTyp T))) \to
+ ((x = b \land (in_list ? y (fv_NTyp T))) \lor
+ (x \neq y \land (in_list ? x (fv_NTyp T)))) \to
+ (in_list ? x (fv_NTyp (swap_NTyp b y T))).
+intros 4;elim T
+ [simplify;simplify in H;simplify in H1;cut (b \neq n)
+ [elim H1
+ [elim H2;cut (y = n)
+ [rewrite > Hcut1;rewrite > swap_right;rewrite > H3;apply in_list_head
+ |inversion H4
+ [intros;destruct H6;autobatch
+ |intros;destruct H8;elim (not_in_list_nil ? ? H5)]]
+ |elim H2;inversion H4
+ [intros;destruct H6;destruct;rewrite > (swap_other b y x)
+ [apply in_list_head
+ |intro;autobatch
+ |assumption]
+ |intros;destruct H8;elim (not_in_list_nil ? ? H5)]]
+ |intro;apply H;apply (in_list_to_in_list_append_r ? ? [y] [n]);
+ rewrite > H2;apply in_list_head]
+ |simplify in H1;elim H1;elim H2;elim (not_in_list_nil ? ? H4)
+ |simplify;simplify in H3;cut (\lnot (in_list ? b (y::var_NTyp n1)))
+ [cut (\lnot (in_list ? b (y::var_NTyp n)))
+ [elim H3
+ [elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
+ [apply in_list_to_in_list_append_l;apply H
+ [assumption
+ |left;split;assumption]
+ |apply in_list_to_in_list_append_r;apply H1
+ [assumption
+ |left;split;assumption]]
+ |elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
+ [apply in_list_to_in_list_append_l;apply H;
+ [assumption
+ |right;split;assumption]
+ |apply in_list_to_in_list_append_r;apply H1
+ [assumption
+ |right;split;assumption]]]
+ |intro;apply H2;inversion H4
+ [intros;destruct H6;apply in_list_head
+ |intros;destruct H8;apply in_list_cons;
+ simplify;apply in_list_to_in_list_append_l;
+ assumption]]
+ |intro;apply H2;inversion H4
+ [intros;destruct H6;apply in_list_head
+ |intros;destruct H8;apply in_list_cons;
+ simplify;apply in_list_to_in_list_append_r;
+ assumption]]
+ |simplify;simplify in H3;cut (\lnot (in_list ? b (y::var_NTyp n1)))
+ [cut (\lnot (in_list ? b (y::var_NTyp n2)))
+ [elim H3
+ [elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
+ [apply in_list_to_in_list_append_l;apply H
+ [assumption
+ |left;split;assumption]
+ |apply in_list_to_in_list_append_r;apply inlist_remove
+ [apply H1;
+ [assumption
+ |left;split
+ [assumption|elim (remove_inlist ? ? ? H7);assumption]]
+ |elim (remove_inlist ? ? ? H7);elim (decidable_eq_nat b n)
+ [rewrite > H10;rewrite > swap_left;intro;apply H9;
+ rewrite < H11;rewrite < H10;assumption
+ |rewrite > swap_other
+ [rewrite > H5;assumption
+ |intro;apply H10;symmetry;assumption
+ |intro;apply H9;symmetry;assumption]]]]
+ |elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
+ [apply in_list_to_in_list_append_l;apply H
+ [assumption
+ |right;split;assumption]
+ |apply in_list_to_in_list_append_r;apply inlist_remove
+ [apply H1;
+ [assumption
+ |right;split
+ [assumption|elim (remove_inlist ? ? ? H7);assumption]]
+ |elim (decidable_eq_nat b n)
+ [rewrite > H8;rewrite > swap_left;assumption
+ |elim (decidable_eq_nat y n)
+ [rewrite > H9;rewrite > swap_right;intro;apply Hcut1;
+ rewrite > H9;apply in_list_cons;
+ apply incl_fv_var;elim (remove_inlist ? ? ? H7);
+ rewrite < H10;assumption
+ |rewrite > (swap_other b y n)
+ [elim (remove_inlist ? ? ? H7);assumption
+ |intro;autobatch
+ |intro;autobatch]]]]]]
+ |intro;apply H2;inversion H4
+ [intros;destruct H6;apply in_list_head
+ |simplify;intros;destruct H8;
+ apply in_list_cons;
+ apply (in_list_to_in_list_append_r ? ? (n::var_NTyp n1) (var_NTyp n2));
+ assumption]]
+ |intro;apply H2;inversion H4
+ [intros;destruct H6;apply in_list_head
+ |simplify;intros;destruct H8;
+ apply in_list_cons;
+ apply (in_list_to_in_list_append_l ? ? (n::var_NTyp n1) (var_NTyp n2));
+ apply in_list_cons;assumption]]]
+qed.
+
+lemma fv_alpha : \forall S,T.(alpha_eq S T) \to
+ (incl ? (fv_NTyp S) (fv_NTyp T)).
+intros;elim H
+ [unfold;intros;assumption
+ |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
+ [apply in_list_to_in_list_append_l;autobatch
+ |apply in_list_to_in_list_append_r;autobatch]
+ |simplify;unfold;intros;
+ elim (in_list_append_to_or_in_list ? ? ? ? H5)
+ [apply in_list_to_in_list_append_l;apply (H2 ? H6)
+ |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
+ apply in_list_to_in_list_append_r;
+ lapply (H4 ? H7);
+ elim (remove_inlist ? ? ? H6);apply inlist_remove
+ [lapply (inlist_fv_swap_r x n4 a n1)
+ [elim (inlist_fv_swap x n5 a n3)
+ [elim H11
+ [rewrite < H12 in H7;elim H7;
+ do 2 apply in_list_cons;
+ apply in_list_to_in_list_append_l;
+ apply (incl_fv_var n1 ? H8);
+ |assumption]
+ |intro;apply H7;inversion H10;intros;destruct;
+ [apply in_list_cons;apply in_list_head
+ |do 2 apply in_list_cons;apply in_list_to_in_list_append_r;
+ assumption]
+ |apply (Hletin ? Hletin1)]
+ |intro;apply H7;inversion H10
+ [intros;destruct H12;apply in_list_head
+ |intros;destruct H14;do 2 apply in_list_cons;
+ apply in_list_to_in_list_append_l;assumption]
+ |right;split;assumption]
+ |intros;intro;lapply (inlist_fv_swap_r x n4 a n1)
+ [lapply (Hletin ? Hletin1);
+ elim (inlist_fv_swap x n5 a n3 ? Hletin2)
+ [apply (H11 H10)
+ |intro;apply H7;elim (decidable_eq_nat a n4)
+ [rewrite > H12;apply in_list_head
+ |apply in_list_cons;inversion H11;intros;destruct;
+ [apply in_list_head
+ |apply in_list_cons;apply in_list_to_in_list_append_r;
+ assumption]]]
+ |intro;apply H7;inversion H11
+ [intros;destruct H13;apply in_list_head
+ |intros;destruct H15;do 2 apply in_list_cons;
+ apply in_list_to_in_list_append_l;assumption]
+ |right;split;assumption]]]]
+qed.
+
+theorem alpha_to_encode : ∀S,T.(alpha_eq S T) →
+ ∀vars.(encodetype S vars) = (encodetype T vars).
+intros 3;elim H
+ [reflexivity
+ |simplify;rewrite > H2;rewrite > H4;reflexivity
+ |simplify;rewrite > H2;
+ cut (encodetype n1 (n4::vars) = encodetype n3 (n5::vars))
+ [rewrite > Hcut;reflexivity
+ |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
+ lapply (encode_swap2 a n4 n1 ? (n4::vars))
+ [intro;apply H5;do 2 apply in_list_cons;
+ apply in_list_to_in_list_append_l;autobatch
+ |lapply (encode_swap2 a n5 n3 ? (n5::vars))
+ [intro;apply H5;do 2 apply in_list_cons;
+ apply in_list_to_in_list_append_r;autobatch
+ |rewrite > Hletin;rewrite > Hletin1;simplify;rewrite > swap_right;
+ rewrite > swap_right;rewrite > (H4 a H5 (a::swap_list a n4 vars));
+ rewrite > (fv_encode2 ? ? (a::swap_list a n5 vars))
+ [reflexivity
+ |intros;elim (decidable_eq_nat n4 n5)
+ [rewrite > H7;autobatch
+ |cut ((x \neq n4) \land (x \neq n5))
+ [elim Hcut;elim (decidable_eq_nat x a)
+ [simplify;rewrite > (eq_to_eqb_true ? ? H10);simplify;
+ autobatch
+ |simplify;rewrite > (not_eq_to_eqb_false ? ? H10);
+ simplify;elim vars
+ [simplify;autobatch
+ |simplify;elim H11;rewrite < H12;
+ rewrite > H13;elim (decidable_eq_nat a t)
+ [rewrite > H14;rewrite > swap_left;
+ rewrite > swap_left;
+ rewrite > (not_eq_to_eqb_false ? ? H8);
+ rewrite > (not_eq_to_eqb_false ? ? H9);
+ simplify;autobatch
+ |elim (decidable_eq_nat n4 t)
+ [rewrite > H15;rewrite > swap_right;
+ rewrite > (swap_other a n5 t)
+ [rewrite > (not_eq_to_eqb_false ? ? H10);
+ rewrite < H15;
+ rewrite > (not_eq_to_eqb_false ? ? H8);
+ autobatch
+ |intro;autobatch
+ |intro;apply H7;autobatch]
+ |rewrite > (swap_other a n4 t);
+ elim (decidable_eq_nat n5 t)
+ [rewrite < H16;rewrite > swap_right;
+ rewrite > (not_eq_to_eqb_false ? ? H9);
+ rewrite > (not_eq_to_eqb_false ? ? H10);
+ autobatch
+ |rewrite > (swap_other a n5 t);try intro;
+ autobatch
+ |*:intro;autobatch]]]]]
+ |split
+ [lapply (H3 ? H5);lapply (alpha_sym ? ? Hletin2);
+ lapply (fv_alpha ? ? Hletin3);
+ lapply (Hletin4 ? H6);
+ elim (inlist_fv_swap ? ? ? ? ? Hletin5)
+ [assumption
+ |intro;apply H5;inversion H8
+ [intros;destruct H10;
+ apply in_list_head
+ |intros;destruct H12;
+ do 2 apply in_list_cons;
+ apply in_list_to_in_list_append_l;assumption]]
+ |elim (inlist_fv_swap ? ? ? ? ? H6)
+ [assumption
+ |intro;apply H5;elim (decidable_eq_nat a n4)
+ [rewrite > H9;apply in_list_head
+ |apply in_list_cons;
+ inversion H8;intros;destruct;
+ [apply in_list_head
+ |apply in_list_cons;
+ apply in_list_to_in_list_append_r;
+ assumption]]]]]]]
+ |apply in_list_head]
+ |apply in_list_head]]]
+qed.
+
+lemma encode_append : ∀T,U,n,l.length ? l ≤ n →
+ subst_type_nat (encodetype T l) U n = encodetype T l.
+intros 2;elim T
+ [simplify;elim (bool_to_decidable_eq (lookup n l) true)
+ [rewrite > H1;simplify;lapply (lookup_in ? ? H1);
+ lapply (posn_length ? ? Hletin);
+ cut (posn l n ≠ n1)
+ [rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;reflexivity
+ |intro;rewrite > H2 in Hletin1;unfold in Hletin1;autobatch;]
+ |cut (lookup n l = false)
+ [rewrite > Hcut;reflexivity
+ |generalize in match H1;elim (lookup n l);
+ [elim H2;reflexivity|reflexivity]]]
+ |simplify;reflexivity
+ |simplify;autobatch
+ |simplify;rewrite > (H ? ? H2);rewrite > H1
+ [reflexivity
+ |simplify;autobatch]]
+qed.
+
+lemma encode_subst_simple : ∀X,T,l.
+ (encodetype T l = subst_type_nat (encodetype T (l@[X])) (TFree X) (length ? l)).
+intros 2;elim T
+ [simplify;cut (lookup n l = true → posn l n = posn (l@[X]) n)
+ [generalize in match Hcut;elim (bool_to_decidable_eq (lookup n l) true)
+ [cut (lookup n (l@[X]) = true)
+ [rewrite > H;rewrite > Hcut1;simplify;
+ cut (eqb (posn (l@[X]) n) (length nat l) = false)
+ [rewrite > Hcut2;simplify;rewrite < (H1 H);reflexivity
+ |generalize in match H;elim l 0
+ [simplify;intro;destruct H2
+ |intros 2;simplify;elim (eqb n t)
+ [simplify;reflexivity
+ |simplify in H3;simplify;apply (H2 H3)]]]
+ |generalize in match H;elim l
+ [simplify in H2;destruct H2
+ |generalize in match H3;simplify;elim (eqb n t) 0
+ [simplify;intro;reflexivity
+ |simplify;intro;apply (H2 H4)]]]
+ |cut (lookup n l = false)
+ [elim (decidable_eq_nat n X)
+ [rewrite > Hcut1;rewrite > H2;cut (lookup X (l@[X]) = true)
+ [rewrite > Hcut2;simplify;
+ cut (eqb (posn (l@[X]) X) (length nat l) = true)
+ [rewrite > Hcut3;simplify;reflexivity
+ |generalize in match Hcut1;elim l 0
+ [intros;simplify;rewrite > eqb_n_n;simplify;reflexivity
+ |simplify;intros 2;rewrite > H2;elim (eqb X t)
+ [simplify in H4;destruct H4
+ |simplify;simplify in H4;apply (H3 H4)]]]
+ |elim l
+ [simplify;rewrite > eqb_n_n;reflexivity
+ |simplify;elim (eqb X t)
+ [simplify;reflexivity
+ |simplify;assumption]]]
+ |cut (lookup n l = lookup n (l@[X]))
+ [rewrite < Hcut2;rewrite > Hcut1;simplify;reflexivity
+ |elim l
+ [simplify;rewrite > (not_eq_to_eqb_false ? ? H2);simplify;
+ reflexivity
+ |simplify;elim (eqb n t)
+ [simplify;reflexivity
+ |simplify;assumption]]]]
+ |generalize in match H;elim (lookup n l);
+ [elim H2;reflexivity|reflexivity]]]
+ |elim l 0
+ [intro;simplify in H;destruct H
+ |simplify;intros 2;elim (eqb n t)
+ [simplify;reflexivity
+ |simplify in H1;simplify;rewrite < (H H1);reflexivity]]]
+ |simplify;reflexivity
+ |simplify;rewrite < H;rewrite < H1;reflexivity
+ |simplify;rewrite < H;rewrite < (append_associative ? [n] l [X]);
+ rewrite < (H1 ([n]@l));reflexivity]
+qed.
+
+lemma encode_subst : ∀T,X,Y,l.¬(X ∈ l) → ¬(Y ∈ l) →
+ (X ∈ (fv_NTyp T) → X = Y) →
+ encodetype (swap_NTyp X Y T) l =
+ subst_type_nat (encodetype T (l@[Y])) (TFree X) (length ? l).
+apply NTyp_len_ind;intro;elim U
+ [elim (decidable_eq_nat n X)
+ [rewrite > H4 in H3;rewrite > H4;rewrite > H3
+ [simplify in \vdash (? ? (? % ?) ?);rewrite > swap_same;
+ cut (lookup Y (l@[Y]) = true)
+ [simplify;rewrite > Hcut;rewrite > (not_nat_in_to_lookup_false ? ? H2);
+ simplify;cut (posn (l@[Y]) Y = length ? l)
+ [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
+ |generalize in match H2;elim l;simplify
+ [rewrite > eqb_n_n;reflexivity
+ |elim (decidable_eq_nat Y t)
+ [elim H6;rewrite > H7;apply in_list_head
+ |rewrite > (not_eq_to_eqb_false ? ? H7);simplify;
+ rewrite < H5
+ [reflexivity
+ |intro;apply H6;apply in_list_cons;assumption]]]]
+ |elim l
+ [simplify;rewrite > eqb_n_n;reflexivity
+ |simplify;rewrite > H5;elim (eqb Y t);reflexivity]]
+ |simplify;apply in_list_head]
+ |elim (decidable_eq_nat Y n);
+ [rewrite < H5;simplify;rewrite > swap_right;
+ rewrite > (not_nat_in_to_lookup_false ? ? H1);
+ cut (lookup Y (l@[Y]) = true)
+ [rewrite > Hcut;simplify;cut (posn (l@[Y]) Y = length ? l)
+ [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
+ |generalize in match H2;elim l;simplify
+ [rewrite > eqb_n_n;reflexivity
+ |elim (decidable_eq_nat Y t)
+ [elim H7;rewrite > H8;apply in_list_head
+ |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;
+ rewrite < H6
+ [reflexivity
+ |intro;apply H7;apply in_list_cons;assumption]]]]
+ |elim l;simplify
+ [rewrite > eqb_n_n;reflexivity
+ |elim (eqb Y t);simplify;autobatch]]
+ |simplify;rewrite > (swap_other X Y n)
+ [cut (lookup n l = lookup n (l@[Y]) ∧
+ (lookup n l = true → posn l n = posn (l@[Y]) n))
+ [elim Hcut;rewrite > H6;generalize in match H7;
+ generalize in match H6;elim (lookup n (l@[Y]))
+ [simplify;rewrite < H9;generalize in match H8;elim l
+ [simplify in H10;destruct H10
+ |elim (decidable_eq_nat n t)
+ [simplify;rewrite > (eq_to_eqb_true ? ? H12);simplify;
+ reflexivity
+ |simplify;rewrite > (not_eq_to_eqb_false ? ? H12);
+ simplify;generalize in match H10;
+ elim (eqb (posn l1 n) (length nat l1))
+ [simplify in H13;simplify in H11;
+ rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
+ simplify in H11;lapply (H13 H11);destruct Hletin
+ |simplify;reflexivity]]
+ |assumption
+ |assumption]
+ |simplify;reflexivity]
+ |elim l;split
+ [simplify;cut (n ≠ Y)
+ [rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;
+ reflexivity
+ |intro;apply H5;symmetry;assumption]
+ |intro;simplify in H6;destruct H6
+ |elim H6;simplify;rewrite < H7;reflexivity
+ |simplify;elim (eqb n t)
+ [simplify;reflexivity
+ |simplify;simplify in H7;elim H6;rewrite < (H9 H7);
+ reflexivity]]]
+ |assumption
+ |intro;apply H5;symmetry;assumption]]]
+ |simplify;reflexivity
+ |simplify;rewrite < (H2 n ? ? ? ? H3 H4)
+ [rewrite < (H2 n1 ? ? ? ? H3 H4);
+ [autobatch|autobatch
+ |intro;apply H5;simplify;apply in_list_to_in_list_append_r;assumption]
+ |autobatch
+ |intro;apply H5;simplify;apply in_list_to_in_list_append_l;assumption]
+ |simplify;rewrite < (H2 n1 ? ? ? ? H3 H4)
+ [cut (l = swap_list X Y l)
+ [|generalize in match H3;generalize in match H4;elim l
+ [simplify;reflexivity
+ |simplify;elim (decidable_eq_nat t X)
+ [elim H8;rewrite > H9;apply in_list_head
+ |elim (decidable_eq_nat t Y)
+ [elim H7;rewrite > H10;apply in_list_head
+ |rewrite > (swap_other X Y t)
+ [rewrite < H6
+ [reflexivity
+ |intro;apply H7;apply in_list_cons;assumption
+ |intro;apply H8;apply in_list_cons;assumption]
+ |*:assumption]]]]]
+ elim (decidable_eq_nat n Y)
+ [rewrite > H6;rewrite > (fv_encode (swap_NTyp X Y n2) (swap X Y Y::l)
+ (swap_list X Y (Y::l)));
+ [rewrite < (encode_swap X Y n2);
+ [rewrite < (fv_encode ? (Y::l) (Y::l@[Y]))
+ [rewrite > encode_append;
+ [rewrite < (fv_encode n2 (Y::l) (Y::l@[Y]));
+ [reflexivity
+ |intros;elim (decidable_eq_nat x Y)
+ [rewrite > H8;simplify;rewrite > eqb_n_n;simplify;
+ split [reflexivity|intro;reflexivity]
+ |simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
+ simplify;elim l
+ [simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
+ simplify;split [reflexivity|intro;destruct H9]
+ |elim H9;simplify;elim (eqb x t)
+ [simplify;split [reflexivity|intro;reflexivity]
+ |simplify;rewrite < H10;generalize in match H11;
+ elim (lookup x l1)
+ [split
+ [reflexivity
+ |intro;rewrite < (H12 H13);reflexivity]
+ |split [reflexivity|intro;destruct H13]]]]]]
+ |simplify;constructor 1]
+ |intros;simplify;elim (decidable_eq_nat x Y)
+ [rewrite > (eq_to_eqb_true ? ? H8);simplify;split
+ [reflexivity|intro;reflexivity]
+ |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;elim l
+ [simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
+ simplify;split [reflexivity|intro;destruct H9]
+ |simplify;elim (eqb x t)
+ [simplify;split [reflexivity|intro;reflexivity]
+ |simplify;elim H9;split
+ [assumption
+ |intro;rewrite < (H11 H12);reflexivity]]]]]
+ |intro;elim (decidable_eq_nat X Y)
+ [rewrite > H8;apply in_list_head
+ |elim H8;apply H5;simplify;apply in_list_to_in_list_append_r;
+ rewrite > H6;apply (in_remove ? ? ? H8 H7)]
+ |apply in_list_head]
+ |intros;simplify;rewrite > swap_right;rewrite < Hcut;
+ split [reflexivity|intro;reflexivity]]
+ |rewrite < Hcut;elim (decidable_eq_nat n X)
+ [rewrite > H7;rewrite > (fv_encode (swap_NTyp X Y n2) (swap X Y X::l)
+ (swap_list X Y (X::l)))
+ [rewrite > (encode_swap X Y n2);
+ [simplify;
+ cut (swap X Y X::swap_list X Y (l@[Y]) =
+ (swap X Y X::swap_list X Y l)@[X])
+ [rewrite > Hcut1;cut (S (length ? l) = (length ? (swap X Y X::swap_list X Y l)))
+ [rewrite > Hcut2;rewrite < (encode_subst_simple X
+ (swap_NTyp X Y n2) (swap X Y X::swap_list X Y l));
+ reflexivity
+ |simplify;elim l
+ [reflexivity
+ |simplify;rewrite < H8;reflexivity]]
+ |simplify;elim l
+ [simplify;rewrite > swap_right;reflexivity
+ |simplify;destruct H8;rewrite > Hcut1;reflexivity]]
+ |intro;apply in_list_head
+ |apply in_list_cons;elim l
+ [simplify;apply in_list_head
+ |simplify;apply in_list_cons;assumption]]
+ |intros;simplify;rewrite < Hcut;
+ split [reflexivity|intro;reflexivity]]
+ |rewrite > (swap_other X Y n)
+ [rewrite < (append_associative ? [n] l [Y]);
+ cut (S (length nat l) = length nat (n::l)) [|reflexivity]
+ rewrite > Hcut1;rewrite < (H2 n2);
+ [reflexivity
+ |autobatch
+ |intro;apply H7;inversion H8;intros
+ [destruct H10;reflexivity
+ |destruct H12;destruct;elim (H3 H9)]
+ |intro;apply H6;inversion H8;intros
+ [destruct H10;reflexivity
+ |destruct H12;destruct;elim (H4 H9)]
+ |intro;apply H5;simplify;apply in_list_to_in_list_append_r;
+ apply (in_remove ? ? ? ? H8);intro;apply H7;symmetry;assumption]
+ |*:assumption]]]
+ |autobatch
+ |intro;apply H5;simplify;apply in_list_to_in_list_append_l;assumption]]
+qed.
+
+lemma swap_case: ∀u,v,x.(swap u v x) = u ∨ (swap u v x) = v ∨ (swap u v x = x).
+intros.unfold in match swap.simplify.elim (eqb x u)
+ [simplify;autobatch
+ |simplify;elim (eqb x v);simplify;autobatch]
+qed.
+
+lemma in_fvNTyp_in_fvNenv : ∀G,T.(NWFType G T) → (incl ? (fv_NTyp T) (fv_Nenv G)).
+intros;elim H
+ [simplify;unfold;intros;inversion H2;intros
+ [destruct H4;assumption
+ |destruct H6;elim (not_in_list_nil ? ? H3)]
+ |simplify;unfold;intros;elim (not_in_list_nil ? ? H1)
+ |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
+ [apply (H2 ? H6)|apply (H4 ? H6)]
+ |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
+ [apply H2;assumption
+ |elim (fresh_name (x::fv_Nenv l@var_NTyp n2));lapply (H4 a)
+ [cut (a ≠ x ∧ x ≠ n)
+ [elim Hcut;lapply (Hletin x)
+ [simplify in Hletin1;inversion Hletin1;intros;
+ [destruct H11;elim H8;reflexivity
+ |destruct H13;assumption]
+ |generalize in match H6;generalize in match H7;elim n2
+ [simplify in H11;elim (decidable_eq_nat n n3)
+ [rewrite > (eq_to_eqb_true ? ? H12) in H11;simplify in H11;
+ elim (not_in_list_nil ? ? H11)
+ |rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
+ simplify in H11;inversion H11;intros
+ [destruct H14;simplify;
+ rewrite > swap_other
+ [apply in_list_head
+ |intro;apply H8;rewrite > H13;reflexivity
+ |intro;apply H9;rewrite > H13;reflexivity]
+ |destruct H16;elim (not_in_list_nil ? ? H13)]]
+ |simplify in H11;elim (not_in_list_nil ? ? H11)
+ |simplify in H13;simplify;elim (remove_inlist ? ? ? H13);
+ elim (in_list_append_to_or_in_list ? ? ? ? H14)
+ [apply in_list_to_in_list_append_l;apply H10
+ [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n4));
+ intro;apply H12;simplify;
+ rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4));
+ elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3) H17);
+ [apply in_list_to_in_list_append_l;assumption
+ |apply in_list_to_in_list_append_r;
+ apply in_list_to_in_list_append_l;assumption]
+ |apply (in_remove ? ? ? H15 H16)]
+ |apply in_list_to_in_list_append_r;apply H11
+ [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3));
+ intro;apply H12;simplify;
+ rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4));
+ elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n4) H17);
+ [apply in_list_to_in_list_append_l;assumption
+ |apply in_list_to_in_list_append_r;
+ apply in_list_to_in_list_append_r;assumption]
+ |apply (in_remove ? ? ? H15 H16)]]
+ |simplify;simplify in H13;elim (remove_inlist ? ? ? H13);
+ elim (nat_in_list_case ? ? ? H14);
+ [apply in_list_to_in_list_append_r;apply in_remove;
+ [elim (remove_inlist ? ? ? H16);intro;apply H18;
+ elim (swap_case a n n3)
+ [elim H20
+ [elim H8;symmetry;rewrite < H21;assumption
+ |elim H9;rewrite < H21;assumption]
+ |rewrite < H20;assumption]
+ |apply H11;
+ [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n5));
+ intro;apply H12;simplify;
+ rewrite < (append_associative ? [x] (fv_Nenv l) (n3::var_NTyp n4 @ var_NTyp n5));
+ elim (nat_in_list_case ? ? ? H17)
+ [apply in_list_to_in_list_append_r;
+ apply in_list_cons;
+ apply in_list_to_in_list_append_r;assumption
+ |apply in_list_to_in_list_append_l;assumption]
+ |elim (remove_inlist ? ? ? H16);apply in_remove
+ [assumption
+ |assumption]]]
+ |apply in_list_to_in_list_append_l;apply H10;
+ [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n4));
+ intro;apply H12;simplify;
+ rewrite < (append_associative ? [x] (fv_Nenv l) (n3::var_NTyp n4@var_NTyp n5));
+ elim (nat_in_list_case ? ? ? H17)
+ [apply in_list_to_in_list_append_r;apply in_list_cons;
+ apply in_list_to_in_list_append_l;assumption
+ |apply in_list_to_in_list_append_l;assumption]
+ |apply in_remove;assumption]]]]
+ |split
+ [intro;apply H7;rewrite > H8;apply in_list_head
+ |elim (remove_inlist ? ? ? H6);assumption]]
+ |intro;apply H7;apply in_list_cons;apply in_list_to_in_list_append_l;
+ assumption
+ |right;intro;apply H7;apply in_list_cons;
+ apply in_list_to_in_list_append_r;apply (incl_fv_var ? ? H8)]]]
+qed.
+
+lemma fv_NTyp_fv_Typ : ∀T,X,l.(X ∈ (fv_NTyp T)) → ¬(X ∈ l) →
+ (X ∈ (fv_type (encodetype T l))).
+intros 2;elim T
+ [simplify;simplify in H;cut (X = n)
+ [rewrite < Hcut;generalize in match (lookup_in X l);elim (lookup X l)
+ [elim H1;apply H2;reflexivity
+ |simplify;apply in_list_head]
+ |(*FIXME*)generalize in match H;intro;inversion H;intros;
+ [destruct H4;reflexivity
+ |destruct H6;elim (not_in_list_nil ? ? H3)]]
+ |simplify in H;elim (not_in_list_nil ? ? H)
+ |simplify;simplify in H2;
+ elim (in_list_append_to_or_in_list ? ? ? ? H2);
+ [apply in_list_to_in_list_append_l;apply (H ? H4 H3)
+ |apply in_list_to_in_list_append_r;apply (H1 ? H4 H3)]
+ |simplify;simplify in H2;
+ elim (in_list_append_to_or_in_list ? ? ? ? H2)
+ [apply in_list_to_in_list_append_l;apply (H ? H4 H3)
+ |apply in_list_to_in_list_append_r;
+ elim (remove_inlist ? ? ? H4);apply (H1 ? H5);intro;apply H6;
+ inversion H7;intros
+ [destruct H9;reflexivity
+ |destruct H11;elim (H3 H8)]]]
+qed.
+
+lemma adeq_WFT : ∀G,T.NWFType G T → WFType (encodeenv G) (encodetype T []).
+intros;elim H
+ [simplify;apply WFT_TFree;rewrite < eq_fv_Nenv_fv_env;assumption
+ |simplify;apply WFT_Top;
+ |simplify;apply WFT_Arrow;assumption
+ |simplify;apply WFT_Forall
+ [assumption
+ |intros;rewrite < (encode_subst n2 X n []);
+ [simplify in H4;apply H4
+ [rewrite > (eq_fv_Nenv_fv_env l);assumption
+ |elim (decidable_eq_nat X n)
+ [left;assumption
+ |right;intro;apply H6;apply (fv_NTyp_fv_Typ ? ? ? H8);intro;
+ apply H7;inversion H9;intros
+ [destruct H11;reflexivity
+ |destruct H13;
+ elim (not_in_list_nil ? ? H10)]]]
+ |4:intro;elim (decidable_eq_nat X n)
+ [assumption
+ |elim H6;cut (¬(X ∈ [n]))
+ [generalize in match Hcut;generalize in match [n];
+ generalize in match H7;elim n2
+ [simplify in H9;generalize in match H9;intro;inversion H9;intros;
+ [destruct H13;destruct;simplify;
+ generalize in match (lookup_in X l1);elim (lookup X l1)
+ [elim H10;apply H12;reflexivity
+ |simplify;apply in_list_head]
+ |destruct H15;
+ elim (not_in_list_nil ? ? H12)]
+ |simplify in H9;elim (not_in_list_nil ? ? H9)
+ |simplify;simplify in H11;
+ elim (in_list_append_to_or_in_list ? ? ? ? H11);autobatch
+ |simplify;simplify in H11;
+ elim (in_list_append_to_or_in_list ? ? ? ? H11);
+ [autobatch
+ |elim (remove_inlist ? ? ? H13);
+ apply in_list_to_in_list_append_r;
+ apply (H10 H14);
+ intro;inversion H16;intros;
+ [destruct H18;destruct;elim H15;reflexivity
+ |destruct H20;elim H12;assumption]]]
+ |intro;elim H8;inversion H9;intros
+ [destruct H11;autobatch
+ |destruct H13;elim (not_in_list_nil ? ? H10)]]]
+ |*:apply not_in_list_nil]]]
+qed.
+
+lemma not_in_list_encodetype : \forall T,l,x.in_list ? x l \to
+ \lnot (in_list ? x (fv_type (encodetype T l))).
+intro;elim T;simplify
+ [apply (bool_elim ? (lookup n l));intro
+ [simplify;apply not_in_list_nil
+ |simplify;intro;inversion H2;intros
+ [destruct H4;
+ rewrite > (in_lookup ? ? H) in H1;destruct H1
+ |destruct H6;apply (not_in_list_nil ? ? H3)]]
+ |apply not_in_list_nil
+ |intro;elim (nat_in_list_case ? ? ? H3)
+ [apply H1;assumption
+ |apply H;assumption]
+ |intro;elim (nat_in_list_case ? ? ? H3)
+ [apply (H1 (n::l) x ? H4);apply in_list_cons;assumption
+ |apply H;assumption]]
+qed.
+
+lemma incl_fv_encode_fv : \forall T,l.incl ? (fv_type (encodetype T l)) (fv_NTyp T).
+intro;elim T;simplify;unfold;
+ [intro;elim (lookup n l)
+ [simplify in H;elim (not_in_list_nil ? ? H)
+ |simplify in H;assumption]
+ |intros;elim (not_in_list_nil ? ? H)
+ |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
+ [apply in_list_to_in_list_append_l;apply H;autobatch
+ |apply in_list_to_in_list_append_r;apply H1;autobatch]
+ |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
+ [apply in_list_to_in_list_append_l;apply H;autobatch
+ |apply in_list_to_in_list_append_r;apply in_remove
+ [intro;apply (not_in_list_encodetype n2 (n::l) x)
+ [rewrite > H4;apply in_list_head
+ |assumption]
+ |apply (H1 (n::l));assumption]]]
+qed.
+
+lemma adeq_WFT2 : ∀G1,T1.WFType G1 T1 →
+ ∀G2,T2.G1 = encodeenv G2 → T1 = encodetype T2 [] →
+ NWFType G2 T2.
+intros 3;elim H
+ [rewrite > H2 in H1;rewrite < eq_fv_Nenv_fv_env in H1;
+ cut (T2 = TName n)
+ [|generalize in match H3;elim T2
+ [simplify in H4;destruct H4;reflexivity
+ |simplify in H4;destruct H4
+ |simplify in H6;destruct H6
+ |simplify in H6;destruct H6]]
+ rewrite > Hcut;apply NWFT_TName;assumption
+ |cut (T2 = NTop)
+ [|generalize in match H2;elim T2
+ [simplify in H3;destruct H3
+ |reflexivity
+ |simplify in H5;destruct H5
+ |simplify in H5;destruct H5]]
+ rewrite > Hcut;apply NWFT_Top;
+ |cut (∃U,V.T2 = (NArrow U V))
+ [|generalize in match H6;elim T2
+ [1,2:simplify in H7;destruct H7
+ |apply (ex_intro ? ? n);apply (ex_intro ? ? n1);reflexivity
+ |simplify in H9;destruct H9]]
+ elim Hcut;elim H7;rewrite > H8 in H6;simplify in H6;destruct H6;
+ apply NWFT_Arrow;autobatch
+ |cut (\exists Z,U,V.T2 = NForall Z U V)
+ [|generalize in match H6;elim T2
+ [1,2:simplify in H7;destruct H7
+ |simplify in H9;destruct H9
+ |apply (ex_intro ? ? n);apply (ex_intro ? ? n1);
+ apply (ex_intro ? ? n2);reflexivity]]
+ elim Hcut;elim H7;elim H8;clear Hcut H7 H8;rewrite > H9;
+ rewrite > H9 in H6;simplify in H6;destruct H6;apply NWFT_Forall
+ [autobatch
+ |intros;elim H6
+ [rewrite > H7;cut (swap_NTyp a a a2 = a2)
+ [|elim a2;simplify
+ [rewrite > swap_same;reflexivity
+ |reflexivity
+ |rewrite > H8;rewrite > H9;reflexivity
+ |rewrite > swap_same;rewrite > H8;rewrite > H9;reflexivity]]
+ rewrite > Hcut;apply (H4 Y)
+ [rewrite < eq_fv_Nenv_fv_env;assumption
+ |rewrite > H7;apply not_in_list_encodetype;
+ apply in_list_head
+ |rewrite > H7;simplify;rewrite < Hcut;reflexivity
+ |rewrite > H7;autobatch]
+ |apply (H4 Y)
+ [rewrite < eq_fv_Nenv_fv_env;assumption
+ |intro;apply H7;apply incl_fv_encode_fv;autobatch
+ |simplify;reflexivity
+ |symmetry;apply (encode_subst a2 Y a []);
+ [3:intro;elim (H7 H8)
+ |*:autobatch]]]]]
+qed.
+
+lemma adeq_WFE : ∀G.NWFEnv G → WFEnv (encodeenv G).
+intros;elim H
+ [simplify;apply WFE_Empty
+ |simplify;apply WFE_cons;
+ [2:rewrite < eq_fv_Nenv_fv_env;]
+ autobatch]
+qed.
+
+lemma NWFT_env_incl : ∀G,T.NWFType G T → ∀H.incl ? (fv_Nenv G) (fv_Nenv H)
+ → NWFType H T.
+intros 3;elim H
+ [apply NWFT_TName;apply (H3 ? H1)
+ |apply NWFT_Top
+ |apply NWFT_Arrow
+ [apply (H2 ? H6)
+ |apply (H4 ? H6)]
+ |apply NWFT_Forall
+ [apply (H2 ? H6)
+ |intros;apply (H4 ? ? H8);
+ [intro;apply H7;apply (H6 ? H9)
+ |unfold;intros;simplify;simplify in H9;inversion H9;intros
+ [destruct H11;apply in_list_head
+ |destruct H13;apply in_list_cons;apply (H6 ? H10)]]]]
+qed.
+
+lemma NJSubtype_to_NWFT : ∀G,T,U.NJSubtype G T U → NWFType G T ∧ NWFType G U.
+intros;elim H
+ [split [assumption|apply NWFT_Top]
+ |split;apply NWFT_TName;assumption
+ |elim H3;split;
+ [apply NWFT_TName;generalize in match H1;elim l
+ [elim (not_in_list_nil ? ? H6)
+ |inversion H7;intros
+ [rewrite < H8;simplify;apply in_list_head
+ |destruct H11;elim t;simplify;apply in_list_cons;
+ apply H6;assumption]]
+ |assumption]
+ |elim H2;elim H4;split;apply NWFT_Arrow;assumption
+ |elim H2;split;apply NWFT_Forall
+ [1,3:assumption
+ |*:intros;elim (H4 Y H7);
+ [apply (NWFT_env_incl ? ? H9);unfold;simplify;intros;inversion H11;intros
+ [destruct H13;apply in_list_head
+ |destruct H15;apply in_list_cons;assumption]
+ |assumption]]
+ |elim H2;split
+ [lapply (adeq_WFT ? ? H5);apply (adeq_WFT2 ? ? Hletin);autobatch
+ |lapply (adeq_WFT ? ? H6);apply (adeq_WFT2 ? ? Hletin);autobatch]]
+qed.
+
+theorem adequacy : ∀G,T,U.NJSubtype G T U →
+ JSubtype (encodeenv G) (encodetype T []) (encodetype U []).
+intros;elim H;simplify
+ [1,3,4:autobatch
+ |apply SA_Refl_TVar
+ [apply (adeq_WFE ? H1)|rewrite < eq_fv_Nenv_fv_env;assumption]
+ |apply SA_All
+ [assumption
+ |intros;lapply (NSA_All ? ? ? ? ? ? H1 H3);rewrite < (encode_subst n2 X n [])
+ [rewrite < (encode_subst n4 X n [])
+ [rewrite < eq_fv_Nenv_fv_env in H5;apply (H4 ? H5)
+ |2,3:apply not_in_list_nil
+ |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);
+ lapply (in_fvNTyp_in_fvNenv ? ? H8);simplify in Hletin1;
+ elim (decidable_eq_nat X n)
+ [assumption
+ |lapply (in_remove ? ? ? H9 H6);elim H5;rewrite < eq_fv_Nenv_fv_env;
+ apply Hletin1;apply in_list_to_in_list_append_r;assumption]]
+ |2,3:apply not_in_list_nil
+ |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);lapply (in_fvNTyp_in_fvNenv ? ? H7);
+ simplify in Hletin1;elim (decidable_eq_nat X n)
+ [assumption
+ |lapply (in_remove ? ? ? H9 H6);elim H5;rewrite < eq_fv_Nenv_fv_env;
+ apply Hletin1;apply in_list_to_in_list_append_r;assumption]]]
+ |rewrite < (alpha_to_encode ? ? H3);rewrite < (alpha_to_encode ? ? H4);
+ assumption]
+qed.
\ No newline at end of file
projects / helm.git / commitdiff