From 13a37618a5cebc5e0088a7da213f1de033d281db Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 29 Jan 2012 16:05:55 +0000 Subject: [PATCH] - transitivity of lenv refinement for atomic arity asignment proved! ... - results on context-free normal forms refacored - some annotation added --- .../contribs/lambda_delta/Basic_2/Basic_1.txt | 18 ++--- .../lambda_delta/Basic_2/reducibility/tnf.ma | 57 -------------- .../Basic_2/reducibility/tnf_trf.ma | 74 +++++++++++++++++++ .../lambda_delta/Basic_2/static/lsuba.ma | 39 ++++++++++ .../lambda_delta/Basic_2/static/lsuba_aaa.ma | 54 ++++++++++++++ .../Basic_2/static/lsuba_ldrop.ma | 63 ++++++++++++++++ .../Basic_2/static/lsuba_lsuba.ma | 35 +++++++++ .../lambda_delta/Basic_2/unfold/ldrops.ma | 3 + .../lambda_delta/Basic_2/unfold/lifts_lift.ma | 4 +- .../Basic_2/unfold/lifts_lift_vector.ma | 2 +- .../Basic_2/unfold/lifts_lifts.ma | 2 +- 11 files changed, 281 insertions(+), 70 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf_trf.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_aaa.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_ldrop.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_lsuba.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt index 67f076030..8f3a63204 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt @@ -102,16 +102,7 @@ csubv/getl csubv_getl_conf csubv/getl csubv_getl_conf_void csubv/props csubv_bind_same csubv/props csubv_refl - -# check ############################################################# - -drop1/fwd drop1_gen_pnil -drop1/fwd drop1_gen_pcons -drop1/props drop1_skip_bind drop1/props drop1_cons_tail - -# waiting #################################################################### - drop/props drop_ctail ex0/props aplus_gz_le ex0/props aplus_gz_ge @@ -141,12 +132,18 @@ leq/props leq_trans leq/props leq_ahead_false_1 leq/props leq_ahead_false_2 lift1/fwd lift1_cons_tail + +# check ############################################################# + lift1/fwd lifts1_flat lift1/fwd lifts1_nil lift1/fwd lifts1_cons lift1/props lift1_free lift/props thead_x_lift_y_y lift/props lifts_tapp + +# waiting #################################################################### + lift/props lifts_inj llt/props lweight_repl llt/props llt_repl @@ -240,6 +237,9 @@ pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux pc3/wcpr0 pc3_wcpr0_t pc3/wcpr0 pc3_wcpr0 pr0/fwd pr0_gen_void + +# check ############################################################# + pr0/dec nf0_dec pr0/subst1 pr0_subst1_back pr0/subst1 pr0_subst1_fwd diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma index 3c0184e55..8c84f092c 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/tps_lift.ma". -include "Basic_2/reducibility/trf.ma". include "Basic_2/reducibility/tpr.ma". (* CONTEXT-FREE NORMAL TERMS ************************************************) @@ -59,58 +57,3 @@ lemma tnf_inv_cast: ∀V,T. ℕ[ⓣV.T] → False. #V #T #H lapply (H T ?) -H /2 width=1/ #H @(discr_tpair_xy_y … H) qed-. - -(* Basic properties *********************************************************) - -lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝕀[T1] → T1 = T2. -#T1 #T2 #H elim H -T1 -T2 -[ // -| * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H - [ elim (tif_inv_appl … H) -H #HV1 #HT1 #_ - >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // - | elim (tif_inv_cast … H) - ] -| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H - elim (tif_inv_appl … H) -H #_ #_ #H - elim (simple_inv_bind … H) -| * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #H - [ -HT2 -IHV1 -IHT1 elim (tif_inv_abbr … H) - | <(tps_inv_refl_SO2 … HT2 ?) -HT2 // - elim (tif_inv_abst … H) -H #HV1 #HT1 - >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // - ] -| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H - elim (tif_inv_appl … H) -H #_ #_ #H - elim (simple_inv_bind … H) -| #V1 #T1 #T2 #T #_ #_ #_ #H - elim (tif_inv_abbr … H) -| #V1 #T1 #T #_ #_ #H - elim (tif_inv_cast … H) -] -qed. - -theorem tif_tnf: ∀T1. 𝕀[T1] → ℕ[T1]. -/2 width=1/ qed. - -(* Note: this property is unusual *) -theorem tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False. -#T1 #H elim H -T1 -[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/ -| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/ -| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/ -| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/ -| #V #T #H elim (tnf_inv_abbr … H) -| #V #T #H elim (tnf_inv_cast … H) -| #V #W #T #H elim (tnf_inv_appl … H) -H #_ #_ #H - elim (simple_inv_bind … H) -] -qed. - -theorem tnf_tif: ∀T1. ℕ[T1] → 𝕀[T1]. -/2 width=3/ qed. - -lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[ⓛV.T]. -/4 width=1/ qed. - -lemma tnf_appl: ∀V,T. ℕ[V] → ℕ[T] → 𝕊[T] → ℕ[ⓐV.T]. -/4 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf_trf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf_trf.ma new file mode 100644 index 000000000..3ffafb2c8 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf_trf.ma @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tps_lift.ma". +include "Basic_2/reducibility/trf.ma". +include "Basic_2/reducibility/tnf.ma". + +(* CONTEXT-FREE NORMAL TERMS ************************************************) + +(* Main properties properties ***********************************************) + +lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝕀[T1] → T1 = T2. +#T1 #T2 #H elim H -T1 -T2 +[ // +| * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H + [ elim (tif_inv_appl … H) -H #HV1 #HT1 #_ + >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // + | elim (tif_inv_cast … H) + ] +| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H + elim (tif_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +| * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #H + [ -HT2 -IHV1 -IHT1 elim (tif_inv_abbr … H) + | <(tps_inv_refl_SO2 … HT2 ?) -HT2 // + elim (tif_inv_abst … H) -H #HV1 #HT1 + >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // + ] +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H + elim (tif_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +| #V1 #T1 #T2 #T #_ #_ #_ #H + elim (tif_inv_abbr … H) +| #V1 #T1 #T #_ #_ #H + elim (tif_inv_cast … H) +] +qed. + +theorem tif_tnf: ∀T1. 𝕀[T1] → ℕ[T1]. +/2 width=1/ qed. + +(* Note: this property is unusual *) +lemma tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False. +#T1 #H elim H -T1 +[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/ +| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/ +| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/ +| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/ +| #V #T #H elim (tnf_inv_abbr … H) +| #V #T #H elim (tnf_inv_cast … H) +| #V #W #T #H elim (tnf_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +] +qed. + +theorem tnf_tif: ∀T1. ℕ[T1] → 𝕀[T1]. +/2 width=3/ qed. + +lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[ⓛV.T]. +/4 width=1/ qed. + +lemma tnf_appl: ∀V,T. ℕ[V] → ℕ[T] → 𝕊[T] → ℕ[ⓐV.T]. +/4 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba.ma index d6750c3d5..5d087c93c 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba.ma @@ -29,6 +29,45 @@ interpretation (* Basic inversion lemmas ***************************************************) +fact lsuba_inv_atom1_aux: ∀L1,L2. L1 ÷⊑ L2 → L1 = ⋆ → L2 = ⋆. +#L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V #_ #H destruct +| #L1 #L2 #V #W #A #_ #_ #_ #H destruct +] +qed. + +lemma lsuba_inv_atom1: ∀L2. ⋆ ÷⊑ L2 → L2 = ⋆. +/2 width=3/ qed-. + +fact lsuba_inv_pair1_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V → + (∃∃K2. K1 ÷⊑ K2 & L2 = K2. ⓑ{I} V) ∨ + ∃∃K2,W,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 & + L2 = K2. ⓛW & I = Abbr. +#L1 #L2 * -L1 -L2 +[ #I #K1 #V #H destruct +| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/ +| #L1 #L2 #V1 #W2 #A #HV1 #HW2 #HL12 #I #K1 #V #H destruct /3 width=7/ +] +qed. + +lemma lsuba_inv_pair1: ∀I,K1,L2,V. K1. ⓑ{I} V ÷⊑ L2 → + (∃∃K2. K1 ÷⊑ K2 & L2 = K2. ⓑ{I} V) ∨ + ∃∃K2,W,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 & + L2 = K2. ⓛW & I = Abbr. +/2 width=3/ qed-. + +fact lsuba_inv_atom2_aux: ∀L1,L2. L1 ÷⊑ L2 → L2 = ⋆ → L1 = ⋆. +#L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V #_ #H destruct +| #L1 #L2 #V #W #A #_ #_ #_ #H destruct +] +qed. + +lemma lsubc_inv_atom2: ∀L1. L1 ÷⊑ ⋆ → L1 = ⋆. +/2 width=3/ qed-. + fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W → (∃∃K1. K1 ÷⊑ K2 & L1 = K1. ⓑ{I} W) ∨ ∃∃K1,V,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 & diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_aaa.ma new file mode 100644 index 000000000..a6a9c3fae --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_aaa.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/aaa_aaa.ma". +include "Basic_2/static/lsuba_ldrop.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************) + +(* Properties concerning atomic arity assignment ****************************) + +lemma lsuba_aaa_conf: ∀L1,V,A. L1 ⊢ V ÷ A → ∀L2. L1 ÷⊑ L2 → L2 ⊢ V ÷ A. +#L1 #V #A #H elim H -L1 -V -A +[ // +| #I #L1 #K1 #V1 #B #i #HLK1 #HV1B #IHV1 #L2 #HL12 + elim (lsuba_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2 + elim (lsuba_inv_pair1 … H) -H * #K2 + [ #HK12 #H destruct /3 width=5/ + | #V2 #A1 #HV1A1 #HV2 #_ #H1 #H2 destruct + >(aaa_mono … HV1B … HV1A1) -B -HV1A1 /2 width=5/ + ] +| /4 width=2/ +| /4 width=1/ +| /3 width=3/ +| /3 width=1/ +] +qed. + +lemma lsuba_aaa_trans: ∀L2,V,A. L2 ⊢ V ÷ A → ∀L1. L1 ÷⊑ L2 → L1 ⊢ V ÷ A. +#L2 #V #A #H elim H -L2 -V -A +[ // +| #I #L2 #K2 #V2 #B #i #HLK2 #HV2B #IHV2 #L1 #HL12 + elim (lsuba_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 + elim (lsuba_inv_pair2 … H) -H * #K1 + [ #HK12 #H destruct /3 width=5/ + | #V1 #A1 #HV1 #HV2A1 #_ #H1 #H2 destruct + >(aaa_mono … HV2B … HV2A1) -B -HV2A1 /2 width=5/ + ] +| /4 width=2/ +| /4 width=1/ +| /3 width=3/ +| /3 width=1/ +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_ldrop.ma new file mode 100644 index 000000000..522252ae1 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_ldrop.ma @@ -0,0 +1,63 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lsuba.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************) + +(* Properties concerning basic local environment slicing ********************) + +(* Note: the constant 0 cannot be generalized *) + +lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ÷⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 → + ∃∃K2. K1 ÷⊑ K2 & ⇩[0, e] L2 ≡ K2. +#L1 #L2 #H elim H -L1 -L2 +[ /2 width=3/ +| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H + elim (ldrop_inv_O1 … H) -H * #He #HLK1 + [ destruct + elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H + <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ + | elim (IHL12 … HLK1) -L1 /3 width=3/ + ] +| #L1 #L2 #V #W #A #HV #HW #_ #IHL12 #K1 #e #H + elim (ldrop_inv_O1 … H) -H * #He #HLK1 + [ destruct + elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H + <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ + | elim (IHL12 … HLK1) -L1 /3 width=3/ + ] +] +qed-. + +lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ÷⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → + ∃∃K1. K1 ÷⊑ K2 & ⇩[0, e] L1 ≡ K1. +#L1 #L2 #H elim H -L1 -L2 +[ /2 width=3/ +| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H + elim (ldrop_inv_O1 … H) -H * #He #HLK2 + [ destruct + elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H + <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ + | elim (IHL12 … HLK2) -L2 /3 width=3/ + ] +| #L1 #L2 #V #W #A #HV #HW #_ #IHL12 #K2 #e #H + elim (ldrop_inv_O1 … H) -H * #He #HLK2 + [ destruct + elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H + <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ + | elim (IHL12 … HLK2) -L2 /3 width=3/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_lsuba.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_lsuba.ma new file mode 100644 index 000000000..24da36ccd --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_lsuba.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lsuba_aaa.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************) + +(* Main properties **********************************************************) + +theorem lsuba_trans: ∀L1,L. L1 ÷⊑ L → ∀L2. L ÷⊑ L2 → L1 ÷⊑ L2. +#L1 #L #H elim H -L1 -L +[ #X #H >(lsuba_inv_atom1 … H) -H // +| #I #L1 #L #V #HL1 #IHL1 #X #H + elim (lsuba_inv_pair1 … H) -H * #L2 + [ #HL2 #H destruct /3 width=1/ + | #V #A #HLV #HL2V #HL2 #H1 #H2 destruct /3 width=3/ + ] +| #L1 #L #V1 #W #A1 #HV1 #HW #HL1 #IHL1 #X #H + elim (lsuba_inv_pair1 … H) -H * #L2 + [ #HL2 #H destruct /3 width=5/ + | #V #A2 #_ #_ #_ #_ #H destruct + ] +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma index d271fe2c6..28b9a8c7e 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma @@ -34,6 +34,7 @@ fact ldrops_inv_nil_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → des = ⟠ → L1 #L1 #L #L2 #d #e #des #_ #_ #H destruct qed. +(* Basic_1: was: drop1_gen_pnil *) lemma ldrops_inv_nil: ∀L1,L2. ⇩*[⟠] L1 ≡ L2 → L1 = L2. /2 width=3/ qed-. @@ -46,6 +47,7 @@ fact ldrops_inv_cons_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → /2 width=3/ qed. +(* Basic_1: was: drop1_gen_pcons *) lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} :: des] L1 ≡ L2 → ∃∃L. ⇩*[des] L1 ≡ L & ⇩[d, e] L ≡ L2. /2 width=3/ qed-. @@ -73,6 +75,7 @@ qed-. (* Basic properties *********************************************************) +(* Basic_1: was: drop1_skip_bind *) lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 → ∀I. ⇩*[des + 1] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2. #L1 #L2 #des #H elim H -L1 -L2 -des diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma index b10b3c17b..3f63d2eb8 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma @@ -20,7 +20,7 @@ include "Basic_2/unfold/lifts.ma". (* Properties concerning basic term relocation ******************************) -(* Basic_1: was: lift1_xhg *) +(* Basic_1: was: lift1_xhg (right to left) *) lemma lifts_lift_trans_le: ∀T1,T,des. ⇧*[des] T1 ≡ T → ∀T2. ⇧[0, 1] T ≡ T2 → ∃∃T0. ⇧[0, 1] T1 ≡ T0 & ⇧*[des + 1] T0 ≡ T2. #T1 #T #des #H elim H -T1 -T -des @@ -45,7 +45,7 @@ lemma lifts_lift_trans: ∀des,i,i0. @[i] des ≡ i0 → >(lifts_inv_nil … H) -T1 /2 width=3/ | #d #e #des #IHdes #i #i0 #H1 #des0 #H2 #T1 #T0 #HT10 #T2 #HT02 elim (at_inv_cons … H1) -H1 * #Hid #Hi0 - [ elim (minuss_inv_cons1_lt … H2 ?) -H2 [2: /2 width=1/ ] #des1 #Hdes1 minus_plus #HT1 #HT0 elim (IHdes … Hi0 … Hdes1 … HT0 … HT02) -IHdes -Hi0 -Hdes1 -T0 #T0 #HT0 #HT02 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift_vector.ma index 727a93f54..0d279c6da 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift_vector.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift_vector.ma @@ -20,7 +20,7 @@ include "Basic_2/unfold/lifts_vector.ma". (* Main properties **********************************************************) -(* Basic_1: was: lifts1_xhg *) +(* Basic_1: was: lifts1_xhg (right to left) *) lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⇧*[des] T1s ≡ Ts → ∀T2s:list term. ⇧[0, 1] Ts ≡ T2s → ∃∃T0s. ⇧[0, 1] T1s ≡ T0s & ⇧*[des + 1] T0s ≡ T2s. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts.ma index 331de05df..6062f89b1 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts.ma @@ -18,7 +18,7 @@ include "Basic_2/unfold/lifts_lift.ma". (* Main properties **********************************************************) -(* Basic_1: was: lift1_lift1 *) +(* Basic_1: was: lift1_lift1 (left to right) *) theorem lifts_trans: ∀T1,T,des1. ⇧*[des1] T1 ≡ T → ∀T2:term. ∀des2. ⇧*[des2] T ≡ T2 → ⇧*[des1 @ des2] T1 ≡ T2. #T1 #T #des1 #H elim H -T1 -T -des1 // /3 width=3/ -- 2.39.2