From 5f6974da8825bf7a7b23a5a9c7b051656d03aa37 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 12 Sep 2007 14:30:28 +0000 Subject: [PATCH] Updated, proofs are now about 750 lines. --- helm/software/matita/library/Fsub/defn.ma | 369 +++++--------------- helm/software/matita/library/Fsub/part1a.ma | 145 ++++---- helm/software/matita/library/Fsub/util.ma | 33 +- 3 files changed, 176 insertions(+), 371 deletions(-) diff --git a/helm/software/matita/library/Fsub/defn.ma b/helm/software/matita/library/Fsub/defn.ma index 3264ed5aa..a56b38eaf 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,14 +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). *) - (*** Various kinds of substitution, not all will be used probably ***) (* substitutes i-th dangling index in type T with type U *) @@ -66,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 @@ -119,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 (list bound) \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 (list bound) \to Prop \def - \lambda x,G.(in_list nat x (fv_env G)). - -definition var_type_in_env : nat \to (list bound) \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 [] @@ -238,81 +152,33 @@ notation "hvbox(|T|)" interpretation "type length" 'tlen T = (cic:/matita/Fsub/defn/t_len.con T). -notation > "hvbox(x ∈ l)" - non associative with precedence 30 for @{ 'inlist $x $l }. -notation < "hvbox(x \nbsp ∈ \nbsp l)" - non associative with precedence 30 for @{ 'inlist $x $l }. -interpretation "item in list" 'inlist x l = - (cic:/matita/Fsub/util/in_list.ind#xpointer(1/1) _ x l). - 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). -(*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)" - non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.*) - (****** PROOFS ********) -(*lemma subst_O_nat : \forall T,U.((subst_type_O T U) = T[#O↦U]). -intros;elim T;simplify;reflexivity; -qed.*) - (*** theorems about lists ***) -(* FIXME: these definitions shouldn't be part of the poplmark challenge - - use destruct instead, when hopefully it will get fixed... *) - -lemma inj_head : \forall h1,h2:bound.\forall t1,t2:(list bound). - (h1::t1 = h2::t2) \to h1 = h2. -intros. -lapply (eq_f ? ? head ? ? H).simplify in Hletin.assumption. -qed. - -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. - -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. - -(* end of fixme *) - 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. @@ -321,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]] @@ -331,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. @@ -375,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 @@ -389,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. @@ -399,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. @@ -408,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 @@ -444,49 +292,24 @@ 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)]] + [apply (ex_intro ? ? O);intros;unfold;intro;elim (in_list_nil ? ? H1) + |elim H;elim (decidable_eq_nat a t) + [apply (ex_intro ? ? (S a));intros;intro;elim (in_cons_case ? ? ? ? H4) + [rewrite < H5 in H2;rewrite < H2 in H3;apply (not_le_Sn_n ? H3) + |elim H5;elim (H1 m ? H7);apply (le_S_S_to_le ? ? (le_S ? ? H3))] |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)]]] + [apply (ex_intro ? ? (S t));intros;intro; + elim (in_cons_case ? ? ? ? H5) + [rewrite > H6 in H4;apply (not_le_Sn_n ? H4) + |elim H6;elim (H1 m ? H8);apply (trans_le a t m) + [lapply (leb_to_Prop a t);rewrite > H3 in Hletin;assumption + |apply (le_S_S_to_le t m (le_S (S t) m H4))]] + |apply (ex_intro ? ? a);intros;intro;elim (in_cons_case ? ? ? ? H5) + [lapply (leb_to_Prop a t);rewrite > H3 in Hletin; + simplify in Hletin;lapply (not_le_to_lt ? ? Hletin); + unfold in Hletin1;rewrite < H6 in Hletin;apply (Hletin H4) + |elim H6;elim (H1 ? H4 H8)]] |elim (leb a t);autobatch]]]] qed. @@ -495,38 +318,23 @@ 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 l)));elim Hletin1; - cut ((\lnot (in_list ? a (fv_type t1))) \land - (\lnot (in_list ? a (fv_env l)))) + [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] + [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. @@ -669,27 +477,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)=[]) - [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 @@ -697,25 +498,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 l) - [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 l) - [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]]] + |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. diff --git a/helm/software/matita/library/Fsub/part1a.ma b/helm/software/matita/library/Fsub/part1a.ma index 0437f1e29..7fb8fed9c 100644 --- a/helm/software/matita/library/Fsub/part1a.ma +++ b/helm/software/matita/library/Fsub/part1a.ma @@ -13,75 +13,20 @@ (**************************************************************************) set "baseuri" "cic:/matita/Fsub/part1a/". -include "logic/equality.ma". -include "nat/nat.ma". -include "datatypes/bool.ma". -include "nat/compare.ma". -include "Fsub/util.ma". include "Fsub/defn.ma". (*** Lemma A.1 (Reflexivity) ***) -theorem JS_Refl : \forall T,G.(WFType G T) \to (WFEnv G) \to (JSubtype G T T). -apply Typ_len_ind;intro;elim U - [(* FIXME *) generalize in match H1;intro;inversion H1 - [intros;destruct H6 - |intros;destruct H5 - |*:intros;destruct H9] - |apply (SA_Refl_TVar ? ? H2);(*FIXME*)generalize in match H1;intro; - inversion H1 - [intros;destruct H6;rewrite > Hcut;assumption - |intros;destruct H5 - |*:intros;destruct H9] - |apply (SA_Top ? ? H2 H1) - |cut ((WFType G t) \land (WFType G t1)) - [elim Hcut;apply SA_Arrow - [apply H2 - [apply t_len_arrow1 - |*:assumption] - |apply H2 - [apply t_len_arrow2 - |*:assumption]] - |(* no shortcut? *) - (*FIXME*)generalize in match H3;intro;inversion H3 - [intros;destruct H8 - |intros;destruct H7 - |intros;destruct H11;rewrite > Hcut;rewrite > Hcut1;split;assumption - |intros;destruct H11]] - |cut (WFType G t) - [lapply (H2 t ? ? Hcut H4) - [apply t_len_forall1 - |apply (SA_All ? ? ? ? ? Hletin);intros;apply H2 - [rewrite < eq_t_len_TFree_subst; - apply t_len_forall2 - |generalize in match H3;intro;inversion H3 - [intros;destruct H9 - |intros;destruct H8 - |intros;destruct H12 - |intros;destruct H12;subst;apply H9 - [assumption - |unfold;intro;apply H5; - elim (fresh_name ((fv_env l)@(fv_type t3))); - cut ((\lnot (in_list ? a (fv_env l))) \land - (\lnot (in_list ? a (fv_type t3)))) - [elim Hcut1;lapply (H9 ? H13 H14); - lapply (fv_WFT ? X ? Hletin1) - [simplify in Hletin2;inversion Hletin2 - [intros;lapply (inj_head_nat ? ? ? ? H16);subst; - elim (H14 H11) - |intros;lapply (inj_tail ? ? ? ? ? H18); - rewrite < Hletin3 in H15;assumption] - |apply varinT_varinT_subst; - assumption] - |split;unfold;intro;apply H12;apply natinG_or_inH_to_natinGH - [right;assumption - |left;assumption]]]] - |apply WFE_cons;assumption]] - |(*FIXME*)generalize in match H3;intro;inversion H3 - [intros;destruct H8 - |intros;destruct H7 - |intros;destruct H11 - |intros;destruct H11;subst;assumption]]] +theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴ T. +intros 3;elim H + [apply (SA_Refl_TVar l n H2 H1); + |apply (SA_Top l Top H1 (WFT_Top l)); + |apply (SA_Arrow l t t1 t t1 (H2 H5) (H4 H5)) + |apply (SA_All ? ? ? ? ? (H2 H5));intros;apply (H4 X H6) + [intro;apply H6;apply (fv_WFT (Forall t t1) X l) + [apply (WFT_Forall ? ? ? H1 H3) + |simplify;autobatch] + |autobatch]] qed. (* @@ -106,12 +51,57 @@ intros 4;elim H |apply WFE_cons [1,2:assumption |apply (JS_to_WFT1 ? ? ? Hletin)] - |unfold;intros;inversion H9 - [intros;lapply (inj_head ? ? ? ? H11);rewrite > Hletin1;apply in_Base - |intros;lapply (inj_tail ? ? ? ? ? H13);rewrite < Hletin1 in H10; - apply in_Skip;apply (H7 ? H10)]]] + |unfold;intros;elim (in_cons_case ? ? ? ? H9) + [rewrite > H10;apply in_Base + |elim H10;apply (in_Skip ? ? ? ? ? H11);apply (H7 ? H12)]]] +qed. + +lemma decidable_eq_Typ : \forall S,T:Typ.(S = T) ∨ (S ≠ T). +intro;elim S + [elim T + [elim (decidable_eq_nat n n1) + [rewrite > H;left;reflexivity + |right;intro;destruct H1;apply (H Hcut)] + |2,3:right;intro;destruct H + |*:right;intro;destruct H2] + |elim T + [2:elim (decidable_eq_nat n n1) + [rewrite > H;left;reflexivity + |right;intro;destruct H1;apply (H Hcut)] + |1,3:right;intro;destruct H + |*:right;intro;destruct H2] + |elim T + [3:left;reflexivity + |1,2:right;intro;destruct H + |*:right;intro;destruct H2] + |elim T + [1,2,3:right;intro;destruct H2 + |elim (H t2) + [rewrite > H4;elim (H1 t3) + [rewrite > H5;left;reflexivity + |right;intro;apply H5;destruct H6;assumption] + |right;intro;apply H4;destruct H5;assumption] + |right;intro;destruct H4] + |elim T + [1,2,3:right;intro;destruct H2 + |right;intro;destruct H4 + |elim (H t2) + [rewrite > H4;elim (H1 t3) + [rewrite > H5;left;reflexivity + |right;intro;apply H5;destruct H6;assumption] + |right;intro;apply H4;destruct H5;assumption]]] qed. +lemma decidable_eq_bound: ∀b1,b2:bound.(b1 = b2) ∨ (b1 ≠ b2). +intros;elim b1;elim b2;elim (decidable_eq_nat n n1) + [rewrite < H;elim (decidable_eq_Typ t t1) + [rewrite < H1;elim (bool_to_decidable_eq b b3) + [rewrite > H2;left;reflexivity + |right;intro;destruct H3;apply (H2 Hcut)] + |right;intro;destruct H2;apply (H1 Hcut1)] + |right;intro;destruct H1;apply (H Hcut1)] +qed. + (* Lemma A.3 (Transitivity and Narrowing) *) lemma JS_trans_narrow : \forall Q. @@ -151,17 +141,28 @@ cut (\forall G,T,P. [apply (SA_Trans_TVar ? ? ? P) [rewrite < H10;elim l1 [simplify;constructor 1 - |simplify;constructor 2;assumption] + |simplify;elim (decidable_eq_bound (mk_bound true X P) t2) + [rewrite < H12;apply in_Base + |apply (in_Skip ? ? ? ? ? H12);assumption]] |apply H7 [lapply (H6 ? H7 H8 H9);lapply (JS_to_WFE ? ? ? Hletin); apply (JS_weakening ? ? ? H3 ? Hletin1);unfold;intros; - elim l1;simplify;constructor 2;assumption + elim l1 + [simplify; + elim (decidable_eq_bound x (mk_bound true X P)) + [rewrite < H12;apply in_Base + |apply (in_Skip ? ? ? ? ? H12);assumption] + |simplify;elim (decidable_eq_bound x t2) + [rewrite < H13;apply in_Base + |apply (in_Skip ? ? ? ? ? H13);assumption]] |lapply (WFE_bound_bound true n t1 U ? ? H4) [apply (JS_to_WFE ? ? ? H5) |rewrite < Hletin;apply (H6 ? H7 H8 H9) |rewrite > H9;rewrite > H10;elim l1;simplify [constructor 1 - |constructor 2;assumption]]]] + |elim (decidable_eq_bound (mk_bound true n U) t2) + [rewrite > H12;apply in_Base + |apply (in_Skip ? ? ? ? ? H12);assumption]]]]] |apply (SA_Trans_TVar ? ? ? t1) [rewrite > H9 in H4; apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H4); diff --git a/helm/software/matita/library/Fsub/util.ma b/helm/software/matita/library/Fsub/util.ma index fa59484f5..5a81f7ec5 100644 --- a/helm/software/matita/library/Fsub/util.ma +++ b/helm/software/matita/library/Fsub/util.ma @@ -24,11 +24,22 @@ let rec max m n \def [true \Rightarrow n |false \Rightarrow m]. -inductive in_list (A : Type) : A \to (list A) \to Prop \def - | in_Base : \forall x:A.\forall l:(list A). - (in_list A x (x :: l)) - | in_Skip : \forall x,y:A.\forall l:(list A). - (in_list A x l) \to (in_list A x (y :: l)). +inductive in_list (A:Type): A → (list A) → Prop ≝ +| in_Base : ∀ x,l.(in_list A x (x::l)) +| in_Skip : ∀ x,y,l.(in_list A x l) → (x ≠ y) → (in_list A x (y::l)). + +notation > "hvbox(x ∈ l)" + non associative with precedence 30 for @{ 'inlist $x $l }. +notation < "hvbox(x \nbsp ∈ \nbsp l)" + non associative with precedence 30 for @{ 'inlist $x $l }. +interpretation "item in list" 'inlist x l = + (cic:/matita/Fsub/util/in_list.ind#xpointer(1/1) _ x l). + +lemma in_Skip2 : ∀x,y,l.(in_list nat x l) → (in_list nat x (y::l)). +intros;elim (decidable_eq_nat x y) + [rewrite > H1;apply in_Base + |apply (in_Skip ? ? ? ? H H1)] +qed. definition incl : \forall A.(list A) \to (list A) \to Prop \def \lambda A,l,m.\forall x.(in_list A x l) \to (in_list A x m). @@ -43,10 +54,14 @@ definition map : \forall A,B,f.((list A) \to (list B)) \def lemma in_list_nil : \forall A,x.\lnot (in_list A x []). intros.unfold.intro.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]] + [intros;lapply (sym_eq ? ? ? H2);destruct Hletin + |intros;destruct H5] +qed. + +lemma in_cons_case : ∀A.∀x,h:A.∀t:list A.x ∈ h::t → x = h ∨ (x ≠ h ∧ (x ∈ t)). +intros;inversion H;intros + [destruct H2;left;symmetry;assumption + |destruct H5;right;split [rewrite > Hcut|rewrite > Hcut1] assumption ] qed. lemma max_case : \forall m,n.(max m n) = match (leb m n) with -- 2.39.2