From: Ferruccio Guidi Date: Wed, 15 Oct 2014 13:43:06 +0000 (+0000) Subject: more automation for cpcs ... X-Git-Tag: make_still_working~815 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8c0dca9afa666cb4c993fef8e4870388b97c5975;p=helm.git more automation for cpcs ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma index 730714b5c..c979cedde 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma @@ -28,14 +28,13 @@ interpretation "context-sensitive parallel equivalence (term)" lemma cpcs_ind: ∀G,L,T1. ∀R:predicate term. R T1 → (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T ⬌ T2 → R T → R T2) → ∀T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → R T2. -#G #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) // +normalize /3 width=6 by TC_star_ind/ qed-. lemma cpcs_ind_dx: ∀G,L,T2. ∀R:predicate term. R T2 → (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌ T → ⦃G, L⦄ ⊢ T ⬌* T2 → R T → R T1) → ∀T1. ⦃G, L⦄ ⊢ T1 ⬌* T2 → R T1. -#G #L #T2 #R #HT2 #IHT2 #T1 #HT12 -@(TC_star_ind_dx … HT2 IHT2 … HT12) // +normalize /3 width=6 by TC_star_ind_dx/ qed-. (* Basic properties *********************************************************) @@ -46,16 +45,18 @@ lemma cpcs_refl: ∀G,L. reflexive … (cpcs G L). (* Basic_1: was: pc3_s *) lemma cpcs_sym: ∀G,L. symmetric … (cpcs G L). -#G #L @TC_symmetric // qed-. +#G #L @TC_symmetric // qed-. (**) (* auto fails even after normalize *) lemma cpc_cpcs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. /2 width=1 by inj/ qed. lemma cpcs_strap1: ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T ⬌ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L @step qed-. +normalize /2 width=3 by step/ +qed-. lemma cpcs_strap2: ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌ T → ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L @TC_strap qed-. +normalize /2 width=3 by TC_strap/ +qed-. (* Basic_1: was: pc3_pr2_r *) lemma cpr_cpcs_dx: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma index 1f437491f..d9db0509f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma @@ -21,12 +21,14 @@ include "basic_2/equivalence/cpcs.ma". (* Basic_1: was: pc3_pr3_r *) lemma cpcs_cprs_dx: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpcs_cpr_strap1, cpcs_strap1, cpc_cpcs/ +#G #L #T1 #T2 #H @(cprs_ind … H) -T2 +/3 width=3 by cpcs_cpr_strap1, cpcs_strap1, cpc_cpcs/ qed. (* Basic_1: was: pc3_pr3_x *) lemma cpcs_cprs_sn: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡* T1 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T2 #H @(cprs_ind_dx … H) -T2 /3 width=3 by cpcs_cpr_div, cpcs_strap1, cpcs_cprs_dx/ +#G #L #T1 #T2 #H @(cprs_ind_dx … H) -T2 +/3 width=3 by cpcs_cpr_div, cpcs_strap1, cpcs_cprs_dx/ qed. lemma cpcs_cprs_strap1: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. @@ -49,7 +51,8 @@ qed-. (* Basic_1: was: pc3_pr3_t *) (* Basic_1: note: pc3_pr3_t should be renamed *) lemma cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /2 width=3 by cpcs_cpr_div, cpcs_cprs_dx/ +#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 +/2 width=3 by cpcs_cpr_div, cpcs_cprs_dx/ qed. lemma cprs_cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2.