From: Ferruccio Guidi Date: Wed, 21 Oct 2015 17:05:02 +0000 (+0000) Subject: parked material ... X-Git-Tag: make_still_working~679 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a5548736278a0b63f6f25c2721934ed8a7d2eef8;p=helm.git parked material ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.etc new file mode 100644 index 000000000..4f5f26fc9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.etc @@ -0,0 +1,145 @@ +(**************************************************************************) +(* ___ *) +(* ||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/append_2.ma". +include "ground_2/ynat/ynat_plus.ma". +include "basic_2/notation/functions/snbind2_3.ma". +include "basic_2/notation/functions/snabbr_2.ma". +include "basic_2/notation/functions/snabst_2.ma". +include "basic_2/grammar/lenv_length.ma". + +(* LOCAL ENVIRONMENTS *******************************************************) + +let rec append L K on K ≝ match K with +[ LAtom ⇒ L +| LPair K I V ⇒ (append L K). ⓑ{I} V +]. + +interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2). + +interpretation "local environment tail binding construction (binary)" + 'SnBind2 I T L = (append (LPair LAtom I T) L). + +interpretation "tail abbreviation (local environment)" + 'SnAbbr T L = (append (LPair LAtom Abbr T) L). + +interpretation "tail abstraction (local environment)" + 'SnAbst L T = (append (LPair LAtom Abst T) L). + +definition d_appendable_sn: predicate (lenv→relation term) ≝ λR. + ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2. + +(* Basic properties *********************************************************) + +lemma append_atom: ∀L. L @@ ⋆ = L. +// qed. + +lemma append_pair: ∀I,L,K,V. L @@ (K.ⓑ{I}V) = (L @@ K).ⓑ{I}V. +// qed. + +lemma append_atom_sn: ∀L. ⋆ @@ L = L. +#L elim L -L // +#L #I #V >append_pair // +qed. + +lemma append_assoc: associative … append. +#L1 #L2 #L3 elim L3 -L3 // +qed. + +lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|. +#L1 #L2 elim L2 -L2 // +#L2 #I #V2 >append_pair >length_pair >length_pair // +qed. + +lemma ltail_length: ∀I,L,V. |ⓑ{I}V.L| = ⫯|L|. +#I #L #V >append_length // +qed. + +(* Basic_1: was just: chead_ctail *) +lemma lpair_ltail: ∀L,I,V. ∃∃J,K,W. L.ⓑ{I}V = ⓑ{J}W.K & |L| = |K|. +#L elim L -L /2 width=5 by ex2_3_intro/ +#L #Z #X #IHL #I #V elim (IHL Z X) -IHL +#J #K #W #H #_ >H -H >ltail_length +@(ex2_3_intro … J (K.ⓑ{I}V) W) // +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| → + L1 = L2 ∧ K1 = K2. +#K1 elim K1 -K1 +[ * /2 width=1 by conj/ + #K2 #I2 #V2 #L1 #L2 #_ >length_atom >length_pair + #H elim (ysucc_inv_O_sn … H) +| #K1 #I1 #V1 #IH * + [ #L1 #L2 #_ >length_atom >length_pair + #H elim (ysucc_inv_O_dx … H) + | #K2 #I2 #V2 #L1 #L2 #H1 #H2 + elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *) + elim (IH … H1) -IH -H1 /3 width=1 by ysucc_inv_inj, conj/ + ] +] +qed-. + +(* Note: lemma 750 *) +lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| → + L1 = L2 ∧ K1 = K2. +#K1 elim K1 -K1 +[ * /2 width=1 by conj/ + #K2 #I2 #V2 #L1 #L2 >append_atom >append_pair #H destruct + >length_pair >append_length append_pair >append_atom #H destruct + >length_pair >append_length append_pair >append_pair #H1 #H2 + elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *) + elim (IH … H1) -IH -H1 /2 width=1 by conj/ + ] +] +qed-. + +lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆. +#L #K #H elim (append_inj_dx … (⋆) … H) // +qed-. + +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,l. |L| = ⫯l → + ∃∃I,K,V. |K| = l & L = ⓑ{I}V.K. +#Y #l #H elim (length_inv_pos_dx … H) -H #I #L #V #Hl #HLK destruct +elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ +qed-. + +lemma length_inv_pos_sn_ltail: ∀L,l. ⫯l = |L| → + ∃∃I,K,V. l = |K| & L = ⓑ{I}V.K. +#Y #l #H elim (length_inv_pos_sn … H) -H #I #L #V #Hl #HLK destruct +elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ +qed-. + +(* Basic eliminators ********************************************************) + +(* Basic_1: was: c_tail_ind *) +lemma lenv_ind_alt: ∀R:predicate lenv. + R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) → + ∀L. R L. +#R #IH1 #IH2 #L @(ynat_f_ind … length … L) -L #x #IHx * // -IH1 +#L #I #V #H destruct elim (lpair_ltail L I V) +/4 width=1 by monotonic_ylt_plus_sn/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.ma deleted file mode 100644 index 4f5f26fc9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.ma +++ /dev/null @@ -1,145 +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/notation/functions/append_2.ma". -include "ground_2/ynat/ynat_plus.ma". -include "basic_2/notation/functions/snbind2_3.ma". -include "basic_2/notation/functions/snabbr_2.ma". -include "basic_2/notation/functions/snabst_2.ma". -include "basic_2/grammar/lenv_length.ma". - -(* LOCAL ENVIRONMENTS *******************************************************) - -let rec append L K on K ≝ match K with -[ LAtom ⇒ L -| LPair K I V ⇒ (append L K). ⓑ{I} V -]. - -interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2). - -interpretation "local environment tail binding construction (binary)" - 'SnBind2 I T L = (append (LPair LAtom I T) L). - -interpretation "tail abbreviation (local environment)" - 'SnAbbr T L = (append (LPair LAtom Abbr T) L). - -interpretation "tail abstraction (local environment)" - 'SnAbst L T = (append (LPair LAtom Abst T) L). - -definition d_appendable_sn: predicate (lenv→relation term) ≝ λR. - ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2. - -(* Basic properties *********************************************************) - -lemma append_atom: ∀L. L @@ ⋆ = L. -// qed. - -lemma append_pair: ∀I,L,K,V. L @@ (K.ⓑ{I}V) = (L @@ K).ⓑ{I}V. -// qed. - -lemma append_atom_sn: ∀L. ⋆ @@ L = L. -#L elim L -L // -#L #I #V >append_pair // -qed. - -lemma append_assoc: associative … append. -#L1 #L2 #L3 elim L3 -L3 // -qed. - -lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|. -#L1 #L2 elim L2 -L2 // -#L2 #I #V2 >append_pair >length_pair >length_pair // -qed. - -lemma ltail_length: ∀I,L,V. |ⓑ{I}V.L| = ⫯|L|. -#I #L #V >append_length // -qed. - -(* Basic_1: was just: chead_ctail *) -lemma lpair_ltail: ∀L,I,V. ∃∃J,K,W. L.ⓑ{I}V = ⓑ{J}W.K & |L| = |K|. -#L elim L -L /2 width=5 by ex2_3_intro/ -#L #Z #X #IHL #I #V elim (IHL Z X) -IHL -#J #K #W #H #_ >H -H >ltail_length -@(ex2_3_intro … J (K.ⓑ{I}V) W) // -qed-. - -(* Basic inversion lemmas ***************************************************) - -lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| → - L1 = L2 ∧ K1 = K2. -#K1 elim K1 -K1 -[ * /2 width=1 by conj/ - #K2 #I2 #V2 #L1 #L2 #_ >length_atom >length_pair - #H elim (ysucc_inv_O_sn … H) -| #K1 #I1 #V1 #IH * - [ #L1 #L2 #_ >length_atom >length_pair - #H elim (ysucc_inv_O_dx … H) - | #K2 #I2 #V2 #L1 #L2 #H1 #H2 - elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *) - elim (IH … H1) -IH -H1 /3 width=1 by ysucc_inv_inj, conj/ - ] -] -qed-. - -(* Note: lemma 750 *) -lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| → - L1 = L2 ∧ K1 = K2. -#K1 elim K1 -K1 -[ * /2 width=1 by conj/ - #K2 #I2 #V2 #L1 #L2 >append_atom >append_pair #H destruct - >length_pair >append_length append_pair >append_atom #H destruct - >length_pair >append_length append_pair >append_pair #H1 #H2 - elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *) - elim (IH … H1) -IH -H1 /2 width=1 by conj/ - ] -] -qed-. - -lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆. -#L #K #H elim (append_inj_dx … (⋆) … H) // -qed-. - -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,l. |L| = ⫯l → - ∃∃I,K,V. |K| = l & L = ⓑ{I}V.K. -#Y #l #H elim (length_inv_pos_dx … H) -H #I #L #V #Hl #HLK destruct -elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ -qed-. - -lemma length_inv_pos_sn_ltail: ∀L,l. ⫯l = |L| → - ∃∃I,K,V. l = |K| & L = ⓑ{I}V.K. -#Y #l #H elim (length_inv_pos_sn … H) -H #I #L #V #Hl #HLK destruct -elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ -qed-. - -(* Basic eliminators ********************************************************) - -(* Basic_1: was: c_tail_ind *) -lemma lenv_ind_alt: ∀R:predicate lenv. - R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) → - ∀L. R L. -#R #IH1 #IH2 #L @(ynat_f_ind … length … L) -L #x #IHx * // -IH1 -#L #I #V #H destruct elim (lpair_ltail L I V) -/4 width=1 by monotonic_ylt_plus_sn/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.etc new file mode 100644 index 000000000..7a0cdfc92 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.etc @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lt.ma". +include "basic_2/grammar/lenv.ma". + +(* LENGTH OF A LOCAL ENVIRONMENT ********************************************) + +let rec length L ≝ match L with +[ LAtom ⇒ 0 +| LPair L _ _ ⇒ ⫯(length L) +]. + +interpretation "length (local environment)" 'card L = (length L). + +(* Basic properties *********************************************************) + +lemma length_atom: |⋆| = 0. +// qed. + +lemma length_pair: ∀I,L,V. |L.ⓑ{I}V| = ⫯|L|. +// qed. + +lemma length_inj: ∀L. |L| < ∞. +#L elim L -L /2 width=1 by ylt_succ_Y/ +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma length_inv_zero_dx: ∀L. |L| = 0 → L = ⋆. +* // #L #I #V >length_pair +#H elim (ysucc_inv_O_dx … H) +qed-. + +lemma length_inv_zero_sn: ∀L. yinj 0 = |L| → L = ⋆. +/2 width=1 by length_inv_zero_dx/ qed-. + +lemma length_inv_pos_dx: ∀l,L. |L| = ⫯l → + ∃∃I,K,V. |K| = l & L = K. ⓑ{I}V. +#l * /3 width=5 by ysucc_inj, ex2_3_intro/ +>length_atom #H elim (ysucc_inv_O_sn … H) +qed-. + +lemma length_inv_pos_sn: ∀l,L. ⫯l = |L| → + ∃∃I,K,V. l = |K| & L = K. ⓑ{I}V. +#l #L #H lapply (sym_eq ??? H) -H +#H elim (length_inv_pos_dx … H) -H /2 width=5 by ex2_3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.ma deleted file mode 100644 index 7a0cdfc92..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.ma +++ /dev/null @@ -1,59 +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_lt.ma". -include "basic_2/grammar/lenv.ma". - -(* LENGTH OF A LOCAL ENVIRONMENT ********************************************) - -let rec length L ≝ match L with -[ LAtom ⇒ 0 -| LPair L _ _ ⇒ ⫯(length L) -]. - -interpretation "length (local environment)" 'card L = (length L). - -(* Basic properties *********************************************************) - -lemma length_atom: |⋆| = 0. -// qed. - -lemma length_pair: ∀I,L,V. |L.ⓑ{I}V| = ⫯|L|. -// qed. - -lemma length_inj: ∀L. |L| < ∞. -#L elim L -L /2 width=1 by ylt_succ_Y/ -qed. - -(* Basic inversion lemmas ***************************************************) - -lemma length_inv_zero_dx: ∀L. |L| = 0 → L = ⋆. -* // #L #I #V >length_pair -#H elim (ysucc_inv_O_dx … H) -qed-. - -lemma length_inv_zero_sn: ∀L. yinj 0 = |L| → L = ⋆. -/2 width=1 by length_inv_zero_dx/ qed-. - -lemma length_inv_pos_dx: ∀l,L. |L| = ⫯l → - ∃∃I,K,V. |K| = l & L = K. ⓑ{I}V. -#l * /3 width=5 by ysucc_inj, ex2_3_intro/ ->length_atom #H elim (ysucc_inv_O_sn … H) -qed-. - -lemma length_inv_pos_sn: ∀l,L. ⫯l = |L| → - ∃∃I,K,V. l = |K| & L = K. ⓑ{I}V. -#l #L #H lapply (sym_eq ??? H) -H -#H elim (length_inv_pos_dx … H) -H /2 width=5 by ex2_3_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma index 9575612e0..192b78637 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma @@ -27,6 +27,14 @@ let rec applv Vs T on Vs ≝ interpretation "application to vector (term)" 'SnApplVector Vs T = (applv Vs T). +(* Basic properties *********************************************************) + +lemma applv_nil: ∀T. Ⓐ ◊.T = T. +// qed. + +lemma applv_cons: ∀V,Vs,T. Ⓐ V@Vs.T = ⓐV.ⒶVs.T. +// qed. + (* properties concerning simple terms ***************************************) lemma applv_simple: ∀T,Vs. 𝐒⦃T⦄ → 𝐒⦃ⒶVs.T⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rlift_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rlift_4.ma deleted file mode 100644 index e2a03284e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rlift_4.ma +++ /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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⬆ [ term 46 l , break term 46 m ] break term 46 T1 ≡ break term 46 T2 )" - non associative with precedence 45 - for @{ 'RLift $l $m $T1 $T2 }.