From: Ferruccio Guidi Date: Mon, 11 Apr 2016 17:15:40 +0000 (+0000) Subject: - advances on drops X-Git-Tag: make_still_working~605 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=3ef251397627da80aeea0cf08b053a4bc781ef88 - advances on drops - partial commit of the "static" component --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/aaa/aaa_freq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/aaa/aaa_freq.etc new file mode 100644 index 000000000..a81eb6166 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/aaa/aaa_freq.etc @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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/multiple/lleq_drop.ma". +include "basic_2/static/aaa.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +(* Properties on lazy equivalence for local environments ********************) + +lemma lleq_aaa_trans: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A → + ∀L1. L1 ≡[T, 0] L2 → ⦃G, L1⦄ ⊢ T ⁝ A. +#G #L2 #T #A #H elim H -G -L2 -T -A /2 width=1 by aaa_sort/ +[ #I #G #L2 #K2 #V2 #A #i #HLK2 #_ #IHV2 #L1 #H elim (lleq_fwd_lref_dx … H … HLK2) -L2 + [ #H elim (ylt_yle_false … H) // + | * /3 width=5 by aaa_lref/ + ] +| #a #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_bind_O … H) -H + /3 width=2 by aaa_abbr/ +| #a #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_bind_O … H) -H + /3 width=1 by aaa_abst/ +| #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_flat … H) -H + /3 width=3 by aaa_appl/ +| #G #L2 #V #T #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_flat … H) -H + /3 width=1 by aaa_cast/ +] +qed-. + +lemma aaa_lleq_conf: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A → + ∀L1. L2 ≡[T, 0] L1 → ⦃G, L1⦄ ⊢ T ⁝ A. +/3 width=3 by lleq_aaa_trans, lleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc index 6c07f6f34..5d51b83c8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc @@ -1,29 +1,2 @@ lemma drop_inv_refl: ∀L,l,m. ⬇[Ⓕ, l, m] L ≡ L → m = 0. /2 width=5 by drop_inv_length_eq/ qed-. - -fact drop_inv_FT_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 → - ∀I,K,V. L2 = K.ⓑ{I}V → s = Ⓣ → l = 0 → - ⬇[Ⓕ, l, m] L1 ≡ K.ⓑ{I}V. -#L1 #L2 #s #l #m #H elim H -L1 -L2 -l -m -[ #l #m #_ #J #K #W #H destruct -| #I #L #V #J #K #W #H destruct // -| #I #L1 #L2 #V #m #_ #IHL12 #J #K #W #H1 #H2 destruct - /3 width=1 by drop_drop/ -| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #_ #J #K #W #_ #_ #H - elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma drop_inv_FT: ∀I,L,K,V,m. ⬇[Ⓣ, 0, m] L ≡ K.ⓑ{I}V → ⬇[m] L ≡ -K.ⓑ{I}V. -/2 width=5 by drop_inv_FT_aux/ qed. - -lemma drop_inv_gen: ∀I,L,K,V,s,m. ⬇[s, 0, m] L ≡ K.ⓑ{I}V → ⬇[m] L ≡ -K.ⓑ{I}V. -#I #L #K #V * /2 width=1 by drop_inv_FT/ -qed-. - -lemma drop_inv_T: ∀I,L,K,V,s,m. ⬇[Ⓣ, 0, m] L ≡ K.ⓑ{I}V → ⬇[s, 0, m] L -≡ K.ⓑ{I}V. -#I #L #K #V * /2 width=1 by drop_inv_FT/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index fd47afae2..b540ec904 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground_2/relocation/rtmap_isfin.ma". include "basic_2/notation/relations/rdropstar_3.ma". include "basic_2/notation/relations/rdropstar_4.ma". include "basic_2/relocation/lreq.ma". @@ -84,6 +83,27 @@ lemma drops_eq_repl_fwd: ∀L1,L2,c. eq_repl_fwd … (λf. ⬇*[c, f] L1 ≡ L2) #L1 #L2 #c @eq_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *) qed-. +lemma drops_inv_tls_at: ∀f,i1,i2. @⦃i1,f⦄ ≡ i2 → + ∀c, L1,L2. ⬇*[c,⫱*[i2]f] L1 ≡ L2 → + ⬇*[c,↑⫱*[⫯i2]f] L1 ≡ L2. +/3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-. + +(* Basic_2A1: includes: drop_FT *) +lemma drops_TF: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → ⬇*[Ⓕ, f] L1 ≡ L2. +#L1 #L2 #f #H elim H -L1 -L2 -f +/3 width=1 by drops_atom, drops_drop, drops_skip/ +qed. + +(* Basic_2A1: includes: drop_gen *) +lemma drops_gen: ∀L1,L2,c,f. ⬇*[Ⓣ, f] L1 ≡ L2 → ⬇*[c, f] L1 ≡ L2. +#L1 #L2 * /2 width=1 by drops_TF/ +qed-. + +(* Basic_2A1: includes: drop_T *) +lemma drops_F: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → ⬇*[Ⓕ, f] L1 ≡ L2. +#L1 #L2 * /2 width=1 by drops_TF/ +qed-. + (* Basic_2A1: includes: drop_refl *) lemma drops_refl: ∀c,L,f. 𝐈⦃f⦄ → ⬇*[c, f] L ≡ L. #c #L elim L -L /2 width=1 by drops_atom/ @@ -112,20 +132,22 @@ lemma drops_split_trans: ∀L1,L2,f,c. ⬇*[c, f] L1 ≡ L2 → ∀f1,f2. f1 ⊚ ] qed-. -(* Basic_2A1: includes: drop_FT *) -lemma drops_TF: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → ⬇*[Ⓕ, f] L1 ≡ L2. -#L1 #L2 #f #H elim H -L1 -L2 -f -/3 width=1 by drops_atom, drops_drop, drops_skip/ -qed. - -(* Basic_2A1: includes: drop_gen *) -lemma drops_gen: ∀L1,L2,c,f. ⬇*[Ⓣ, f] L1 ≡ L2 → ⬇*[c, f] L1 ≡ L2. -#L1 #L2 * /2 width=1 by drops_TF/ -qed-. - -(* Basic_2A1: includes: drop_T *) -lemma drops_F: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → ⬇*[Ⓕ, f] L1 ≡ L2. -#L1 #L2 * /2 width=1 by drops_TF/ +lemma drops_split_div: ∀L1,L,f1,c. ⬇*[c, f1] L1 ≡ L → ∀f2,f. f1 ⊚ f2 ≡ f → 𝐔⦃f2⦄ → + ∃∃L2. ⬇*[Ⓕ, f2] L ≡ L2 & ⬇*[Ⓕ, f] L1 ≡ L2. +#L1 #L #f1 #c #H elim H -L1 -L -f1 +[ #f1 #Hc #f2 #f #Hf #Hf2 @(ex2_intro … (⋆)) @drops_atom #H destruct +| #I #L1 #L #V #f1 #HL1 #IH #f2 #f #Hf #Hf2 elim (after_inv_nxx … Hf) -Hf [2,3: // ] + #g #Hg #H destruct elim (IH … Hg) -IH -Hg /3 width=5 by drops_drop, ex2_intro/ +| #I #L1 #L #V1 #V #f1 #HL1 #HV1 #IH #f2 #f #Hf #Hf2 + elim (after_inv_pxx … Hf) -Hf [1,3: * |*: // ] + #g2 #g #Hg #H2 #H0 destruct + [ lapply (isuni_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH + lapply (after_isid_inv_dx … Hg … Hg2) -Hg #Hg + /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, lifts_eq_repl_back, isid_push, ex2_intro/ + | lapply (isuni_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HV1 + elim (IH … Hg) -f1 /3 width=3 by drops_drop, ex2_intro/ + ] +] qed-. (* Basic forward lemmas *****************************************************) @@ -236,6 +258,39 @@ lemma drops_inv_skip2: ∀I,X,K2,V2,c,f. ⬇*[c, ↑f] X ≡ K2.ⓑ{I}V2 → ∃∃K1,V1. ⬇*[c, f] K1 ≡ K2 & ⬆*[f] V2 ≡ V1 & X = K1.ⓑ{I}V1. /2 width=5 by drops_inv_skip2_aux/ qed-. +fact drops_inv_TF_aux: ∀L1,L2,f. ⬇*[Ⓕ, f] L1 ≡ L2 → 𝐔⦃f⦄ → + ∀I,K,V. L2 = K.ⓑ{I}V → + ⬇*[Ⓣ, f] L1 ≡ K.ⓑ{I}V. +#L1 #L2 #f #H elim H -L1 -L2 -f +[ #f #_ #_ #J #K #W #H destruct +| #I #L1 #L2 #V #f #_ #IH #Hf #J #K #W #H destruct + /4 width=3 by drops_drop, isuni_inv_next/ +| #I #L1 #L2 #V1 #V2 #f #HL12 #HV21 #_ #Hf #J #K #W #H destruct + lapply (isuni_inv_push … Hf ??) -Hf [1,2: // ] #Hf + <(drops_fwd_isid … HL12) -K // <(lifts_fwd_isid … HV21) -V1 + /3 width=3 by drops_refl, isid_push/ +] +qed-. + +(* Basic_2A1: includes: drop_inv_FT *) +lemma drops_inv_TF: ∀I,L,K,V,f. ⬇*[Ⓕ, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ → + ⬇*[Ⓣ, f] L ≡ K.ⓑ{I}V. +/2 width=3 by drops_inv_TF_aux/ qed-. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_2A1: includes: drop_inv_gen *) +lemma drops_inv_gen: ∀I,L,K,V,c,f. ⬇*[c, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ → + ⬇*[Ⓣ, f] L ≡ K.ⓑ{I}V. +#I #L #K #V * /2 width=1 by drops_inv_TF/ +qed-. + +(* Basic_2A1: includes: drop_inv_T *) +lemma drops_inv_F: ∀I,L,K,V,c,f. ⬇*[Ⓕ, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ → + ⬇*[c, f] L ≡ K.ⓑ{I}V. +#I #L #K #V * /2 width=1 by drops_inv_TF/ +qed-. + (* Inversion lemmas with test for uniformity ********************************) lemma drops_inv_isuni: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐔⦃f⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma index 66d0f47d9..e0d6aa164 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma @@ -12,23 +12,22 @@ (* *) (**************************************************************************) -include "basic_2/substitution/drop_drop.ma". include "basic_2/static/aaa.ma". (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) -(* Main properties **********************************************************) +(* Main inversion lemmas ****************************************************) theorem aaa_mono: ∀G,L,T,A1. ⦃G, L⦄ ⊢ T ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T ⁝ A2 → A1 = A2. #G #L #T #A1 #H elim H -G -L -T -A1 -[ #G #L #s #A2 #H - >(aaa_inv_sort … H) -H // -| #I1 #G #L #K1 #V1 #B #i #HLK1 #_ #IHA1 #A2 #H - elim (aaa_inv_lref … H) -H #I2 #K2 #V2 #HLK2 #HA2 - lapply (drop_mono … HLK1 … HLK2) -L #H destruct /2 width=1 by/ -| #a #G #L #V #T #B1 #A1 #_ #_ #_ #IHA1 #A2 #H +[ #G #L #s #A2 #H >(aaa_inv_sort … H) -H // +| #I1 #G #L #V1 #B #_ #IH #A2 #H + elim (aaa_inv_zero … H) -H #I2 #K2 #V2 #H #HA2 destruct /2 width=1 by/ +| #I1 #G #L #V1 #B #i #_ #IH #A2 #H + elim (aaa_inv_lref … H) -H #I2 #K2 #V2 #H #HA2 destruct /2 width=1 by/ +| #p #G #L #V #T #B1 #A1 #_ #_ #_ #IH #A2 #H elim (aaa_inv_abbr … H) -H /2 width=1 by/ -| #a #G #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H +| #p #G #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H elim (aaa_inv_abst … H) -H #B2 #A2 #HB2 #HA2 #H destruct /3 width=1 by eq_f2/ | #G #L #V1 #T1 #B1 #A1 #_ #_ #_ #IHA1 #A2 #H elim (aaa_inv_appl … H) -H #B2 #_ #HA2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_drops.ma index 9fc9a9ebd..5ef58ee9f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_drops.ma @@ -12,12 +12,14 @@ (* *) (**************************************************************************) -include "basic_2/relocation/drops.ma". +include "basic_2/relocation/drops_drops.ma". +include "basic_2/s_computation/fqup_weight.ma". +include "basic_2/s_computation/fqup_drops.ma". include "basic_2/static/aaa.ma". (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) -(* Properties with generic slicing for local environments *******************) +(* Advanced properties ******************************************************) (* Basic_2A1: was: aaa_lref *) lemma aaa_lref_gen: ∀I,G,K,V,B,i,L. ⬇*[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ⁝ B → ⦃G, L⦄ ⊢ #i ⁝ B. @@ -29,46 +31,7 @@ lemma aaa_lref_gen: ∀I,G,K,V,B,i,L. ⬇*[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ ] qed. -(* Basic_2A1: includes: aaa_lift *) -lemma aaa_lifts: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀L2,c,f. ⬇*[c, f] L2 ≡ L1 → - ∀T2. ⬆*[f] T1 ≡ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. -#G #L1 #T1 #A #H elim H -G -L1 -T1 -A -[ #G #L1 #s #L2 #c #f #_ #T2 #H - >(lifts_inv_sort1 … H) -H // -| #I #G #L1 #V1 #B #_ #IHB #L2 #c #f #HL21 #T2 #H - elim (lifts_inv_lref1 … H) -H #i2 #Hi #H destruct - @aaa_lref_gen [5: @IHB ] -| #I #G #L1 #V1 #B #i1 #_ #IHB #L2 #c #f #HL21 #T2 #H - elim (lifts_inv_lref1 … H) -H #i2 #Hi #H destruct - lapply (at_inv_nxx … H) - - - - -| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #c #l #k #HL21 #T2 #H - elim (lift_inv_lref1 … H) -H * #Hil #H destruct - [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by ylt_fwd_le/ #X #HLK2 #H - elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K2 #V2 #HK21 #HV12 #H destruct - /3 width=9 by aaa_lref/ - | lapply (drop_trans_ge … HL21 … HLK1 ?) -L1 - /3 width=9 by aaa_lref, drop_inv_gen/ - ] -| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #c #l #k #HL21 #X #H - elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - /4 width=5 by aaa_abbr, drop_skip/ -| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #c #l #k #HL21 #X #H - elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - /4 width=5 by aaa_abst, drop_skip/ -| #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #c #l #k #HL21 #X #H - elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - /3 width=5 by aaa_appl/ -| #G #L1 #V1 #T1 #A #_ #_ #IH1 #IH2 #L2 #c #l #k #HL21 #X #H - elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - /3 width=5 by aaa_cast/ -] -qed. - -(* Inversion lemmas with generic slicing for local environments *************) +(* Advanced inversion lemmas ************************************************) (* Basic_2A1: was: aaa_inv_lref *) lemma aaa_inv_lref_gen: ∀G,A,i,L. ⦃G, L⦄ ⊢ #i ⁝ A → @@ -80,27 +43,78 @@ lemma aaa_inv_lref_gen: ∀G,A,i,L. ⦃G, L⦄ ⊢ #i ⁝ A → ] qed-. -lemma aaa_inv_lift: ∀G,L2,T2,A. ⦃G, L2⦄ ⊢ T2 ⁝ A → ∀L1,c,l,k. ⬇[c, l, k] L2 ≡ L1 → - ∀T1. ⬆[l, k] T1 ≡ T2 → ⦃G, L1⦄ ⊢ T1 ⁝ A. -#G #L2 #T2 #A #H elim H -G -L2 -T2 -A -[ #G #L2 #s #L1 #c #l #k #_ #T1 #H - >(lift_inv_sort2 … H) -H // -| #I #G #L2 #K2 #V2 #B #i #HLK2 #_ #IHB #L1 #c #l #k #HL21 #T1 #H - elim (lift_inv_lref2 … H) -H * #Hil #H destruct - [ elim (drop_conf_lt … HL21 … HLK2) -L2 /3 width=9 by aaa_lref/ - | lapply (drop_conf_ge … HL21 … HLK2 ?) -L2 /3 width=9 by aaa_lref/ +(* Properties with generic slicing for local environments *******************) + +(* Basic_2A1: includes: aaa_lift *) +lemma aaa_lifts: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀L2,c,f. ⬇*[c, f] L2 ≡ L1 → + ∀T2. ⬆*[f] T1 ≡ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. +@fqup_wf_ind_eq #G0 #L0 #T0 #IH #G #L1 * * +[ #s #HG #HL #HT #A #H #L2 #c #f #HL21 #X #HX -IH -c + lapply (aaa_inv_sort … H) -H #H destruct + >(lifts_inv_sort1 … HX) -HX // +| #i1 #HG #HL #HT #A #H #L2 #c #f #HL21 #X #HX + elim (aaa_inv_lref_gen … H) -H #J #K1 #V1 #HLK1 #HA + elim (lifts_inv_lref1 … HX) -HX #i2 #Hf #H destruct + lapply (drops_trans … HL21 … HLK1 ??) -HL21 [1,2: // ] #H + elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK2 #HY + lapply (drops_inv_tls_at … Hf … HY) -HY #HY -Hf + elim (drops_inv_skip2 … HY) -HY #K2 #V2 #HK21 #HV12 #H destruct + /4 width=12 by aaa_lref_gen, fqup_lref, drops_inv_gen/ +| #l #HG #HL #HT #A #H #L2 #c #f #HL21 #X #HX -IH -c -f + elim (aaa_inv_gref … H) +| #p * #V1 #T1 #HG #HL #HT #A #H #L2 #c #f #HL21 #X #HX + [ elim (aaa_inv_abbr … H) -H #B #HB #HA + elim (lifts_inv_bind1 … HX) -HX #V2 #T2 #HV12 #HT12 #H destruct + /4 width=9 by aaa_abbr, drops_skip/ + | elim (aaa_inv_abst … H) -H #B #A0 #HB #HA #H0 + elim (lifts_inv_bind1 … HX) -HX #V2 #T2 #HV12 #HT12 #H destruct + /4 width=8 by aaa_abst, drops_skip/ + ] +| * #V1 #T1 #HG #HL #HT #A #H #L2 #c #f #HL21 #X #HX + [ elim (aaa_inv_appl … H) -H #B #HB #HA + elim (lifts_inv_flat1 … HX) -HX #V2 #T2 #HV12 #HT12 #H destruct + /3 width=10 by aaa_appl/ + | elim (aaa_inv_cast … H) -H #H1A #H2A + elim (lifts_inv_flat1 … HX) -HX #V2 #T2 #HV12 #HT12 #H destruct + /3 width=8 by aaa_cast/ + ] +] +qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +(* Basic_2A1: includes: aaa_inv_lift *) +lemma aaa_inv_lifts: ∀G,L2,T2,A. ⦃G, L2⦄ ⊢ T2 ⁝ A → ∀L1,c,f. ⬇*[c, f] L2 ≡ L1 → + ∀T1. ⬆*[f] T1 ≡ T2 → ⦃G, L1⦄ ⊢ T1 ⁝ A. +@fqup_wf_ind_eq #G0 #L0 #T0 #IH #G #L2 * * +[ #s #HG #HL #HT #A #H #L1 #c #f #HL21 #X #HX -IH -c + lapply (aaa_inv_sort … H) -H #H destruct + >(lifts_inv_sort2 … HX) -HX // +| #i2 #HG #HL #HT #A #H #L1 #c #f #HL21 #X #HX + elim (aaa_inv_lref_gen … H) -H #J #K2 #V2 #HLK2 #HA + elim (lifts_inv_lref2 … HX) -HX #i1 #Hf #H destruct + lapply (drops_split_div … HL21 (𝐔❴i1❵) ???) -HL21 [4: * |*: // ] #Y #HLK1 #HY + lapply (drops_conf … HLK2 … HY ??) -HY [1,2: /2 width=6 by after_uni_dx/ ] #HY + lapply (drops_inv_tls_at … Hf … HY) -HY #HY -Hf + elim (drops_inv_skip1 … HY) -HY #K1 #V1 #HK21 #HV12 #H destruct + /4 width=12 by aaa_lref_gen, fqup_lref, drops_inv_F/ +| #l #HG #HL #HT #A #H #L1 #c #f #HL21 #X #HX -IH -c -f + elim (aaa_inv_gref … H) +| #p * #V2 #T2 #HG #HL #HT #A #H #L1 #c #f #HL21 #X #HX + [ elim (aaa_inv_abbr … H) -H #B #HB #HA + elim (lifts_inv_bind2 … HX) -HX #V1 #T1 #HV12 #HT12 #H destruct + /4 width=9 by aaa_abbr, drops_skip/ + | elim (aaa_inv_abst … H) -H #B #A0 #HB #HA #H0 + elim (lifts_inv_bind2 … HX) -HX #V1 #T1 #HV12 #HT12 #H destruct + /4 width=8 by aaa_abst, drops_skip/ + ] +| * #V2 #T2 #HG #HL #HT #A #H #L1 #c #f #HL21 #X #HX + [ elim (aaa_inv_appl … H) -H #B #HB #HA + elim (lifts_inv_flat2 … HX) -HX #V1 #T1 #HV12 #HT12 #H destruct + /3 width=10 by aaa_appl/ + | elim (aaa_inv_cast … H) -H #H1A #H2A + elim (lifts_inv_flat2 … HX) -HX #V1 #T1 #HV12 #HT12 #H destruct + /3 width=8 by aaa_cast/ ] -| #a #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #c #l #k #HL21 #X #H - elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct - /4 width=5 by aaa_abbr, drop_skip/ -| #a #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #c #l #k #HL21 #X #H - elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct - /4 width=5 by aaa_abst, drop_skip/ -| #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #c #l #k #HL21 #X #H - elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct - /3 width=5 by aaa_appl/ -| #G #L2 #V2 #T2 #A #_ #_ #IH1 #IH2 #L1 #c #l #k #HL21 #X #H - elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct - /3 width=5 by aaa_cast/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma index 576b0814e..7905a6a9f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/multiple/fqus_alt.ma". -include "basic_2/static/aaa_lift.ma". +include "basic_2/s_computation/fqus_fqup.ma". +include "basic_2/static/aaa_drops.ma". (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) @@ -22,16 +22,15 @@ include "basic_2/static/aaa_lift.ma". lemma aaa_fqu_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[ #I #G #L #T #A #H elim (aaa_inv_lref … H) -H - #J #K #V #H #HA lapply (drop_inv_O2 … H) -H - #H destruct /2 width=2 by ex_intro/ -| * [ #a ] * #G #L #V #T #X #H +[ #I #G #L #T #A #H elim (aaa_inv_zero … H) -H + #J #K #V #H #HA destruct /2 width=2 by ex_intro/ +| * [ #p ] * #G #L #V #T #X #H [ elim (aaa_inv_abbr … H) | elim (aaa_inv_abst … H) | elim (aaa_inv_appl … H) | elim (aaa_inv_cast … H) ] -H /2 width=2 by ex_intro/ -| #a * #G #L #V #T #X #H +| #p * #G #L #V #T #X #H [ elim (aaa_inv_abbr … H) | elim (aaa_inv_abst … H) ] -H /2 width=2 by ex_intro/ @@ -39,13 +38,13 @@ lemma aaa_fqu_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ [ elim (aaa_inv_appl … H) | elim (aaa_inv_cast … H) ] -H /2 width=2 by ex_intro/ -| /3 width=9 by aaa_inv_lift, ex_intro/ +| /5 width=8 by aaa_inv_lifts, drops_refl, drops_drop, ex_intro/ ] qed-. lemma aaa_fquq_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim(fquq_inv_gen … H) -H /2 width=6 by aaa_fqu_conf/ +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H /2 width=6 by aaa_fqu_conf/ * #H1 #H2 #H3 destruct /2 width=2 by ex_intro/ qed-. @@ -58,6 +57,6 @@ qed-. lemma aaa_fqus_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim(fqus_inv_gen … H) -H /2 width=6 by aaa_fqup_conf/ +#G1 #G2 #L1 #L2 #T1 #T2 #H elim(fqus_inv_fqup … H) -H /2 width=6 by aaa_fqup_conf/ * #H1 #H2 #H3 destruct /2 width=2 by ex_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lleq.ma deleted file mode 100644 index a81eb6166..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lleq.ma +++ /dev/null @@ -1,42 +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/multiple/lleq_drop.ma". -include "basic_2/static/aaa.ma". - -(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) - -(* Properties on lazy equivalence for local environments ********************) - -lemma lleq_aaa_trans: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A → - ∀L1. L1 ≡[T, 0] L2 → ⦃G, L1⦄ ⊢ T ⁝ A. -#G #L2 #T #A #H elim H -G -L2 -T -A /2 width=1 by aaa_sort/ -[ #I #G #L2 #K2 #V2 #A #i #HLK2 #_ #IHV2 #L1 #H elim (lleq_fwd_lref_dx … H … HLK2) -L2 - [ #H elim (ylt_yle_false … H) // - | * /3 width=5 by aaa_lref/ - ] -| #a #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_bind_O … H) -H - /3 width=2 by aaa_abbr/ -| #a #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_bind_O … H) -H - /3 width=1 by aaa_abst/ -| #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_flat … H) -H - /3 width=3 by aaa_appl/ -| #G #L2 #V #T #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_flat … H) -H - /3 width=1 by aaa_cast/ -] -qed-. - -lemma aaa_lleq_conf: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A → - ∀L1. L2 ≡[T, 0] L1 → ⦃G, L1⦄ ⊢ T ⁝ A. -/3 width=3 by lleq_aaa_trans, lleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma new file mode 100644 index 000000000..8b182b560 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/rtmap_id.ma". +include "basic_2/s_computation/fqup_weight.ma". +include "basic_2/static/frees.ma". + +(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) + +(* Advanced properties ******************************************************) + +(* Notes: this replaces lemma 1400 concluding the "big tree" theorem *) +lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≡ f. +#L #T @(fqup_wf_ind_eq … (⋆) L T) -L -T +#G0 #L0 #T0 #IH #G #L * +[ cases L -L /3 width=2 by frees_atom, ex_intro/ + #L #I #V * + [ #s #HG #HL #HT destruct + elim (IH G L (⋆s)) -IH /3 width=2 by frees_sort_gen, fqu_fqup, fqu_drop, lifts_sort, ex_intro/ + | * [2: #i ] #HG #HL #HT destruct + [ elim (IH G L (#i)) -IH /3 width=2 by frees_lref, fqu_fqup, ex_intro/ + | elim (IH G L V) -IH /3 width=2 by frees_zero, fqu_fqup, fqu_lref_O, ex_intro/ + ] + | #l #HG #HL #HT destruct + elim (IH G L (§l)) -IH /3 width=2 by frees_gref_gen, fqu_fqup, fqu_drop, lifts_gref, ex_intro/ + ] +| * [ #p ] #I #V #T #HG #HL #HT destruct elim (IH G L V) // #f1 #HV + [ elim (IH G (L.ⓑ{I}V) T) -IH // #f2 #HT + elim (sor_isfin_ex f1 (⫱f2)) + /3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/ + | elim (IH G L T) -IH // #f2 #HT + elim (sor_isfin_ex f1 f2) + /3 width=6 by frees_fwd_isfin, frees_flat, ex_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_frees.ma index e59b029c7..4cf172a1c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_frees.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/frees.ma". +include "basic_2/static/frees.ma". (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma index a1f7ab05e..07e0d5e80 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/relocation/lreq.ma". -include "basic_2/relocation/frees.ma". +include "basic_2/static/frees.ma". (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_weight.ma deleted file mode 100644 index 04e8c370f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_weight.ma +++ /dev/null @@ -1,44 +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/relocation/rtmap_id.ma". -include "basic_2/grammar/cl_restricted_weight.ma". -include "basic_2/relocation/frees.ma". - -(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) - -(* Advanced properties ******************************************************) - -(* Notes: this replaces lemma 1400 concluding the "big tree" theorem *) -lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≡ f. -@(f2_ind … rfw) #n #IH #L * -[ cases L -L /3 width=2 by frees_atom, ex_intro/ - #L #I #V * - [ #s #Hn destruct elim (IH L (⋆s)) -IH /3 width=2 by frees_sort, ex_intro/ - | * [2: #i ] #Hn destruct - [ elim (IH L (#i)) -IH /3 width=2 by frees_lref, ex_intro/ - | elim (IH L V) -IH /3 width=2 by frees_zero, ex_intro/ - ] - | #l #Hn destruct elim (IH L (§l)) -IH /3 width=2 by frees_gref, ex_intro/ - ] -| * [ #p ] #I #V #T #Hn destruct elim (IH L V) // #f1 #HV - [ elim (IH (L.ⓑ{I}V) T) -IH // #f2 #HT - elim (sor_isfin_ex f1 (⫱f2)) - /3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/ - | elim (IH L T) -IH // #f2 #HT - elim (sor_isfin_ex f1 f2) - /3 width=6 by frees_fwd_isfin, frees_flat, ex_intro/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/freq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/freq.ma index 0f3868536..a66eb6487 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/freq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/freq.ma @@ -14,8 +14,8 @@ include "basic_2/notation/relations/lazyeq_6.ma". include "basic_2/grammar/genv.ma". -include "basic_2/relocation/frees_weight.ma". -include "basic_2/relocation/frees_lreq.ma". +include "basic_2/static/frees_fqup.ma". +include "basic_2/static/frees_lreq.ma". (* RANGED EQUIVALENCE FOR CLOSURES ******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/freq_freq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/freq_freq.ma index d4d8f76de..4ff819570 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/freq_freq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/freq_freq.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/relocation/lreq_lreq.ma". -include "basic_2/relocation/frees_frees.ma". -include "basic_2/relocation/freq.ma". +include "basic_2/static/frees_frees.ma". +include "basic_2/static/freq.ma". (* RANGED EQUIVALENCE FOR CLOSURES *****************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma index 613a8f321..91b50e3fc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma @@ -13,10 +13,9 @@ (**************************************************************************) include "basic_2/notation/relations/lrsubeqa_3.ma". -include "basic_2/static/lsubr.ma". include "basic_2/static/aaa.ma". -(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************) +(* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************) inductive lsuba (G:genv): relation lenv ≝ | lsuba_atom: lsuba G (⋆) (⋆) @@ -87,58 +86,8 @@ lemma lsuba_inv_pair2: ∀I,G,L1,K2,W. G ⊢ L1 ⫃⁝ K2.ⓑ{I}W → I = Abst & L1 = K1.ⓓⓝW.V. /2 width=3 by lsuba_inv_pair2_aux/ qed-. -(* Basic forward lemmas *****************************************************) - -lemma lsuba_fwd_lsubr: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → L1 ⫃ L2. -#G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/ -qed-. - (* Basic properties *********************************************************) lemma lsuba_refl: ∀G,L. G ⊢ L ⫃⁝ L. #G #L elim L -L /2 width=1 by lsuba_atom, lsuba_pair/ qed. - -(* Note: the constant 0 cannot be generalized *) -lemma lsuba_drop_O1_conf: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K1,c,k. ⬇[c, 0, k] L1 ≡ K1 → - ∃∃K2. G ⊢ K1 ⫃⁝ K2 & ⬇[c, 0, k] L2 ≡ K2. -#G #L1 #L2 #H elim H -L1 -L2 -[ /2 width=3 by ex2_intro/ -| #I #L1 #L2 #V #_ #IHL12 #K1 #c #k #H - elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1 - [ destruct - elim (IHL12 L1 c 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_pair, drop_pair, ex2_intro/ - | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/ - ] -| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K1 #c #k #H - elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1 - [ destruct - elim (IHL12 L1 c 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/ - | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/ - ] -] -qed-. - -(* Note: the constant 0 cannot be generalized *) -lemma lsuba_drop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 → - ∃∃K1. G ⊢ K1 ⫃⁝ K2 & ⬇[c, 0, k] L1 ≡ K1. -#G #L1 #L2 #H elim H -L1 -L2 -[ /2 width=3 by ex2_intro/ -| #I #L1 #L2 #V #_ #IHL12 #K2 #c #k #H - elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2 - [ destruct - elim (IHL12 L2 c 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_pair, drop_pair, ex2_intro/ - | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/ - ] -| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K2 #c #k #H - elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2 - [ destruct - elim (IHL12 L2 c 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/ - | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma index 6f8e00c84..9f1f9bcc5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma @@ -15,7 +15,7 @@ include "basic_2/static/aaa_aaa.ma". include "basic_2/static/lsuba.ma". -(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************) +(* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************) (* Properties concerning atomic arity assignment ****************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_drops.ma new file mode 100644 index 000000000..f2440c801 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_drops.ma @@ -0,0 +1,65 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/lrsubeqa_3.ma". +include "basic_2/static/lsubr.ma". +include "basic_2/static/aaa.ma". + +(* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************) + +(* Basic properties *********************************************************) + +(* Note: the constant 0 cannot be generalized *) +lemma lsuba_drop_O1_conf: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K1,c,k. ⬇[c, 0, k] L1 ≡ K1 → + ∃∃K2. G ⊢ K1 ⫃⁝ K2 & ⬇[c, 0, k] L2 ≡ K2. +#G #L1 #L2 #H elim H -L1 -L2 +[ /2 width=3 by ex2_intro/ +| #I #L1 #L2 #V #_ #IHL12 #K1 #c #k #H + elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1 + [ destruct + elim (IHL12 L1 c 0) -IHL12 // #X #HL12 #H + <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_pair, drop_pair, ex2_intro/ + | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/ + ] +| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K1 #c #k #H + elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1 + [ destruct + elim (IHL12 L1 c 0) -IHL12 // #X #HL12 #H + <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/ + | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/ + ] +] +qed-. + +(* Note: the constant 0 cannot be generalized *) +lemma lsuba_drop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 → + ∃∃K1. G ⊢ K1 ⫃⁝ K2 & ⬇[c, 0, k] L1 ≡ K1. +#G #L1 #L2 #H elim H -L1 -L2 +[ /2 width=3 by ex2_intro/ +| #I #L1 #L2 #V #_ #IHL12 #K2 #c #k #H + elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2 + [ destruct + elim (IHL12 L2 c 0) -IHL12 // #X #HL12 #H + <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_pair, drop_pair, ex2_intro/ + | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/ + ] +| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K2 #c #k #H + elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2 + [ destruct + elim (IHL12 L2 c 0) -IHL12 // #X #HL12 #H + <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/ + | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma index bb77403bd..ee7ab0de5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma @@ -14,7 +14,7 @@ include "basic_2/static/lsuba_aaa.ma". -(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************) +(* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************) (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsubr.ma new file mode 100644 index 000000000..3655ce112 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsubr.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lsubr.ma". +include "basic_2/static/lsuba.ma". + +(* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************) + +(* Forward lemmas with restricted refinement for local environments *********) + +lemma lsuba_fwd_lsubr: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → L1 ⫃ L2. +#G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/ +qed-. 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 09bab5e10..15969a23c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma @@ -401,8 +401,8 @@ qed-. (* Properties with at *******************************************************) -lemma after_isuni_dx: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 → - ∀f. f2 ⊚ 𝐔❴i1❵ ≡ f → 𝐔❴i2❵ ⊚ ⫱*[i2] f2 ≡ f. +lemma after_uni_dx: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 → + ∀f. f2 ⊚ 𝐔❴i1❵ ≡ f → 𝐔❴i2❵ ⊚ ⫱*[i2] f2 ≡ f. #i2 elim i2 -i2 [ #i1 #f2 #Hf2 #f #Hf elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct @@ -420,8 +420,8 @@ lemma after_isuni_dx: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 → ] qed. -lemma after_isuni_sn: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 → - ∀f. 𝐔❴i2❵ ⊚ ⫱*[i2] f2 ≡ f → f2 ⊚ 𝐔❴i1❵ ≡ f. +lemma after_uni_sn: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 → + ∀f. 𝐔❴i2❵ ⊚ ⫱*[i2] f2 ≡ f → f2 ⊚ 𝐔❴i1❵ ≡ f. #i2 elim i2 -i2 [ #i1 #f2 #Hf2 #f #Hf elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct