From: Wilmer Ricciotti Date: Fri, 5 Jun 2009 13:27:14 +0000 (+0000) Subject: - replaced part1a/defn with the version based on induction/inversion and deleted X-Git-Tag: make_still_working~3915 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3fb8cc2606e15f256f93c653b5136f609b385208;p=helm.git - replaced part1a/defn with the version based on induction/inversion and deleted older version - more minor improvements --- diff --git a/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma b/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma index a8a5a2340..056a5105b 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma @@ -13,13 +13,7 @@ (* *) (**************************************************************************) -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/defn2.ma". +include "Fsub/part1a.ma". inductive NTyp : Set \def | TName : nat \to NTyp @@ -27,126 +21,80 @@ inductive NTyp : Set \def | 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]]. +definition swap : nat → nat → nat → nat ≝ + λu,v,x.match (eqb x u) with + [true ⇒ v + |false ⇒ match (eqb x v) with + [true ⇒ u + |false ⇒ 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 +lemma swap_left : ∀x,y.(swap x y x) = y. +intros;unfold swap;rewrite > eqb_n_n;simplify;reflexivity; +qed. + +lemma swap_right : ∀x,y.(swap x y y) = x. +intros;unfold swap;rewrite > eqb_n_n;apply (eqb_elim y x);intro;autobatch; +qed. + +lemma swap_other : \forall x,y,z.(z \neq x) \to (z \neq y) \to (swap x y z) = z. +intros;unfold swap;apply (eqb_elim z x);intro;simplify + [elim H;assumption + |rewrite > not_eq_to_eqb_false;autobatch] +qed. + +lemma swap_inv : \forall u,v,x.(swap u v (swap u v x)) = x. +intros;unfold in match (swap u v x);apply (eqb_elim x u);intro;simplify + [autobatch paramodulation + |apply (eqb_elim x v);intro;simplify + [autobatch paramodulation + |apply swap_other;assumption]] +qed. + +lemma swap_inj : ∀u,v,x,y.swap u v x = swap u v y → x = y. +intros 4;unfold swap;apply (eqb_elim x u);simplify;intro + [apply (eqb_elim y u);simplify;intro + [intro;autobatch paramodulation + |apply (eqb_elim y v);simplify;intros + [autobatch paramodulation + |elim H2;symmetry;assumption]] + |apply (eqb_elim y u);simplify;intro + [apply (eqb_elim x v);simplify;intros; + [autobatch paramodulation + |elim H2;assumption] + |apply (eqb_elim x v);simplify;intro + [apply (eqb_elim y v);simplify;intros + [autobatch paramodulation + |elim H1;symmetry;assumption] + |apply (eqb_elim y v);simplify;intros + [elim H;assumption + |assumption]]]] +qed. + +let rec swap_NTyp u v T on T ≝ 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 + [(TName X) ⇒ (TName (swap u v X)) + |NTop ⇒ NTop + |(NArrow T1 T2) ⇒ (NArrow (swap_NTyp u v T1) (swap_NTyp u v T2)) + |(NForall X T1 T2) ⇒ (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))]. + [(TVar n) ⇒ (TVar n) + |(TFree X) ⇒ (TFree (swap u v X)) + |Top ⇒ Top + |(Arrow T1 T2) ⇒ (Arrow (swap_Typ u v T1) (swap_Typ u v T2)) + |(Forall T1 T2) ⇒ (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). @@ -169,27 +117,27 @@ inductive alpha_eq : NTyp \to NTyp \to Prop \def \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 +let rec posn l x on l ≝ match l with - [ nil \Rightarrow O - | (cons (y:nat) l2) \Rightarrow + [ nil ⇒ O + | (cons (y:nat) l2) ⇒ match (eqb x y) with - [ true \Rightarrow O - | false \Rightarrow S (posn l2 x)]]. + [ true ⇒ O + | false ⇒ S (posn l2 x)]]. -let rec length A l on l \def +let rec length A l on l ≝ match l with - [ nil \Rightarrow O - | (cons (y:A) l2) \Rightarrow S (length A l2)]. + [ nil ⇒ O + | (cons (y:A) l2) ⇒ S (length A l2)]. -let rec lookup n l on l \def +let rec lookup n l on l ≝ match l with [ nil ⇒ false - | cons (x:nat) l1 \rArr match (eqb n x) with - [true \rArr true - |false \rArr (lookup n l1)]]. + | cons (x:nat) l1 ⇒ match (eqb n x) with + [true ⇒ true + |false ⇒ (lookup n l1)]]. -let rec encodetype T vars on T \def +let rec encodetype T vars on T ≝ match T with [ (TName n) ⇒ match (lookup n vars) with [ true ⇒ (TVar (posn vars n)) @@ -199,22 +147,17 @@ let rec encodetype T vars on T \def | (NForall n2 T1 T2) ⇒ Forall (encodetype T1 vars) (encodetype T2 (n2::vars))]. -let rec head (A:Type) l on l \def +let rec head (A:Type) l on l ≝ match l with - [ nil \Rightarrow None A - | (cons (x:A) l2) \Rightarrow Some A x]. + [ nil ⇒ None A + | (cons (x:A) l2) ⇒ 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 +let rec nth n l on n ≝ match n with - [ O \Rightarrow match l with + [ O ⇒ match l with [ nil ⇒ O | (cons x l2) ⇒ x] - | (S n2) \Rightarrow (nth n2 (tail ? l))]. + | (S n2) ⇒ (nth n2 (tail ? l))]. definition max_list : (list nat) \to nat \def \lambda l.let rec aux l0 m on l0 \def @@ -225,12 +168,12 @@ definition max_list : (list nat) \to nat \def 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))]. + [ TVar n ⇒ TName (nth n vars) + | TFree x ⇒ TName x + | Top ⇒ 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). @@ -274,11 +217,10 @@ inductive NWFType : (list nbound) → NTyp → Prop ≝ | 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))) → + (∀Y.¬(in_list ? Y (fv_Nenv G)) → + (Y = X ∨ ¬(in_list ? 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 ?)) @@ -301,7 +243,7 @@ inductive NJSubtype : (list nbound) → NTyp → NTyp → Prop ≝ (NWFType G (NForall X S1 S2)) \to (NWFType G (NForall Y T1 T2)) \to (NJSubtype G T1 S1) → - (∀Z.¬(Z ∈ fv_Nenv G) → + (∀Z.¬(in_list ? Z (fv_Nenv G)) → (Z = X \lor \lnot in_list ? Z (fv_NTyp S2)) \to (Z = Y \lor \lnot in_list ? Z (fv_NTyp T2)) \to (NJSubtype ((mk_nbound true Z T1) :: G) @@ -324,49 +266,85 @@ definition encodeenv : list nbound → list 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] +intro;elim G;simplify + [reflexivity + |rewrite < H;elim a;simplify;reflexivity] qed. -(* palloso *) -axiom decidable_eq_bound : \forall b,c:bound.decidable (b = c). +lemma decidable_eq_Typ : ∀T,U:Typ.decidable (T = U). +intro;elim T +[cases U + [cases (decidable_eq_nat n n1) + [left;autobatch + |right;intro;apply H;destruct H1;reflexivity] + |*:right;intro;destruct] +|cases U + [2:cases (decidable_eq_nat n n1) + [left;autobatch + |right;intro;apply H;destruct H1;reflexivity] + |*:right;intro;destruct] +|cases U + [3:left;reflexivity + |*:right;intro;destruct] +|cases U + [4:cases (H t2) + [cases (H1 t3) + [left;autobatch + |right;intro;destruct H4;elim H3;reflexivity] + |right;intro;destruct H3;elim H2;reflexivity] + |*:right;intro;destruct] +|cases U + [5:cases (H t2) + [cases (H1 t3) + [left;autobatch + |right;intro;destruct H4;elim H3;reflexivity] + |right;intro;destruct H3;elim H2;reflexivity] + |*:right;intro;destruct]] +qed. -lemma in_Nenv_to_in_env: ∀l,n,n2.mk_nbound true n n2 ∈ l → - mk_bound true n (encodetype n2 []) ∈ encodeenv l. +lemma decidable_eq_bound : ∀b,c:bound.decidable (b = c). +intros;cases b;cases c;cases (bool_to_decidable_eq b1 b2) +[cases (decidable_eq_nat n n1) + [cases (decidable_eq_Typ t t1) + [left;autobatch + |right;intro;destruct H3;elim H2;reflexivity] + |right;intro;destruct H2;elim H1;reflexivity] +|right;intro;destruct H1;elim H;reflexivity] +qed. + +lemma in_Nenv_to_in_env: ∀l,n,n2.in_list ? (mk_nbound true n n2) l → + in_list ? (mk_bound true n (encodetype n2 [])) (encodeenv l). intros 3;elim l [elim (not_in_list_nil ? ? H) - |inversion H1;intros - [destruct;simplify;apply in_list_head - |destruct;elim t;simplify;apply in_list_cons;apply H;assumption]] + |inversion H1;intros;destruct; + [simplify;apply in_list_head + |elim a;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] +intros;elim H;simplify + [rewrite > eqb_n_n;reflexivity + |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]] + |generalize in match H1;simplify;elim (decidable_eq_nat x a) + [applyS in_list_head + |apply in_list_cons;apply H; + rewrite > (not_eq_to_eqb_false ? ? H2) in H3;simplify in H3;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;simplify;rewrite > eqb_n_n;simplify; + |inversion H1;intros;destruct;simplify + [rewrite > eqb_n_n;simplify; apply lt_O_S - |intros;destruct;simplify;elim (eqb x t);simplify + |elim (eqb x a);simplify [apply lt_O_S |apply le_S_S;apply H;assumption]]] qed. @@ -375,40 +353,87 @@ 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;simplify;rewrite > not_eq_to_eqb_false + |inversion H2;intros;destruct;simplify + [rewrite > not_eq_to_eqb_false [simplify;apply in_list_head |intro;apply H;symmetry;assumption] - |destruct;simplify;elim (eqb b t) - [simplify;apply H1;assumption - |simplify;apply in_list_cons;apply H1;assumption]]] + |elim (eqb b a1);simplify + [apply H1;assumption + |apply in_list_cons;apply H1;assumption]]] qed. -axiom NTyp_len_ind : \forall P:NTyp \to Prop. +lemma 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. +intros; +cut (∀m,n.max m n = m ∨ max m n = n) as Hmax +[|intros;unfold max;cases (leb m n);simplify + [right;reflexivity + |left;reflexivity]] +cut (∀S.nt_len S ≤ nt_len T → P S) +[|elim T + [1,2:simplify in H1;apply H;intros;lapply (trans_le ??? H2 H1); + elim (not_le_Sn_O ? Hletin) + |simplify in H3;apply H;intros;lapply (trans_le ??? H4 H3); + lapply (le_S_S_to_le ?? Hletin) as H5;clear Hletin; + cases (Hmax (nt_len n) (nt_len n1));rewrite > H6 in H5 + [apply H1;assumption + |apply H2;assumption] + |simplify in H3;apply H;intros;lapply (trans_le ??? H4 H3); + lapply (le_S_S_to_le ?? Hletin) as H5;clear Hletin; + cases (Hmax (nt_len n1) (nt_len n2));rewrite > H6 in H5 + [apply H1;assumption + |apply H2;assumption]]] +apply Hcut;apply le_n; +qed. + +(*** even with this lemma, the following autobatch doesn't work properly +lemma aaa : ∀x,y.S x ≤ y → x < y. +intros;apply H; +qed. +*) + +lemma ntlen_arrow1 : ∀T1,T2.(nt_len T1) < (nt_len (NArrow T1 T2)). +intros;cases T2 +[1,2:simplify;(*** autobatch *)apply le_S_S;autobatch +|*:whd in ⊢ (??%);apply le_S_S;apply le_m_max_m_n] +qed. + +lemma ntlen_arrow2 : ∀T1,T2.(nt_len T2) < (nt_len (NArrow T1 T2)). +intros;cases T2 +[1,2:simplify;autobatch +|*:whd in ⊢ (??%);apply le_S_S;apply le_n_max_m_n] +qed. +lemma ntlen_forall1 : ∀X,T1,T2.(nt_len T1) < (nt_len (NForall X T1 T2)). +intros;cases T2 +[1,2:simplify;(*** autobatch *)apply le_S_S;autobatch +|*:whd in ⊢ (??%);apply le_S_S;apply le_m_max_m_n] +qed. + +lemma ntlen_forall2 : ∀X,T1,T2.(nt_len T2) < (nt_len (NForall X T1 T2)). +intros;cases T2 +[1,2:simplify;autobatch +|*:whd in ⊢ (??%);apply le_S_S;apply le_n_max_m_n] +qed. + +lemma eq_ntlen_swap : ∀X,Y,T.nt_len T = nt_len (swap_NTyp X Y T). +intros;elim T;simplify +[1,2:reflexivity +|*:autobatch paramodulation] +qed. + 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) +lemma not_nat_in_to_lookup_false : ∀l,X.¬(in_list ? X l) → lookup X l = false. +intros 2;elim l;simplify + [reflexivity + |elim (decidable_eq_nat X a) [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);]] @@ -421,9 +446,9 @@ lemma fv_encode : ∀T,l1,l2. (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] + [simplify;rewrite < H1;generalize in match H2;elim (lookup n l1);simplify + [rewrite > H3;autobatch + |reflexivity] |apply in_list_head] |simplify;reflexivity |simplify;rewrite > (H l1 l2) @@ -437,74 +462,71 @@ intro;elim T |intros;elim (decidable_eq_nat x n) [simplify;rewrite > (eq_to_eqb_true ? ? H4);simplify;split [reflexivity|intro;reflexivity] - |elim (H2 x) + |elim (H2 x);simplify [split - [simplify;rewrite < H5;reflexivity - |simplify;elim (eqb x n); + [rewrite < H5;reflexivity + |elim (eqb x n) [simplify;reflexivity |simplify in H7;rewrite < (H6 H7);reflexivity]] - |simplify;apply in_list_to_in_list_append_r; + |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) +lemma lookup_swap : ∀a,b,x,vars. + lookup (swap a b x) (swap_list a b vars) = + lookup x vars. +intros 4;elim vars;simplify + [reflexivity + |elim (decidable_eq_nat x a1) [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) + elim (decidable_eq_nat b a1) [rewrite < H3;rewrite > swap_right; rewrite > (not_eq_to_eqb_false b a) [reflexivity |intro;autobatch] - |rewrite > (swap_other a b t) + |rewrite > (swap_other a b a1) [rewrite > (not_eq_to_eqb_false ? ? H3);simplify;reflexivity - |intro;autobatch - |intro;autobatch]] + |*:intro;autobatch]] |elim (decidable_eq_nat x b) [rewrite > H;rewrite > H3;rewrite > swap_right; - elim (decidable_eq_nat t a) + elim (decidable_eq_nat a1 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) + |rewrite > (swap_other a b a1) + [rewrite > (not_eq_to_eqb_false a a1) [reflexivity |intro;autobatch] |assumption |intro;autobatch]] |rewrite > H;rewrite > (swap_other a b x) - [elim (decidable_eq_nat a t) + [elim (decidable_eq_nat a a1) [rewrite > H4;rewrite > swap_left; rewrite > (not_eq_to_eqb_false ? ? H3);reflexivity - |elim (decidable_eq_nat b t) + |elim (decidable_eq_nat b a1) [rewrite > H5;rewrite > swap_right; rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity - |rewrite > (swap_other a b t) + |rewrite > (swap_other a b a1) [rewrite > (not_eq_to_eqb_false ? ? H1);reflexivity - |intro;autobatch - |intro;autobatch]]] - |assumption - |assumption]]]]] + |*:intro;autobatch]]] + |*: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) +lemma posn_swap : ∀a,b,x,vars. + posn vars x = posn (swap_list a b vars) (swap a b x). +intros 4;elim vars;simplify + [reflexivity + |rewrite < H;elim (decidable_eq_nat x a1) [rewrite > H1;do 2 rewrite > eqb_n_n;reflexivity - |elim (decidable_eq_nat (swap a b x) (swap a b t)) + |elim (decidable_eq_nat (swap a b x) (swap a b a1)) [elim H1;autobatch |rewrite > (not_eq_to_eqb_false ? ? H1); rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity]]] -qed. +qed. theorem encode_swap : ∀a,x,T,vars. ((in_list ? a (fv_NTyp T)) → (in_list ? a vars)) → @@ -515,15 +537,9 @@ 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;rewrite > (H3 ? H5); - elim (eqb n1 t);reflexivity]]] + rewrite > Hletin; + rewrite > (in_lookup ?? H1);simplify;lapply (posn_swap a x x vars); + rewrite > swap_right in Hletin1;rewrite < Hletin1;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; @@ -532,39 +548,38 @@ intros 3;elim T |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) + [rewrite > Hcut;elim vars;simplify + [split [reflexivity|intro;reflexivity] + |elim H5;cut + (a1 = a ∨a1 = x ∨ (a1 ≠ a ∧ a1 ≠ x)) + [|elim (decidable_eq_nat a1 a) [left;left;assumption - |elim (decidable_eq_nat t x) + |elim (decidable_eq_nat a1 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;reflexivity - |intros;destruct;elim (not_in_list_nil ? ? H5)]] + decompose; + [rewrite > H10;rewrite > swap_left; + rewrite > (not_eq_to_eqb_false ? ? H2); + rewrite > (not_eq_to_eqb_false ? ? H3);simplify; + split + [assumption + |intro;rewrite < (H7 H5);reflexivity] + |rewrite > H10;rewrite > swap_right; + rewrite > (not_eq_to_eqb_false ? ? H2); + rewrite > (not_eq_to_eqb_false ? ? H3);simplify; + split + [assumption + |intro;rewrite < (H7 H5);reflexivity] + |rewrite > (swap_other a x a1) + [rewrite < H6;split + [reflexivity + |elim (eqb n a1) + [simplify;reflexivity + |simplify in H5;rewrite < (H7 H5);reflexivity]] + |*:assumption]]] + |inversion H4;intros;destruct; + [reflexivity + |elim (not_in_list_nil ? ? H5)]] |*:assumption]]] |simplify;reflexivity |simplify;simplify in H2;rewrite < H @@ -579,71 +594,60 @@ intros 3;elim T [rewrite < (H1 (n::vars)); [reflexivity |intro;rewrite > H4;apply in_list_head - |apply in_list_cons;assumption] + |autobatch] |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]] + |autobatch]] |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 + ¬(in_list ? a (fv_NTyp T)) → + ∀vars.in_list ? 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) +intros 3;elim l 0;simplify;intro + [elim (not_in_list_nil ? ? H) + |elim (decidable_eq_nat y a) [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;split - [apply in_list_head - |intro;autobatch] - |intros;destruct; - elim (H1 H3);split - [apply in_list_cons;assumption - |assumption]]]] + inversion H2;intros;destruct; + [split;autobatch + |elim (H1 H3);split;autobatch]]] qed. -lemma inlist_remove : \forall x,y,l.(in_list ? x l \to x \neq y \to +lemma inlist_remove : ∀x,y,l.(in_list ? x l → x \neq y → (in_list ? x (remove_nat y l))). intros 3;elim l [elim (not_in_list_nil ? ? H); - |simplify;elim (decidable_eq_nat y t) + |simplify;elim (decidable_eq_nat y a) [rewrite > (eq_to_eqb_true ? ? H3);simplify;apply H - [(*FIXME*)generalize in match H1;intro;inversion H1 - [intros;destruct;elim H2;reflexivity - |intros;destruct;assumption] + [inversion H1;intros;destruct; + [elim H2;reflexivity + |assumption] |assumption] |rewrite > (not_eq_to_eqb_false ? ? H3);simplify; - (*FIXME*)generalize in match H1;intro;inversion H4 - [intros;destruct;apply in_list_head - |intros;destruct;apply in_list_cons;apply (H H5 H2) - ]]] + inversion H1;intros;destruct;autobatch]] 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) +intro;elim T;simplify;unfold;intros + [1,2:assumption + |elim (in_list_append_to_or_in_list ? ? ? ? H2);autobatch + |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) + [autobatch |apply in_list_to_in_list_append_r;elim (remove_inlist ? ? ? H4); apply (H1 ? H5)]]] qed. @@ -665,223 +669,186 @@ intros;elim H [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;apply in_list_head - |intros;destruct;apply in_list_cons;inversion H9 - [intros;destruct;elim H7;reflexivity - |intros;destruct; - 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]]]]]] + |apply in_list_cons;inversion H6;intros;destruct; + [apply in_list_head + |apply in_list_cons;inversion H8;intros;destruct; + [elim H7;reflexivity + |elim (in_list_append_to_or_in_list ? ? ? ? H10);autobatch]]]]] +qed. + +(*legacy*) +lemma nat_in_list_case :∀G,H,n.in_list nat n (H@G) → + in_list nat n G ∨ in_list nat n H. +intros;elim (in_list_append_to_or_in_list ???? H1) +[right;assumption +|left;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)))). +lemma inlist_fv_swap : ∀x,y,b,T. + (¬ in_list ? b (y::var_NTyp T)) → + in_list ? x (fv_NTyp (swap_NTyp b y T)) → + x ≠ y ∧ (x = b ∨ (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;split - [unfold;intro;apply H;rewrite > H2;apply in_list_head - |left;reflexivity] - |intros;destruct;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;intro;apply H2; - symmetry;assumption - |intros;destruct; - 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;apply in_list_head - |intros;destruct; - 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;apply in_list_head - |intros;destruct;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;apply in_list_head - |intros;destruct; - 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;apply in_list_head - |intros;destruct;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]]] +[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; + [split + [unfold;intro;apply H;rewrite > H2;apply in_list_head + |left;reflexivity] + |elim (not_in_list_nil ? ? H3)] + |elim (decidable_eq_nat b n) + [rewrite > H3 in H;elim H;autobatch + |rewrite > swap_other in H1 + [split + [inversion H1;intros;destruct; + [intro;apply H2;symmetry;assumption + |elim (not_in_list_nil ? ? H4)] + |autobatch] + |*:intro;autobatch]]] +|simplify in H1;elim (not_in_list_nil ? ? H1) +|simplify;simplify in H3;simplify in H2;elim (in_list_append_to_or_in_list ? ? ? ? H3) + [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; + [apply in_list_head + |apply in_list_cons;apply in_list_to_in_list_append_l;assumption] + |assumption] + |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; + [apply in_list_head + |elim (not_in_list_nil ? ? H7)]] + |assumption]] +|simplify;simplify in H3;simplify in H2;elim (in_list_append_to_or_in_list ? ? ? ? H3) + [elim H + [split + [assumption + |elim H6 + [left;assumption + |right;autobatch]] + |intro;apply H2;inversion H5;intros;destruct; + [apply in_list_head + |apply in_list_cons;elim (decidable_eq_nat b n);autobatch] + |assumption] + |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;autobatch + |destruct;assumption]]]] + |intro;apply H2;inversion H5;intros;destruct; + [apply in_list_head + |apply in_list_cons;change in ⊢ (???%) with ((n::var_NTyp n1)@var_NTyp n2); + elim (n::var_NTyp n1);simplify + [assumption + |elim (decidable_eq_nat b a);autobatch]] + |elim(remove_inlist ? ? ? H4);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 +lemma inlist_fv_swap_r : ∀x,y,b,T. + (¬(in_list ? b (y::var_NTyp T))) → + ((x = b ∧ (in_list ? y (fv_NTyp T))) ∨ + (x \neq y ∧ (in_list ? x (fv_NTyp T)))) → (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;autobatch - |intros;destruct;elim (not_in_list_nil ? ? H5)]] - |elim H2;inversion H4 - [intros;destruct;rewrite > (swap_other b y x) - [apply in_list_head - |intro;autobatch - |assumption] - |intros;destruct;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;apply in_list_head - |intros;destruct;apply in_list_cons; - simplify;apply in_list_to_in_list_append_l; - assumption]] - |intro;apply H2;inversion H4 - [intros;destruct;apply in_list_head - |intros;destruct;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;apply in_list_head - |simplify;intros;destruct; - 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;apply in_list_head - |simplify;intros;destruct; - apply in_list_cons; - apply (in_list_to_in_list_append_l ? ? (n::var_NTyp n1) (var_NTyp n2)); - apply in_list_cons;assumption]]] +[simplify;simplify in H;simplify in H1;cut (b ≠ n) + [elim H1 + [elim H2;cut (y = n) + [rewrite > Hcut1;rewrite > swap_right;rewrite > H3;apply in_list_head + |inversion H4;intros;destruct; + [autobatch + |elim (not_in_list_nil ? ? H5)]] + |elim H2;inversion H4;intros;destruct; + [rewrite > (swap_other b y x) + [apply in_list_head + |intro;autobatch + |assumption] + |elim (not_in_list_nil ? ? H5)]] + |intro;apply H;autobatch] +|simplify in H1;decompose;elim (not_in_list_nil ? ? H3) +|simplify;simplify in H3;cut (\lnot (in_list ? b (y::var_NTyp n1))) + [cut (¬(in_list ? b (y::var_NTyp n))) + [decompose + [elim (in_list_append_to_or_in_list ? ? ? ? H5) + [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 (in_list_append_to_or_in_list ? ? ? ? H5) + [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;simplify;autobatch] + |intro;apply H2;inversion H4;intros;destruct;simplify;autobatch] +|simplify;simplify in H3;cut (¬(in_list ? b (y::var_NTyp n1))) + [cut (¬(in_list ? b (y::var_NTyp n2))) + [decompose + [elim (in_list_append_to_or_in_list ? ? ? ? H5) + [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 ? ? ? H4);assumption]] + |elim (remove_inlist ? ? ? H4);elim (decidable_eq_nat b n) + [rewrite > H8;rewrite > swap_left;intro;apply H7;autobatch paramodulation + |rewrite > swap_other + [rewrite > H3;assumption + |intro;apply H8;symmetry;assumption + |intro;apply H7;symmetry;assumption]]]] + |elim (in_list_append_to_or_in_list ? ? ? ? H5) + [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 ? ? ? H4);assumption]] + |elim (decidable_eq_nat b n) + [rewrite > H6;rewrite > swap_left;assumption + |elim (decidable_eq_nat y n) + [rewrite > H7;rewrite > swap_right;intro;apply Hcut1; + apply in_list_cons;apply incl_fv_var;elim (remove_inlist ? ? ? H4); + rewrite < H8;assumption + |rewrite > (swap_other b y n) + [elim (remove_inlist ? ? ? H4);assumption + |intro;apply H6;symmetry;assumption + |intro;apply H7;symmetry;assumption]]]]]] + |intro;apply H2;inversion H4;simplify;intros;destruct; + [apply in_list_head + |change in ⊢ (???%) with ((y::n::var_NTyp n1)@var_NTyp n2);autobatch]] + |intro;apply H2;inversion H4;simplify;intros;destruct;autobatch depth=4]] 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) +lemma fv_alpha : ∀S,T.alpha_eq S T → incl ? (fv_NTyp S) (fv_NTyp T). +intros;elim H;simplify;unfold;intros + [assumption + |elim (in_list_append_to_or_in_list ? ? ? ? H5);autobatch + |elim (in_list_append_to_or_in_list ? ? ? ? H5) + [autobatch |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3)); apply in_list_to_in_list_append_r; lapply (H4 ? H7); @@ -889,570 +856,468 @@ intros;elim H [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); + [rewrite < H12 in H7;elim H7;autobatch depth=5; |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;apply in_list_head - |intros;destruct;do 2 apply in_list_cons; - apply in_list_to_in_list_append_l;assumption] + |intro;apply H7;inversion H10;intros;destruct;autobatch depth=4 + |autobatch] + |intro;apply H7;inversion H10;intros;destruct;autobatch depth=4 |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) + [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;apply in_list_head - |intros;destruct;do 2 apply in_list_cons; - apply in_list_to_in_list_append_l;assumption] + |apply in_list_cons;inversion H11;intros;destruct;autobatch]] + |intro;apply H7;inversion H11;intros;destruct;autobatch depth=4 |right;split;assumption]]]] qed. -theorem alpha_to_encode : ∀S,T.(alpha_eq S T) → - ∀vars.(encodetype S vars) = (encodetype T vars). +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; - apply in_list_head - |intros;destruct; - 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]]] +[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;autobatch depth=5 + |lapply (encode_swap2 a n5 n3 ? (n5::vars)) + [intro;autobatch depth=5 + |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) + [autobatch + |cut ((x ≠ n4) ∧ (x ≠ n5)) + [elim Hcut;elim (decidable_eq_nat x a);simplify + [rewrite > (eq_to_eqb_true ? ? H10);simplify;autobatch + |rewrite > (not_eq_to_eqb_false ? ? H10);simplify;elim vars;simplify + [autobatch + |elim H11;rewrite < H12;rewrite > H13;elim (decidable_eq_nat a a1) + [rewrite > H14;do 2 rewrite > swap_left; + rewrite > (not_eq_to_eqb_false ? ? H8); + rewrite > (not_eq_to_eqb_false ? ? H9);simplify;autobatch + |elim (decidable_eq_nat n4 a1) + [rewrite > H15;rewrite > swap_right;rewrite > (swap_other a n5 a1) + [rewrite > (not_eq_to_eqb_false ? ? H10);rewrite < H15; + rewrite > (not_eq_to_eqb_false ? ? H8);autobatch + |intro;autobatch + |intro;autobatch] + |rewrite > (swap_other a n4 a1);elim (decidable_eq_nat n5 a1) + [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 a1);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;autobatch depth=4] + |elim (inlist_fv_swap ? ? ? ? ? H6) + [assumption + |intro;apply H5;elim (decidable_eq_nat a n4) + [applyS in_list_head + |apply in_list_cons;inversion H8;intros;destruct;autobatch]]]]]] + |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) +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) + 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;] + |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 + |autobatch + |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] + 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 a);simplify + [reflexivity + |simplify in H3;apply (H2 H3)]]] + |generalize in match H;elim l + [simplify in H2;destruct H2 + |generalize in match H3;simplify;elim (eqb n a) 0;simplify;intro + [reflexivity + |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 a);simplify in H4 + [destruct H4 + |apply (H3 H4)]]] + |elim l;simplify + [rewrite > eqb_n_n;reflexivity + |elim (eqb X a);simplify + [reflexivity + |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 + |elim (eqb n a);simplify + [reflexivity + |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 a);simplify + [reflexivity + |simplify in H1;rewrite < (H H1);reflexivity]]] +|reflexivity +|rewrite < H;rewrite < H1;reflexivity +|rewrite < H;rewrite < (associative_append ? [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) → +lemma encode_subst : ∀T,X,Y,l.¬(in_list ? X l) → ¬(in_list ? Y l) → + (in_list ? 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; - [reflexivity(*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;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;reflexivity - |destruct;elim (H3 H9)] - |intro;apply H6;inversion H8;intros - [destruct;reflexivity - |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]]] +[elim (decidable_eq_nat n X) + [rewrite > H4 in H3;rewrite > H4;rewrite > H3 + [simplify in ⊢ (?? (?%?) ?);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 a) + [elim H6;rewrite > H7;apply in_list_head + |rewrite > (not_eq_to_eqb_false ? ? H7);simplify;rewrite < H5 + [reflexivity + |intro;autobatch]]]] + |elim l;simplify + [rewrite > eqb_n_n;reflexivity + |rewrite > H5;elim (eqb Y a);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 a) + [elim H7;rewrite > H8;apply in_list_head + |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;rewrite < H6 + [reflexivity + |intro;autobatch]]]] + |elim l;simplify + [rewrite > eqb_n_n;reflexivity + |elim (eqb Y a);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 a);simplify + [rewrite > (eq_to_eqb_true ? ? H12);reflexivity + |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 + |reflexivity]] + |*:assumption] + |reflexivity] + |elim l;split + [simplify;cut (n ≠ Y) + [rewrite > (not_eq_to_eqb_false ? ? Hcut);reflexivity + |intro;apply H5;symmetry;assumption] + |intro;simplify in H6;destruct H6 + |elim H6;simplify;rewrite < H7;reflexivity + |simplify;elim (eqb n a);simplify + [reflexivity + |simplify in H7;elim H6;rewrite < (H9 H7);reflexivity]]] + |assumption + |intro;apply H5;symmetry;assumption]]] +|reflexivity +|simplify;rewrite < (H2 n ? ? ? ? H3 H4) + [rewrite < (H2 n1 ? ? ? ? H3 H4); + [1,2:autobatch + |intro;apply H5;simplify;autobatch] + |autobatch + |intro;apply H5;simplify;autobatch] +|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 + |elim (decidable_eq_nat a X) + [elim H8;rewrite > H9;apply in_list_head + |elim (decidable_eq_nat a Y) + [elim H7;rewrite > H10;apply in_list_head + |rewrite > (swap_other X Y a) + [rewrite < H6 + [reflexivity + |*:intro;autobatch] + |*: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; + [reflexivity + |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] + |elim (eqb x a);simplify + [split [reflexivity|intro;reflexivity] + |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]] + |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 + |destruct;rewrite > Hcut1;reflexivity]] + |intro;apply in_list_head + |apply in_list_cons;elim l;simplify;autobatch] + |intros;simplify;rewrite < Hcut; + split [reflexivity|intro;reflexivity]] + |rewrite > (swap_other X Y n) + [rewrite < (associative_append ? [n] l [Y]); + cut (S (length nat l) = length nat (n::l)) [|reflexivity] + rewrite > Hcut1;rewrite < (H2 n2); + [reflexivity |autobatch - |intro;apply H5;simplify;apply in_list_to_in_list_append_l;assumption]] + |intro;apply H7;inversion H8;intros;destruct; + [reflexivity + |elim (H3 H9)] + |intro;apply H6;inversion H8;intros;destruct; + [reflexivity + |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;autobatch]] 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] +intros;unfold in match swap;simplify;elim (eqb x u);simplify + [autobatch + |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;assumption - |destruct;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;elim H8;reflexivity - |destruct;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;simplify; - rewrite > swap_other - [apply in_list_head - |intro;apply H8;rewrite > H13;reflexivity - |intro;apply H9;rewrite > H13;reflexivity] - |destruct;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 - [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 - [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)]]] +intros;elim H;simplify;unfold;intros; +[inversion H2;intros;destruct; + [assumption + |elim (not_in_list_nil ? ? H3)] +|elim (not_in_list_nil ? ? H1) +|elim (in_list_append_to_or_in_list ? ? ? ? H5) + [apply (H2 ? H6)|apply (H4 ? H6)] +|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; + [elim H8;reflexivity + |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;simplify;rewrite > swap_other + [apply in_list_head + |intro;apply H8;rewrite > H13;reflexivity + |intro;apply H9;rewrite > H13;reflexivity] + |destruct;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 + [intro;apply H12;simplify; + rewrite < (associative_append ? [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); + autobatch depth=4 + |apply (in_remove ? ? ? H15 H16)] + |apply in_list_to_in_list_append_r;apply H11 + [intro;apply H12;simplify; + rewrite < (associative_append ? [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); + autobatch depth=5 + |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 < (associative_append ? [x] (fv_Nenv l) (var_NTyp n5)); + intro;apply H12;simplify; + rewrite < (associative_append ? [x] (fv_Nenv l) (n3::var_NTyp n4 @ var_NTyp n5)); + elim (nat_in_list_case ? ? ? H17);autobatch depth=4 + |elim (remove_inlist ? ? ? H16);autobatch]] + |apply in_list_to_in_list_append_l;apply H10; + [rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n4)); + intro;apply H12;simplify; + rewrite < (associative_append ? [x] (fv_Nenv l) (n3::var_NTyp n4@var_NTyp n5)); + elim (nat_in_list_case ? ? ? H17);autobatch depth=4 + |autobatch]]]] + |split + [intro;apply H7;rewrite > H8;apply in_list_head + |elim (remove_inlist ? ? ? H6);assumption]] + |intro;autobatch depth=4 + |right;intro;autobatch depth=5]]] 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) +lemma fv_NTyp_fv_Typ : ∀T,X,l.(in_list ? X (fv_NTyp T)) → ¬(in_list ? X l) → + (in_list ? 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;reflexivity - |destruct;elim (not_in_list_nil ? ? H3)]] + |inversion H;intros;destruct; + [reflexivity + |elim (not_in_list_nil ? ? H2)]] |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; + |simplify in H2;elim (in_list_append_to_or_in_list ? ? ? ? H2);autobatch + |simplify in H2; elim (in_list_append_to_or_in_list ? ? ? ? H2) - [apply in_list_to_in_list_append_l;apply (H ? H4 H3) + [autobatch |apply in_list_to_in_list_append_r; elim (remove_inlist ? ? ? H4);apply (H1 ? H5);intro;apply H6; - inversion H7;intros - [destruct;reflexivity - |destruct;elim (H3 H8)]]] + inversion H7;intros;destruct; + [reflexivity + |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;reflexivity - |destruct; - 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;simplify; - generalize in match (lookup_in X l1);elim (lookup X l1) - [elim H10;apply H12;reflexivity - |simplify;apply in_list_head] - |destruct; - 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;elim H15;reflexivity - |destruct;elim H12;assumption]]] - |intro;elim H8;inversion H9;intros - [destruct;autobatch - |destruct;elim (not_in_list_nil ? ? H10)]]] - |*:apply not_in_list_nil]]] +intros;elim H;simplify +[apply WFT_TFree;rewrite < eq_fv_Nenv_fv_env;assumption +|2,3:autobatch +|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; + [reflexivity + |elim (not_in_list_nil ? ? H10)]]] + |4:intro;elim (decidable_eq_nat X n) + [assumption + |elim H6;cut (¬(in_list ? 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; + [simplify;generalize in match (lookup_in X l1);elim (lookup X l1) + [elim H10;apply H12;reflexivity + |simplify;apply in_list_head] + |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; + [elim H15;reflexivity + |elim H12;assumption]]] + |intro;elim H8;inversion H9;intros;destruct; + [autobatch + |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; - rewrite > (in_lookup ? ? H) in H1;destruct H1 - |destruct;apply (not_in_list_nil ? ? H3)]] + [apply (bool_elim ? (lookup n l));intro;simplify + [apply not_in_list_nil + |intro;inversion H2;intros;destruct; + [rewrite > (in_lookup ? ? H) in H1;destruct H1 + |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) + |intro;elim (nat_in_list_case ? ? ? H3);autobatch + |intro;elim (nat_in_list_case ? ? ? H3); [apply (H1 (n::l) x ? H4);apply in_list_cons;assumption - |apply H;assumption]] + |autobatch]] 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] + [intro;elim (lookup n l);simplify in H + [elim (not_in_list_nil ? ? H) + |assumption] |intros;elim (not_in_list_nil ? ? H) + |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2);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 H1;autobatch] - |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2) - [apply in_list_to_in_list_append_l;apply H;autobatch + [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]]] + [intro;apply (not_in_list_encodetype n2 (n::l) x);autobatch; + |autobatch]]] qed. lemma adeq_WFT2 : ∀G1,T1.WFType G1 T1 → @@ -1461,127 +1326,87 @@ lemma adeq_WFT2 : ∀G1,T1.WFType G1 T1 → 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;reflexivity - |simplify in H4;destruct H4 - |simplify in H6;destruct H6 - |simplify in H6;destruct H6]] + [|elim T2 in H3 + [simplify in H3;destruct;reflexivity + |simplify in H3;destruct H3 + |simplify in H5;destruct H5 + |simplify in H5;destruct H5]] rewrite > Hcut;apply NWFT_TName;assumption |cut (T2 = NTop) - [|generalize in match H2;elim T2 - [simplify in H3;destruct H3 + [|elim T2 in H2 + [simplify in H2;destruct H2 |reflexivity - |simplify in H5;destruct H5 - |simplify in H5;destruct H5]] + |simplify in H4;destruct H4 + |simplify in H4;destruct H4]] 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; - apply NWFT_Arrow;autobatch + [|elim T2 in H6 + [1,2:simplify in H6;destruct H6 + |autobatch; + |simplify in H8;destruct H8]] + elim Hcut;elim H7;rewrite > H8 in H6;simplify in H6;destruct;autobatch size=7 |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 T2 in H6 + [1,2:simplify in H6;destruct + |simplify in H8;destruct + |autobatch depth=4]]] elim Hcut;elim H7;elim H8;clear Hcut H7 H8;rewrite > H9; rewrite > H9 in H6;simplify in H6;destruct;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]] + [|elim a2;simplify;autobatch] 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;reflexivity - |rewrite > H7;autobatch] + [4:rewrite > H7;(*** autobatch *) + change in ⊢ (? ? (? (? ? %) ? ?) ?) with ([]@[a]); + symmetry;rewrite < Hcut in ⊢ (??%?); + change in ⊢ (? ? ? (? ? ? %)) with (length nat []);autobatch + |*:autobatch] |apply (H4 Y) - [rewrite < eq_fv_Nenv_fv_env;assumption - |intro;apply H7;apply incl_fv_encode_fv;autobatch - |simplify;reflexivity + [1,3:autobatch + |intro;autobatch |symmetry;apply (encode_subst a2 Y a []); [3:intro;elim (H7 H8) - |*:autobatch]]]]] + |*: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] +intros;elim H;simplify;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) + [4:apply NWFT_Forall + [autobatch |intros;apply (H4 ? ? H8); [intro;apply H7;apply (H6 ? H9) - |unfold;intros;simplify;simplify in H9;inversion H9;intros - [destruct;apply in_list_head - |destruct;apply in_list_cons;apply (H6 ? H10)]]]] + |unfold;intros;simplify;simplify in H9;inversion H9;intros; + destruct;autobatch]] + |*:autobatch] qed. -(*lemma NWFT_subst : - \forall T,U,a,X,Y,G. - NWFType (mk_nbound true a U::G) (swap_NTyp a X T) \to - \lnot (in_list ? a (Y::X::fv_NTyp T@fv_Nenv G)) \to - \lnot (in_list ? Y (fv_Nenv G)) \to - (Y = X \lor \lnot (in_list ? Y (fv_NTyp T))) \to - NWFType (mk_nbound true Y U::G) (swap_NTyp Y X T). -apply NTyp_len_ind;intro;cases U - [4:simplify;intros;apply NWFT_Forall - [ - |intros;apply (H ? ? ? Y) - [2:inversion H1;simplify;intros;destruct; - [ - -intros 7;elim T - [4:simplify;apply NWFT_Forall - [ - |intros;*) - - 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 + [1,2:split;autobatch |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;elim t;simplify;apply in_list_cons; - apply H6;assumption]] + [apply NWFT_TName;elim l in H1 + [elim (not_in_list_nil ? ? H1) + |inversion H6;intros;destruct; + [simplify;autobatch + |elim a;simplify;autobatch]] |assumption] - |elim H2;elim H4;split;apply NWFT_Arrow;assumption + |elim H2;elim H4;split;autobatch |split;assumption |elim H2;split - [lapply (adeq_WFT ? ? H5);apply (adeq_WFT2 ? ? Hletin);autobatch - |lapply (adeq_WFT ? ? H6);apply (adeq_WFT2 ? ? Hletin);autobatch]] + [lapply (adeq_WFT ? ? H5);autobatch; + |lapply (adeq_WFT ? ? H6);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] + [1,2,3,4:autobatch |apply SA_All [assumption |intros;lapply (NSA_All ? ? ? ? ? ? ? H1 H2 H3 H5); @@ -1596,24 +1421,22 @@ intros;elim H;simplify [elim (decidable_eq_nat X n) [left;assumption |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7; - apply Hletin1;apply in_list_to_in_list_append_r;assumption] + autobatch] |elim (decidable_eq_nat X n1) [left;assumption |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7; - apply Hletin2;apply in_list_to_in_list_append_r;assumption]] + autobatch]] |2,3:apply not_in_list_nil |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin); lapply (in_fvNTyp_in_fvNenv ? ? H10);simplify in Hletin1; elim (decidable_eq_nat X n1) [assumption - |lapply (in_remove ? ? ? H11 H8);elim H7;rewrite < eq_fv_Nenv_fv_env; - apply Hletin1;apply in_list_to_in_list_append_r;assumption]] - |2,3:apply not_in_list_nil + |lapply (in_remove ? ? ? H11 H8);elim H7;autobatch]] + |2,3:autobatch |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);lapply (in_fvNTyp_in_fvNenv ? ? H9); simplify in Hletin1;elim (decidable_eq_nat X n) [assumption - |lapply (in_remove ? ? ? H11 H8);elim H7;rewrite < eq_fv_Nenv_fv_env; - apply Hletin1;apply in_list_to_in_list_append_r;assumption]]] + |lapply (in_remove ? ? ? H11 H8);elim H7;autobatch]]] |rewrite < (alpha_to_encode ? ? H3);rewrite < (alpha_to_encode ? ? H4); assumption] qed. @@ -1637,7 +1460,7 @@ intro;elim l [simplify in H1;elim (not_le_Sn_O ? H1) |simplify in H2;generalize in match H2;elim n [simplify;rewrite > eqb_n_n;simplify;reflexivity - |simplify;cut (nth ? (t::l1) O (S n1) ≠ nth ? (t::l1) O O) + |simplify;cut (nth ? (a::l1) O (S n1) ≠ nth ? (a::l1) O O) [simplify in Hcut;rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify; rewrite > (H n1) [reflexivity @@ -1650,26 +1473,29 @@ intro;elim l [6:apply H5 |skip |skip - |*:autobatch]]]] + |(*** *:autobatch; *) + apply H4 + |simplify;autobatch + |intro;elim (not_eq_O_S n1);symmetry;assumption]]]] qed. -lemma nth_in_list : ∀l,n. n < length ? l → nth ? l O n ∈ l. +lemma nth_in_list : ∀l,n. n < length ? l → in_list ? (nth ? l O n) l. intro;elim l [simplify in H;elim (not_le_Sn_O ? H) - |generalize in match H1;elim n - [simplify;apply in_list_head - |simplify;apply in_list_cons;apply H;simplify in H3;apply (le_S_S_to_le ? ? H3)]] + |generalize in match H1;elim n;simplify + [apply in_list_head + |apply in_list_cons;apply H;simplify in H3;apply (le_S_S_to_le ? ? H3)]] qed. lemma lookup_nth : \forall l,n.n < length ? l \to lookup (nth nat l O n) l = true. intro;elim l [elim (not_le_Sn_O ? H); - |generalize in match H1;elim n - [simplify;rewrite > eqb_n_n;reflexivity - |simplify;elim (eqb (nth nat l1 O n1) t) + |generalize in match H1;elim n;simplify + [rewrite > eqb_n_n;reflexivity + |elim (eqb (nth nat l1 O n1) a);simplify; [reflexivity - |simplify;apply H;apply le_S_S_to_le;assumption]]] + |apply H;apply le_S_S_to_le;assumption]]] qed. lemma decoder : ∀T,n.closed_type T n → @@ -1678,10 +1504,7 @@ lemma decoder : ∀T,n.closed_type T n → ∃U.T = encodetype U l. intro;elim T [simplify in H;apply (ex_intro ? ? (TName (nth ? l O n)));simplify; - rewrite > lookup_nth - [simplify;rewrite > posn_nth; - [reflexivity|assumption|rewrite > H1;assumption] - |rewrite > H1;assumption] + rewrite > lookup_nth;simplify;autobatch; |apply (ex_intro ? ? (TName n));rewrite > (fv_encode (TName n) l []); [simplify;reflexivity |intros;simplify in H3;simplify in H4;lapply (H3 ? H4); @@ -1696,15 +1519,13 @@ intro;elim T |simplify in H2;elim H2;lapply (H ? H6 ? H3 H4); [lapply (H1 ? H7 ? H3 H4) [elim Hletin;elim Hletin1; - apply (ex_intro ? ? (NArrow a a1));simplify; - rewrite < H9;rewrite < H8;reflexivity - |intros;apply H5;simplify;apply in_list_to_in_list_append_r;assumption] - |intros;apply H5;simplify;apply in_list_to_in_list_append_l;assumption] + apply (ex_intro ? ? (NArrow a a1));autobatch; + |intros;apply H5;simplify;autobatch] + |intros;apply H5;simplify;autobatch] |simplify in H2;elim H2;elim (H ? H6 ? H3 H4);elim (fresh_name (fv_type t1@l)); [elim (H1 ? H7 (a1::l)) - [apply (ex_intro ? ? (NForall a1 a a2));simplify;rewrite < H8;rewrite < H10; - reflexivity - |simplify;rewrite > H3;reflexivity + [apply (ex_intro ? ? (NForall a1 a a2));simplify;autobatch + |simplify;autobatch |unfold;intros;intro;apply H12;generalize in match H13;generalize in match H10; generalize in match H11;generalize in match H9; generalize in match m;generalize in match n1; @@ -1712,25 +1533,19 @@ intro;elim T [intro;elim n2 [reflexivity |simplify in H18;rewrite > H18 in H9;elim H9;simplify in H16; - lapply (le_S_S_to_le ? ? H16);apply in_list_to_in_list_append_r; - autobatch] + lapply (le_S_S_to_le ? ? H16);autobatch depth=4] |intro;intros;change in H17:(? ? % ?) with (nth nat l O n2); simplify in H17:(? ? ? %);elim H9;rewrite < H17; apply in_list_to_in_list_append_r;apply nth_in_list; - simplify in H16;apply (le_S_S_to_le ? ? H16) + simplify in H16;autobatch |intros;change in H18 with (nth nat l O n2 = nth nat l O m1); unfold in H4;elim (decidable_eq_nat n2 m1) - [rewrite > H19;reflexivity - |simplify in H17;simplify in H16;elim (H4 ? ? ? ? H19) - [assumption - |apply (le_S_S_to_le ? ? H17) - |apply (le_S_S_to_le ? ? H16)]]] + [autobatch + |simplify in H17;simplify in H16;elim (H4 ? ? ? ? H19);autobatch]] |intro;elim (in_list_cons_case ? ? ? ? H11) [apply H9;apply in_list_to_in_list_append_l;rewrite < H12;assumption - |apply (H5 x) - [simplify;apply in_list_to_in_list_append_r;assumption - |assumption]]] - |apply H5;simplify;apply in_list_to_in_list_append_l;assumption]] + |apply (H5 x);simplify;autobatch]] + |apply H5;simplify;autobatch]] qed. lemma closed_subst : \forall T,X,n.closed_type (subst_type_nat T (TFree X) n) n @@ -1747,15 +1562,13 @@ qed. lemma WFT_to_closed: ∀G,T.WFType G T → closed_type T O. intros;elim H;simplify - [apply I - |apply I + [1,2:apply I |split;assumption |split [assumption |elim (fresh_name (fv_env l@fv_type t1));lapply (H4 a) [autobatch - |intro;apply H5;apply in_list_to_in_list_append_l;assumption - |intro;apply H5;apply in_list_to_in_list_append_r;assumption]]] + |*:intro;autobatch]]] qed. lemma adeq_WFE2 : ∀G1.WFEnv G1 → ∀G2.(G1 = encodeenv G2) → NWFEnv G2. @@ -1765,10 +1578,7 @@ intros 2;elim H 0 |simplify in H2;destruct H2] |intros 9;elim G2 [simplify in H5;destruct H5 - |generalize in match H6;elim t1;simplify in H7;destruct H7;apply NWFE_cons - [apply H2;reflexivity - |rewrite > eq_fv_Nenv_fv_env;assumption - |autobatch]]] + |elim a in H6;simplify in H6;destruct H6;apply NWFE_cons;autobatch]] qed. lemma xxx : \forall b,X,T,l. @@ -1777,9 +1587,9 @@ lemma xxx : \forall b,X,T,l. in_list ? (mk_nbound b X U) l. intros 4;elim l [simplify in H;elim (not_in_list_nil ? ? H) - |simplify in H1;inversion H1;elim t 0;simplify;intros;destruct; + |simplify in H1;inversion H1;elim a 0;simplify;intros;destruct; [apply (ex_intro ? ? n1);split;autobatch - |elim (H H2);elim H4;apply (ex_intro ? ? a);split;autobatch]] + |elim (H H2);elim H4;apply (ex_intro ? ? a1);split;autobatch]] qed. lemma eq_swap_NTyp_to_case : @@ -1792,7 +1602,7 @@ intros 4;elim T [left;assumption |right;intro;apply H3;apply in_list_singleton_to_eq;assumption] |elim (decidable_eq_nat Y n) - [elim H;rewrite > H3;apply in_list_cons;apply in_list_head + [elim H;autobatch; |rewrite > (swap_other Y X n) in H1 [elim (decidable_eq_nat Z n) [rewrite > H4 in H1;do 2 rewrite > swap_left in H1; @@ -1803,10 +1613,8 @@ intros 4;elim T [right;intro;apply H3;simplify in H6; rewrite > (in_list_singleton_to_eq ? ? ? H6) in H1; rewrite > swap_left in H1;destruct H1;reflexivity - |intro;apply H4;symmetry;assumption - |intro;apply H2;symmetry;assumption]]] - |intro;apply H3;symmetry;assumption - |intro;apply H2;symmetry;assumption]]] + |*:intro;autobatch]]] + |*:intro;autobatch]]] |simplify;right;apply not_in_list_nil |elim H [left;assumption @@ -1815,13 +1623,9 @@ intros 4;elim T |right;simplify;intro;elim (in_list_append_to_or_in_list ? ? ? ? H6) [elim (H4 H7) |elim (H5 H7)] - |intro;apply H2;simplify;inversion H5;intros;destruct; - [apply in_list_head - |apply in_list_cons;apply in_list_to_in_list_append_r;assumption] + |intro;apply H2;simplify;inversion H5;intros;destruct;autobatch; |simplify in H3;destruct H3;assumption] - |intro;apply H2;simplify;inversion H4;intros;destruct; - [apply in_list_head - |apply in_list_cons;apply in_list_to_in_list_append_l;assumption] + |intro;apply H2;simplify;inversion H4;intros;destruct;autobatch |simplify in H3;destruct H3;assumption] |elim H [left;assumption @@ -1830,13 +1634,9 @@ intros 4;elim T |right;simplify;intro;elim (in_list_append_to_or_in_list ? ? ? ? H6) [elim (H4 H7) |elim H5;elim (remove_inlist ? ? ? H7);assumption] - |intro;apply H2;simplify;inversion H5;intros;destruct; - [apply in_list_head - |do 2 apply in_list_cons;apply in_list_to_in_list_append_r;assumption] + |intro;apply H2;simplify;inversion H5;intros;destruct;autobatch |simplify in H3;destruct H3;assumption] - |intro;apply H2;simplify;inversion H4;intros;destruct; - [apply in_list_head - |do 2 apply in_list_cons;apply in_list_to_in_list_append_l;assumption] + |intro;apply H2;simplify;inversion H4;intros;destruct;autobatch depth=4; |simplify in H3;destruct H3;assumption]] qed. @@ -1850,68 +1650,52 @@ theorem faithfulness : ∀G1,T1,U1.G1 ⊢ T1 ⊴ U1 → intros 4;elim H 0 [intros;cut (U2 = NTop) [|generalize in match H5;elim U2 0;simplify;intros;destruct;reflexivity] - rewrite > Hcut;apply NSA_Top; - [apply (adeq_WFE2 ? H1);assumption - |apply (adeq_WFT2 ? ? H2);assumption] + rewrite > Hcut;apply NSA_Top;autobatch; |intros;cut (T2 = TName n ∧ U2 = TName n) [|split - [generalize in match H4;elim T2 0;simplify;intros;destruct;reflexivity - |generalize in match H5;elim U2 0;simplify;intros;destruct;reflexivity]] + [elim T2 in H4 0;simplify;intros;destruct;reflexivity + |elim U2 in H5 0;simplify;intros;destruct;reflexivity]] elim Hcut; rewrite > H6;rewrite > H7;apply NSA_Refl_TVar; - [apply (adeq_WFE2 ? H1);assumption + [autobatch |rewrite > H3 in H2;rewrite < eq_fv_Nenv_fv_env in H2;assumption] |intros;cut (T2 = TName n) - [|generalize in match H5;elim T2 0;simplify;intros;destruct;reflexivity] + [|elim T2 in H5 0;simplify;intros;destruct;reflexivity] rewrite > Hcut; elim (decoder t1 O ? []); [rewrite > H4 in H1;rewrite > H7 in H1;elim (xxx ? ? ? ? H1);elim H8; - apply NSA_Trans_TVar - [apply a1 - |assumption - |apply H3;autobatch] - |apply (WFT_to_closed l);apply (JS_to_WFT1 ? ? ? H2) - |simplify;reflexivity - |unfold;intros;simplify in H7;elim (not_le_Sn_O ? H7) - |apply not_in_list_nil] + autobatch + |4:unfold;intros;simplify in H7;elim (not_le_Sn_O ? H7) + |*:autobatch] |intros;cut (∃u,u1,u2,u3.T2 = NArrow u u1 ∧ U2 = NArrow u2 u3) - [elim Hcut;elim H8;elim H9;elim H10;elim H11;clear Hcut H8 H9 H10 H11; - rewrite > H12;rewrite > H13;rewrite > H13 in H7;simplify in H7;destruct; - simplify in H6;destruct;apply NSA_Arrow - [apply H2;reflexivity - |apply H4;reflexivity] + [decompose;rewrite > H8;rewrite > H10;rewrite > H10 in H7;simplify in H7;destruct; + simplify in H6;destruct;autobatch width=4 size=9 |generalize in match H6;elim T2 0;simplify;intros;destruct; generalize in match H7;elim U2 0;simplify;intros;destruct; autobatch depth=6 width=2 size=7] |intros;cut (∃n,u,u1,n1,u2,u3.T2 = NForall n u u1 ∧ U2 = NForall n1 u2 u3) - [elim Hcut;elim H8;elim H9;elim H10;elim H11;elim H12;elim H13; - clear Hcut H8 H9 H10 H11 H12 H13;rewrite > H14;rewrite > H15; - rewrite > H14 in H6;rewrite > H15 in H7;simplify in H6;simplify in H7; - destruct H6;destruct H7;lapply (SA_All ? ? ? ? ? H1 H3);destruct H5; + [decompose;rewrite > H8;rewrite > H10; + rewrite > H8 in H6;rewrite > H10 in H7;simplify in H6;simplify in H7; + destruct;lapply (SA_All ? ? ? ? ? H1 H3); lapply (JS_to_WFT1 ? ? ? Hletin);lapply (JS_to_WFT2 ? ? ? Hletin); apply NSA_All - [apply (adeq_WFT2 ? ? Hletin1);reflexivity - |apply (adeq_WFT2 ? ? Hletin2);reflexivity - |apply H2;reflexivity + [1,2,3:autobatch; |intros;apply H4; [apply Z - |rewrite < eq_fv_Nenv_fv_env;assumption - |simplify;reflexivity + |2,3:autobatch |rewrite < (encode_subst a2 Z a []); - [reflexivity - |2,3:apply not_in_list_nil + [1,2,3:autobatch |lapply (SA_All ? ? ? ? ? H1 H3);lapply (JS_to_WFT1 ? ? ? Hletin); intro;elim (decidable_eq_nat Z a) [assumption |lapply (fv_WFT ? Z ? Hletin1) - [elim H5;rewrite > eq_fv_Nenv_fv_env;assumption + [elim H5;autobatch |simplify;apply in_list_to_in_list_append_r; apply fv_NTyp_fv_Typ [assumption - |intro;apply H9;autobatch]]]] + |intro;autobatch]]]] |rewrite < (encode_subst a5 Z a3 []) - [reflexivity - |2,3:apply not_in_list_nil + [1,2,3:autobatch |intro;elim H7 [assumption |elim (H9 H8)]]]] @@ -1919,3 +1703,7 @@ intros 4;elim H 0 generalize in match H7;elim U2 0;simplify;intros;destruct; autobatch depth=8 width=2 size=9]] qed. + +theorem NJS_trans : ∀G,T,U,V.NJSubtype G T U → NJSubtype G U V → NJSubtype G T V. +intros;apply faithfulness [5,6,7:autobatch|4:autobatch|*:skip] +qed. \ No newline at end of file diff --git a/helm/software/matita/contribs/POPLmark/Fsub/defn2.ma b/helm/software/matita/contribs/POPLmark/Fsub/defn2.ma deleted file mode 100644 index 812c6687d..000000000 --- a/helm/software/matita/contribs/POPLmark/Fsub/defn2.ma +++ /dev/null @@ -1,360 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "Fsub/util.ma". - -(*** representation of Fsub types ***) -inductive Typ : Set \def - | TVar : nat \to Typ (* type var *) - | TFree: nat \to Typ (* free type name *) - | Top : Typ (* maximum type *) - | Arrow : Typ \to Typ \to Typ (* functions *) - | Forall : Typ \to Typ \to Typ. (* universal type *) - -(* representation of bounds *) - -record bound : Set \def { - istype : bool; (* is subtyping bound? *) - name : nat ; (* name *) - btype : Typ (* type to which the name is bound *) - }. - -(*** Various kinds of substitution, not all will be used probably ***) - -(* substitutes i-th dangling index in type T with type U *) -let rec subst_type_nat T U i \def - match T with - [ (TVar n) \Rightarrow match (eqb n i) with - [ true \Rightarrow U - | false \Rightarrow T] - | (TFree X) \Rightarrow T - | Top \Rightarrow T - | (Arrow T1 T2) \Rightarrow (Arrow (subst_type_nat T1 U i) (subst_type_nat T2 U i)) - | (Forall T1 T2) \Rightarrow (Forall (subst_type_nat T1 U i) (subst_type_nat T2 U (S i))) ]. - -(*** definitions about lists ***) - -definition fv_env : (list bound) \to (list nat) \def - \lambda G.(map ? ? (\lambda b.match b with - [(mk_bound B X T) \Rightarrow X]) G). - -let rec fv_type T \def - match T with - [(TVar n) \Rightarrow [] - |(TFree x) \Rightarrow [x] - |Top \Rightarrow [] - |(Arrow U V) \Rightarrow ((fv_type U) @ (fv_type V)) - |(Forall U V) \Rightarrow ((fv_type U) @ (fv_type V))]. - -(*** Type Well-Formedness judgement ***) - -inductive WFType : (list bound) \to Typ \to Prop \def - | WFT_TFree : \forall X,G.(in_list ? X (fv_env G)) - \to (WFType G (TFree X)) - | WFT_Top : \forall G.(WFType G Top) - | WFT_Arrow : \forall G,T,U.(WFType G T) \to (WFType G U) \to - (WFType G (Arrow T U)) - | WFT_Forall : \forall G,T,U.(WFType G T) \to - (\forall X:nat. - (\lnot (in_list ? X (fv_env G))) \to - (\lnot (in_list ? X (fv_type U))) \to - (WFType ((mk_bound true X T) :: G) - (subst_type_nat U (TFree X) O))) \to - (WFType G (Forall T U)). - -(*** Environment Well-Formedness judgement ***) - -inductive WFEnv : (list bound) \to Prop \def - | WFE_Empty : (WFEnv (nil ?)) - | WFE_cons : \forall B,X,T,G.(WFEnv G) \to - \lnot (in_list ? X (fv_env G)) \to - (WFType G T) \to (WFEnv ((mk_bound B X T) :: G)). - -(*** Subtyping judgement ***) -inductive JSubtype : (list bound) \to Typ \to Typ \to Prop \def - | SA_Top : \forall G.\forall T:Typ.(WFEnv G) \to - (WFType G T) \to (JSubtype G T Top) - | SA_Refl_TVar : \forall G.\forall X:nat.(WFEnv G) - \to (in_list ? X (fv_env G)) - \to (JSubtype G (TFree X) (TFree X)) - | SA_Trans_TVar : \forall G.\forall X:nat.\forall T:Typ. - \forall U:Typ. - (in_list ? (mk_bound true X U) G) \to - (JSubtype G U T) \to (JSubtype G (TFree X) T) - | SA_Arrow : \forall G.\forall S1,S2,T1,T2:Typ. - (JSubtype G T1 S1) \to (JSubtype G S2 T2) \to - (JSubtype G (Arrow S1 S2) (Arrow T1 T2)) - | SA_All : \forall G.\forall S1,S2,T1,T2:Typ. - (JSubtype G T1 S1) \to - (\forall X:nat.\lnot (in_list ? X (fv_env G)) \to - (JSubtype ((mk_bound true X T1) :: G) - (subst_type_nat S2 (TFree X) O) (subst_type_nat T2 (TFree X) O))) \to - (JSubtype G (Forall S1 S2) (Forall T1 T2)). - -notation "hvbox(e ⊢ break ta ⊴ break tb)" - non associative with precedence 30 for @{ 'subjudg $e $ta $tb }. -interpretation "Fsub subtype judgement" 'subjudg e ta tb = - (cic:/matita/Fsub/defn2/JSubtype.ind#xpointer(1/1) e ta tb). - -notation > "hvbox(\Forall S.T)" - non associative with precedence 60 for @{ 'forall $S $T}. -notation < "hvbox('All' \sub S. break T)" - non associative with precedence 60 for @{ 'forall $S $T}. -interpretation "universal type" 'forall S T = - (cic:/matita/Fsub/defn2/Typ.ind#xpointer(1/1/5) S T). - -notation "#x" with precedence 79 for @{'tvar $x}. -interpretation "bound tvar" 'tvar x = - (cic:/matita/Fsub/defn2/Typ.ind#xpointer(1/1/1) x). - -notation "!x" with precedence 79 for @{'tname $x}. -interpretation "bound tname" 'tname x = - (cic:/matita/Fsub/defn2/Typ.ind#xpointer(1/1/2) x). - -notation "⊤" with precedence 90 for @{'toptype}. -interpretation "toptype" 'toptype = - (cic:/matita/Fsub/defn2/Typ.ind#xpointer(1/1/3)). - -notation "hvbox(s break ⇛ t)" - right associative with precedence 55 for @{ 'arrow $s $t }. -interpretation "arrow type" 'arrow S T = - (cic:/matita/Fsub/defn2/Typ.ind#xpointer(1/1/4) S T). - -notation "hvbox(S [# n ↦ T])" - non associative with precedence 80 for @{ 'substvar $S $T $n }. -interpretation "subst bound var" 'substvar S T n = - (cic:/matita/Fsub/defn2/subst_type_nat.con S T n). - -notation "hvbox(!X ⊴ T)" - non associative with precedence 60 for @{ 'subtypebound $X $T }. -interpretation "subtyping bound" 'subtypebound X T = - (cic:/matita/Fsub/defn2/bound.ind#xpointer(1/1/1) true X T). - -(****** PROOFS ********) - -(*** theorems about lists ***) - -lemma boundinenv_natinfv : \forall x,G. - (\exists B,T.(in_list ? (mk_bound B x T) G)) \to - (in_list ? x (fv_env G)). -intros 2;elim G - [elim H;elim H1;lapply (not_in_list_nil ? ? H2);elim Hletin - |elim H1;elim H2;elim (in_list_cons_case ? ? ? ? H3) - [rewrite < H4;simplify;apply in_list_head - |simplify;apply in_list_cons;apply H;apply (ex_intro ? ? a1); - apply (ex_intro ? ? a2);assumption]] -qed. - -lemma natinfv_boundinenv : \forall x,G.(in_list ? x (fv_env G)) \to - \exists B,T.(in_list ? (mk_bound B x T) G). -intros 2;elim G 0 - [simplify;intro;lapply (not_in_list_nil ? ? H);elim Hletin - |intros 3; - elim a;simplify in H1;elim (in_list_cons_case ? ? ? ? H1) - [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t);apply in_list_head - |elim (H H2);elim H3;apply (ex_intro ? ? a1); - apply (ex_intro ? ? a2);apply in_list_cons;assumption]] -qed. - -lemma incl_bound_fv : \forall l1,l2.(incl ? l1 l2) \to - (incl ? (fv_env l1) (fv_env l2)). -intros.unfold in H.unfold.intros.apply boundinenv_natinfv. -lapply (natinfv_boundinenv ? ? H1).elim Hletin.elim H2.apply ex_intro - [apply a - |apply ex_intro - [apply a1 - |apply (H ? H3)]] -qed. - -lemma incl_cons : \forall x,l1,l2. - (incl ? l1 l2) \to (incl nat (x :: l1) (x :: l2)). -intros.unfold in H.unfold.intros.elim (in_list_cons_case ? ? ? ? H1) - [rewrite > H2;apply in_list_head|apply in_list_cons;apply (H ? H2)] -qed. - -lemma WFT_env_incl : \forall G,T.(WFType G T) \to - \forall H.(incl ? (fv_env G) (fv_env H)) \to (WFType H T). -intros 3.elim H - [apply WFT_TFree;unfold in H3;apply (H3 ? H1) - |apply WFT_Top - |apply WFT_Arrow [apply (H2 ? H6)|apply (H4 ? H6)] - |apply WFT_Forall - [apply (H2 ? H6) - |intros;apply (H4 ? ? H8) - [unfold;intro;apply H7;apply(H6 ? H9) - |simplify;apply (incl_cons ? ? ? H6)]]] -qed. - -lemma fv_env_extends : \forall H,x,B,C,T,U,G. - (fv_env (H @ ((mk_bound B x T) :: G))) = - (fv_env (H @ ((mk_bound C x U) :: G))). -intros;elim H - [simplify;reflexivity|elim a;simplify;rewrite > H1;reflexivity] -qed. - -lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y. - (in_list ? (mk_bound D y V) (H @ ((mk_bound C x U) :: G))) \to - (y \neq x) \to - (in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G))). -intros 10;elim H - [simplify in H1;elim (in_list_cons_case ? ? ? ? H1) - [destruct H3;elim (H2);reflexivity - |simplify;apply (in_list_cons ? ? ? ? H3);] - |simplify in H2;simplify;elim (in_list_cons_case ? ? ? ? H2) - [rewrite > H4;apply in_list_head - |apply (in_list_cons ? ? ? ? (H1 H4 H3))]] -qed. - -lemma in_FV_subst : \forall x,T,U,n.(in_list ? x (fv_type T)) \to - (in_list ? x (fv_type (subst_type_nat T U n))). -intros 3;elim T - [simplify in H;elim (not_in_list_nil ? ? H) - |2,3:simplify;simplify in H;assumption - |*:simplify in H2;simplify;elim (in_list_append_to_or_in_list ? ? ? ? H2) - [1,3:apply in_list_to_in_list_append_l;apply (H ? H3) - |*:apply in_list_to_in_list_append_r;apply (H1 ? H3)]] -qed. - -(*** lemma on fresh names ***) - -lemma fresh_name : \forall l:(list nat).\exists n.\lnot (in_list ? n l). -cut (\forall l:(list nat).\exists n.\forall m. - (n \leq m) \to \lnot (in_list ? m l)) - [intros;lapply (Hcut l);elim Hletin;apply ex_intro - [apply a - |apply H;constructor 1] - |intros;elim l - [apply (ex_intro ? ? O);intros;unfold;intro;elim (not_in_list_nil ? ? H1) - |elim H; - apply (ex_intro ? ? (S (max a1 a))). - intros.unfold. intro. - elim (in_list_cons_case ? ? ? ? H3) - [rewrite > H4 in H2.autobatch - |elim H4 - [apply (H1 m ? H4).apply (trans_le ? (max a1 a));autobatch - |assumption]]]] -qed. - -(*** lemmata on well-formedness ***) - -lemma fv_WFT : \forall T,x,G.(WFType G T) \to (in_list ? x (fv_type T)) \to - (in_list ? x (fv_env G)). -intros 4.elim H - [simplify in H2;elim (in_list_cons_case ? ? ? ? H2) - [rewrite > H3;assumption|elim (not_in_list_nil ? ? H3)] - |simplify in H1;elim (not_in_list_nil ? x H1) - |simplify in H5;elim (in_list_append_to_or_in_list ? ? ? ? H5);autobatch - |simplify in H5;elim (in_list_append_to_or_in_list ? ? ? ? H5) - [apply (H2 H6) - |elim (fresh_name ((fv_type t1) @ (fv_env l))); - cut (¬ (a ∈ (fv_type t1)) ∧ ¬ (a ∈ (fv_env l))) - [elim Hcut;lapply (H4 ? H9 H8) - [cut (x ≠ a) - [simplify in Hletin;elim (in_list_cons_case ? ? ? ? Hletin) - [elim (Hcut1 H10) - |assumption] - |intro;apply H8;applyS H6] - |apply in_FV_subst;assumption] - |split - [intro;apply H7;apply in_list_to_in_list_append_l;assumption - |intro;apply H7;apply in_list_to_in_list_append_r;assumption]]]] -qed. - -(*** lemmata relating subtyping and well-formedness ***) - -lemma JS_to_WFE : \forall G,T,U.(G \vdash T ⊴ U) \to (WFEnv G). -intros;elim H;assumption. -qed. - -lemma JS_to_WFT : \forall G,T,U.(JSubtype G T U) \to ((WFType G T) \land - (WFType G U)). -intros;elim H - [split [assumption|apply WFT_Top] - |split;apply WFT_TFree;assumption - |split - [apply WFT_TFree;apply boundinenv_natinfv;apply ex_intro - [apply true | apply ex_intro [apply t1 |assumption]] - |elim H3;assumption] - |elim H2;elim H4;split;apply WFT_Arrow;assumption - |elim H2;split - [apply (WFT_Forall ? ? ? H6);intros;elim (H4 X H7); - apply (WFT_env_incl ? ? H9);simplify;unfold;intros;assumption - |apply (WFT_Forall ? ? ? H5);intros;elim (H4 X H7); - apply (WFT_env_incl ? ? H10);simplify;unfold;intros;assumption]] -qed. - -lemma JS_to_WFT1 : \forall G,T,U.(JSubtype G T U) \to (WFType G T). -intros;lapply (JS_to_WFT ? ? ? H);elim Hletin;assumption. -qed. - -lemma JS_to_WFT2 : \forall G,T,U.(JSubtype G T U) \to (WFType G U). -intros;lapply (JS_to_WFT ? ? ? H);elim Hletin;assumption. -qed. - -lemma WFE_Typ_subst : \forall H,x,B,C,T,U,G. - (WFEnv (H @ ((mk_bound B x T) :: G))) \to (WFType G U) \to - (WFEnv (H @ ((mk_bound C x U) :: G))). -intros 7;elim H 0 - [simplify;intros;(*FIXME*)generalize in match H1;intro;inversion H1;intros - [lapply (nil_cons ? G (mk_bound B x T));elim (Hletin H4) - |destruct H8;apply (WFE_cons ? ? ? ? H4 H6 H2)] - |intros;simplify;generalize in match H2;elim a;simplify in H4; - inversion H4;intros - [destruct H5 - |destruct H9;apply WFE_cons - [apply (H1 H5 H3) - |rewrite < (fv_env_extends ? x B C T U); assumption - |apply (WFT_env_incl ? ? H8); - rewrite < (fv_env_extends ? x B C T U);unfold;intros; - assumption]]] -qed. - -lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to - (in_list ? (mk_bound B x T) G) \to - (in_list ? (mk_bound B x U) G) \to T = U. -intros 6;elim H - [lapply (not_in_list_nil ? ? H1);elim Hletin - |elim (in_list_cons_case ? ? ? ? H6) - [destruct H7;destruct;elim (in_list_cons_case ? ? ? ? H5) - [destruct H7;reflexivity - |elim H7;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B); - apply (ex_intro ? ? T);assumption] - |elim (in_list_cons_case ? ? ? ? H5) - [destruct H8;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B); - apply (ex_intro ? ? U);assumption - |apply (H2 H8 H7)]]] -qed. - -lemma WFT_to_incl: ∀G,T,U. - (∀X.(¬(X ∈ fv_env G)) → (¬(X ∈ fv_type U)) → - (WFType (mk_bound true X T::G) (subst_type_nat U (TFree X) O))) - → incl ? (fv_type U) (fv_env G). -intros.elim (fresh_name ((fv_type U)@(fv_env G))).lapply(H a) - [unfold;intros;lapply (fv_WFT ? x ? Hletin) - [simplify in Hletin1;inversion Hletin1;intros - [destruct H4;elim H1;autobatch - |destruct H6;assumption] - |apply in_FV_subst;assumption] - |*:intro;apply H1;autobatch] -qed. - -lemma incl_fv_env: ∀X,G,G1,U,P. - incl ? (fv_env (G1@(mk_bound true X U::G))) - (fv_env (G1@(mk_bound true X P::G))). -intros.rewrite < fv_env_extends.apply incl_A_A. -qed. - -lemma fv_append : ∀G,H.fv_env (G @ H) = (fv_env G @ fv_env H). -intro;elim G;simplify;autobatch paramodulation; -qed. diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma index b113769dd..f38b5b332 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma @@ -14,8 +14,6 @@ include "Fsub/defn.ma". -axiom daemon : False. - (*** Lemma A.1 (Reflexivity) ***) theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴ T. intros 3; elim H; diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma deleted file mode 100644 index c1e909097..000000000 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma +++ /dev/null @@ -1,176 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "Fsub/defn.ma". - -(*** Lemma A.1 (Reflexivity) ***) -theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴ T. -intros 3.elim H - [apply SA_Refl_TVar [apply H2|assumption] - |apply SA_Top [assumption|apply WFT_Top] - |apply (SA_Arrow ? ? ? ? ? (H2 H5) (H4 H5)) - |apply (SA_All ? ? ? ? ? (H2 H5));intros;apply (H4 ? H6) - [intro;apply H6;apply (fv_WFT ? ? ? (WFT_Forall ? ? ? H1 H3)); - simplify; - autobatch; - |autobatch]] -qed. - -(* - * A slightly more general variant to lemma A.2.2, where weakening isn't - * defined as concatenation of any two disjoint environments, but as - * set inclusion. - *) - -lemma JS_weakening : ∀G,T,U.G ⊢ T ⊴ U → ∀H.WFEnv H → incl ? G H → H ⊢ T ⊴ U. -intros 4;elim H - [apply (SA_Top ? ? H4);apply (WFT_env_incl ? ? H2 ? (incl_bound_fv ? ? H5)) - |apply (SA_Refl_TVar ? ? H4);apply (incl_bound_fv ? ? H5 ? H2) - |apply (SA_Trans_TVar ? ? ? ? ? (H3 ? H5 H6));apply H6;assumption - |apply (SA_Arrow ? ? ? ? ? (H2 ? H6 H7) (H4 ? H6 H7)) - |apply (SA_All ? ? ? ? ? (H2 ? H6 H7));intros;apply H4 - [unfold;intro;apply H8;apply (incl_bound_fv ? ? H7 ? H9) - |apply (WFE_cons ? ? ? ? H6 H8);autobatch - |unfold;intros;inversion H9;intros - [destruct H11;apply in_list_head - |destruct H13;apply in_list_cons;apply (H7 ? H10)]]] -qed. - -theorem narrowing:∀X,G,G1,U,P,M,N. - G1 ⊢ P ⊴ U → (∀G2,T.G2@G1 ⊢ U ⊴ T → G2@G1 ⊢ P ⊴ T) → G ⊢ M ⊴ N → - ∀l.G=l@(mk_bound true X U::G1) → l@(mk_bound true X P::G1) ⊢ M ⊴ N. -intros 10.elim H2 - [apply SA_Top - [rewrite > H5 in H3; - apply (WFE_Typ_subst ? ? ? ? ? ? ? H3 (JS_to_WFT1 ? ? ? H)) - |rewrite > H5 in H4;apply (WFT_env_incl ? ? H4);apply incl_fv_env] - |apply SA_Refl_TVar - [rewrite > H5 in H3;apply (WFE_Typ_subst ? ? ? ? ? ? ? H3); - apply (JS_to_WFT1 ? ? ? H) - |rewrite > H5 in H4;rewrite < fv_env_extends;apply H4] - |elim (decidable_eq_nat X n) - [apply (SA_Trans_TVar ? ? ? P) - [rewrite < H7;elim l1;simplify - [constructor 1|constructor 2;assumption] - |rewrite > append_cons;apply H1; - lapply (WFE_bound_bound true n t1 U ? ? H3) - [apply (JS_to_WFE ? ? ? H4) - |rewrite < Hletin;rewrite < append_cons;apply (H5 ? H6) - |rewrite < H7;rewrite > H6;elim l1;simplify - [constructor 1|constructor 2;assumption]]] - |apply (SA_Trans_TVar ? ? ? t1) - [rewrite > H6 in H3;apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H3); - unfold;intro;apply H7;symmetry;assumption - |apply (H5 ? H6)]] - |apply (SA_Arrow ? ? ? ? ? (H4 ? H7) (H6 ? H7)) - |apply (SA_All ? ? ? ? ? (H4 ? H7));intros; - apply (H6 ? ? (mk_bound true X1 t2::l1)) - [rewrite > H7;rewrite > fv_env_extends;apply H8 - |simplify;rewrite < H7;reflexivity]] -qed. - -lemma JSubtype_Arrow_inv: - ∀G:list bound.∀T1,T2,T3:Typ. - ∀P:list bound → Typ → Prop. - (∀n,t1. - (mk_bound true n t1) ∈ G → G ⊢ t1 ⊴ (Arrow T2 T3) → P G t1 → P G (TFree n)) → - (∀t,t1. G ⊢ T2 ⊴ t → G ⊢ t1 ⊴ T3 → P G (Arrow t t1)) → - G ⊢ T1 ⊴ (Arrow T2 T3) → P G T1. - intros; - generalize in match (refl_eq ? (Arrow T2 T3)); - generalize in match (refl_eq ? G); - elim H2 in ⊢ (? ? ? % → ? ? ? % → %); - [1,2: destruct H6 - |5: destruct H8 - | lapply (H5 H6 H7); destruct; clear H5; - apply H; - assumption - | destruct; - clear H4 H6; - apply H1; - assumption - ] -qed. - -lemma JSubtype_Forall_inv: - ∀G:list bound.∀T1,T2,T3:Typ. - ∀P:list bound → Typ → Prop. - (∀n,t1. - (mk_bound true n t1) ∈ G → G ⊢ t1 ⊴ (Forall T2 T3) → P G t1 → P G (TFree n)) → - (∀t,t1. G ⊢ T2 ⊴ t → (∀X. ¬(X ∈ fv_env G) → (mk_bound true X T2)::G ⊢ subst_type_nat t1 (TFree X) O ⊴ subst_type_nat T3 (TFree X) O) - → P G (Forall t t1)) → - G ⊢ T1 ⊴ (Forall T2 T3) → P G T1. - intros; - generalize in match (refl_eq ? (Forall T2 T3)); - generalize in match (refl_eq ? G); - elim H2 in ⊢ (? ? ? % → ? ? ? % → %); - [1,2: destruct H6 - |4: destruct H8 - | lapply (H5 H6 H7); destruct; clear H5; - apply H; - assumption - | destruct; - clear H4 H6; - apply H1; - assumption - ] -qed. - - -lemma JS_trans_prova: ∀T,G1.WFType G1 T → -∀G,R,U.incl ? (fv_env G1) (fv_env G) → G ⊢ R ⊴ T → G ⊢ T ⊴ U → G ⊢ R ⊴ U. -intros 3;elim H;clear H; try autobatch; - [rewrite > (JSubtype_Top ? ? H3);autobatch - |apply (JSubtype_Arrow_inv ? ? ? ? ? ? ? H6); intros; - [ autobatch - | inversion H7;intros; destruct; autobatch depth=4 width=4 size=9] - |apply (JSubtype_Forall_inv ? ? ? ? ? ? ? H6); intros; - [ autobatch - | inversion H7;intros; destruct; - [ apply SA_Top - [ assumption - | apply WFT_Forall; - [ autobatch - | intros;lapply (H8 ? H11); - autobatch]] - | apply SA_All - [ autobatch - | intros;apply (H4 X); - [intro;apply H13;apply H5;assumption - |intro;apply H13;apply H5;apply (WFT_to_incl ? ? ? H3); - assumption - |simplify;autobatch - |apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H9 ? ? []) - [intros;apply H2 - [unfold;intros;lapply (H5 ? H15);rewrite > fv_append; - autobatch - |apply (JS_weakening ? ? ? H9) - [autobatch - |unfold;intros;autobatch] - |assumption] - |*:autobatch] - |autobatch]]]]] -qed. - -theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V. -intros 5;apply (JS_trans_prova ? G);autobatch; -qed. - -theorem JS_narrow : ∀G1,G2,X,P,Q,T,U. - (G2 @ (mk_bound true X Q :: G1)) ⊢ T ⊴ U → G1 ⊢ P ⊴ Q → - (G2 @ (mk_bound true X P :: G1)) ⊢ T ⊴ U. -intros;apply (narrowing ? ? ? ? ? ? ? H1 ? H) [|autobatch] -intros;apply (JS_trans ? ? ? ? ? H2);apply (JS_weakening ? ? ? H1); - [autobatch|unfold;intros;autobatch] -qed. diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion2.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion2.ma deleted file mode 100644 index a9ad6d28d..000000000 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion2.ma +++ /dev/null @@ -1,154 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "Fsub/defn2.ma". - -(*** Lemma A.1 (Reflexivity) ***) -theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴ T. -intros 3.elim H - [apply SA_Refl_TVar [apply H2|assumption] - |apply SA_Top [assumption|apply WFT_Top] - |apply (SA_Arrow ? ? ? ? ? (H2 H5) (H4 H5)) - |apply (SA_All ? ? ? ? ? (H2 H5));intros;apply (H4 ? H6) - [intro;apply H6;apply (fv_WFT ? ? ? (WFT_Forall ? ? ? H1 H3)); - simplify;autobatch - |autobatch]] -qed. - -(* - * A slightly more general variant to lemma A.2.2, where weakening isn't - * defined as concatenation of any two disjoint environments, but as - * set inclusion. - *) - -lemma JS_weakening : ∀G,T,U.G ⊢ T ⊴ U → ∀H.WFEnv H → incl ? G H → H ⊢ T ⊴ U. -intros 4;elim H - [apply (SA_Top ? ? H4);apply (WFT_env_incl ? ? H2 ? (incl_bound_fv ? ? H5)) - |apply (SA_Refl_TVar ? ? H4);apply (incl_bound_fv ? ? H5 ? H2) - |apply (SA_Trans_TVar ? ? ? ? ? (H3 ? H5 H6));apply H6;assumption - |apply (SA_Arrow ? ? ? ? ? (H2 ? H6 H7) (H4 ? H6 H7)) - |apply (SA_All ? ? ? ? ? (H2 ? H6 H7));intros;apply H4 - [unfold;intro;apply H8;apply (incl_bound_fv ? ? H7 ? H9) - |apply (WFE_cons ? ? ? ? H6 H8);autobatch - |unfold;intros;inversion H9;intros - [destruct H11;apply in_list_head - |destruct H13;apply in_list_cons;apply (H7 ? H10)]]] -qed. - -theorem narrowing:∀X,G,G1,U,P,M,N. - G1 ⊢ P ⊴ U → (∀G2,T.G2@G1 ⊢ U ⊴ T → G2@G1 ⊢ P ⊴ T) → G ⊢ M ⊴ N → - ∀l.G=l@(mk_bound true X U::G1) → l@(mk_bound true X P::G1) ⊢ M ⊴ N. -intros 10.elim H2 - [apply SA_Top - [rewrite > H5 in H3; - apply (WFE_Typ_subst ? ? ? ? ? ? ? H3 (JS_to_WFT1 ? ? ? H)) - |rewrite > H5 in H4;apply (WFT_env_incl ? ? H4);apply incl_fv_env] - |apply SA_Refl_TVar - [rewrite > H5 in H3;apply (WFE_Typ_subst ? ? ? ? ? ? ? H3); - apply (JS_to_WFT1 ? ? ? H) - |rewrite > H5 in H4;rewrite < fv_env_extends;apply H4] - |elim (decidable_eq_nat X n) - [apply (SA_Trans_TVar ? ? ? P) - [rewrite < H7;elim l1;simplify - [constructor 1|constructor 2;assumption] - |rewrite > append_cons;apply H1; - lapply (WFE_bound_bound true n t1 U ? ? H3) - [apply (JS_to_WFE ? ? ? H4) - |rewrite < Hletin;rewrite < append_cons;apply (H5 ? H6) - |rewrite < H7;rewrite > H6;elim l1;simplify - [constructor 1|constructor 2;assumption]]] - |apply (SA_Trans_TVar ? ? ? t1) - [rewrite > H6 in H3;apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H3); - unfold;intro;apply H7;symmetry;assumption - |apply (H5 ? H6)]] - |apply (SA_Arrow ? ? ? ? ? (H4 ? H7) (H6 ? H7)) - |apply (SA_All ? ? ? ? ? (H4 ? H7));intros; - apply (H6 ? ? (mk_bound true X1 t2::l1)) - [rewrite > H7;rewrite > fv_env_extends;apply H8 - |simplify;rewrite < H7;reflexivity]] -qed. - -lemma JSubtype_inv: - ∀G:list bound.∀T1,T:Typ. - ∀P:list bound → Typ → Prop. - (∀t. WFEnv G → WFType G t → T=Top → P G t) → - (∀n. T=TFree n → P G (TFree n)) → - (∀n,t1. - (mk_bound true n t1) ∈ G → G ⊢ t1 ⊴ T → P G t1 → P G (TFree n)) → - (∀s1,s2,t1,t2. G ⊢ t1 ⊴ s1 → G ⊢ s2 ⊴ t2 → T=Arrow t1 t2 → P G (Arrow s1 s2)) → - (∀s1,s2,t1,t2. G ⊢ t1 ⊴ s1 → - (∀X. ¬(X ∈ fv_env G) → (mk_bound true X t1)::G ⊢ subst_type_nat s2 (TFree X) O ⊴ subst_type_nat t2 (TFree X) O) - → T=Forall t1 t2 → P G (Forall s1 s2)) → - G ⊢ T1 ⊴ T → P G T1. - intros; - generalize in match (refl_eq ? T); - generalize in match (refl_eq ? G); - elim H5 in ⊢ (? ? ? % → ? ? ? % → %); - [1,2: destruct; autobatch - | rewrite < H9 in H6 H7 H8 ⊢ %; - rewrite < H10 in H7 H8; - autobatch - | rewrite < H10 in H6 H8 ⊢ %; - autobatch - | rewrite < H10 in H6 H8 ⊢ %; - apply (H4 t t1 t2 t3); assumption - ] -qed. - - -lemma JS_trans_prova: ∀T,G1.WFType G1 T → -∀G,R,U.incl ? (fv_env G1) (fv_env G) → G ⊢ R ⊴ T → G ⊢ T ⊴ U → G ⊢ R ⊴ U. -intros 3;elim H;clear H; try autobatch; - [ apply (JSubtype_inv ? ? ? ? ? ? ? ? ? H3); intros; destruct; autobatch - | inversion H3; intros; destruct; assumption - |*: apply (JSubtype_inv ? ? ? ? ? ? ? ? ? H6); intros; destruct; - [1,3: autobatch - |*: inversion H7; intros; destruct; - [1,2: autobatch depth=4 width=4 size=9 - | apply SA_Top - [ assumption - | apply WFT_Forall; - [ autobatch - | intros;lapply (H8 ? H11); - autobatch]] - | apply SA_All - [ autobatch - | intros;apply (H4 X); - [intro; autobatch; - |intro; apply H13;apply H5; apply (WFT_to_incl ? ? ? H3); - assumption - |simplify;autobatch - |apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H9 ? ? []) - [intros;apply H2 - [unfold;intros;lapply (H5 ? H15);rewrite > fv_append; - autobatch - |apply (JS_weakening ? ? ? H9) - [autobatch - |unfold;intros;autobatch] - |assumption] - |*:autobatch] - |autobatch]]]]] -qed. - -theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V. -intros 5;apply (JS_trans_prova ? G);autobatch; -qed. - -theorem JS_narrow : ∀G1,G2,X,P,Q,T,U. - (G2 @ (mk_bound true X Q :: G1)) ⊢ T ⊴ U → G1 ⊢ P ⊴ Q → - (G2 @ (mk_bound true X P :: G1)) ⊢ T ⊴ U. -intros;apply (narrowing ? ? ? ? ? ? ? H1 ? H) [|autobatch] -intros;apply (JS_trans ? ? ? ? ? H2);apply (JS_weakening ? ? ? H1); - [autobatch|unfold;intros;autobatch] -qed. diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma deleted file mode 100644 index 234c6aa39..000000000 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma +++ /dev/null @@ -1,103 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "Fsub/defn2.ma". - -(*** Lemma A.1 (Reflexivity) ***) -theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴ T. -intros 3; elim H; - [1,2,3: autobatch - | apply SA_All; [ autobatch | intros; autobatch depth=4 size=10] - ] -qed. - -(* - * A slightly more general variant to lemma A.2.2, where weakening isn't - * defined as concatenation of any two disjoint environments, but as - * set inclusion. - *) - -lemma JS_weakening : ∀G,T,U.G ⊢ T ⊴ U → ∀H.WFEnv H → incl ? G H → H ⊢ T ⊴ U. -intros 4; elim H; - [1,2,3,4: autobatch depth=4 size=7 - | apply (SA_All ? ? ? ? ? (H2 ? H6 H7)); - intros; apply H4; autobatch depth=4 size=7] -qed. - -lemma JSubtype_inv: - ∀G:list bound.∀T1,T:Typ. - ∀P:list bound → Typ → Typ → Prop. - (∀t. WFEnv G → WFType G t → T=Top → P G t Top) → - (∀n. WFEnv G → n ∈ fv_env G → T=TFree n → P G (TFree n) (TFree n)) → - (∀n,t1,t. - (mk_bound true n t1) ∈ G → G ⊢ t1 ⊴ t → P G t1 t → T=t → P G (TFree n) T) → - (∀s1,s2,t1,t2. G ⊢ t1 ⊴ s1 → G ⊢ s2 ⊴ t2 → T=Arrow t1 t2 → P G (Arrow s1 s2) (Arrow t1 t2)) → - (∀s1,s2,t1,t2. G ⊢ t1 ⊴ s1 → - (∀X. ¬(X ∈ fv_env G) → (mk_bound true X t1)::G ⊢ subst_type_nat s2 (TFree X) O ⊴ subst_type_nat t2 (TFree X) O) - → T=Forall t1 t2 → P G (Forall s1 s2) (Forall t1 t2)) → - G ⊢ T1 ⊴ T → P G T1 T. - intros; - generalize in match (refl_eq ? T); - generalize in match (refl_eq ? G); - elim H5 in ⊢ (? ? ? % → ? ? ? % → %); destruct; autobatch width=4 size=7; -qed. - -theorem narrowing:∀X,G,G1,U,P,M,N. - G1 ⊢ P ⊴ U → (∀G2,T.G2@G1 ⊢ U ⊴ T → G2@G1 ⊢ P ⊴ T) → G ⊢ M ⊴ N → - ∀l.G=l@(mk_bound true X U::G1) → l@(mk_bound true X P::G1) ⊢ M ⊴ N. -intros 10.elim H2; destruct; - [letin x \def fv_env. letin y ≝incl. autobatch depth=4 size=8. - | autobatch depth=4 size=7; - | elim (decidable_eq_nat X n) - [apply (SA_Trans_TVar ? ? ? P); destruct; - [ autobatch - | lapply (WFE_bound_bound true X t1 U ? ? H3); autobatch] - | apply (SA_Trans_TVar ? ? ? t1); autobatch] - | autobatch - | apply SA_All; - [ autobatch - | intros; apply (H6 ? ? (mk_bound true X1 t2::l1));autobatch]] -qed. - -lemma JS_trans_prova: ∀T,G1.WFType G1 T → -∀G,R,U.incl ? (fv_env G1) (fv_env G) → G ⊢ R ⊴ T → G ⊢ T ⊴ U → G ⊢ R ⊴ U. -intros 3;elim H;clear H; try autobatch; - [ apply (JSubtype_inv ? ? ? ? ? ? ? ? ? H3); intros; destruct; autobatch - | inversion H3; intros; destruct; assumption - |*: apply (JSubtype_inv ? ? ? ? ? ? ? ? ? H6); intros; destruct; - [1,3: autobatch - |*: inversion H7; intros; destruct; - [1,2: autobatch depth=4 width=4 size=9 - | apply SA_Top - [ assumption - | apply WFT_Forall;intros;autobatch depth=4] - | apply SA_All - [ autobatch - | intros;apply (H4 X);simplify; - [4: apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H9 ? ? []) - [intros;apply H2;try unfold;intros;autobatch; - |*:autobatch] - |*: autobatch]]]]] -qed. - -theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V. -intros 5; apply (JS_trans_prova ? G); autobatch depth=2. -qed. - -theorem JS_narrow : ∀G1,G2,X,P,Q,T,U. - (G2 @ (mk_bound true X Q :: G1)) ⊢ T ⊴ U → G1 ⊢ P ⊴ Q → - (G2 @ (mk_bound true X P :: G1)) ⊢ T ⊴ U. -intros;apply (narrowing ? ? ? ? ? ? ? H1 ? H) [|autobatch] -intros;apply (JS_trans ? ? ? ? ? H2);apply (JS_weakening ? ? ? H1);autobatch. -qed.