From 98c91e19a9cc31c77a0151f5df7f7690813cbd07 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 9 Jun 2014 20:38:31 +0000 Subject: [PATCH] advances on append allow to complete the long awaited "big tree" theorem by closing the last comjecure! --- .../basic_2/etc/append/lenv_append.etc | 27 ---- .../basic_2/etc/{top => cpr}/lenv_top.etc | 0 .../lambdadelta/basic_2/etc/llor/llor.etc | 56 -------- .../lambdadelta/basic_2/etc/llor/llor_alt.etc | 66 --------- .../basic_2/etc/llor/lpxs_llor.etc | 125 ------------------ .../basic_2/grammar/lenv_append.ma | 12 ++ .../basic_2/multiple/frees_append.ma | 52 ++++++++ .../multiple/{llor_etc.ma => llor_alt.ma} | 48 +++++-- .../basic_2/multiple/llor_ldrop.ma | 18 ++- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 10 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 12 +- .../lambdadelta/ground_2/lib/arith.ma | 21 +-- 12 files changed, 142 insertions(+), 305 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/append/lenv_append.etc rename matita/matita/contribs/lambdadelta/basic_2/etc/{top => cpr}/lenv_top.etc (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llor/llor.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llor/llor_alt.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llor/lpxs_llor.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/multiple/frees_append.ma rename matita/matita/contribs/lambdadelta/basic_2/multiple/{llor_etc.ma => llor_alt.ma} (52%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/lenv_append.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/lenv_append.etc deleted file mode 100644 index 234c2666b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/append/lenv_append.etc +++ /dev/null @@ -1,27 +0,0 @@ -lemma length_inv_pos_dx_append: ∀d,L. |L| = d + 1 → - ∃∃I,K,V. |K| = d & L = ⋆.ⓑ{I}V @@ K. -#d @(nat_ind_plus … d) -d -[ #L #H - elim (length_inv_pos_dx … H) -H #I #K #V #H - >(length_inv_zero_dx … H) -H #H destruct - @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (**) (* /3/ does not work *) -| #d #IHd #L #H - elim (length_inv_pos_dx … H) -H #I #K #V #H - elim (IHd … H) -IHd -H #I0 #K0 #V0 #H1 #H2 #H3 destruct - @(ex2_3_intro … (K0.ⓑ{I}V)) // -] -qed-. - -lemma length_inv_pos_sn_append: ∀d,L. 1 + d = |L| → - ∃∃I,K,V. d = |K| & L = ⋆. ⓑ{I}V @@ K. -#d >commutative_plus @(nat_ind_plus … d) -d -[ #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct - >(length_inv_zero_sn … H1) -K - @(ex2_3_intro … (⋆)) // (**) (* explicit constructor *) -| #d #IHd #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct - >H1 in IHd; -H1 #IHd - elim (IHd K) -IHd // #J #L #W #H1 #H2 destruct - @(ex2_3_intro … (L.ⓑ{I}V)) // (**) (* explicit constructor *) - >append_length /2 width=1/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/top/lenv_top.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lenv_top.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/top/lenv_top.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lenv_top.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llor/llor.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llor/llor.etc deleted file mode 100644 index 9d0122cca..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/llor/llor.etc +++ /dev/null @@ -1,56 +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/notation/relations/lazyor_4.ma". -include "basic_2/relocation/lpx_sn.ma". -include "basic_2/substitution/cofrees.ma". - -(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) - -inductive clor (T) (L2) (K1) (V1): predicate term ≝ -| clor_sn: |K1| < |L2| → K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → clor T L2 K1 V1 V1 -| clor_dx: ∀I,K2,V2. |K1| < |L2| → (K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) → - ⇩[|L2|-|K1|-1] L2 ≡ K2.ⓑ{I}V2 → clor T L2 K1 V1 V2 -. - -definition llor: relation4 term lenv lenv lenv ≝ - λT,L2. lpx_sn (clor T L2). - -interpretation - "lazy union (local environment)" - 'LazyOr L1 T L2 L = (llor T L2 L1 L). - -(* Basic properties *********************************************************) - -lemma llor_pair_sn: ∀I,L1,L2,L,V,T. L1 ⩖[T] L2 ≡ L → - |L1| < |L2| → L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → - L1.ⓑ{I}V ⩖[T] L2 ≡ L.ⓑ{I}V. -/3 width=2 by clor_sn, lpx_sn_pair/ qed. - -lemma llor_pair_dx: ∀I,J,L1,L2,L,K2,V1,V2,T. L1 ⩖[T] L2 ≡ L → - |L1| < |L2| → (L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) → - ⇩[|L2|-|L1|-1] L2 ≡ K2.ⓑ{J}V2 → - L1.ⓑ{I}V1 ⩖[T] L2 ≡ L.ⓑ{I}V2. -/4 width=3 by clor_dx, lpx_sn_pair/ qed. - -lemma llor_total: ∀T,L2,L1. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L. -#T #L2 #L1 elim L1 -L1 /2 width=2 by ex_intro/ -#L1 #I1 #V1 #IHL1 normalize -#H elim IHL1 -IHL1 /2 width=3 by transitive_le/ -#L #HT elim (cofrees_dec L1 T 0 (|L2|-|L1|-1)) -[ /3 width=2 by llor_pair_sn, ex_intro/ -| elim (ldrop_O1_lt (Ⓕ) L2 (|L2|-|L1|-1)) - /5 width=4 by llor_pair_dx, monotonic_lt_minus_l, ex_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llor/llor_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llor/llor_alt.etc deleted file mode 100644 index b62a00263..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/llor/llor_alt.etc +++ /dev/null @@ -1,66 +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/lpx_sn_alt.ma". -include "basic_2/substitution/llor.ma". - -(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) - -(* Alternative definition ***************************************************) - -theorem llor_intro_alt: ∀T,L2,L1,L. |L1| ≤ |L2| → |L1| = |L| → - (∀I1,I,K1,K,V1,V,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V → - (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → I1 = I ∧ V1 = V) ∧ - (∀I2,K2,V2. (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) → - ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I ∧ V2 = V - ) - ) → L1 ⩖[T] L2 ≡ L. -#T #L2 #L1 #L #HL12 #HL1 #IH @lpx_sn_intro_alt // -HL1 -#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK -lapply (ldrop_fwd_length_minus4 … HLK1) -lapply (ldrop_fwd_length_le4 … HLK1) -normalize in ⊢ (%→%→?); #HKL1 #Hi -lapply (plus_minus_minus_be_aux … HL12 Hi) // -Hi Hi -Hi -elim (IH … HLK1 HLK) -IH #HI1 * -/4 width=5 by or_introl, or_intror, and3_intro, ex4_3_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lpxs_llor.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lpxs_llor.etc deleted file mode 100644 index a94a47791..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lpxs_llor.etc +++ /dev/null @@ -1,125 +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/llor.ma". -include "basic_2/computation/cpxs_lleq.ma". -include "basic_2/computation/lpxs_ldrop.ma". -include "basic_2/computation/lpxs_cpxs.ma". -include "basic_2/computation/lpxs_lpxs.ma". - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -axiom llor_fwd_sort: ∀L1,L2,L,d,k. L1 ⩖ [⋆k, d] L2 ≡ L → L = L2. - -axiom llor_fwd_lref: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → - ∨∨ (|L| ≤ i ∧ L = L2) - | (yinj i < d ∧ L = L2) - | ∃∃I1,I2,K1,K2,K,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 & - ⇩[i] L2 ≡ K2.ⓑ{I2}V2 & - ⇩[i] L ≡ K.ⓑ{I2}V1 & - L2 ≃[yinj 0, yinj i] L & - K1 ⩖[V1, yinj 0] K2 ≡ K & - d ≤ yinj i. - - -axiom llor_fwd_lref_lt: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → i < d → L = L2. - -axiom llor_inv_lref_be: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → d ≤ i → - ∀I1,I2,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∃∃K. ⇩[i] L ≡ K.ⓑ{I2}V1 & L2 ≃[0, i] L & - K1 ⩖[V1, 0] K2 ≡ K. - -axiom llor_fwd_gref: ∀L1,L2,L,d,p. L1 ⩖ [§p, d] L2 ≡ L → L = L2. - -axiom llor_inv_bind: ∀a,I,L1,L2,L,V,T,d. L1 ⩖ [ⓑ{a,I}V.T, d] L2 ≡ L → - ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1.ⓑ{I}V ⩖ [T, ⫯d] L0.ⓑ{I}V ≡ L.ⓑ{I}V. - -axiom llor_inv_flat: ∀I,L1,L2,L,V,T,d. L1 ⩖ [ⓕ{I}V.T, d] L2 ≡ L → - ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1 ⩖ [T, d] L0 ≡ L. - -axiom llor_fwd_length_13: ∀L1,L2,L,T,d. L1 ⩖ [T, d] L2 ≡ L → |L1| = |L|. - -(* Properties obn lazy union for local environments *************************) - -lemma lpxs_llor_sn: ∀h,g,G,L1s,L0,L1d,T,d. L1s ⩖[T, d] L0 ≡ L1d → - ∀L2s,L2d. L2s ⩖[T, d] L0 ≡ L2d → - ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d. -#h #g #G #L1s #L0 #L1d #T #d #H elim H -L1s -L0 -L1d -T -d -[ #L1s #L0 #d #k #_ #L2s #L2d #H #_ >(llor_fwd_sort … H) // -| #L1s #L0 #d #i #_ #Hid #L2s #L2d #H #_ >(llor_fwd_lref_lt … H) // -| #I1s #I0 #L1s #L0 #L1d #K1s #K0 #K1d #V1s #V0 #d #i #Hdi #HLK1s #HLK0 #HLK1d #HL01d #HV1s #IHV1s #L2s #L2d #H #HL12s - elim (lpxs_ldrop_conf … HLK1s … HL12s) -L1s #Y #H #HLK2s - elim (lpxs_inv_pair1 … H) -H #K2s #V2s #HK12s #HV12s #H destruct - elim (llor_inv_lref_be … H … HLK2s HLK0) // -L2s -HLK0 -Hdi #K2d #HLK2d #HL02d #HV2s - lapply (leq_canc_sn … HL01d … HL02d) -L0 #HL12d - lapply (IHV1s … K2d … HK12s) -IHV1s -HK12s [2: #HK12d - - - - -[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d - elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H - elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct - elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct - lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d - lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d - lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s - elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H - lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY - lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H - lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY - >(leq_inv_O_Y … HL2sY) -HL2sY // - - - - - -lemma lleq_lpxs_trans_llor: ∀h,g,G,L1s,L2s,L2d,T,d. L2d ⩖[T, d] L1s ≡ L2s → - ∀L1d. L1s ⋕[T, d] L1d → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s. -#h #g #G #L1s #L2s #L2d #T #d #H elim H -L1s -L2s -L2d -T -d // -[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d - elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H - elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct - elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct - lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d - lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d - lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s - elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H - lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY - lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H - lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY - >(leq_inv_O_Y … HL2sY) -HL2sY // -(* -| #a #I #L2d #L1s #L0 #L2s #V #T #d #H0 #_ #IHV #IHT #L1d #H #HL12d - elim (lleq_inv_bind … H) -H #HV #HT -*) -| #I #L2d #L1s #LV #LT #L2s #V #T #d #H0 #_ #_ #IHV #IHT #IH #L1d #H #HL12d - elim (lleq_inv_flat … H) -H #HV #HT - lapply (IHV … HV HL12d) -HV #H1 - lapply (IHT … HT HL12d) #H2 - - - - @(lpxs_trans … LV) /2 width=3 by/ -IHV - lapply (IHT … HL12d) // -IHT #H @(IH … H) -IH -H - - @(IH … HL12d) -IHT -IHV - - /4 width=5 by lpxs_trans/ - - -lemma lleq_lpx_conf_llor: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 → - ∀K2. K1 ⩖[T, d] L2 ≡ K2 → ⦃G, L2⦄ ⊢ ➡[h, g] K2. -#h #g #G #L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d -[ #L1 #L2 #d #k #HL12 #K1 #HLK1 #K2 #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma index 61b0648b6..3fdb1ad37 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma @@ -108,6 +108,18 @@ lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V. #I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) // qed-. +lemma length_inv_pos_dx_ltail: ∀L,d. |L| = d + 1 → + ∃∃I,K,V. |K| = d & L = ⓑ{I}V.K. +#Y #d #H elim (length_inv_pos_dx … H) -H #I #L #V #Hd #HLK destruct +elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ +qed-. + +lemma length_inv_pos_sn_ltail: ∀L,d. d + 1 = |L| → + ∃∃I,K,V. d = |K| & L = ⓑ{I}V.K. +#Y #d #H elim (length_inv_pos_sn … H) -H #I #L #V #Hd #HLK destruct +elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ +qed-. + (* Basic_eliminators ********************************************************) (* Basic_1: was: c_tail_ind *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_append.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_append.ma new file mode 100644 index 000000000..29894e7b6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_append.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/ldrop_append.ma". +include "basic_2/multiple/frees.ma". + +(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) + +(* Properties on append for local environments ******************************) + +lemma frees_append: ∀L2,U,d,i. L2 ⊢ i ϵ 𝐅*[d]⦃U⦄ → i ≤ |L2| → + ∀L1. L1 @@ L2 ⊢ i ϵ 𝐅*[d]⦃U⦄. +#L2 #U #d #i #H elim H -L2 -U -d -i /3 width=2 by frees_eq/ +#I #L2 #K2 #U #W #d #i #j #Hdj #Hji #HnU #HLK2 #_ #IHW #Hi #L1 +lapply (ldrop_fwd_length_minus2 … HLK2) normalize #H0 +lapply (ldrop_O1_append_sn_le … HLK2 … L1) -HLK2 +[ -I -L1 -K2 -U -W -d /3 width=3 by lt_to_le, lt_to_le_to_lt/ +| #HLK2 @(frees_be … HnU HLK2) // -HnU -HLK2 @IHW -IHW + >(minus_plus_m_m (|K2|) 1) >H0 -H0 /2 width=1 by monotonic_le_minus_l2/ +] +qed. + +(* Inversion lemmas on append for local environments ************************) + +fact frees_inv_append_aux: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ → ∀L1,L2. L = L1 @@ L2 → + i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[d]⦃U⦄. +#L #U #d #i #H elim H -L -U -d -i /3 width=2 by frees_eq/ +#Z #L #Y #U #X #d #i #j #Hdj #Hji #HnU #HLY #_ #IHW #L1 #L2 #H #Hi destruct +elim (ldrop_O1_lt (Ⓕ) L2 j) [2: -Z -Y -L1 -X -U -d /2 width=3 by lt_to_le_to_lt/ ] +#I #K2 #W #HLK2 lapply (ldrop_fwd_length_minus2 … HLK2) normalize #H0 +lapply (ldrop_O1_inv_append1_le … HLY … HLK2) -HLY +[ -Z -I -Y -K2 -L1 -X -U -W -d /3 width=3 by lt_to_le, lt_to_le_to_lt/ +| normalize #H destruct + @(frees_be … HnU HLK2) -HnU -HLK2 // @IHW -IHW // + >(minus_plus_m_m (|K2|) 1) >H0 -H0 /2 width=1 by monotonic_le_minus_l2/ +] +qed-. + +lemma frees_inv_append: ∀L1,L2,U,d,i. L1 @@ L2 ⊢ i ϵ 𝐅*[d]⦃U⦄ → + i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[d]⦃U⦄. +/2 width=4 by frees_inv_append_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_alt.ma similarity index 52% rename from matita/matita/contribs/lambdadelta/basic_2/multiple/llor_etc.ma rename to matita/matita/contribs/lambdadelta/basic_2/multiple/llor_alt.ma index a1a80baa3..430df9936 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_etc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_alt.ma @@ -12,16 +12,14 @@ (* *) (**************************************************************************) -include "basic_2/substitution/ldrop_append.ma". -include "basic_2/multiple/llor_ldrop.ma". +include "basic_2/multiple/frees_append.ma". +include "basic_2/multiple/llor.ma". (* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) -lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y. -/2 width=1 by monotonic_pred/ qed-. +(* Alternative definition ***************************************************) - -lemma llor_tail_frees: ∀L1,L2,L,U,d. L1 ⩖[U, d] L2 ≡ L → d < yinj (|L1|) → +lemma llor_tail_frees: ∀L1,L2,L,U,d. L1 ⩖[U, d] L2 ≡ L → d ≤ yinj (|L1|) → ∀I1,W1. ⓑ{I1}W1.L1 ⊢ |L1| ϵ 𝐅*[d]⦃U⦄ → ∀I2,W2. ⓑ{I1}W1.L1 ⩖[U, d] ⓑ{I2}W2.L2 ≡ ⓑ{I2}W2.L. #L1 #L2 #L #U #d * #HL12 #HL1 #IH #Hd #I1 #W1 #HU #I2 #W2 @@ -31,18 +29,46 @@ lapply (ldrop_fwd_length_lt2 … HLK1) >ltail_length #H lapply (lt_plus_SO_to_le … H) -H #H elim (le_to_or_lt_eq … H) -H #H [ elim (ldrop_O1_lt (Ⓕ) … H) #Z1 #Y1 #X1 #HLY1 - elim (ldrop_O1_lt (Ⓕ) L2 i) [2: /2 width=3 by lt_to_le_to_lt/ ] #Z2 #Y2 #X2 #HLY2 + elim (ldrop_O1_lt (Ⓕ) L2 i) // #Z2 #Y2 #X2 #HLY2 elim (ldrop_O1_lt (Ⓕ) L i) // #Z #Y #X #HLY lapply (ldrop_O1_inv_append1_le … HLK1 … HLY1) /2 width=1 by lt_to_le/ -HLK1 normalize #H destruct - lapply (ldrop_O1_inv_append1_le … HLK2 … HLY2) /3 width=3 by lt_to_le_to_lt, lt_to_le/ -HLK2 normalize #H destruct + lapply (ldrop_O1_inv_append1_le … HLK2 … HLY2) /2 width=1 by lt_to_le/ -HLK2 normalize #H destruct lapply (ldrop_O1_inv_append1_le … HLK … HLY) /2 width=1 by lt_to_le/ -HLK normalize #H destruct elim (IH … HLY1 HLY2 HLY) -IH -HLY1 -HLY2 -HLY * [ /3 width=1 by and3_intro, or3_intro0/ - | #HnU #HZ #HX - | #Hdi #H2U #HZ #HX + | /6 width=2 by frees_inv_append, lt_to_le, or3_intro1, and3_intro/ + | /5 width=1 by frees_append, lt_to_le, or3_intro2, and4_intro/ ] | -IH -HLK1 destruct lapply (ldrop_O1_inv_append1_le … HLK2 … (⋆) ?) // -HLK2 normalize #H destruct lapply (ldrop_O1_inv_append1_le … HLK … (⋆) ?) // -HLK normalize #H destruct - /4 width=1 by ylt_fwd_le, or3_intro2, and4_intro/ + /3 width=1 by or3_intro2, and4_intro/ +] +qed. + +lemma llor_tail_cofrees: ∀L1,L2,L,U,d. L1 ⩖[U, d] L2 ≡ L → + ∀I1,W1. (ⓑ{I1}W1.L1 ⊢ |L1| ϵ 𝐅*[d]⦃U⦄ → ⊥) → + ∀I2,W2. ⓑ{I1}W1.L1 ⩖[U, d] ⓑ{I2}W2.L2 ≡ ⓑ{I1}W1.L. +#L1 #L2 #L #U #d * #HL12 #HL1 #IH #I1 #W1 #HU #I2 #W2 +@and3_intro [1,2: >ltail_length /2 width=1 by le_S_S/ ] +#J1 #J2 #J #K1 #K2 #K #V1 #V2 #V #i #HLK1 #HLK2 #HLK +lapply (ldrop_fwd_length_lt2 … HLK1) >ltail_length #H +lapply (lt_plus_SO_to_le … H) -H #H +elim (le_to_or_lt_eq … H) -H #H +[ elim (ldrop_O1_lt (Ⓕ) … H) #Z1 #Y1 #X1 #HLY1 + elim (ldrop_O1_lt (Ⓕ) L2 i) // #Z2 #Y2 #X2 #HLY2 + elim (ldrop_O1_lt (Ⓕ) L i) // #Z #Y #X #HLY + lapply (ldrop_O1_inv_append1_le … HLK1 … HLY1) /2 width=1 by lt_to_le/ -HLK1 normalize #H destruct + lapply (ldrop_O1_inv_append1_le … HLK2 … HLY2) /2 width=1 by lt_to_le/ -HLK2 normalize #H destruct + lapply (ldrop_O1_inv_append1_le … HLK … HLY) /2 width=1 by lt_to_le/ -HLK normalize #H destruct + elim (IH … HLY1 HLY2 HLY) -IH -HLY1 -HLY2 -HLY * + [ /3 width=1 by and3_intro, or3_intro0/ + | /6 width=2 by frees_inv_append, lt_to_le, or3_intro1, and3_intro/ + | /5 width=1 by frees_append, lt_to_le, or3_intro2, and4_intro/ + ] +| -IH -HLK2 destruct + lapply (ldrop_O1_inv_append1_le … HLK1 … (⋆) ?) // -HLK1 normalize #H destruct + lapply (ldrop_O1_inv_append1_le … HLK … (⋆) ?) // -HLK normalize #H destruct + /4 width=1 by or3_intro1, and3_intro/ ] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma index afc0924d9..5f82638e0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/multiple/frees_lift.ma". -include "basic_2/multiple/llor.ma". +include "basic_2/multiple/llor_alt.ma". (* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) @@ -27,4 +27,18 @@ lapply (ldrop_fwd_length_lt2 … HLK1) -K1 /5 width=3 by ylt_yle_trans, ylt_inj, or3_intro0, and3_intro/ qed. -axiom llor_total: ∀L1,L2,T,d. |L1| = |L2| → ∃L. L1 ⩖[T, d] L2 ≡ L. +lemma llor_total: ∀L1,L2,T,d. |L1| = |L2| → ∃L. L1 ⩖[T, d] L2 ≡ L. +#L1 @(lenv_ind_alt … L1) -L1 +[ #L2 #T #d #H >(length_inv_zero_sn … H) -L2 /2 width=2 by ex_intro/ +| #I1 #L1 #V1 #IHL1 #Y #T #d >ltail_length #H + elim (length_inv_pos_sn_ltail … H) -H #I2 #L2 #V2 #HL12 #H destruct + elim (ylt_split d (|ⓑ{I1}V1.L1|)) + [ elim (frees_dec (ⓑ{I1}V1.L1) T d (|L1|)) #HnU + elim (IHL1 L2 T d) // -IHL1 -HL12 + [ #L #HL12 >ltail_length /4 width=2 by llor_tail_frees, ylt_fwd_succ2, ex_intro/ + | /4 width=2 by llor_tail_cofrees, ex_intro/ + ] + | -IHL1 /4 width=3 by llor_skip, plus_to_minus, ex_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index 02b1b78ac..4ccbf25fc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -32,12 +32,16 @@ for native type assignment. - Closure of native validity - for context-sensitive extended computation. + Preservation of stratified native validity + for "big tree" computation on closures. + + + "Big tree" strong normalization + for simply typed terms. lazy equivalence on local environments - serves as irrelevant step in "big tree" computation + serves as irrelevant step in "big tree" computation on closures (anniversary milestone). diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index ea0a44131..0abb6cb23 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -91,8 +91,8 @@ table { } ] [ { "\"big tree\" parallel computation" * } { - [ "fpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbg" * ] - [ "fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )" "fpbc_fleq" + "fpbc_fpbs" * ] + [ "fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbg" * ] + [ "fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )" "fpbc_fleq" + "fpbc_fpbs" * ] [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_lleq" "fpbu_fleq" * ] [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_aaa" + "fpbs_fpbs" + "fpbs_ext" * ] } @@ -210,8 +210,8 @@ table { class "yellow" [ { "multiple substitution" * } { [ { "lazy equivalence" * } { - [ "fleq ( ⦃?,?,?⦄ ⋕[?] ⦃?,?,?⦄ )" "fleq_fleq" * ] - [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ] + [ "fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )" "fleq_fleq" * ] + [ "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ] } ] [ { "lazy pointwise extension of a relation" * } { @@ -219,11 +219,11 @@ table { } ] [ { "pointwise union for local environments" * } { - [ "llor ( ? ⩖[?,?] ? ≡ ? )" "llor_ldrop" * ] + [ "llor ( ? ⩖[?,?] ? ≡ ? )" "llor_alt" + "llor_ldrop" * ] } ] [ { "context-sensitive exclusion from free variables" * } { - [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_leq" + "frees_lift" * ] + [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_append" + "frees_leq" + "frees_lift" * ] } ] [ { "contxt-sensitive extended multiple substitution" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index dcf7e2de0..1afc42ebc 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -60,6 +60,16 @@ lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z. (* Properties ***************************************************************) +axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2). + +axiom lt_dec: ∀n1,n2. Decidable (n1 < n2). + +lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m. +#m #n elim (lt_or_ge m n) /2 width=1 by or3_intro0/ +#H elim H -m /2 width=1 by or3_intro1/ +#m #Hm * /3 width=1 by not_le_to_lt, le_S_S, or3_intro2/ +qed-. + fact le_repl_sn_conf_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z. // qed-. @@ -94,15 +104,8 @@ qed. (* Inversion & forward lemmas ***********************************************) -axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2). - -axiom lt_dec: ∀n1,n2. Decidable (n1 < n2). - -lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m. -#m #n elim (lt_or_ge m n) /2 width=1 by or3_intro0/ -#H elim H -m /2 width=1 by or3_intro1/ -#m #Hm * /3 width=1 by not_le_to_lt, le_S_S, or3_intro2/ -qed-. +lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y. +/2 width=1 by monotonic_pred/ qed-. lemma lt_refl_false: ∀n. n < n → ⊥. #n #H elim (lt_to_not_eq … H) -H /2 width=1 by/ -- 2.39.2