From: Ferruccio Guidi Date: Fri, 18 Mar 2016 14:25:19 +0000 (+0000) Subject: advances in the theory of drops, lexs, and frees ... X-Git-Tag: make_still_working~630 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=629687db8a55432e95c82f0c79e3f51c023e65a6 advances in the theory of drops, lexs, and frees ... --- 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 index d7356d0b7..906c85c73 100644 --- 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 @@ -1,23 +1,13 @@ -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 +(* Inversion lemmas on equivalence ******************************************) -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/ +lemma drop_O1_inj: ∀i,L1,L2,K. ⬇[i] L1 ≡ K → ⬇[i] L2 ≡ K → L1 ⩬[i, ∞] L2. +#i @(ynat_ind … i) -i +[ #L1 #L2 #K #H <(drop_inv_O2 … H) -K #H <(drop_inv_O2 … H) -L1 // +| #i #IHi * [2: #L1 #I1 #V1 ] * [2,4: #L2 #I2 #V2 ] #K #HLK1 #HLK2 // + lapply (drop_fwd_length … HLK1) + <(drop_fwd_length … HLK2) [ /4 width=5 by drop_inv_drop1, lreq_succ/ ] + #H [ elim (ysucc_inv_O_sn … H) | elim (ysucc_inv_O_dx … H) ] +| #L1 #L2 #K #H1 lapply (drop_fwd_Y2 … H1) -H1 + #H elim (ylt_yle_false … H) // +] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc index 8953abb9a..a0926cad1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc @@ -150,3 +150,24 @@ elim (drop_conf_lt … HLK … HLK0 … H0) -HLK -HLK0 -H0 #K1 #V1 #HK1 #_ #_ lapply (drop_fwd_length_lt2 … HK1) -I -K1 -V1 #H elim (ylt_yle_false … H) -H // qed-. + +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_O1_ex: ∀K2,i,L1. |L1| = |K2| + i → + ∃∃L2. L1 ⩬[0, i] L2 & ⬇[i] L2 ≡ K2. +#K2 #i @(ynat_ind … i) -i +[ /3 width=3 by lreq_O2, ex2_intro/ +| #i #IHi #Y >yplus_succ2 #Hi + elim (drop_O1_lt (Ⓕ) Y 0) [2: >Hi // ] + #I #L1 #V #H lapply (drop_inv_O2 … H) -H #H destruct + >length_pair in Hi; #H lapply (ysucc_inv_inj … H) -H + #HL1K2 elim (IHi L1) -IHi // -HL1K2 + /3 width=5 by lreq_pair, drop_drop, ex2_intro/ +| #L1 >yplus_Y2 #H elim (ylt_yle_false (|L1|) (∞)) // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.etc deleted file mode 100644 index f69814078..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.etc +++ /dev/null @@ -1,58 +0,0 @@ -definition dropable_dx: predicate (relation lenv) ≝ - λR. ∀L1,L2. R L1 L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 → - ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & R K1 K2. - -lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R). -#R #HR #L1 #L2 #H elim H -L2 -[ #L2 #HL12 #K2 #c #k #HLK2 elim (HR … HL12 … HLK2) -HR -L2 - /3 width=3 by inj, ex2_intro/ -| #L #L2 #_ #HL2 #IHL1 #K2 #c #k #HLK2 elim (HR … HL2 … HLK2) -HR -L2 - #K #HLK #HK2 elim (IHL1 … HLK) -L - /3 width=5 by step, ex2_intro/ -] -qed-. - - -fact lpx_sn_dropable_aux: ∀R,L2,K2,c,l,k. ⬇[c, l, k] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → - l = 0 → ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & lpx_sn R K1 K2. -#R #L2 #K2 #c #l #k #H elim H -L2 -K2 -l -k -[ #l #k #Hm #X #H >(lpx_sn_inv_atom2 … H) -H - /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/ -| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H - #K1 #V1 #HK12 #HV12 #H destruct - /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/ -| #I #L2 #K2 #V2 #k #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H - #L1 #V1 #HL12 #HV12 #H destruct - elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/ -| #I #L2 #K2 #V2 #W2 #l #k #_ #_ #_ #L1 #_ #H elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R). -/2 width=5 by lpx_sn_dropable_aux/ qed-. - -lemma lpx_sn_drop_trans: ∀R,L1,L2. lpx_sn R L1 L2 → - ∀I,K2,V2,i. ⬇[i] L2 ≡ K2.ⓑ{I}V2 → - ∃∃K1,V1. ⬇[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2. -#R #L1 #L2 #H elim H -L1 -L2 -[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H - [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ - | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 - /3 width=5 by drop_drop_lt, ex3_2_intro/ - ] -] -qed-. - -lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 → - ∀I,K1,V1,i. ⬇[i] L1 ≡ K1.ⓑ{I}V1 → - ∃∃K2,V2. ⬇[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2. -#R #L1 #L2 #H elim H -L1 -L2 -[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H - [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ - | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 - /3 width=5 by drop_drop_lt, ex3_2_intro/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.etc deleted file mode 100644 index 3cb7451ec..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.etc +++ /dev/null @@ -1,49 +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 "ground_2/ynat/ynat_plus.ma". -include "basic_2/grammar/lreq.ma". - -(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************) - -(* Main properties **********************************************************) - -theorem lreq_trans: ∀f. Transitive … (lreq f). -#f #L1 #L2 #H elim H -L1 -L2 -l -m -[ #l #m #X #H lapply (lreq_inv_atom1 … H) -H - #H destruct // -| #I1 #I #L1 #L #V1 #V #_ #IHL1 #X #H elim (lreq_inv_zero1 … H) -H - #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lreq_zero/ -| #I #L1 #L #V #m #_ #IHL1 #X #H elim (lreq_inv_pair1 … H) -H // - #L2 #HL2 #H destruct /3 width=1 by lreq_pair/ -| #I1 #I #L1 #L #V1 #V #l #m #_ #IHL1 #X #H elim (lreq_inv_succ1 … H) -H // - #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lreq_succ/ -] -qed-. - -theorem lreq_canc_sn: ∀l,m,L,L1,L2. L ⩬[l, m] L1 → L ⩬[l, m] L2 → L1 ⩬[l, m] L2. -/3 width=3 by lreq_trans, lreq_sym/ qed-. - -theorem lreq_canc_dx: ∀l,m,L,L1,L2. L1 ⩬[l, m] L → L2 ⩬[l, m] L → L1 ⩬[l, m] L2. -/3 width=3 by lreq_trans, lreq_sym/ qed-. - -theorem lreq_join: ∀L1,L2,l,i. L1 ⩬[l, i] L2 → - ∀m. L1 ⩬[i+l, m] L2 → L1 ⩬[l, i+m] L2. -#L1 #L2 #l #i #H elim H -L1 -L2 -l -i // -[ #I #L1 #L2 #V #m #_ #IHL12 #m #H - lapply (lreq_inv_succ … H ?) -H // >ypred_succ /3 width=1 by lreq_pair/ -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #IHL12 #m #H - lapply (lreq_inv_succ … H ?) -H // >yplus_succ2 >ypred_succ /3 width=1 by lreq_succ/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index 27281ee17..09d381cd8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/rdropstar_4.ma". -include "basic_2/grammar/lenv.ma". +include "basic_2/relocation/lreq.ma". include "basic_2/relocation/lifts.ma". (* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) @@ -52,6 +52,17 @@ definition dropable_sn: predicate (rtmap → relation lenv) ≝ ∀f1. f ⊚ f1 ≡ f2 → ∃∃K2. R f1 K1 K2 & ⬇*[c, f] L2 ≡ K2. +definition dropable_dx: predicate (rtmap → relation lenv) ≝ + λR. ∀L1,L2,f2. R f2 L1 L2 → + ∀K2,c,f. ⬇*[c, f] L2 ≡ K2 → 𝐔⦃f⦄ → + ∀f1. f ⊚ f1 ≡ f2 → + ∃∃K1. ⬇*[c, f] L1 ≡ K1 & R f1 K1 K2. + +definition dedropable_sn: predicate (rtmap → relation lenv) ≝ + λR. ∀L1,K1,c,f. ⬇*[c, f] L1 ≡ K1 → ∀K2,f1. R f1 K1 K2 → + ∀f2. f ⊚ f1 ≡ f2 → + ∃∃L2. R f2 L1 L2 & ⬇*[c, f] L2 ≡ K2 & L1 ≡[f] L2. + (* Basic inversion lemmas ***************************************************) fact drops_inv_atom1_aux: ∀X,Y,c,f. ⬇*[c, f] X ≡ Y → X = ⋆ → @@ -156,6 +167,15 @@ qed-. (* Basic forward lemmas *****************************************************) +(* Basic_1: includes: drop_gen_refl *) +(* Basic_2A1: includes: drop_inv_O2 *) +lemma drops_fwd_isid: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → 𝐈⦃f⦄ → L1 = L2. +#L1 #L2 #c #f #H elim H -L1 -L2 -f // +[ #I #L1 #L2 #V #f #_ #_ #H elim (isid_inv_next … H) // +| /5 width=5 by isid_inv_push, lifts_fwd_isid, eq_f3, sym_eq/ +] +qed-. + fact drops_fwd_drop2_aux: ∀X,Y,c,f2. ⬇*[c, f2] X ≡ Y → ∀I,K,V. Y = K.ⓑ{I}V → ∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[c, f] X ≡ K. #X #Y #c #f2 #H elim H -X -Y -f2 @@ -167,8 +187,6 @@ fact drops_fwd_drop2_aux: ∀X,Y,c,f2. ⬇*[c, f2] X ≡ Y → ∀I,K,V. Y = K. ] qed-. -(* Basic_1: includes: drop_S *) -(* Basic_2A1: includes: drop_fwd_drop2 *) lemma drops_fwd_drop2: ∀I,X,K,V,c,f2. ⬇*[c, f2] X ≡ K.ⓑ{I}V → ∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[c, f] X ≡ K. /2 width=5 by drops_fwd_drop2_aux/ qed-. @@ -180,14 +198,10 @@ lemma drops_after_fwd_drop2: ∀I,X,K,V,c,f2. ⬇*[c, f2] X ≡ K.ⓑ{I}V → /3 width=5 by drops_eq_repl_back, isid_inv_eq_repl, eq_next/ qed-. -(* Basic_1: includes: drop_gen_refl *) -(* Basic_2A1: includes: drop_inv_O2 *) -lemma drops_fwd_isid: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → 𝐈⦃f⦄ → L1 = L2. -#L1 #L2 #c #f #H elim H -L1 -L2 -f // -[ #I #L1 #L2 #V #f #_ #_ #H elim (isid_inv_next … H) // -| /5 width=5 by isid_inv_push, lifts_fwd_isid, eq_f3, sym_eq/ -] -qed-. +(* Basic_1: was: drop_S *) +(* Basic_2A1: was: drop_fwd_drop2 *) +lemma drops_isuni_fwd_drop2: ∀I,X,K,V,c,f. 𝐔⦃f⦄ → ⬇*[c, f] X ≡ K.ⓑ{I}V → ⬇*[c, ⫯f] X ≡ K. +/3 width=7 by drops_after_fwd_drop2, after_isid_isuni/ qed-. (* Basic_2A1: removed theorems 14: drops_inv_nil drops_inv_cons d1_liftable_liftables diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma new file mode 100644 index 000000000..1e0ae189a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/drops.ma". + +(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) + +(* Properties on context sensitive equivalence for terms ********************) + +lemma ceq_lift: d_liftable2 ceq. +/2 width=3 by ex2_intro/ qed-. + +lemma ceq_inv_lift: d_deliftable2_sn ceq. +/2 width=3 by ex2_intro/ qed-. + +(* Note: cfull_inv_lift does not hold *) +lemma cfull_lift: d_liftable2 cfull. +#K #T1 #T2 #_ #L #c #f #_ #U1 #_ -K -T1 -c +elim (lifts_total T2 f) /2 width=3 by ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma index 1bb1ee484..8dec08adc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/relocation/lifts_lifts.ma". -include "basic_2/relocation/drops.ma". +include "basic_2/relocation/drops_weight.ma". (* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) @@ -59,6 +59,29 @@ theorem drops_trans: ∀L1,L,c1,f1. ⬇*[c1, f1] L1 ≡ L → ] qed-. +theorem drops_conf_div: ∀L,K,f1. ⬇*[Ⓣ,f1] L ≡ K → ∀f2. ⬇*[Ⓣ,f2] L ≡ K → + 𝐔⦃f1⦄ → 𝐔⦃f2⦄ → f1 ≗ f2. +#L #K #f1 #H elim H -L -K -f1 +[ #f1 #Hf1 #f2 #Hf2 elim (drops_inv_atom1 … Hf2) -Hf2 + /3 width=1 by isid_inv_eq_repl/ +| #I #L #K #V #f1 #Hf1 #IH #f2 elim (pn_split f2) * + #g2 #H2 #Hf2 #HU1 #HU2 destruct + [ elim (drops_inv_skip1 … Hf2) -IH -HU1 -Hf2 #Y2 #X2 #HY2 #_ #H destruct + lapply (drops_fwd_isid … HY2 ?) -HY2 /2 width=3 by isuni_inv_push/ -HU2 + #H destruct elim (drops_inv_x_pair_xy … Hf1) + | /4 width=5 by drops_inv_drop1, isuni_inv_next, eq_next/ + ] +| #I #L #K #V #W #f1 #Hf1 #_ #IH #f2 elim (pn_split f2) * + #g2 #H2 #Hf2 #HU1 #HU2 destruct + [ elim (drops_inv_skip1 … Hf2) -Hf2 #Y2 #X2 #HY2 #_ #H destruct -Hf1 + /4 width=5 by isuni_fwd_push, eq_push/ + | lapply (drops_inv_drop1 … Hf2) -Hf2 -IH -HU2 #Hg2 + lapply (drops_fwd_isid … Hf1 ?) -Hf1 /2 width=3 by isuni_inv_push/ -HU1 + #H destruct elim (drops_inv_x_pair_xy … Hg2) + ] +] +qed-. + (* Advanced properties ******************************************************) (* Basic_2A1: includes: drop_mono *) @@ -88,3 +111,17 @@ lemma drops_trans_skip2: ∀L1,L,c1,f1. ⬇*[c1, f1] L1 ≡ L → lapply (drops_trans … H1 … H2 … Hf) -L -Hf #H elim (drops_inv_skip2 … H) -H /2 width=5 by ex3_2_intro/ qed-. + +(* Basic_2A1: includes: drops_conf_div *) +lemma drops_conf_div_pair: ∀I1,I2,L,K,V1,V2,f1,f2. + ⬇*[Ⓣ,f1] L ≡ K.ⓑ{I1}V1 → ⬇*[Ⓣ,f2] L ≡ K.ⓑ{I2}V2 → + 𝐔⦃f1⦄ → 𝐔⦃f2⦄ → ∧∧ f1 ≗ f2 & I1 = I2 & V1 = V2. +#I1 #I2 #L #K #V1 #V2 #f1 #f2 #Hf1 #Hf2 #HU1 #HU2 +lapply (drops_isuni_fwd_drop2 … Hf1) // #H1 +lapply (drops_isuni_fwd_drop2 … Hf2) // #H2 +lapply (drops_conf_div … H1 … H2 ??) /2 width=3 by isuni_next/ -H1 -H2 -HU1 -HU2 #H +lapply (eq_inv_nn … H ????) -H [5: |*: // ] #H12 +lapply (drops_eq_repl_back … Hf1 … H12) -Hf1 #H0 +lapply (drops_mono … H0 … Hf2) -L #H +destruct /2 width=1 by and3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma new file mode 100644 index 000000000..f639424f4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma @@ -0,0 +1,151 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/drops.ma". + +(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) + +(* Properties on general entrywise extension of context-sensitive relations *) + +(* Basic_2A1: includes: lpx_sn_deliftable_dropable *) +lemma lexs_deliftable_dropable: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP → + dropable_sn (lexs RN RP). +#RN #RP #HN #HP #L1 #K1 #c #f #H elim H -L1 -K1 -f +[ #f #Hf #X #f2 #H #f1 #Hf2 >(lexs_inv_atom1 … H) -X + /4 width=3 by lexs_atom, drops_atom, ex2_intro/ +| #I #L1 #K1 #V1 #f #_ #IH #X #f2 #H #f1 #Hf2 elim (after_inv_nxx … Hf2) -Hf2 [2,3: // ] + #g2 #Hg2 #H2 destruct elim (lexs_inv_next1 … H) -H + #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2 + /3 width=3 by drops_drop, ex2_intro/ +| #I #L1 #K1 #V1 #W1 #f #HLK #HWV #IH #X #f2 #H #f1 #Hf2 elim (after_inv_pxx … Hf2) -Hf2 [1,3:* |*: // ] + #g1 #g2 #Hg2 #H1 #H2 destruct + [ elim (lexs_inv_push1 … H) | elim (lexs_inv_next1 … H) ] -H + #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2 + [ elim (HP … HV12 … HLK … HWV) | elim (HN … HV12 … HLK … HWV) ] -V1 + /3 width=5 by lexs_next, lexs_push, drops_skip, ex2_intro/ +] +qed-. + +(* Basic_2A1: includes: lpx_sn_liftable_dedropable *) +lemma lexs_liftable_dedropable: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) → + d_liftable2 RN → d_liftable2 RP → dedropable_sn (lexs RN RP). +#RN #RP #H1RN #H1RP #H2RN #H2RP #L1 #K1 #c #f #H elim H -L1 -K1 -f +[ #f #Hf #X #f1 #H #f2 #Hf2 >(lexs_inv_atom1 … H) -X + /4 width=4 by drops_atom, lexs_atom, ex3_intro/ +| #I #L1 #K1 #V1 #f #_ #IHLK1 #K2 #f1 #HK12 #f2 #Hf2 + elim (after_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct + elim (IHLK1 … HK12 … Hg2) -K1 + /3 width=6 by drops_drop, lexs_next, ex3_intro/ +| #I #L1 #K1 #V1 #W1 #f #HLK1 #HWV1 #IHLK1 #X #f1 #H #f2 #Hf2 + elim (after_inv_pxx … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct + [ elim (lexs_inv_push1 … H) | elim (lexs_inv_next1 … H) ] -H #K2 #W2 #HK12 #HW12 #H destruct + [ elim (H2RP … HW12 … HLK1 … HWV1) | elim (H2RN … HW12 … HLK1 … HWV1) ] -W1 + elim (IHLK1 … HK12 … Hg2) -K1 + /3 width=6 by drops_skip, lexs_next, lexs_push, ex3_intro/ +] +qed-. + +fact lexs_dropable_aux: ∀RN,RP,L2,K2,c,f. ⬇*[c, f] L2 ≡ K2 → 𝐔⦃f⦄ → + ∀L1,f2. L1 ⦻*[RN, RP, f2] L2 → ∀f1. f ⊚ f1 ≡ f2 → + ∃∃K1. ⬇*[c, f] L1 ≡ K1 & K1 ⦻*[RN, RP, f1] K2. +#RN #RP #L2 #K2 #c #f #H elim H -L2 -K2 -f +[ #f #Hf #_ #X #f2 #H #f1 #Hf2 lapply (lexs_inv_atom2 … H) -H + #H destruct /4 width=3 by lexs_atom, drops_atom, ex2_intro/ +| #I #L2 #K2 #V2 #f #_ #IH #Hf #X #f2 #HX #f1 #Hf2 + elim (after_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct + elim (lexs_inv_next2 … HX) -HX #L1 #V1 #HL12 #HV12 #H destruct + elim (IH … HL12 … Hg2) -L2 -V2 -g2 + /3 width=3 by drops_drop, isuni_inv_next, ex2_intro/ +| #I #L2 #K2 #V2 #W2 #f #_ #HWV2 #IH #Hf #X #f2 #HX #f1 #Hf2 + elim (after_inv_pxx … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct + [ elim (lexs_inv_push2 … HX) | elim (lexs_inv_next2 … HX) ] -HX #L1 #V1 #HL12 #HV12 #H destruct + elim (IH … HL12 … Hg2) -L2 -g2 /2 width=3 by isuni_fwd_push/ #K1 #HLK1 #HK12 + lapply (isuni_inv_push … Hf ??) -Hf [3,6: |*: // ] #Hf + lapply (lifts_fwd_isid … HWV2 … Hf) #H destruct -HWV2 + lapply (drops_fwd_isid … HLK1 … Hf) #H destruct -HLK1 + /4 width=5 by lexs_next, lexs_push, drops_refl, isid_push, ex2_intro/ +] +qed-. + +(* Basic_2A1: includes: lpx_sn_dropable *) +lemma lexs_dropable: ∀RN,RP. dropable_dx (lexs RN RP). +/2 width=5 by lexs_dropable_aux/ qed-. + +(* Basic_2A1: includes: lpx_sn_drop_conf *) +lemma lexs_drops_conf_next: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP → + ∀L1,L2,f2. L1 ⦻*[RN, RP, f2] L2 → + ∀I,K1,V1,c,f. ⬇*[c,f] L1 ≡ K1.ⓑ{I}V1 → + ∀f1. f ⊚ ⫯f1 ≡ f2 → + ∃∃K2,V2. ⬇*[c,f] L2 ≡ K2.ⓑ{I}V2 & K1 ⦻*[RN, RP, f1] K2 & RN K1 V1 V2. +#RN #RP #HRN #HRP #L1 #L2 #f2 #HL12 #I #K1 #V1 #c #f #HLK1 #f1 #Hf2 +elim (lexs_deliftable_dropable … HRN HRP … HLK1 … HL12 … Hf2) -L1 -f2 -HRN -HRP +#X #HX #HLK2 elim (lexs_inv_next1 … HX) -HX +#K2 #V2 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ +qed-. + +lemma lexs_drops_conf_push: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP → + ∀L1,L2,f2. L1 ⦻*[RN, RP, f2] L2 → + ∀I,K1,V1,c,f. ⬇*[c,f] L1 ≡ K1.ⓑ{I}V1 → + ∀f1. f ⊚ ↑f1 ≡ f2 → + ∃∃K2,V2. ⬇*[c,f] L2 ≡ K2.ⓑ{I}V2 & K1 ⦻*[RN, RP, f1] K2 & RP K1 V1 V2. +#RN #RP #HRN #HRP #L1 #L2 #f2 #HL12 #I #K1 #V1 #c #f #HLK1 #f1 #Hf2 +elim (lexs_deliftable_dropable … HRN HRP … HLK1 … HL12 … Hf2) -L1 -f2 -HRN -HRP +#X #HX #HLK2 elim (lexs_inv_push1 … HX) -HX +#K2 #V2 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ +qed-. + +(* Basic_2A1: includes: lpx_sn_drop_trans *) +lemma lexs_drops_trans_next: ∀RN,RP,L1,L2,f2. L1 ⦻*[RN, RP, f2] L2 → + ∀I,K2,V2,c,f. ⬇*[c,f] L2 ≡ K2.ⓑ{I}V2 → 𝐔⦃f⦄ → + ∀f1. f ⊚ ⫯f1 ≡ f2 → + ∃∃K1,V1. ⬇*[c,f] L1 ≡ K1.ⓑ{I}V1 & K1 ⦻*[RN, RP, f1] K2 & RN K1 V1 V2. +#RN #RP #L1 #L2 #f2 #HL12 #I #K1 #V1 #c #f #HLK1 #Hf #f1 #Hf2 +elim (lexs_dropable … HL12 … HLK1 … Hf … Hf2) -L2 -f2 -Hf +#X #HLK1 #HX elim (lexs_inv_next2 … HX) -HX +#K1 #V1 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ +qed-. + +lemma lexs_drops_trans_push: ∀RN,RP,L1,L2,f2. L1 ⦻*[RN, RP, f2] L2 → + ∀I,K2,V2,c,f. ⬇*[c,f] L2 ≡ K2.ⓑ{I}V2 → 𝐔⦃f⦄ → + ∀f1. f ⊚ ↑f1 ≡ f2 → + ∃∃K1,V1. ⬇*[c,f] L1 ≡ K1.ⓑ{I}V1 & K1 ⦻*[RN, RP, f1] K2 & RP K1 V1 V2. +#RN #RP #L1 #L2 #f2 #HL12 #I #K1 #V1 #c #f #HLK1 #Hf #f1 #Hf2 +elim (lexs_dropable … HL12 … HLK1 … Hf … Hf2) -L2 -f2 -Hf +#X #HLK1 #HX elim (lexs_inv_push2 … HX) -HX +#K1 #V1 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ +qed-. + +lemma drops_lexs_trans_next: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) → + d_liftable2 RN → d_liftable2 RP → + ∀K1,K2,f1. K1 ⦻*[RN, RP, f1] K2 → + ∀I,L1,V1,c,f. ⬇*[c,f] L1.ⓑ{I}V1 ≡ K1 → + ∀f2. f ⊚ f1 ≡ ⫯f2 → + ∃∃L2,V2. ⬇*[c,f] L2.ⓑ{I}V2 ≡ K2 & L1 ⦻*[RN, RP, f2] L2 & RN L1 V1 V2 & L1.ⓑ{I}V1≡[f]L2.ⓑ{I}V2. +#RN #RP #H1RN #H1RP #H2RN #H2RP #K1 #K2 #f1 #HK12 #I #L1 #V1 #c #f #HLK1 #f2 #Hf2 +elim (lexs_liftable_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP +#X #HX #HLK2 #H1L12 elim (lexs_inv_next1 … HX) -HX +#L2 #V2 #H2L12 #HV12 #H destruct /2 width=6 by ex4_2_intro/ +qed-. + +lemma drops_lexs_trans_push: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) → + d_liftable2 RN → d_liftable2 RP → + ∀K1,K2,f1. K1 ⦻*[RN, RP, f1] K2 → + ∀I,L1,V1,c,f. ⬇*[c,f] L1.ⓑ{I}V1 ≡ K1 → + ∀f2. f ⊚ f1 ≡ ↑f2 → + ∃∃L2,V2. ⬇*[c,f] L2.ⓑ{I}V2 ≡ K2 & L1 ⦻*[RN, RP, f2] L2 & RP L1 V1 V2 & L1.ⓑ{I}V1≡[f]L2.ⓑ{I}V2. +#RN #RP #H1RN #H1RP #H2RN #H2RP #K1 #K2 #f1 #HK12 #I #L1 #V1 #c #f #HLK1 #f2 #Hf2 +elim (lexs_liftable_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP +#X #HX #HLK2 #H1L12 elim (lexs_inv_push1 … HX) -HX +#L2 #V2 #H2L12 #HV12 #H destruct /2 width=6 by ex4_2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma index 5b451af83..cde181037 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma @@ -12,88 +12,46 @@ (* *) (**************************************************************************) -include "basic_2/relocation/drops.ma". -include "basic_2/relocation/lreq_lreq.ma". +include "basic_2/relocation/drops_ceq.ma". +include "basic_2/relocation/drops_lexs.ma". (* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) -definition dedropable_sn: predicate (rtmap → relation lenv) ≝ - λR. ∀L1,K1,c,f. ⬇*[c, f] L1 ≡ K1 → ∀K2,f1. R f1 K1 K2 → - ∀f2. f ⊚ f1 ≡ f2 → - ∃∃L2. R f2 L1 L2 & ⬇*[c, f] L2 ≡ K2 & L1 ≡[f] L2. +(* Properties on ranged equivalence for local environments ******************) -(* Properties on equivalence ************************************************) - -lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (LTC … R). -#R #HR #L1 #K1 #c #f #HLK1 #K2 #f1 #H elim H -K2 -[ #K2 #HK12 #f2 #Hf elim (HR … HLK1 … HK12 … Hf) -HR -K1 -f1 - /3 width=4 by inj, ex3_intro/ -| #K #K2 #_ #HK2 #IH #f2 #Hf elim (IH … Hf) -IH -K1 - #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2 … Hf) -HR -K -f1 - /3 width=6 by lreq_trans, step, ex3_intro/ -] -qed-. -(* -lemma lreq_drop_trans_be: ∀L1,L2,l,k. L1 ⩬[l, k] L2 → - ∀I,K2,W,c,i. ⬇[c, 0, i] L2 ≡ K2.ⓑ{I}W → - l ≤ i → ∀k0. i + ⫯k0 = l + k → - ∃∃K1. K1 ⩬[0, k0] K2 & ⬇[c, 0, i] L1 ≡ K1.ⓑ{I}W. -#L1 #L2 #l #k #H elim H -L1 -L2 -l -k -[ #l #k #J #K2 #W #c #i #H - elim (drop_inv_atom1 … H) -H #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J #K2 #W #c #i #_ #_ #k0 - >yplus_succ2 #H elim (ysucc_inv_O_dx … H) -| #I #L1 #L2 #V #k #HL12 #IHL12 #J #K2 #W #c #i #H #_ >yplus_O1 #k0 #H0 - elim (drop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ] - [ destruct - /2 width=3 by drop_pair, ex2_intro/ - | lapply (ylt_inv_O1 … Hi) #H yplus_succ1 #H lapply (ysucc_inv_inj … H) -H <(yplus_O1 k) - #H0 elim (IHL12 … HLK1 … H0) -IHL12 -HLK1 -H0 // - /3 width=3 by drop_drop_lt, ex2_intro/ - ] -| #I1 #I2 #L1 #L2 #V1 #V2 #l #k #_ #IHL12 #J #K2 #W #c #i #HLK2 #Hli #k0 - elim (yle_inv_succ1 … Hli) -Hli - #Hli #Hi yplus_succ1 >yplus_succ1 #H lapply (ysucc_inv_inj … H) -H - #H0 lapply (drop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O1/ - #HLK1 elim (IHL12 … HLK1 … H0) -IHL12 -HLK1 -H0 - /4 width=3 by ylt_O1, drop_drop_lt, ex2_intro/ -] +lemma lreq_dedropable: dedropable_sn lreq. +@lexs_liftable_dedropable +/2 width=6 by cfull_lift, ceq_lift, cfull_refl, ceq_refl/ qed-. -lemma lreq_drop_conf_be: ∀L1,L2,l,k. L1 ⩬[l, k] L2 → - ∀I,K1,W,c,i. ⬇[c, 0, i] L1 ≡ K1.ⓑ{I}W → - l ≤ i → ∀k0. i + ⫯k0 = l + k → - ∃∃K2. K1 ⩬[0, k0] K2 & ⬇[c, 0, i] L2 ≡ K2.ⓑ{I}W. -#L1 #L2 #l #k #HL12 #I #K1 #W #c #i #HLK1 #Hli #k0 #H0 -elim (lreq_drop_trans_be … (lreq_sym … HL12) … HLK1 … H0) // -L1 -Hli -H0 -/3 width=3 by lreq_sym, ex2_intro/ +lemma lreq_dropable: ∀RN,RP. dropable_dx (lexs RN RP). +@lexs_dropable qed-. + +(* Basic_2A1: includes: lreq_drop_trans_be *) +lemma lreq_drops_trans_next: ∀L1,L2,f2. L1 ≡[f2] L2 → + ∀I,K2,V,c,f. ⬇*[c,f] L2 ≡ K2.ⓑ{I}V → 𝐔⦃f⦄ → + ∀f1. f ⊚ ⫯f1 ≡ f2 → + ∃∃K1. ⬇*[c,f] L1 ≡ K1.ⓑ{I}V & K1 ≡[f1] K2. +#L1 #L2 #f2 #HL12 #I #K1 #V #c #f #HLK1 #Hf #f1 #Hf2 +elim (lexs_drops_trans_next … HL12 … HLK1 Hf … Hf2) -L2 -f2 -Hf +/2 width=3 by ex2_intro/ qed-. -lemma drop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i → - ∃∃L2. L1 ⩬[0, i] L2 & ⬇[i] L2 ≡ K2. -#K2 #i @(ynat_ind … i) -i -[ /3 width=3 by lreq_O2, ex2_intro/ -| #i #IHi #Y >yplus_succ2 #Hi - elim (drop_O1_lt (Ⓕ) Y 0) [2: >Hi // ] - #I #L1 #V #H lapply (drop_inv_O2 … H) -H #H destruct - >length_pair in Hi; #H lapply (ysucc_inv_inj … H) -H - #HL1K2 elim (IHi L1) -IHi // -HL1K2 - /3 width=5 by lreq_pair, drop_drop, ex2_intro/ -| #L1 >yplus_Y2 #H elim (ylt_yle_false (|L1|) (∞)) // -] +(* Basic_2A1: includes: lreq_drop_conf_be *) +lemma lreq_drops_conf_next: ∀L1,L2,f2. L1 ≡[f2] L2 → + ∀I,K1,V,c,f. ⬇*[c,f] L1 ≡ K1.ⓑ{I}V → 𝐔⦃f⦄ → + ∀f1. f ⊚ ⫯f1 ≡ f2 → + ∃∃K2. ⬇*[c,f] L2 ≡ K2.ⓑ{I}V & K1 ≡[f1] K2. +#L1 #L2 #f2 #HL12 #I #K1 #V #c #f #HLK1 #Hf #f1 #Hf2 +elim (lreq_drops_trans_next … (lreq_sym … HL12) … HLK1 … Hf2) // -L1 -f2 -Hf +/3 width=3 by lreq_sym, ex2_intro/ qed-. -(* Inversion lemmas on equivalence ******************************************) - -lemma drop_O1_inj: ∀i,L1,L2,K. ⬇[i] L1 ≡ K → ⬇[i] L2 ≡ K → L1 ⩬[i, ∞] L2. -#i @(ynat_ind … i) -i -[ #L1 #L2 #K #H <(drop_inv_O2 … H) -K #H <(drop_inv_O2 … H) -L1 // -| #i #IHi * [2: #L1 #I1 #V1 ] * [2,4: #L2 #I2 #V2 ] #K #HLK1 #HLK2 // - lapply (drop_fwd_length … HLK1) - <(drop_fwd_length … HLK2) [ /4 width=5 by drop_inv_drop1, lreq_succ/ ] - #H [ elim (ysucc_inv_O_sn … H) | elim (ysucc_inv_O_dx … H) ] -| #L1 #L2 #K #H1 lapply (drop_fwd_Y2 … H1) -H1 - #H elim (ylt_yle_false … H) // -] +lemma drops_lreq_trans_next: ∀K1,K2,f1. K1 ≡[f1] K2 → + ∀I,L1,V,c,f. ⬇*[c,f] L1.ⓑ{I}V ≡ K1 → + ∀f2. f ⊚ f1 ≡ ⫯f2 → + ∃∃L2. ⬇*[c,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V≡[f]L2.ⓑ{I}V. +#K1 #K2 #f1 #HK12 #I #L1 #V #c #f #HLK1 #f2 #Hf2 +elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -K1 -f1 +/2 width=6 by cfull_lift, ceq_lift, cfull_refl, ceq_refl, ex3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma index 428fcd460..0b1ef4ff2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "ground_2/lib/lstar.ma". +include "basic_2/relocation/lreq_lreq.ma". include "basic_2/relocation/drops.ma". (* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) @@ -71,3 +72,23 @@ lemma d2_deliftable_sn_llstar: ∀R. d_deliftable2_sn R → elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/ ] qed-. + +lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (LTC … R). +#R #HR #L1 #L2 #f2 #H elim H -L2 +[ #L2 #HL12 #K2 #c #f #HLK2 #Hf #f1 #Hf2 elim (HR … HL12 … HLK2 … Hf … Hf2) -HR -L2 -f2 -Hf + /3 width=3 by inj, ex2_intro/ +| #L #L2 #_ #HL2 #IHL1 #K2 #c #f #HLK2 #Hf #f1 #Hf2 elim (HR … HL2 … HLK2 … Hf … Hf2) -HR -L2 + #K #HLK #HK2 elim (IHL1 … HLK … Hf … Hf2) -L -f2 -Hf + /3 width=5 by step, ex2_intro/ +] +qed-. + +lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (LTC … R). +#R #HR #L1 #K1 #c #f #HLK1 #K2 #f1 #H elim H -K2 +[ #K2 #HK12 #f2 #Hf elim (HR … HLK1 … HK12 … Hf) -HR -K1 -f1 + /3 width=4 by inj, ex3_intro/ +| #K #K2 #_ #HK2 #IH #f2 #Hf elim (IH … Hf) -IH -K1 + #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2 … Hf) -HR -K -f1 + /3 width=6 by lreq_trans, step, ex3_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma index d0dc9e7a0..2df6d9832 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma @@ -30,7 +30,6 @@ lemma drops_fwd_lw: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}. qed-. (* Basic_2A1: includes: drop_fwd_lw_lt *) -(* Note: 𝐈⦃t⦄ → ⊥ is ∥l∥ < |L| *) lemma drops_fwd_lw_lt: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → (𝐈⦃f⦄ → ⊥) → ♯{L2} < ♯{L1}. #L1 #L2 #f #H elim H -L1 -L2 -f @@ -48,3 +47,10 @@ lemma drops_pair2_fwd_rfw: ∀I,L,K,V,c,f. ⬇*[c, f] L ≡ K.ⓑ{I}V → ∀T. #I #L #K #V #c #f #HLK lapply (drops_fwd_lw … HLK) -HLK normalize in ⊢ (%→?→?%%); /3 width=3 by le_to_lt_to_lt/ qed-. + +(* Advanced inversion lemma *************************************************) + +lemma drops_inv_x_pair_xy: ∀I,L,V,c,f. ⬇*[c,f] L ≡ L.ⓑ{I}V → ⊥. +#I #L #V #c #f #H lapply (drops_fwd_lw … H) -c -f +/2 width=4 by lt_le_false/ (**) (* full auto is a bit slow: 19s *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma index 604a918c5..dee6950e3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma @@ -12,95 +12,158 @@ (* *) (**************************************************************************) -include "ground_2/relocation/trace_sor.ma". -include "ground_2/relocation/trace_isun.ma". +include "ground_2/relocation/rtmap_sor.ma". include "basic_2/notation/relations/freestar_3.ma". include "basic_2/grammar/lenv.ma". (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) -inductive frees: relation3 lenv term trace ≝ -| frees_atom: ∀I. frees (⋆) (⓪{I}) (◊) -| frees_sort: ∀I,L,V,s,t. frees L (⋆s) t → - frees (L.ⓑ{I}V) (⋆s) (Ⓕ @ t) -| frees_zero: ∀I,L,V,t. frees L V t → - frees (L.ⓑ{I}V) (#0) (Ⓣ @ t) -| frees_lref: ∀I,L,V,i,t. frees L (#i) t → - frees (L.ⓑ{I}V) (#⫯i) (Ⓕ @ t) -| frees_gref: ∀I,L,V,p,t. frees L (§p) t → - frees (L.ⓑ{I}V) (§p) (Ⓕ @ t) -| frees_bind: ∀I,L,V,T,t1,t2,t,b,a. frees L V t1 → frees (L.ⓑ{I}V) T (b @ t2) → - t1 ⋓ t2 ≡ t → frees L (ⓑ{a,I}V.T) t -| frees_flat: ∀I,L,V,T,t1,t2,t. frees L V t1 → frees L T t2 → - t1 ⋓ t2 ≡ t → frees L (ⓕ{I}V.T) t +inductive frees: relation3 lenv term rtmap ≝ +| frees_atom: ∀I,f. 𝐈⦃f⦄ → frees (⋆) (⓪{I}) f +| frees_sort: ∀I,L,V,s,f. frees L (⋆s) f → + frees (L.ⓑ{I}V) (⋆s) (↑f) +| frees_zero: ∀I,L,V,f. frees L V f → + frees (L.ⓑ{I}V) (#0) (⫯f) +| frees_lref: ∀I,L,V,i,f. frees L (#i) f → + frees (L.ⓑ{I}V) (#⫯i) (↑f) +| frees_gref: ∀I,L,V,p,f. frees L (§p) f → + frees (L.ⓑ{I}V) (§p) (↑f) +| frees_bind: ∀I,L,V,T,a,f1,f2,f. frees L V f1 → frees (L.ⓑ{I}V) T f2 → + f1 ⋓ ⫱f2 ≡ f → frees L (ⓑ{a,I}V.T) f +| frees_flat: ∀I,L,V,T,f1,f2,f. frees L V f1 → frees L T f2 → + f1 ⋓ f2 ≡ f → frees L (ⓕ{I}V.T) f . interpretation "context-sensitive free variables (term)" 'FreeStar L T t = (frees L T t). -(* Basic forward lemmas *****************************************************) +(* Basic inversion lemmas ***************************************************) -fact frees_fwd_sort_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀x. X = ⋆x → 𝐔⦃t⦄. -#L #X #t #H elim H -L -X -t /3 width=2 by isun_id, isun_false/ -[ #_ #L #V #t #_ #_ #x #H destruct -| #_ #L #_ #i #t #_ #_ #x #H destruct -| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #_ #_ #x #H destruct -| #I #L #V #T #t1 #t2 #t #_ #_ #_ #_ #_ #x #H destruct +fact frees_inv_sort_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = ⋆x → 𝐈⦃f⦄. +#L #X #f #H elim H -L -X -f /3 width=3 by isid_push/ +[ #_ #L #V #f #_ #_ #x #H destruct +| #_ #L #_ #i #f #_ #_ #x #H destruct +| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct +| #I #L #V #T #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct ] qed-. -lemma frees_fwd_sort: ∀L,t,s. L ⊢ 𝐅*⦃⋆s⦄ ≡ t → 𝐔⦃t⦄. -/2 width=5 by frees_fwd_sort_aux/ qed-. +lemma frees_inv_sort: ∀L,s,f. L ⊢ 𝐅*⦃⋆s⦄ ≡ f → 𝐈⦃f⦄. +/2 width=5 by frees_inv_sort_aux/ qed-. -fact frees_fwd_gref_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀x. X = §x → 𝐔⦃t⦄. -#L #X #t #H elim H -L -X -t /3 width=2 by isun_id, isun_false/ -[ #_ #L #V #t #_ #_ #x #H destruct -| #_ #L #_ #i #t #_ #_ #x #H destruct -| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #_ #_ #x #H destruct -| #I #L #V #T #t1 #t2 #t #_ #_ #_ #_ #_ #x #H destruct +fact frees_inv_gref_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = §x → 𝐈⦃f⦄. +#L #X #f #H elim H -L -X -f /3 width=3 by isid_push/ +[ #_ #L #V #f #_ #_ #x #H destruct +| #_ #L #_ #i #f #_ #_ #x #H destruct +| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct +| #I #L #V #T #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct ] qed-. -lemma frees_fwd_gref: ∀L,t,p. L ⊢ 𝐅*⦃§p⦄ ≡ t → 𝐔⦃t⦄. -/2 width=5 by frees_fwd_gref_aux/ qed-. - -(* Basic inversion lemmas ***************************************************) +lemma frees_inv_gref: ∀L,p,f. L ⊢ 𝐅*⦃§p⦄ ≡ f → 𝐈⦃f⦄. +/2 width=5 by frees_inv_gref_aux/ qed-. -fact frees_inv_zero_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → X = #0 → - (L = ⋆ ∧ t = ◊) ∨ - ∃∃I,K,V,u. K ⊢ 𝐅*⦃V⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓣ@u. -#L #X #t * -L -X -t +fact frees_inv_zero_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → X = #0 → + (L = ⋆ ∧ 𝐈⦃f⦄) ∨ + ∃∃I,K,V,g. K ⊢ 𝐅*⦃V⦄ ≡ g & L = K.ⓑ{I}V & f = ⫯g. +#L #X #f * -L -X -f [ /3 width=1 by or_introl, conj/ -| #I #L #V #s #t #_ #H destruct +| #I #L #V #s #f #_ #H destruct | /3 width=7 by ex3_4_intro, or_intror/ -| #I #L #V #i #t #_ #H destruct -| #I #L #V #p #t #_ #H destruct -| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #H destruct -| #I #L #V #T #t1 #t2 #t #_ #_ #_ #H destruct +| #I #L #V #i #f #_ #H destruct +| #I #L #V #p #f #_ #H destruct +| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #H destruct +| #I #L #V #T #f1 #f2 #f #_ #_ #_ #H destruct ] qed-. -lemma frees_inv_zero: ∀L,t. L ⊢ 𝐅*⦃#0⦄ ≡ t → - (L = ⋆ ∧ t = ◊) ∨ - ∃∃I,K,V,u. K ⊢ 𝐅*⦃V⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓣ@u. +lemma frees_inv_zero: ∀L,f. L ⊢ 𝐅*⦃#0⦄ ≡ f → + (L = ⋆ ∧ 𝐈⦃f⦄) ∨ + ∃∃I,K,V,g. K ⊢ 𝐅*⦃V⦄ ≡ g & L = K.ⓑ{I}V & f = ⫯g. /2 width=3 by frees_inv_zero_aux/ qed-. -fact frees_inv_lref_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀j. X = #(⫯j) → - (L = ⋆ ∧ t = ◊) ∨ - ∃∃I,K,V,u. K ⊢ 𝐅*⦃#j⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓕ@u. -#L #X #t * -L -X -t +fact frees_inv_lref_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀j. X = #(⫯j) → + (L = ⋆ ∧ 𝐈⦃f⦄) ∨ + ∃∃I,K,V,g. K ⊢ 𝐅*⦃#j⦄ ≡ g & L = K.ⓑ{I}V & f = ↑g. +#L #X #f * -L -X -f [ /3 width=1 by or_introl, conj/ -| #I #L #V #s #t #_ #j #H destruct -| #I #L #V #t #_ #j #H destruct -| #I #L #V #i #t #Ht #j #H destruct /3 width=7 by ex3_4_intro, or_intror/ -| #I #L #V #p #t #_ #j #H destruct -| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #j #H destruct -| #I #L #V #T #t1 #t2 #t #_ #_ #_ #j #H destruct +| #I #L #V #s #f #_ #j #H destruct +| #I #L #V #f #_ #j #H destruct +| #I #L #V #i #f #Ht #j #H destruct /3 width=7 by ex3_4_intro, or_intror/ +| #I #L #V #p #f #_ #j #H destruct +| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #j #H destruct +| #I #L #V #T #f1 #f2 #f #_ #_ #_ #j #H destruct ] qed-. -lemma frees_inv_lref: ∀L,i,t. L ⊢ 𝐅*⦃#(⫯i)⦄ ≡ t → - (L = ⋆ ∧ t = ◊) ∨ - ∃∃I,K,V,u. K ⊢ 𝐅*⦃#i⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓕ@u. +lemma frees_inv_lref: ∀L,i,f. L ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f → + (L = ⋆ ∧ 𝐈⦃f⦄) ∨ + ∃∃I,K,V,g. K ⊢ 𝐅*⦃#i⦄ ≡ g & L = K.ⓑ{I}V & f = ↑g. /2 width=3 by frees_inv_lref_aux/ qed-. + +fact frees_inv_bind_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T,a. X = ⓑ{a,I}V.T → + ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f. +#L #X #f * -L -X -f +[ #I #f #_ #J #W #U #b #H destruct +| #I #L #V #s #f #_ #J #W #U #b #H destruct +| #I #L #V #f #_ #J #W #U #b #H destruct +| #I #L #V #i #f #_ #J #W #U #b #H destruct +| #I #L #V #p #f #_ #J #W #U #b #H destruct +| #I #L #V #T #a #f1 #f2 #f #HV #HT #Hf #J #W #U #b #H destruct /2 width=5 by ex3_2_intro/ +| #I #L #V #T #f1 #f2 #f #_ #_ #_ #J #W #U #b #H destruct +] +qed-. + +lemma frees_inv_bind: ∀I,L,V,T,a,f. L ⊢ 𝐅*⦃ⓑ{a,I}V.T⦄ ≡ f → + ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f. +/2 width=4 by frees_inv_bind_aux/ qed-. + +fact frees_inv_flat_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T. X = ⓕ{I}V.T → + ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f. +#L #X #f * -L -X -f +[ #I #f #_ #J #W #U #H destruct +| #I #L #V #s #f #_ #J #W #U #H destruct +| #I #L #V #f #_ #J #W #U #H destruct +| #I #L #V #i #f #_ #J #W #U #H destruct +| #I #L #V #p #f #_ #J #W #U #H destruct +| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #J #W #U #H destruct +| #I #L #V #T #f1 #f2 #f #HV #HT #Hf #J #W #U #H destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma frees_inv_flat: ∀I,L,V,T,f. L ⊢ 𝐅*⦃ⓕ{I}V.T⦄ ≡ f → + ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f. +/2 width=4 by frees_inv_flat_aux/ qed-. + +(* Basic properties ********************************************************) + +lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f). +#L #T #f1 #H elim H -L -T -f1 +[ /3 width=3 by frees_atom, isid_eq_repl_back/ +| #I #L #V #s #f1 #_ #IH #f2 #Hf12 + elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_sort/ +| #I #L #V #f1 #_ #IH #f2 #Hf12 + elim (eq_inv_nx … Hf12) -Hf12 /3 width=3 by frees_zero/ +| #I #L #V #i #f1 #_ #IH #f2 #Hf12 + elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_lref/ +| #I #L #V #p #f1 #_ #IH #f2 #Hf12 + elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_gref/ +| /3 width=7 by frees_bind, sor_eq_repl_back3/ +| /3 width=7 by frees_flat, sor_eq_repl_back3/ +] +qed-. + +lemma frees_eq_repl_fwd: ∀L,T. eq_repl_fwd … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f). +#L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/ +qed-. + +lemma frees_sort_gen: ∀L,s,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃⋆s⦄ ≡ f. +#L elim L -L +/4 width=3 by frees_eq_repl_back, frees_sort, frees_atom, eq_push_inv_isid/ +qed. + +lemma frees_gref_gen: ∀L,p,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃§p⦄ ≡ f. +#L elim L -L +/4 width=3 by frees_eq_repl_back, frees_gref, frees_atom, eq_push_inv_isid/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index d89370b41..8140a5d31 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -16,7 +16,7 @@ include "ground_2/relocation/rtmap_sle.ma". include "basic_2/notation/relations/relationstar_5.ma". include "basic_2/grammar/lenv.ma". -(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) +(* GENERAL ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) definition relation5 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] ≝ λA,B,C,D,E.A→B→C→D→E→Prop. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_drops.ma deleted file mode 100644 index fa066595f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_drops.ma +++ /dev/null @@ -1,95 +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/relocation/lexs.ma". -include "basic_2/relocation/drops.ma". - -(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) - -(* Basic_2A1: includes: lpx_sn_deliftable_dropable *) -lemma lexs_deliftable_dropable: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP → - dropable_sn (lexs RN RP). -#RN #RP #HN #HP #L1 #K1 #c #f #H elim H -L1 -K1 -f -[ #f #Hf #X #f2 #H #f1 #Hf2 >(lexs_inv_atom1 … H) -X - /4 width=3 by lexs_atom, drops_atom, ex2_intro/ -| #I #L1 #K1 #V1 #f #_ #IH #X #f2 #H #f1 #Hf2 elim (after_inv_nxx … Hf2) -Hf2 [2,3: // ] - #g2 #Hg2 #H2 destruct elim (lexs_inv_next1 … H) -H - #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2 - /3 width=3 by drops_drop, ex2_intro/ -| #I #L1 #K1 #V1 #W1 #f #HLK #HWV #IH #X #f2 #H #f1 #Hf2 elim (after_inv_pxx … Hf2) -Hf2 [1,3:* |*: // ] - #g1 #g2 #Hg2 #H1 #H2 destruct - [ elim (lexs_inv_push1 … H) | elim (lexs_inv_next1 … H) ] -H - #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2 - [ elim (HP … HV12 … HLK … HWV) | elim (HN … HV12 … HLK … HWV) ] -V1 - /3 width=5 by lexs_next, lexs_push, drops_skip, ex2_intro/ -] -qed-. -(* -lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → - d_liftable2 R → dedropable_sn (lpx_sn R). -#R #H1R #H2R #L1 #K1 #s #l #m #H elim H -L1 -K1 -l -m -[ #l #m #Hm #X #H >(lpx_sn_inv_atom1 … H) -H - /4 width=4 by drop_atom, lpx_sn_atom, ex3_intro/ -| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H - #K2 #V2 #HK12 #HV12 #H destruct - lapply (lpx_sn_fwd_length … HK12) - #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *) - /3 width=1 by lpx_sn_pair, lreq_O2/ -| #I #L1 #K1 #V1 #m #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 - /3 width=5 by drop_drop, lreq_pair, lpx_sn_pair, ex3_intro/ -| #I #L1 #K1 #V1 #W1 #l #m #HLK1 #HWV1 #IHLK1 #X #H - elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct - elim (H2R … HW12 … HLK1 … HWV1) -W1 - elim (IHLK1 … HK12) -K1 - /3 width=6 by drop_skip, lreq_succ, lpx_sn_pair, ex3_intro/ -] -qed-. -*) -include "ground_2/relocation/trace_isun.ma". - -lemma lpx_sn_dropable: ∀R,L2,K2,c,t. ⬇*[c, t] L2 ≡ K2 → 𝐔⦃t⦄ → - ∀L1,u2. lpx_sn R u2 L1 L2 → ∀u1. t ⊚ u1 ≡ u2 → - ∃∃K1. ⬇*[c, t] L1 ≡ K1 & lpx_sn R u1 K1 K2. -#R #L2 #K2 #c #t #H elim H -L2 -K2 -t -[ #t #Ht #_ #X #u2 #H #u1 #Hu elim (lpx_sn_inv_atom2 … H) -H - #H1 #H2 destruct elim (after_inv_empty3 … Hu) -Hu - /4 width=3 by drops_atom, lpx_sn_atom, ex2_intro/ -| #I #L2 #K2 #V2 #t #_ #IH #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair2 … H) -H - #L1 #V1 #y2 #x #HL #HV #H1 #H2 destruct elim (after_inv_false1 … Hu) -Hu - #u #H #Hu destruct elim (IH … HL … Hu) -L2 /3 width=3 by drops_drop, isun_inv_false, ex2_intro/ -| #I #L2 #K2 #V2 #W2 #t #_ #HWV #IHLK #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair2 … H) -H - #L1 #V1 #y2 #x #HL #HV #H1 #H2 destruct elim (after_inv_true1 … Hu) -Hu - #y1 #y #x2 #H1 #H2 #Hu destruct lapply (isun_inv_true … Ht) -Ht - #Ht elim (IHLK … HL … Hu) -L2 -Hu /2 width=1 by isun_id/ - #K1 #HLK1 #HK12 lapply (lifts_fwd_isid … HWV ?) // -HWV - #H destruct lapply (drops_fwd_isid … HLK1 ?) // - #H destruct - @ex2_intro - [ - | @(drops_skip … HLK1) - | @(lpx_sn_pair … HK12 … HV) - - - lapply (drops_fwd_isid … HLK1 ?) // -HLK1 - 2: - - - - - elim (HR … HV … HLK … HWV) -V1 - elim (IHLK … HL … Hu) -L1 /3 width=5 by drops_skip, lpx_sn_pair, ex2_intro/ - - -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma index c8d3536de..3f40c553c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma @@ -15,7 +15,7 @@ include "basic_2/grammar/lenv_length.ma". include "basic_2/relocation/lexs.ma". -(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) +(* GENERAL ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) (* Forward lemmas on length for local environments **************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma index 1b8aa44cb..a22e62c86 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma @@ -17,7 +17,7 @@ include "ground_2/relocation/rtmap_sor.ma". include "basic_2/grammar/lenv_weight.ma". include "basic_2/relocation/lexs.ma". -(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) +(* GENERAL ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) (* Main properties **********************************************************) @@ -58,7 +58,7 @@ theorem lexs_conf: ∀RN1,RP1,RN2,RP2. ] qed-. -theorem lexs_canc_sx: ∀RN,RP,f. Transitive … (lexs RN RP f) → +theorem lexs_canc_sn: ∀RN,RP,f. Transitive … (lexs RN RP f) → symmetric … (lexs RN RP f) → left_cancellable … (lexs RN RP f). /3 width=3 by/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma new file mode 100644 index 000000000..70abd6f5b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/lexs_lexs.ma". +include "basic_2/relocation/lreq.ma". + +(* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************) + +(* Main properties **********************************************************) + +theorem lreq_trans: ∀f. Transitive … (lreq f). +/2 width=3 by lexs_trans/ qed-. + +theorem lreq_canc_sn: ∀f. left_cancellable … (lreq f). +/3 width=3 by lexs_canc_sn, lreq_trans, lreq_sym/ qed-. + +theorem lreq_canc_dx: ∀f. right_cancellable … (lreq f). +/3 width=3 by lexs_canc_dx, lreq_trans, lreq_sym/ qed-. + +theorem lreq_join: ∀L1,L2,f1. L1 ≡[f1] L2 → ∀f2. L1 ≡[f2] L2 → + ∀f. f1 ⋓ f2 ≡ f → L1 ≡[f] L2. +/2 width=5 by lexs_join/ qed-. + +theorem lreq_meet: ∀L1,L2,f1. L1 ≡[f1] L2 → ∀f2. L1 ≡[f2] L2 → + ∀f. f1 ⋒ f2 ≡ f → L1 ≡[f] L2. +/2 width=5 by lexs_meet/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/isuniform_1.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/isuniform_1.etc deleted file mode 100644 index 349f2b3bf..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/isuniform_1.etc +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) - -notation "hvbox( 𝐔 ⦃ term 46 f ⦄ )" - non associative with precedence 45 - for @{ 'IsUniform $f }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isuniform_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isuniform_1.ma new file mode 100644 index 000000000..349f2b3bf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isuniform_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( 𝐔 ⦃ term 46 f ⦄ )" + non associative with precedence 45 + for @{ 'IsUniform $f }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma index 3db5d524f..fdfefbba5 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma @@ -14,6 +14,7 @@ include "ground_2/notation/relations/rafter_3.ma". include "ground_2/relocation/rtmap_istot.ma". +include "ground_2/relocation/rtmap_isuni.ma". (* RELOCATION MAP ***********************************************************) @@ -313,6 +314,13 @@ qed-. lemma after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄. /3 width=4 by after_fwd_isid2, after_fwd_isid1, conj/ qed-. +(* Properties on isuni ******************************************************) + +lemma after_isid_isuni: ∀f1,f2. 𝐈⦃f2⦄ → 𝐔⦃f1⦄ → f1 ⊚ ⫯f2 ≡ ⫯f1. +#f1 #f2 #Hf2 #H elim H -H +/5 width=7 by isid_after_dx, after_eq_repl_back_2, after_next, after_push, eq_push_inv_isid/ +qed. + (* Forward lemmas on at *****************************************************) lemma after_at_fwd: ∀i,i1,f. @⦃i1, f⦄ ≡ i → ∀f2,f1. f2 ⊚ f1 ≡ f → diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isuni.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isuni.ma new file mode 100644 index 000000000..efde1a120 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isuni.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/notation/relations/isuniform_1.ma". +include "ground_2/relocation/rtmap_isid.ma". + +(* RELOCATION MAP ***********************************************************) + +inductive isuni: predicate rtmap ≝ +| isuni_isid: ∀f. 𝐈⦃f⦄ → isuni f +| isuni_next: ∀f. isuni f → ∀g. ⫯f = g → isuni g +. + +interpretation "test for uniformity (rtmap)" + 'IsUniform f = (isuni f). + +(* Basic inversion lemmas ***************************************************) + +lemma isuni_inv_push: ∀g. 𝐔⦃g⦄ → ∀f. ↑f = g → 𝐈⦃f⦄. +#g * -g /2 width=3 by isid_inv_push/ +#f #_ #g #H #x #Hx destruct elim (discr_push_next … Hx) +qed-. + +lemma isuni_inv_next: ∀g. 𝐔⦃g⦄ → ∀f. ⫯f = g → 𝐔⦃f⦄. +#g * -g #f #Hf +[ #x #Hx elim (isid_inv_next … Hf … Hx) +| #g #H #x #Hx destruct /2 width=1 by injective_push/ +] +qed-. + +(* basic forward lemmas *****************************************************) + +lemma isuni_fwd_push: ∀g. 𝐔⦃g⦄ → ∀f. ↑f = g → 𝐔⦃f⦄. +/3 width=3 by isuni_inv_push, isuni_isid/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma index 86ad267c6..fcf82d2cc 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma @@ -73,6 +73,39 @@ qed-. (* Basic properties *********************************************************) +corec lemma sand_eq_repl_back1: ∀f2,f. eq_repl_back … (λf1. f1 ⋒ f2 ≡ f). +#f2 #f #f1 * -f1 -f2 -f +#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x #Hx +try cases (eq_inv_px … Hx … H1) try cases (eq_inv_nx … Hx … H1) -g1 +/3 width=7 by sand_pp, sand_np, sand_pn, sand_nn/ +qed-. + +lemma sand_eq_repl_fwd1: ∀f2,f. eq_repl_fwd … (λf1. f1 ⋒ f2 ≡ f). +#f2 #f @eq_repl_sym /2 width=3 by sand_eq_repl_back1/ +qed-. + +corec lemma sand_eq_repl_back2: ∀f1,f. eq_repl_back … (λf2. f1 ⋒ f2 ≡ f). +#f1 #f #f2 * -f1 -f2 -f +#f1 #f2 #f #g1 #g2 #g #Hf #H #H2 #H0 #x #Hx +try cases (eq_inv_px … Hx … H2) try cases (eq_inv_nx … Hx … H2) -g2 +/3 width=7 by sand_pp, sand_np, sand_pn, sand_nn/ +qed-. + +lemma sand_eq_repl_fwd2: ∀f1,f. eq_repl_fwd … (λf2. f1 ⋒ f2 ≡ f). +#f1 #f @eq_repl_sym /2 width=3 by sand_eq_repl_back2/ +qed-. + +corec lemma sand_eq_repl_back3: ∀f1,f2. eq_repl_back … (λf. f1 ⋒ f2 ≡ f). +#f1 #f2 #f * -f1 -f2 -f +#f1 #f2 #f #g1 #g2 #g #Hf #H #H2 #H0 #x #Hx +try cases (eq_inv_px … Hx … H0) try cases (eq_inv_nx … Hx … H0) -g +/3 width=7 by sand_pp, sand_np, sand_pn, sand_nn/ +qed-. + +lemma sand_eq_repl_fwd3: ∀f1,f2. eq_repl_fwd … (λf. f1 ⋒ f2 ≡ f). +#f1 #f2 @eq_repl_sym /2 width=3 by sand_eq_repl_back3/ +qed-. + corec lemma sand_refl: ∀f. f ⋒ f ≡ f. #f cases (pn_split f) * #g #H [ @(sand_pp … H H H) | @(sand_nn … H H H) ] -H // diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma index 9b093603c..0bc38867e 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma @@ -73,6 +73,39 @@ qed-. (* Basic properties *********************************************************) +corec lemma sor_eq_repl_back1: ∀f2,f. eq_repl_back … (λf1. f1 ⋓ f2 ≡ f). +#f2 #f #f1 * -f1 -f2 -f +#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x #Hx +try cases (eq_inv_px … Hx … H1) try cases (eq_inv_nx … Hx … H1) -g1 +/3 width=7 by sor_pp, sor_np, sor_pn, sor_nn/ +qed-. + +lemma sor_eq_repl_fwd1: ∀f2,f. eq_repl_fwd … (λf1. f1 ⋓ f2 ≡ f). +#f2 #f @eq_repl_sym /2 width=3 by sor_eq_repl_back1/ +qed-. + +corec lemma sor_eq_repl_back2: ∀f1,f. eq_repl_back … (λf2. f1 ⋓ f2 ≡ f). +#f1 #f #f2 * -f1 -f2 -f +#f1 #f2 #f #g1 #g2 #g #Hf #H #H2 #H0 #x #Hx +try cases (eq_inv_px … Hx … H2) try cases (eq_inv_nx … Hx … H2) -g2 +/3 width=7 by sor_pp, sor_np, sor_pn, sor_nn/ +qed-. + +lemma sor_eq_repl_fwd2: ∀f1,f. eq_repl_fwd … (λf2. f1 ⋓ f2 ≡ f). +#f1 #f @eq_repl_sym /2 width=3 by sor_eq_repl_back2/ +qed-. + +corec lemma sor_eq_repl_back3: ∀f1,f2. eq_repl_back … (λf. f1 ⋓ f2 ≡ f). +#f1 #f2 #f * -f1 -f2 -f +#f1 #f2 #f #g1 #g2 #g #Hf #H #H2 #H0 #x #Hx +try cases (eq_inv_px … Hx … H0) try cases (eq_inv_nx … Hx … H0) -g +/3 width=7 by sor_pp, sor_np, sor_pn, sor_nn/ +qed-. + +lemma sor_eq_repl_fwd3: ∀f1,f2. eq_repl_fwd … (λf. f1 ⋓ f2 ≡ f). +#f1 #f2 @eq_repl_sym /2 width=3 by sor_eq_repl_back3/ +qed-. + corec lemma sor_refl: ∀f. f ⋓ f ≡ f. #f cases (pn_split f) * #g #H [ @(sor_pp … H H H) | @(sor_nn … H H H) ] -H // diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index cfbe19cf3..6d0741909 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -23,8 +23,8 @@ table { class "grass" [ { "multiple relocation" * } { [ { "" * } { - [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ] - [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ] + [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ] + [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ] (* [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]