X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FFsub%2Fdefn.ma;h=573b2afe885a1b4768b11c1ac70a4f4e5f65d9da;hb=e5025e47c9354d1bccdcbc5408579d305a493620;hp=1c88186dd30f725fbd20e12a048f2dfca789a361;hpb=b67ae9ad098b77a0458d783019eab58f79f59fcd;p=helm.git diff --git a/helm/software/matita/library/Fsub/defn.ma b/helm/software/matita/library/Fsub/defn.ma index 1c88186dd..573b2afe8 100644 --- a/helm/software/matita/library/Fsub/defn.ma +++ b/helm/software/matita/library/Fsub/defn.ma @@ -13,11 +13,6 @@ (**************************************************************************) set "baseuri" "cic:/matita/Fsub/defn". -include "logic/equality.ma". -include "nat/nat.ma". -include "datatypes/bool.ma". -include "nat/compare.ma". -include "list/list.ma". include "Fsub/util.ma". (*** representation of Fsub types ***) @@ -27,16 +22,7 @@ inductive Typ : Set \def | Top : Typ (* maximum type *) | Arrow : Typ \to Typ \to Typ (* functions *) | Forall : Typ \to Typ \to Typ. (* universal type *) - -(*** representation of Fsub terms ***) -inductive Term : Set \def - | Var : nat \to Term (* variable *) - | Free : nat \to Term (* free name *) - | Abs : Typ \to Term \to Term (* abstraction *) - | App : Term \to Term \to Term (* function application *) - | TAbs : Typ \to Term \to Term (* type abstraction *) - | TApp : Term \to Typ \to Term. (* type application *) - + (* representation of bounds *) record bound : Set \def { @@ -45,48 +31,6 @@ record bound : Set \def { btype : Typ (* type to which the name is bound *) }. -(* representation of Fsub typing environments *) -definition Env \def (list bound). -definition Empty \def (nil bound). -definition Cons \def \lambda G,X,T.((mk_bound false X T) :: G). -definition TCons \def \lambda G,X,T.((mk_bound true X T) :: G). - -definition env_append : Env \to Env \to Env \def \lambda G,H.(H @ G). - -(* notation "hvbox(\Forall S. break T)" - non associative with precedence 90 -for @{ 'forall $S $T}. - -notation "hvbox(#x)" - with precedence 60 - for @{'var $x}. - -notation "hvbox(##x)" - with precedence 61 - for @{'tvar $x}. - -notation "hvbox(!x)" - with precedence 60 - for @{'name $x}. - -notation "hvbox(!!x)" - with precedence 61 - for @{'tname $x}. - -notation "hvbox(s break \mapsto t)" - right associative with precedence 55 - for @{ 'arrow $s $t }. - -interpretation "universal type" 'forall S T = (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/5) S T). - -interpretation "bound var" 'var x = (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/1) x). - -interpretation "bound tvar" 'tvar x = (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/3) x). - -interpretation "bound tname" 'tname x = (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/2) x). - -interpretation "arrow type" 'arrow S T = (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/4) S T). *) - (*** Various kinds of substitution, not all will be used probably ***) (* substitutes i-th dangling index in type T with type U *) @@ -100,49 +44,6 @@ let rec subst_type_nat T U i \def | (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))) ]. -(* substitutes 0-th dangling index in type T with type U *) -let rec subst_type_O T U \def subst_type_nat T U O. - -(* substitutes 0-th dangling index in term t with term u *) -let rec subst_term_O t u \def - let rec aux t0 i \def - match t0 with - [ (Var n) \Rightarrow match (eqb n i) with - [ true \Rightarrow u - | false \Rightarrow t0] - | (Free X) \Rightarrow t0 - | (Abs T1 t1) \Rightarrow (Abs T1 (aux t1 (S i))) - | (App t1 t2) \Rightarrow (App (aux t1 i) (aux t2 i)) - | (TAbs T1 t1) \Rightarrow (TAbs T1 (aux t1 (S i))) - | (TApp t1 T1) \Rightarrow (TApp (aux t1 i) T1) ] - in aux t O. - -(* substitutes 0-th dangling index in term T, which shall be a TVar, - with type U *) -let rec subst_term_tO t T \def - let rec aux t0 i \def - match t0 with - [ (Var n) \Rightarrow t0 - | (Free X) \Rightarrow t0 - | (Abs T1 t1) \Rightarrow (Abs (subst_type_nat T1 T i) (aux t1 (S i))) - | (App t1 t2) \Rightarrow (App (aux t1 i) (aux t2 i)) - | (TAbs T1 t1) \Rightarrow (TAbs (subst_type_nat T1 T i) (aux t1 (S i))) - | (TApp t1 T1) \Rightarrow (TApp (aux t1 i) (subst_type_nat T1 T i)) ] - in aux t O. - -(* substitutes (TFree X) in type T with type U *) -let rec subst_type_tfree_type T X U on T \def - match T with - [ (TVar n) \Rightarrow T - | (TFree Y) \Rightarrow match (eqb X Y) with - [ true \Rightarrow U - | false \Rightarrow T ] - | Top \Rightarrow T - | (Arrow T1 T2) \Rightarrow (Arrow (subst_type_tfree_type T1 X U) - (subst_type_tfree_type T2 X U)) - | (Forall T1 T2) \Rightarrow (Forall (subst_type_tfree_type T1 X U) - (subst_type_tfree_type T2 X U)) ]. - (*** height of T's syntactic tree ***) let rec t_len T \def @@ -153,33 +54,12 @@ let rec t_len T \def |(Arrow T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2))) |(Forall T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))]. -definition head \def - \lambda G:(list bound).match G with - [ nil \Rightarrow (mk_bound false O Top) - | (cons b H) \Rightarrow b]. - -definition head_nat \def - \lambda G:(list nat).match G with - [ nil \Rightarrow O - | (cons n H) \Rightarrow n]. - (*** definitions about lists ***) -(* var binding is in env judgement *) -definition var_bind_in_env : bound \to Env \to Prop \def - \lambda b,G.(in_list bound b G). - 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). -(* variable is in env judgement *) -definition var_in_env : nat \to Env \to Prop \def - \lambda x,G.(in_list nat x (fv_env G)). - -definition var_type_in_env : nat \to Env \to Prop \def - \lambda x,G.\exists T.(var_bind_in_env (mk_bound true x T) G). - let rec fv_type T \def match T with [(TVar n) \Rightarrow [] @@ -190,7 +70,7 @@ let rec fv_type T \def (*** Type Well-Formedness judgement ***) -inductive WFType : Env \to Typ \to Prop \def +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) @@ -201,131 +81,104 @@ inductive WFType : Env \to Typ \to Prop \def (\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_O U (TFree X)))) \to + (subst_type_nat U (TFree X) O))) \to (WFType G (Forall T U)). (*** Environment Well-Formedness judgement ***) -inductive WFEnv : Env \to Prop \def - | WFE_Empty : (WFEnv Empty) +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 : Env \to Typ \to Typ \to Prop \def - | SA_Top : \forall G:Env.\forall T:Typ.(WFEnv G) \to +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:Env.\forall X:nat.(WFEnv G) \to (var_in_env X G) + | 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:Env.\forall X:nat.\forall T:Typ. + | SA_Trans_TVar : \forall G.\forall X:nat.\forall T:Typ. \forall U:Typ. - (var_bind_in_env (mk_bound true X U) G) \to + (in_list ? (mk_bound true X U) G) \to (JSubtype G U T) \to (JSubtype G (TFree X) T) - | SA_Arrow : \forall G:Env.\forall S1,S2,T1,T2:Typ. + | 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:Env.\forall S1,S2,T1,T2:Typ. + | SA_All : \forall G.\forall S1,S2,T1,T2:Typ. (JSubtype G T1 S1) \to - (\forall X:nat.\lnot (var_in_env X G) \to + (\forall X:nat.\lnot (in_list ? X (fv_env G)) \to (JSubtype ((mk_bound true X T1) :: G) - (subst_type_O S2 (TFree X)) (subst_type_O T2 (TFree X)))) \to + (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 \nbsp 'V' \nbsp tb (= \above \alpha))" - non associative with precedence 30 for @{ 'subjudg $e $ta $tb }. -notation > "hvbox(e break ⊢ ta 'Fall' break tb)" - non associative with precedence 30 for @{ 'subjudg $e $ta $tb }. -notation "hvbox(e break ⊢ ta \lessdot break tb)" +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/defn/JSubtype.ind#xpointer(1/1) e ta tb). -lemma xx : \forall e,ta,tb. e \vdash ta Fall tb. -*) - -(*** Typing judgement ***) -inductive JType : Env \to Term \to Typ \to Prop \def - | T_Var : \forall G:Env.\forall x:nat.\forall T:Typ. - (WFEnv G) \to (var_bind_in_env (mk_bound false x T) G) \to - (JType G (Free x) T) - | T_Abs : \forall G.\forall T1,T2:Typ.\forall t2:Term. - \forall x:nat. - (JType ((mk_bound false x T1)::G) (subst_term_O t2 (Free x)) T2) \to - (JType G (Abs T1 t2) (Arrow T1 T2)) - | T_App : \forall G.\forall t1,t2:Term.\forall T2:Typ. - \forall T1:Typ.(JType G t1 (Arrow T1 T2)) \to (JType G t2 T1) \to - (JType G (App t1 t2) T2) - | T_TAbs : \forall G:Env.\forall T1,T2:Typ.\forall t2:Term. - \forall X:nat. - (JType ((mk_bound true X T1)::G) - (subst_term_tO t2 (TFree X)) (subst_type_O T2 (TFree X))) - \to (JType G (TAbs T1 t2) (Forall T1 T2)) - | T_TApp : \forall G:Env.\forall t1:Term.\forall T2,T12:Typ. - \forall X:nat.\forall T11:Typ. - (JType G t1 (Forall T11 (subst_type_tfree_type T12 X (TVar O)))) \to - (JSubtype G T2 T11) - \to (JType G (TApp t1 T2) (subst_type_tfree_type T12 X T2)) - | T_Sub : \forall G:Env.\forall t:Term.\forall T:Typ. - \forall S:Typ.(JType G t S) \to (JSubtype G S T) \to (JType G t T). - -(****** PROOFS ********) - -lemma subst_O_nat : \forall T,U.((subst_type_O T U) = (subst_type_nat T U O)). -intros;elim T;simplify;reflexivity; -qed. - -(*** theorems about lists ***) +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/defn/Typ.ind#xpointer(1/1/5) S T). + +notation "#x" with precedence 79 for @{'tvar $x}. +interpretation "bound tvar" 'tvar x = + (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/1) x). -(* FIXME: these definitions shouldn't be part of the poplmark challenge - - use destruct instead, when hopefully it will get fixed... *) +notation "!x" with precedence 79 for @{'tname $x}. +interpretation "bound tname" 'tname x = + (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/2) x). + +notation "⊤" with precedence 90 for @{'toptype}. +interpretation "toptype" 'toptype = + (cic:/matita/Fsub/defn/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/defn/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/defn/subst_type_nat.con S T n). -lemma inj_head : \forall h1,h2:bound.\forall t1,t2:Env. - ((h1::t1) = (h2::t2)) \to (h1 = h2). -intros. -lapply (eq_f ? ? head ? ? H).simplify in Hletin.assumption. -qed. +notation "hvbox(|T|)" + non associative with precedence 30 for @{ 'tlen $T }. +interpretation "type length" 'tlen T = + (cic:/matita/Fsub/defn/t_len.con T). -lemma inj_head_nat : \forall h1,h2:nat.\forall t1,t2:(list nat). - ((h1::t1) = (h2::t2)) \to (h1 = h2). -intros. -lapply (eq_f ? ? head_nat ? ? H).simplify in Hletin.assumption. -qed. +notation "hvbox(!X ⊴ T)" + non associative with precedence 60 for @{ 'subtypebound $X $T }. +interpretation "subtyping bound" 'subtypebound X T = + (cic:/matita/Fsub/defn/bound.ind#xpointer(1/1/1) true X T). -lemma inj_tail : \forall A.\forall h1,h2:A.\forall t1,t2:(list A). - ((h1::t1) = (h2::t2)) \to (t1 = t2). -intros.lapply (eq_f ? ? (tail ?) ? ? H).simplify in Hletin.assumption. -qed. +(****** PROOFS ********) -(* end of fixme *) +(*** 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 (in_list_nil ? ? H2);elim Hletin - |elim H1;elim H2;inversion H3 - [intros;rewrite < H4;simplify;apply in_Base - |intros;elim a3;simplify;apply in_Skip; - lapply (inj_tail ? ? ? ? ? H7);rewrite > Hletin in H;apply H; - apply ex_intro - [apply a - |apply ex_intro - [apply a1 - |rewrite > H6;assumption]]]] + |elim H1;elim H2;elim (in_cons_case ? ? ? ? H3) + [rewrite < H4;simplify;apply in_Base + |elim H4;elim t;simplify;apply in_Skip2;apply H;apply (ex_intro ? ? a); + apply (ex_intro ? ? a1);assumption]] qed. lemma nat_in_list_case : \forall G,H,n.(in_list nat n (H @ G)) \to (in_list nat n G) \lor (in_list nat n H). intros 3.elim H [simplify in H1;left;assumption - |simplify in H2;inversion H2 - [intros;lapply (inj_head_nat ? ? ? ? H4);rewrite > Hletin; - right;apply in_Base - |intros;lapply (inj_tail ? ? ? ? ? H6);rewrite < Hletin in H3; - rewrite > H5 in H1;lapply (H1 H3);elim Hletin1 - [left;assumption|right;apply in_Skip;assumption]]] + |simplify in H2;elim (in_cons_case ? ? ? ? H2) + [right;rewrite > H3;apply in_Base + |elim H3;elim (H1 H5) [left;assumption|right;apply in_Skip2;assumption]]] qed. lemma natinG_or_inH_to_natinGH : \forall G,H,n. @@ -334,7 +187,7 @@ lemma natinG_or_inH_to_natinGH : \forall G,H,n. intros.elim H1 [elim H [simplify;assumption - |simplify;apply in_Skip;assumption] + |simplify;apply in_Skip2;assumption] |generalize in match H2;elim H2 [simplify;apply in_Base |lapply (H4 H3);simplify;apply in_Skip;assumption]] @@ -344,19 +197,12 @@ 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 (in_list_nil ? ? H);elim Hletin - |intros 3;elim t;simplify in H1;inversion H1 - [intros;rewrite < H2;simplify;apply ex_intro - [apply b - |apply ex_intro - [apply t1 - |lapply (inj_head_nat ? ? ? ? H3);rewrite > H2;rewrite < Hletin; - apply in_Base]] - |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2; - rewrite < H4 in H2;lapply (H H2);elim Hletin1;elim H6;apply ex_intro - [apply a2 - |apply ex_intro - [apply a3 - |apply in_Skip;rewrite < H4;assumption]]]] + |intros 3;elim t;simplify in H1;elim (in_cons_case ? ? ? ? H1) + [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t1);apply in_Base + |elim H2;elim (H H4);elim H5;apply (ex_intro ? ? a); + apply (ex_intro ? ? a1);apply in_Skip + [assumption + |intro;destruct H7;elim (H3 Hcut1)]]] qed. theorem varinT_varinT_subst : \forall X,Y,T. @@ -388,10 +234,8 @@ qed. lemma incl_nat_cons : \forall x,l1,l2. (incl nat l1 l2) \to (incl nat (x :: l1) (x :: l2)). -intros.unfold in H.unfold.intros.inversion H1 - [intros;lapply (inj_head_nat ? ? ? ? H3);rewrite > Hletin;apply in_Base - |intros;apply in_Skip;apply H;lapply (inj_tail ? ? ? ? ? H5);rewrite > Hletin; - assumption] +intros.unfold in H.unfold.intros.elim (in_cons_case ? ? ? ? H1) + [rewrite > H2;apply in_Base|elim H2;apply in_Skip2;apply (H ? H4)] qed. lemma WFT_env_incl : \forall G,T.(WFType G T) \to @@ -402,9 +246,8 @@ intros 3.elim H |apply WFT_Arrow [apply (H2 ? H6)|apply (H4 ? H6)] |apply WFT_Forall [apply (H2 ? H6) - |intros;apply H4 + |intros;apply (H4 ? ? H8) [unfold;intro;apply H7;apply(H6 ? H9) - |assumption |simplify;apply (incl_nat_cons ? ? ? H6)]]] qed. @@ -412,8 +255,7 @@ 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 t;simplify;rewrite > H1;reflexivity] + [simplify;reflexivity|elim t;simplify;rewrite > H1;reflexivity] qed. lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y. @@ -421,26 +263,19 @@ lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y. (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;(*FIXME*)generalize in match H1;intro;inversion H1 - [intros;lapply (inj_head ? ? ? ? H5);rewrite < H4 in Hletin; - destruct Hletin;absurd (y = x) [symmetry;assumption|assumption] - |intros;simplify;lapply (inj_tail ? ? ? ? ? H7);rewrite > Hletin; - apply in_Skip;assumption] - |(*FIXME*)generalize in match H2;intro;inversion H2 - [intros;simplify in H6;lapply (inj_head ? ? ? ? H6);rewrite > Hletin; - simplify;apply in_Base - |simplify;intros;lapply (inj_tail ? ? ? ? ? H8);rewrite > Hletin in H1; - rewrite > H7 in H1;apply in_Skip;apply (H1 H5 H3)]] + [simplify in H1;elim (in_cons_case ? ? ? ? H1) + [destruct H3;elim (H2 Hcut1) + |simplify;elim H3;apply (in_Skip ? ? ? ? H5);intro;destruct H6; + apply (H2 Hcut1)] + |simplify in H2;simplify;elim (in_cons_case ? ? ? ? H2) + [rewrite > H4;apply in_Base + |elim H4;apply (in_Skip ? ? ? ? (H1 H6 H3) H5)]] 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;inversion H - [intros;lapply (sym_eq ? ? ? H2);absurd (a::l = []) - [assumption|apply nil_cons] - |intros;lapply (sym_eq ? ? ? H4);absurd (a1::l = []) - [assumption|apply nil_cons]] + [simplify in H;elim (in_list_nil ? ? H) |2,3:simplify;simplify in H;assumption |*:simplify in H2;simplify;apply natinG_or_inH_to_natinGH; lapply (nat_in_list_case ? ? ? H2);elim Hletin @@ -457,50 +292,14 @@ cut (\forall l:(list nat).\exists n.\forall m. [apply a |apply H;constructor 1] |intros;elim l - [apply ex_intro - [apply O - |intros;unfold;intro;inversion H1 - [intros;lapply (sym_eq ? ? ? H3);absurd (a::l1 = []) - [assumption|apply nil_cons] - |intros;lapply (sym_eq ? ? ? H5);absurd (a1::l1 = []) - [assumption|apply nil_cons]]] - |elim H;lapply (decidable_eq_nat a t);elim Hletin - [apply ex_intro - [apply (S a) - |intros;unfold;intro;inversion H4 - [intros;lapply (inj_head_nat ? ? ? ? H6);rewrite < Hletin1 in H5; - rewrite < H2 in H5;rewrite > H5 in H3; - apply (not_le_Sn_n ? H3) - |intros;lapply (inj_tail ? ? ? ? ? H8);rewrite < Hletin1 in H5; - rewrite < H7 in H5; - apply (H1 m ? H5);lapply (le_S ? ? H3); - apply (le_S_S_to_le ? ? Hletin2)]] - |cut ((leb a t) = true \lor (leb a t) = false) - [elim Hcut - [apply ex_intro - [apply (S t) - |intros;unfold;intro;inversion H5 - [intros;lapply (inj_head_nat ? ? ? ? H7);rewrite > H6 in H4; - rewrite < Hletin1 in H4;apply (not_le_Sn_n ? H4) - |intros;lapply (inj_tail ? ? ? ? ? H9); - rewrite < Hletin1 in H6;lapply (H1 a1) - [apply (Hletin2 H6) - |lapply (leb_to_Prop a t);rewrite > H3 in Hletin2; - simplify in Hletin2;rewrite < H8; - apply (trans_le ? ? ? Hletin2); - apply (trans_le ? ? ? ? H4);constructor 2;constructor 1]]] - |apply ex_intro - [apply a - |intros;lapply (leb_to_Prop a t);rewrite > H3 in Hletin1; - simplify in Hletin1;lapply (not_le_to_lt ? ? Hletin1); - unfold in Hletin2;unfold;intro;inversion H5 - [intros;lapply (inj_head_nat ? ? ? ? H7); - rewrite < Hletin3 in H6;rewrite > H6 in H4; - apply (Hletin1 H4) - |intros;lapply (inj_tail ? ? ? ? ? H9); - rewrite < Hletin3 in H6;rewrite < H8 in H6; - apply (H1 ? H4 H6)]]] - |elim (leb a t);autobatch]]]] + [apply (ex_intro ? ? O);intros;unfold;intro;elim (in_list_nil ? ? H1) + |elim H; + apply (ex_intro ? ? (S (max a t))). + intros.unfold. intro. + elim (in_cons_case ? ? ? ? H3) + [rewrite > H4 in H2.autobatch + |elim H4.apply (H1 m ? H6). + apply (trans_le ? (max a t));autobatch]]] qed. (*** lemmata on well-formedness ***) @@ -508,43 +307,35 @@ qed. 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;inversion H2 - [intros;lapply (inj_head_nat ? ? ? ? H4);rewrite < Hletin;assumption - |intros;lapply (inj_tail ? ? ? ? ? H6);rewrite < Hletin in H3; - inversion H3 - [intros;lapply (sym_eq ? ? ? H8);absurd (a2 :: l2 = []) - [assumption|apply nil_cons] - |intros;lapply (sym_eq ? ? ? H10); - absurd (a3 :: l2 = []) [assumption|apply nil_cons]]] - |simplify in H1;lapply (in_list_nil ? x H1);elim Hletin - |simplify in H5;lapply (nat_in_list_case ? ? ? H5);elim Hletin - [apply (H4 H6) - |apply (H2 H6)] - |simplify in H5;lapply (nat_in_list_case ? ? ? H5);elim Hletin - [lapply (fresh_name ((fv_type t1) @ (fv_env e)));elim Hletin1; - cut ((\lnot (in_list ? a (fv_type t1))) \land - (\lnot (in_list ? a (fv_env e)))) + [simplify in H2;elim (in_cons_case ? ? ? ? H2) + [rewrite > H3;assumption|elim H3;elim (in_list_nil ? ? H5)] + |simplify in H1;elim (in_list_nil ? x H1) + |simplify in H5;elim (nat_in_list_case ? ? ? H5);autobatch + |simplify in H5;elim (nat_in_list_case ? ? ? H5) + [elim (fresh_name ((fv_type t1) @ (fv_env l))); + cut ((¬ (in_list ? a (fv_type t1))) ∧ + (¬ (in_list ? a (fv_env l)))) [elim Hcut;lapply (H4 ? H9 H8) - [cut (x \neq a) - [simplify in Hletin2; - (* FIXME trick *);generalize in match Hletin2;intro; - inversion Hletin2 - [intros;lapply (inj_head_nat ? ? ? ? H12); - rewrite < Hletin3 in H11;lapply (Hcut1 H11);elim Hletin4 - |intros;lapply (inj_tail ? ? ? ? ? H14);rewrite > Hletin3; - assumption] - |unfold;intro;apply H8;rewrite < H10;assumption] - |rewrite > subst_O_nat;apply in_FV_subst;assumption] + [cut (x ≠ a) + [simplify in Hletin;elim (in_cons_case ? ? ? ? Hletin) + [elim (Hcut1 H10)|elim H10;assumption] + |intro;apply H8;rewrite < H10;assumption] + |apply in_FV_subst;assumption] |split - [unfold;intro;apply H7;apply natinG_or_inH_to_natinGH;right; - assumption - |unfold;intro;apply H7;apply natinG_or_inH_to_natinGH;left; - assumption]] + [intro;apply H7;apply natinG_or_inH_to_natinGH;right;assumption + |intro;apply H7;apply natinG_or_inH_to_natinGH;left;assumption]] |apply (H2 H6)]] qed. (*** some exotic inductions and related lemmas ***) +lemma O_lt_t_len: \forall T.O < (t_len T). +intros;elim T + [1,2,3:simplify;apply le_n + |*:simplify;apply lt_O_S] +qed. + +(* lemma not_t_len_lt_SO : \forall T.\lnot (t_len T) < (S O). intros;elim T [1,2,3:simplify;unfold;intro;unfold in H;elim (not_le_Sn_n ? H) @@ -552,6 +343,7 @@ intros;elim T [1,3:simplify in H2;apply H1;apply (trans_lt ? ? ? ? H2);unfold;constructor 1 |*:simplify in H2;apply H;apply (trans_lt ? ? ? ? H2);unfold;constructor 1]] qed. +*) lemma Typ_len_ind : \forall P:Typ \to Prop. (\forall U.(\forall V.((t_len V) < (t_len U)) \to (P V)) @@ -564,7 +356,7 @@ cut (\forall P:Typ \to Prop. [intros;apply (Hcut ? H ? (t_len T));reflexivity |intros 4;generalize in match T;apply (nat_elim1 n);intros; generalize in match H2;elim t - [1,2,3:apply H;intros;simplify in H4;elim (not_t_len_lt_SO ? H4) + [1,2,3:apply H;intros;simplify in H4;elim (lt_to_not_le ? ? H4 (O_lt_t_len ?)) |*:apply H;intros;apply (H1 (t_len V)) [1,3:rewrite > H5;assumption |*:reflexivity]]] @@ -572,68 +364,22 @@ qed. lemma t_len_arrow1 : \forall T1,T2.(t_len T1) < (t_len (Arrow T1 T2)). intros.simplify. -(* FIXME!!! BUG?!?! *) -cut ((max (t_len T1) (t_len T2)) = match (leb (t_len T1) (t_len T2)) with - [ false \Rightarrow (t_len T2) - | true \Rightarrow (t_len T1) ]) - [rewrite > Hcut;cut ((leb (t_len T1) (t_len T2)) = false \lor - (leb (t_len T1) (t_len T2)) = true) - [lapply (leb_to_Prop (t_len T1) (t_len T2));elim Hcut1 - [rewrite > H;rewrite > H in Hletin;simplify;constructor 1 - |rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin; - unfold;apply le_S_S;assumption] - |elim (leb (t_len T1) (t_len T2));autobatch] - |elim T1;simplify;reflexivity] +apply le_S_S.apply le_m_max_m_n. qed. lemma t_len_arrow2 : \forall T1,T2.(t_len T2) < (t_len (Arrow T1 T2)). intros.simplify. -(* FIXME!!! BUG?!?! *) -cut ((max (t_len T1) (t_len T2)) = match (leb (t_len T1) (t_len T2)) with - [ false \Rightarrow (t_len T2) - | true \Rightarrow (t_len T1) ]) - [rewrite > Hcut;cut ((leb (t_len T1) (t_len T2)) = false \lor - (leb (t_len T1) (t_len T2)) = true) - [lapply (leb_to_Prop (t_len T1) (t_len T2));elim Hcut1 - [rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin; - lapply (not_le_to_lt ? ? Hletin);unfold in Hletin1;unfold; - constructor 2;assumption - |rewrite > H;simplify;unfold;constructor 1] - |elim (leb (t_len T1) (t_len T2));autobatch] - |elim T1;simplify;reflexivity] +apply le_S_S.apply le_n_max_m_n. qed. lemma t_len_forall1 : \forall T1,T2.(t_len T1) < (t_len (Forall T1 T2)). intros.simplify. -(* FIXME!!! BUG?!?! *) -cut ((max (t_len T1) (t_len T2)) = match (leb (t_len T1) (t_len T2)) with - [ false \Rightarrow (t_len T2) - | true \Rightarrow (t_len T1) ]) - [rewrite > Hcut;cut ((leb (t_len T1) (t_len T2)) = false \lor - (leb (t_len T1) (t_len T2)) = true) - [lapply (leb_to_Prop (t_len T1) (t_len T2));elim Hcut1 - [rewrite > H;rewrite > H in Hletin;simplify;constructor 1 - |rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin; - unfold;apply le_S_S;assumption] - |elim (leb (t_len T1) (t_len T2));autobatch] - |elim T1;simplify;reflexivity] +apply le_S_S.apply le_m_max_m_n. qed. lemma t_len_forall2 : \forall T1,T2.(t_len T2) < (t_len (Forall T1 T2)). intros.simplify. -(* FIXME!!! BUG?!?! *) -cut ((max (t_len T1) (t_len T2)) = match (leb (t_len T1) (t_len T2)) with - [ false \Rightarrow (t_len T2) - | true \Rightarrow (t_len T1) ]) - [rewrite > Hcut;cut ((leb (t_len T1) (t_len T2)) = false \lor - (leb (t_len T1) (t_len T2)) = true) - [lapply (leb_to_Prop (t_len T1) (t_len T2));elim Hcut1 - [rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin; - lapply (not_le_to_lt ? ? Hletin);unfold in Hletin1;unfold; - constructor 2;assumption - |rewrite > H;simplify;unfold;constructor 1] - |elim (leb (t_len T1) (t_len T2));autobatch] - |elim T1;simplify;reflexivity] +apply le_S_S.apply le_n_max_m_n. qed. lemma eq_t_len_TFree_subst : \forall T,n,X.(t_len T) = @@ -649,7 +395,7 @@ qed. (*** lemmata relating subtyping and well-formedness ***) -lemma JS_to_WFE : \forall G,T,U.(G \vdash T \lessdot U) \to (WFEnv G). +lemma JS_to_WFE : \forall G,T,U.(G \vdash T ⊴ U) \to (WFEnv G). intros;elim H;assumption. qed. @@ -682,27 +428,20 @@ 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));lapply (Hletin H4); - elim Hletin1 - |intros;lapply (inj_tail ? ? ? ? ? H8);lapply (inj_head ? ? ? ? H8); - destruct Hletin1;rewrite < Hletin in H6;rewrite < Hletin in H4; - rewrite < Hcut1 in H6;apply (WFE_cons ? ? ? ? H4 H6 H2)] + [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;rewrite < Hcut2 in H6;rewrite < Hcut in H4; + rewrite < Hcut in H6;apply (WFE_cons ? ? ? ? H4 H6 H2)] |intros;simplify;generalize in match H2;elim t;simplify in H4; - inversion H4 - [intros;absurd (mk_bound b n t1::l@(mk_bound B x T::G)=Empty) - [assumption - |apply nil_cons] - |intros;lapply (inj_tail ? ? ? ? ? H9);lapply (inj_head ? ? ? ? H9); - destruct Hletin1;apply WFE_cons - [apply H1 - [rewrite > Hletin;assumption - |assumption] - |rewrite > Hcut1;generalize in match H7;rewrite < Hletin; - rewrite > (fv_env_extends ? x B C T U);intro;assumption - |rewrite < Hletin in H8;rewrite > Hcut2; - apply (WFT_env_incl ? ? H8);rewrite > (fv_env_extends ? x B C T U); - unfold;intros;assumption]]] + inversion H4;intros + [destruct H5 + |destruct H9;apply WFE_cons + [rewrite < Hcut in H5;apply (H1 H5 H3) + |rewrite < (fv_env_extends ? x B C T U);rewrite > Hcut;rewrite > Hcut2; + assumption + |rewrite < Hcut3 in H8;rewrite > Hcut1;apply (WFT_env_incl ? ? H8); + rewrite < (fv_env_extends ? x B C T U);unfold;intros; + rewrite > Hcut;assumption]]] qed. lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to @@ -710,25 +449,13 @@ lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to (in_list ? (mk_bound B x U) G) \to T = U. intros 6;elim H [lapply (in_list_nil ? ? H1);elim Hletin - |inversion H6 - [intros;rewrite < H7 in H8;lapply (inj_head ? ? ? ? H8); - rewrite > Hletin in H5;inversion H5 - [intros;rewrite < H9 in H10;lapply (inj_head ? ? ? ? H10); - destruct Hletin1;symmetry;assumption - |intros;lapply (inj_tail ? ? ? ? ? H12);rewrite < Hletin1 in H9; - rewrite < H11 in H9;lapply (boundinenv_natinfv x e) - [destruct Hletin;rewrite < Hcut1 in Hletin2;lapply (H3 Hletin2); - elim Hletin3 - |apply ex_intro - [apply B|apply ex_intro [apply T|assumption]]]] - |intros;lapply (inj_tail ? ? ? ? ? H10);rewrite < H9 in H7; - rewrite < Hletin in H7;(*FIXME*)generalize in match H5;intro;inversion H5 - [intros;rewrite < H12 in H13;lapply (inj_head ? ? ? ? H13); - destruct Hletin1;rewrite < Hcut1 in H7; - lapply (boundinenv_natinfv n e) - [lapply (H3 Hletin2);elim Hletin3 - |apply ex_intro - [apply B|apply ex_intro [apply U|assumption]]] - |intros;apply (H2 ? H7);rewrite > H14;lapply (inj_tail ? ? ? ? ? H15); - rewrite > Hletin1;assumption]]] -qed. \ No newline at end of file + |elim (in_cons_case ? ? ? ? H6) + [destruct H7;subst;elim (in_cons_case ? ? ? ? H5) + [destruct H7;assumption + |elim H7;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? b); + apply (ex_intro ? ? T);assumption] + |elim H7;elim (in_cons_case ? ? ? ? H5) + [destruct H10;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B); + apply (ex_intro ? ? U);rewrite < Hcut1;assumption + |elim H10;apply (H2 H12 H9)]]] +qed.