From 84713c9446ff13dd26533590985a0df67cb5ec7e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 23 Mar 2012 14:40:59 +0000 Subject: [PATCH] - pts: we restored the former hierarchy - nat: we added a missing lemma - lambda_delta: subject reduction continues ... --- .../lambda_delta/basic_2/grammar/cl_weight.ma | 16 ++++ .../basic_2/grammar/term_weight.ma | 2 +- .../contribs/lambda_delta/basic_2/notation.ma | 8 ++ .../basic_2/reducibility/ltpr_aaa.ma | 88 +++++++++++++++++++ .../lambda_delta/basic_2/static/aaa_lift.ma | 25 ++++++ .../basic_2/substitution/ldrop.ma | 9 +- matita/matita/lib/arithmetics/nat.ma | 4 +- matita/matita/lib/basics/pts.ma | 1 - 8 files changed, 149 insertions(+), 4 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma index af3b3496b..e3dee1e0b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma @@ -41,6 +41,22 @@ lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T]. @transitive_le [3: @IHL |2: /2 width=2/ | skip ] qed. +lemma cw_tpair_sn: ∀I,L,V,T. #[L, V] < #[L, ②{I}V.T]. +#I #L #V #T normalize in ⊢ (? % %); // +qed. + +lemma cw_tpair_dx: ∀I,L,V,T. #[L, T] < #[L, ②{I}V.T]. +#I #L #V #T normalize in ⊢ (? % %); // +qed. + +lemma cw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #[L, V2] < #[L, ②{I1}V1.②{I2}V2.T]. +#I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/ +qed. + +lemma cw_tpair_dx_sn_shift: ∀I1,I2,L,V1,V2,T. #[L.ⓑ{I2}V2, T] < #[L, ②{I1}V1.②{I2}V2.T]. +#I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/ +qed. + (* Basic_1: removed theorems 6: flt_thead_sx flt_thead_dx flt_arith0 flt_arith1 flt_arith2 flt_trans *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma index 00050032d..e567df208 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma @@ -38,6 +38,6 @@ axiom tw_wf_ind: ∀R:predicate term. (* Basic_1: removed theorems 11: wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O - weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind + weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind removed local theorems 1: q_ind *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index ce9a370e2..9ec72083a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -308,8 +308,16 @@ notation "hvbox( L ⊢ break term 90 T1 ⬌ break T2 )" non associative with precedence 45 for @{ 'PConv $L $T1 $T2 }. +notation "hvbox( T1 ⬌ break T2 )" + non associative with precedence 45 + for @{ 'PConv $T1 $T2 }. + (* Equivalence **************************************************************) notation "hvbox( L ⊢ break term 90 T1 ⬌* break T2 )" non associative with precedence 45 for @{ 'PConvStar $L $T1 $T2 }. + +notation "hvbox( T1 ⬌* break T2 )" + non associative with precedence 45 + for @{ 'PConvStar $T1 $T2 }. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma new file mode 100644 index 000000000..b4f73c9fa --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma @@ -0,0 +1,88 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/ltpr_ldrop.ma". +include "basic_2/static/aaa_ltps.ma". +include "basic_2/static/lsuba_aaa.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) + +(* Properties about atomic arity assignment on terms ************************) + +fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ÷ A → L = L1 → T = T1 → + ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → L2 ⊢ T2 ÷ A. +#L #T @(cw_wf_ind … L T) -L -T #L #T #IH +#L1 #T1 #A * -L1 -T1 -A +[ -IH #L1 #k #H1 #H2 #L2 #_ #T2 #H destruct + >(tpr_inv_atom1 … H) -H // +| #I #L1 #K1 #V1 #B #i #HLK1 #HK1 #H1 #H2 #L2 #HL12 #T2 #H destruct + >(tpr_inv_atom1 … H) -T2 + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + lapply (IH … HKV1 … HK1 … HK12 … HV12) // -L1 -K1 -V1 /2 width=5/ +| #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct + elim (tpr_inv_abbr1 … H) -H * + [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct + lapply (tps_lsubs_conf … HT02 (L2.ⓓV2) ?) -HT02 /2 width=1/ #HT02 + lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB + lapply (IH … HA … (L2.ⓓV2) … HT10) -IH -HA -HT10 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/ + | -B #T #HT1 #HTX + elim (lift_total X 0 1) #X1 #HX1 + lapply (tpr_lift … HTX … HT1 … HX1) -T #HTX1 + lapply (IH … HA … (L2.ⓓV1) … HTX1) /width=5/ -T1 /2 width=1/ -L1 #HA + @(aaa_inv_lift … HA … HX1) /2 width=1/ + ] +| #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct + elim (tpr_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB + lapply (IH … HA … (L2.ⓛV2) … HT12) -IH -HA -HT12 /width=5/ -T1 /2 width=1/ +| #L1 #V1 #T1 #B #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct + elim (tpr_inv_appl1 … H) -H * + [ #V2 #T2 #HV12 #HT12 #H destruct + lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB + lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ /2 width=3/ + | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct + elim (aaa_inv_abst … HT1) -HT1 #B0 #A0 #HB0 #HA0 #H destruct + lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB + lapply (IH … HB0 … HL12 W2 ?) -HB0 /width=5/ #HB0 + lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/ + | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct + elim (aaa_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0 + lapply (IH … HW0 … HL12 … HW02) -HW0 /width=5/ #HW2 + lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0 + lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2 + @(aaa_abbr … HW2) -HW2 + @(aaa_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *) + ] +| #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct + elim (tpr_inv_cast1 … H) -H + [ * #V2 #T2 #HV12 #HT12 #H destruct + lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2 + lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/ + | -HV1 #HT1X + lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/ + ] +] +qed. + +lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ➡ L2 → + ∀T2. T1 ➡ T2 → L2 ⊢ T2 ÷ A. +/2 width=9/ qed. + +lemma aaa_ltpr_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L1 ➡ L2 → L2 ⊢ T ÷ A. +/2 width=5/ qed. + +lemma aaa_tpr_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2. T1 ➡ T2 → L ⊢ T2 ÷ A. +/2 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma index 2d62640ad..b243338ee 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma @@ -45,3 +45,28 @@ lemma aaa_lift: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 /3 width=4/ ] qed. + +lemma aaa_inv_lift: ∀L2,T2,A. L2 ⊢ T2 ÷ A → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → + ∀T1. ⇧[d, e] T1 ≡ T2 → L1 ⊢ T1 ÷ A. +#L2 #T2 #A #H elim H -L2 -T2 -A +[ #L2 #k #L1 #d #e #_ #T1 #H + >(lift_inv_sort2 … H) -H // +| #I #L2 #K2 #V2 #B #i #HLK2 #_ #IHB #L1 #d #e #HL21 #T1 #H + elim (lift_inv_lref2 … H) -H * #Hid #H destruct + [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // -Hid /3 width=8/ + | lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 // -Hid /3 width=8/ + ] +| #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H + elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct + /4 width=4/ +| #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H + elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct + /4 width=4/ +| #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H + elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct + /3 width=4/ +| #L2 #V2 #T2 #A #_ #_ #IH1 #IH2 #L1 #d #e #HL21 #X #H + elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct + /3 width=4/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma index 3dfc35639..4550fde4b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/grammar/lenv_weight.ma". +include "basic_2/grammar/cl_weight.ma". include "basic_2/grammar/lsubs.ma". include "basic_2/substitution/lift.ma". @@ -187,6 +187,13 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. ] qed-. +lemma ldrop_pair2_fwd_fw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V → + ∀T. #[K, V] < #[L, T]. +#I #L #K #V #d #e #H #T +lapply (ldrop_fwd_lw … H) -H #H +@(le_to_lt_to_lt … H) -H /3 width=1/ +qed-. + lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e. ⇩[0, e] L1 ≡ K2. ⓑ{I2} V2 → e < |L1|. #L1 elim L1 -L1 diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index 44c3119fa..31d5ced7f 100644 --- a/matita/matita/lib/arithmetics/nat.ma +++ b/matita/matita/lib/arithmetics/nat.ma @@ -374,6 +374,9 @@ theorem lt_plus_to_minus_r: ∀a,b,c. a + b < c → a < c - b. #a #b #c #H @le_plus_to_minus_r // qed. +lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + (S n). +/2 width=1/ qed. + theorem lt_S_S_to_lt: ∀n,m:nat. S n < S m → n < m. (* demo *) /2/ qed-. @@ -780,4 +783,3 @@ lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i. lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i. #i #n #m #leni #lemi normalize (cases (leb n m)) normalize // qed. - diff --git a/matita/matita/lib/basics/pts.ma b/matita/matita/lib/basics/pts.ma index 237c0c2b3..446305ecf 100644 --- a/matita/matita/lib/basics/pts.ma +++ b/matita/matita/lib/basics/pts.ma @@ -19,4 +19,3 @@ universe constraint Type[1] < Type[2]. universe constraint Type[2] < Type[3]. universe constraint Type[3] < Type[4]. universe constraint Type[4] < Type[5]. -universe constraint Type[5] < Type[6]. -- 2.39.2