From 1185204d6a1e634a107fac71a45c9f87f49ccc31 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 19 Mar 2012 15:11:24 +0000 Subject: [PATCH] - basics: bug fix in Conf3, it was not generic enough - lambda_delta: subject reduction of static typestarted ... --- .../lambda_delta/basic_2/static/aaa_ltps.ma | 65 +++++++++++++++++++ .../lambda_delta/basic_2/static/aaa_ltpss.ma | 34 ++++++++++ matita/matita/lib/basics/relations.ma | 5 +- matita/matita/lib/basics/star.ma | 8 +-- 4 files changed, 107 insertions(+), 5 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltps.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltps.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltps.ma new file mode 100644 index 000000000..162fa3898 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltps.ma @@ -0,0 +1,65 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/substitution/ltps_ldrop.ma". +include "basic_2/static/aaa_lift.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +(* Properties about parallel substitution ***********************************) + +(* Note: lemma 500 *) +lemma aaa_ltps_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶ L2 → + ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ÷ A. +#L1 #T1 #A #H elim H -L1 -T1 -A +[ #L1 #k #L2 #d #e #_ #T2 #H + >(tps_inv_sort1 … H) -H // +| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #L2 #d #e #HL12 #T2 #H + elim (tps_inv_lref1 … H) -H + [ #H destruct + elim (lt_or_ge i d) #Hdi + [ elim (ltps_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 + elim (ltps_inv_tps11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct + /3 width=8/ + | elim (lt_or_ge i (d + e)) #Hide + [ elim (ltps_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2 + elim (ltps_inv_tps21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct + /3 width=8/ + | -Hdi + lapply (ltps_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide #HLK2 + /3 width=8/ + ] + ] + | * #K2 #V2 #Hdi #Hide #HLK2 #HVT2 + elim (ltps_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0 + elim (ltps_inv_tps21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct + lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /3 width=7/ + ] +| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H + elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=4/ +| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H + elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=4/ +| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H + elim (tps_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/ +| #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H + elim (tps_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/ +] +qed. + +lemma aaa_ltps_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2,d,e. L1 [d, e] ▶ L2 → L2 ⊢ T ÷ A. +/2 width=7/ qed. + +lemma aaa_tps_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2,d,e. L ⊢ T1 [d, e] ▶ T2 → L ⊢ T2 ÷ A. +/2 width=7/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma new file mode 100644 index 000000000..171dd6b9c --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/unfold/ltpss.ma". +include "basic_2/static/aaa_ltps.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +(* Properties about parallel unfold *****************************************) + +lemma aaa_ltpss_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 → L2 ⊢ T ÷ A. +#L1 #T #A #HT #L2 #d #e #HL12 +@(TC_Conf3 … (λL,A. L ⊢ T ÷ A) … HT ? HL12) /2 width=5/ +qed. + +lemma aaa_tpss_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T2 ÷ A. +#L #T1 #A #HT1 #T2 #d #e #HT12 +@(TC_Conf3 … HT1 ? HT12) /2 width=5/ +qed. + +lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 → + ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ÷ A. +/3 width=5/ qed. diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma index a82f314f6..ff190e5e3 100644 --- a/matita/matita/lib/basics/relations.ma +++ b/matita/matita/lib/basics/relations.ma @@ -11,7 +11,7 @@ include "basics/logic.ma". -(********** preducates *********) +(********** predicates *********) definition predicate: Type[0] → Type[0] ≝ λA.A→Prop. @@ -20,6 +20,9 @@ definition predicate: Type[0] → Type[0] definition relation : Type[0] → Type[0] ≝ λA.A→A→Prop. +definition relation2 : Type[0] → Type[0] → Type[0] +≝ λA,B.A→B→Prop. + definition reflexive: ∀A.∀R :relation A.Prop ≝ λA.λR.∀x:A.R x x. diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma index bff1aaeef..8fd32c2e1 100644 --- a/matita/matita/lib/basics/star.ma +++ b/matita/matita/lib/basics/star.ma @@ -192,9 +192,9 @@ lemma TC_star_ind_dx: ∀A,R. reflexive A R → @(TC_star_ind_dx_aux … HR … Ha2 H … Ha12) // qed-. -definition Conf3: ∀A. relation A → relation A → Prop ≝ λA,S,R. - ∀a,a1. S a1 a → ∀a2. R a1 a2 → S a2 a. +definition Conf3: ∀A,B. relation2 A B → relation A → Prop ≝ λA,B,S,R. + ∀b,a1. S a1 b → ∀a2. R a1 a2 → S a2 b. -lemma TC_Conf3: ∀A,S,R. Conf3 A S R → Conf3 A S (TC … R). -#A #S #R #HSR #a #a1 #Ha1 #a2 #H elim H -a2 /2 width=3/ +lemma TC_Conf3: ∀A,B,S,R. Conf3 A B S R → Conf3 A B S (TC … R). +#A #B #S #R #HSR #b #a1 #Ha1 #a2 #H elim H -a2 /2 width=3/ qed. -- 2.39.2