From: Andrea Asperti Date: Mon, 11 May 2009 16:19:42 +0000 (+0000) Subject: More automation X-Git-Tag: make_still_working~3998 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=27104a52afaa7844d8410e24a3de6c33326dc8be;p=helm.git More automation --- diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma index 7ae8763cf..4ae057be9 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma @@ -50,39 +50,52 @@ 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] + [letin x \def fv_env. letin y ≝incl. + (* autobatch depth=4 size=8 by SA_Top, WFE_Typ_subst, H3, JS_to_WFT1, H, H4, WFT_env_incl, incl_fv_env]*) + apply SA_Top + [autobatch by WFE_Typ_subst, H3, JS_to_WFT1, H. + (* + rewrite > H5 in H3; + apply (WFE_Typ_subst ? ? ? ? ? ? ? H3 (JS_to_WFT1 ? ? ? H)) *) + |autobatch by H4, WFT_env_incl, incl_fv_env] + (* rewrite > H5 in H4;apply (WFT_env_incl ? ? H4);apply incl_fv_env] *) + |autobatch depth=4 by SA_Refl_TVar, WFE_Typ_subst, H3, JS_to_WFT1, H, H4. + (* + apply SA_Refl_TVar; + [autobatch by WFE_Typ_subst, H3, JS_to_WFT1, H. + (* + rewrite > H5 in H3;apply (WFE_Typ_subst ? ? ? ? ? ? ? H3); + apply (JS_to_WFT1 ? ? ? H) *) + |autobatch by H4. (* 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 + |applyS H1. + lapply (WFE_bound_bound true n t1 U ? ? H3); + [autobatch. (* apply (JS_to_WFE ? ? ? H4) *) + |autobatch. (* rewrite < Hletin;rewrite < append_cons;apply (H5 ? H6) *) + |destruct.elim l1;autobatch. + ]] + |(* autobatch depth=4 size=7 by SA_Trans_TVar, lookup_env_extends, H3, sym_neq, H5, H6, H7. *) + apply (SA_Trans_TVar ? ? ? t1); + [autobatch by lookup_env_extends, H3, sym_neq, H7. + (* 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; + |autobatch; (* apply (SA_Arrow ? ? ? ? ? (H4 ? H7) (H6 ? H7)) *) + |apply (SA_All ? ? ? ? ? (H4 ? H7));intros;autobatch] + (* apply (H6 ? ? (mk_bound true X1 t2::l1)) [rewrite > H7;rewrite > fv_env_extends;apply H8 - |simplify;rewrite < H7;reflexivity]] + |simplify;rewrite < H7;reflexivity]] *) 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 + [ + rewrite > (JSubtype_Top ? ? H3);autobatch |generalize in match H7;generalize in match H4;generalize in match H2; generalize in match H5;clear H7 H4 H2 H5; generalize in match (refl_eq ? (Arrow t t1)); diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma index 16f38322a..0f32da349 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma @@ -18,12 +18,8 @@ include "Fsub/defn2.ma". 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; apply (H4 ? H6); - [ intro; apply H6; apply (fv_WFT ? ? ? (WFT_Forall ? ? ? H1 H3)); - simplify; autobatch - | autobatch]]] + | apply SA_All; [ autobatch | intros; autobatch depth=4 size=10] + ] qed. (* @@ -34,12 +30,9 @@ qed. 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 width=4 size=7 - | apply (SA_All ? ? ? ? ? (H2 ? H6 H7));intros; - apply H4 - [ intro; autobatch - | apply WFE_cons; autobatch - | unfold;intros; elim (in_list_cons_case ? ? ? ? H9); destruct; autobatch]] + [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: @@ -57,34 +50,25 @@ lemma JSubtype_inv: intros; generalize in match (refl_eq ? T); generalize in match (refl_eq ? G); - elim H5 in ⊢ (? ? ? % → ? ? ? % → %); destruct; - [1,2,3,4: autobatch depth=10 width=10 size=8 - | apply H4; first [assumption | autobatch]] + elim H5 in ⊢ (? ? ? % → ? ? ? % → %); destruct; autobatch depth=3 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; - [1,2,4: autobatch width=10 depth=10 size=8 + [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 | rewrite > append_cons; apply H1; - lapply (WFE_bound_bound true X t1 U ? ? H3); destruct; - [1,3: autobatch - | rewrite < append_cons; autobatch - ]] - | apply (SA_Trans_TVar ? ? ? t1) - [ apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H3); - intro; autobatch - | autobatch]] + lapply (WFE_bound_bound true X t1 U ? ? H3); destruct;autobatch] + | apply (SA_Trans_TVar ? ? ? t1); autobatch] + | autobatch | apply SA_All; [ autobatch - | intros; - apply (H6 ? ? (mk_bound true X1 t2::l1)) - [ rewrite > fv_env_extends; autobatch - | autobatch]]] + | intros; apply (H6 ? ? (mk_bound true X1 t2::l1));autobatch]] qed. lemma JS_trans_prova: ∀T,G1.WFType G1 T → @@ -100,35 +84,29 @@ intros 3;elim H;clear H; try autobatch; [ assumption | apply WFT_Forall; [ autobatch - | intros;lapply (H8 ? H11); - autobatch]] + | intros;autobatch depth =4]] | apply SA_All [ autobatch | intros;apply (H4 X); - [intro; autobatch; - |intro; apply H13;apply H5; apply (WFT_to_incl ? ? ? H3); - assumption - |simplify;autobatch + [intro; autobatch + |intro; autobatch depth=4. + |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] + [unfold;intros;lapply (H5 ? H15);rewrite > fv_append;autobatch + |autobatch |assumption] |*:autobatch] |autobatch]]]]] qed. theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V. -intros 5; autobatch. +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|unfold;intros;autobatch] +intros;apply (narrowing ? ? ? ? ? ? ? H1 ? H) [|autobatch] +intros;apply (JS_trans ? ? ? ? ? H2);apply (JS_weakening ? ? ? H1);autobatch. qed.