From: Ferruccio Guidi Date: Sun, 25 Oct 2015 18:58:13 +0000 (+0000) Subject: theory of relocation updated ..... X-Git-Tag: make_still_working~677 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=46815bb7af06b235ead2fd67a4aee2d294b51928 theory of relocation updated ..... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc new file mode 100644 index 000000000..d7356d0b7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc @@ -0,0 +1,23 @@ +lemma pippo: ∀L1,L2,t1. ⬇*[Ⓕ, t1] L1 ≡ L2 → ∀t2. ⬇*[Ⓕ, t2] L1 ≡ L2 → +|t1| + ∥t2∥ = ∥t1∥ + |t2|. +#L1 #L2 #t1 #H elim H -L1 -L2 -t1 +[ #t1 #Ht1 #t2 #H elim (drops_inv_atom1 … H) -H + #_ #Ht2 >Ht1 -Ht1 // >Ht2 -Ht2 // +| #I #L1 #L2 #V #t1 #_ #IH #t2 #H normalize + +lemma drop_conf_div: ∀I1,L,K,V1,m1. ⬇[m1] L ≡ K.ⓑ{I1}V1 → + ∀I2,V2,m2. ⬇[m2] L ≡ K.ⓑ{I2}V2 → + ∧∧ m1 = m2 & I1 = I2 & V1 = V2. +#I1 #L #K #V1 #m1 #HLK1 #I2 #V2 #m2 #HLK2 +elim (yle_split m1 m2) #H +elim (yle_inv_plus_sn … H) -H #m #Hm +[ lapply (drop_conf_ge … HLK1 … HLK2 … Hm ?) +| lapply (drop_conf_ge … HLK2 … HLK1 … Hm ?) +] -HLK1 -HLK2 // #HK +lapply (drop_fwd_length … HK) #H +elim (discr_yplus_x_xy … H) -H +[1,3: #H elim (ylt_yle_false (|K.ⓑ{I1}V1|) (∞)) // ] +#H destruct +lapply (drop_inv_O2 … HK) -HK #H destruct +/2 width=1 by and3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drop.ma deleted file mode 100644 index 2bf29c636..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drop.ma +++ /dev/null @@ -1,35 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/drop_drop.ma". -include "basic_2/multiple/drops.ma". - -(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************) - -(* Properties concerning basic local environment slicing ********************) - -lemma drops_drop_trans: ∀L1,L,cs. ⬇*[Ⓕ, cs] L1 ≡ L → ∀L2,i. ⬇[i] L ≡ L2 → - ∃∃L0,cs0,i0. ⬇[i0] L1 ≡ L0 & ⬇*[Ⓕ, cs0] L0 ≡ L2 & - @⦃i, cs⦄ ≡ i0 & cs ▭ i ≡ cs0. -#L1 #L #cs #H elim H -L1 -L -cs -[ /2 width=7 by drops_nil, minuss_nil, at_nil, ex4_3_intro/ -| #L1 #L0 #L #cs #l #m #_ #HL0 #IHL0 #L2 #i #HL2 - elim (ylt_split i l) #Hil - [ elim (drop_trans_le … HL0 … HL2) -L /2 width=2 by ylt_fwd_le/ - #L #HL0 #HL2 elim (IHL0 … HL0) -L0 /3 width=7 by drops_cons, minuss_lt, at_lt, ex4_3_intro/ - | lapply (drop_trans_ge … HL0 … HL2 ?) -L // #HL02 - elim (IHL0 … HL02) -L0 /3 width=7 by minuss_ge, at_ge, ex4_3_intro/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma index 0ca46fa3c..6a66289bd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma @@ -16,7 +16,7 @@ include "ground_2/relocation/trace_isid.ma". include "basic_2/notation/relations/rliftstar_3.ma". include "basic_2/grammar/term.ma". -(* GENERIC TERM RELOCATION **************************************************) +(* GENERIC RELOCATION FOR TERMS *********************************************) (* Basic_1: includes: lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat @@ -334,11 +334,11 @@ lemma is_lifts_dec: ∀T2,t. Decidable (∃T1. ⬆*[t] T1 ≡ T2). ] qed-. -(* Basic_2A1: removed theorems 17: - lifts_inv_nil lifts_inv_cons lifts_total +(* Basic_2A1: removed theorems 14: + lifts_inv_nil lifts_inv_cons lift_inv_Y1 lift_inv_Y2 lift_inv_lref_Y1 lift_inv_lref_Y2 lift_lref_Y lift_Y1 lift_lref_lt_eq lift_lref_ge_eq lift_lref_plus lift_lref_pred - lift_lref_ge_minus lift_lref_ge_minus_eq lift_total lift_refl + lift_lref_ge_minus lift_lref_ge_minus_eq *) (* Basic_1: removed theorems 8: lift_lref_gt diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma index b0e32002c..3ac75012c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma @@ -14,7 +14,7 @@ include "basic_2/relocation/lifts.ma". -(* GENERIC RELOCATION *******************************************************) +(* GENERIC RELOCATION FOR TERMS *********************************************) (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma index fb5953c26..c1a088ee5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma @@ -15,7 +15,7 @@ include "basic_2/relocation/lifts_lifts.ma". include "basic_2/relocation/lifts_vector.ma". -(* GENERIC TERM VECTOR RELOCATION *******************************************) +(* GENERIC RELOCATION FOR TERM VECTORS *************************************) (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma index 389f724d2..ae73703f7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma @@ -15,7 +15,7 @@ include "basic_2/grammar/term_simple.ma". include "basic_2/relocation/lifts.ma". -(* GENERIC TERM RELOCATION **************************************************) +(* GENERIC RELOCATION FOR TERMS *********************************************) (* Forward lemmas on simple terms *******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma index 89ead4cf5..159e9d869 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma @@ -15,7 +15,7 @@ include "basic_2/grammar/term_vector.ma". include "basic_2/relocation/lifts.ma". -(* GENERIC TERM VECTOR RELOCATION *******************************************) +(* GENERIC RELOCATION FOR TERM VECTORS *************************************) (* Basic_2A1: includes: liftv_nil liftv_cons *) inductive liftsv (t:trace) : relation (list term) ≝ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma index 17952bba8..ace77ad27 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma @@ -15,7 +15,7 @@ include "basic_2/grammar/term_weight.ma". include "basic_2/relocation/lifts.ma". -(* GENERIC TERM RELOCATION **************************************************) +(* GENERIC RELOCATION FOR TERMS *********************************************) (* Forward lemmas on weight for terms ***************************************)