From: Ferruccio Guidi Date: Wed, 25 May 2016 12:12:25 +0000 (+0000) Subject: initial support for lfpx_drops ... X-Git-Tag: make_still_working~575 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=199ba569adf94f9948053352c2c0a1c6deb62bc5 initial support for lfpx_drops ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma new file mode 100644 index 000000000..8edb998d2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma @@ -0,0 +1,192 @@ +(**************************************************************************) +(* ___ *) +(* ||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_pushs.ma". +include "basic_2/relocation/drops.ma". +include "basic_2/static/frees.ma". + +(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) + +(* Advanced properties ******************************************************) + +lemma drops_atom_F: ∀f. ⬇*[Ⓕ, f] ⋆ ≡ ⋆. +#f @drops_atom #H destruct +qed. + +lemma frees_inv_lref_drops: ∀i,f,L. L ⊢ 𝐅*⦃#i⦄ ≡ f → + (⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ ∧ 𝐈⦃f⦄) ∨ + ∃∃g,I,K,V. K ⊢ 𝐅*⦃V⦄ ≡ g & + ⬇*[i] L ≡ K.ⓑ{I}V & f = ↑*[i] ⫯g. +#i elim i -i +[ #f #L #H elim (frees_inv_zero … H) -H * + /4 width=7 by ex3_4_intro, or_introl, or_intror, conj, drops_refl/ +| #i #IH #f #L #H elim (frees_inv_lref … H) -H * /3 width=1 by or_introl, conj/ + #g #I #K #V #Hg #H1 #H2 destruct + elim (IH … Hg) -IH -Hg * + [ /4 width=3 by or_introl, conj, isid_push, drops_drop/ + | /4 width=7 by drops_drop, ex3_4_intro, or_intror/ + ] +] +qed-. + + + +lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i). +#L #U @(f2_ind … rfw … L U) -L -U +#x #IH #L * * +[ -IH /3 width=5 by frees_inv_sort, or_intror/ +| #j #Hx #l #i elim (ylt_split_eq i j) #Hji + [ -x @or_intror #H elim (ylt_yle_false … Hji) + lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by ylt_fwd_le/ + | -x /2 width=1 by or_introl/ + | elim (ylt_split j l) #Hli + [ -x @or_intror #H elim (ylt_yle_false … Hji) + lapply (frees_inv_lref_skip … H ?) -L // + | elim (lt_or_ge j (|L|)) #Hj + [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct + elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW + @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l + lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/ + | -x @or_intror #H elim (ylt_yle_false … Hji) + lapply (frees_inv_lref_free … H ?) -l // + ] + ] + ] +| -IH /3 width=5 by frees_inv_gref, or_intror/ +| #a #I #W #U #Hx #l #i destruct + elim (IH L W … l i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW + elim (IH (L.ⓑ{I}W) U … (⫯l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU + @or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/ +| #I #W #U #Hx #l #i destruct + elim (IH L W … l i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW + elim (IH L U … l i) -IH [1,3: /3 width=1 by frees_flat_dx, or_introl/ ] #HnU + @or_intror #H elim (frees_inv_flat … H) -H /2 width=1 by/ +] +qed-. + +lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W → + (K ⊢ ⫰(i-l) ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄. +#L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/ +* #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0 +lapply (yle_inv_inj … Hlj) -Hlj #Hlj +elim (le_to_or_lt_eq … Hlj) -Hlj +[ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/ +| -Hji -HnU #H destruct + lapply (drop_mono … HLK0 … HLK) #H destruct -I + elim HnW0 -L -U -HnW0 // +] +qed. + +(* Note: lemma 1250 *) +lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ → + L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄. +#a #I #L #W #U #i #HU elim (frees_dec L W 0 i) +/4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/ +qed. + +(* Properties on relocation *************************************************) + +lemma frees_lift_ge: ∀K,T,l,i. K ⊢ i ϵ𝐅*[l]⦃T⦄ → + ∀L,s,l0,m0. ⬇[s, l0, m0] L ≡ K → + ∀U. ⬆[l0, m0] T ≡ U → l0 ≤ i → + L ⊢ i+m0 ϵ 𝐅*[l]⦃U⦄. +#K #T #l #i #H elim H -K -T -l -i +[ #K #T #l #i #HnT #L #s #l0 #m0 #_ #U #HTU #Hl0i -K -s + @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/ +| #I #K #K0 #T #V #l #i #j #Hlj #Hji #HnT #HK0 #HV #IHV #L #s #l0 #m0 #HLK #U #HTU #Hl0i + elim (ylt_split j l0) #H0 + [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 >yminus_SO2 #HLK0 #HVW + @(frees_be … HL0) -HL0 -HV /3 width=3 by ylt_plus_dx2_trans/ + [ lapply (ylt_fwd_lt_O1 … H0) #H1 + #X #HXU <(ymax_pre_sn l0 1) in HTU; /2 width=1 by ylt_fwd_le_succ1/ #HTU + <(ylt_inv_O1 l0) in H0; // -H1 #H0 + elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by ylt_fwd_succ2/ + | >yplus_minus_comm_inj /2 width=1 by ylt_fwd_le/ + commutative_plus -HLK0 #HLK0 + @(frees_be … HLK0) -HLK0 -IHV + /2 width=1 by monotonic_ylt_plus_dx, yle_plus_dx1_trans/ + [ #X yplus_pred1 /2 width=1 by ylt_to_minus/ + ymax_pre_sn /2 width=2 by/ +| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hlm0i + elim (ylt_split j l0) #H1 + [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW + elim (yle_inv_plus_inj2 … Hlm0i) #H0 #Hm0i + @(frees_be … H) -H + [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/ + | /2 width=3 by ylt_yle_trans/ + | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by ylt_fwd_le_succ1/ + | lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s + >yplus_pred1 /2 width=1 by ylt_to_minus/ + minus_minus_associative /2 width=1 by ylt_inv_inj/ yminus_SO2 >yplus_pred2 /2 width=1 by ylt_fwd_le_pred2/ + ] + | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0 + elim ( yle_inv_plus_inj2 … H2) -H2 #H2 #Hm0j + @(frees_be … HK0) + [ /2 width=1 by monotonic_yle_minus_dx/ + | /2 width=1 by monotonic_ylt_minus_dx/ + | #X #HXT elim (lift_trans_le … HXT … HTU) -T // + ymax_pre_sn /2 width=2 by/ + | yplus_minus_assoc_comm_inj // + >ymax_pre_sn /3 width=5 by yle_trans, ylt_fwd_le/ + ] + ] + ] +] +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 index 797e4f324..c82690309 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma @@ -19,7 +19,7 @@ include "basic_2/static/frees.ma". (* Advanced properties ******************************************************) -(* Notes: this replaces lemma 1400 concluding the "big tree" theorem *) +(* Note: 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 * diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/liftstar_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/liftstar_2.ma new file mode 100644 index 000000000..8b9ac4da5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/liftstar_2.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 n ] term 46 T )" + non associative with precedence 46 + for @{ 'LiftStar $n $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_pushs.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_pushs.ma new file mode 100644 index 000000000..f64590e7a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_pushs.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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/functions/liftstar_2.ma". +include "ground_2/relocation/rtmap_eq.ma". + +(* RELOCATION MAP ***********************************************************) + +rec definition pushs (f:rtmap) (n:nat) on n: rtmap ≝ match n with +[ O ⇒ f | S m ⇒ ↑(pushs f m) ]. + +interpretation "pushs (rtmap)" 'LiftStar n f = (pushs f n). + +(* Basic properties *********************************************************) + +lemma pushs_O: ∀f. f = ↑*[0] f. +// qed. + +lemma pushs_S: ∀f,n. ↑↑*[n] f = ↑*[⫯n] f. +// qed. + +lemma pushs_eq_repl: ∀n. eq_repl (λf1,f2. ↑*[n] f1 ≗ ↑*[n] f2). +#n elim n -n /3 width=5 by eq_push/ +qed. + +(* Advancedd properties *****************************************************) + +lemma pushs_xn: ∀n,f. ↑*[n] ↑f = ↑*[⫯n] f. +#n elim n -n // +qed. 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 c3291e628..2b4e99109 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 @@ -20,8 +20,8 @@ table { class "green" [ { "multiple relocation" * } { [ { "" * } { - [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )" "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_pushs ( ↑*[?]? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )" "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 ( ∁ ? )" * ]