From: Ferruccio Guidi Date: Sun, 27 Mar 2016 16:39:33 +0000 (+0000) Subject: - minor corrections X-Git-Tag: make_still_working~622 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=d3636c8688ec08cc39eb7ce6c1918b25bbccc349 - minor corrections - web pages for nasoc_2 and apps_2 are up again --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma index 9039ce783..172f475fa 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma @@ -18,9 +18,9 @@ notation "hvbox( T . break ④ { term 46 I } break { term 46 T1 , break term 46 non associative with precedence 50 for @{ 'DxItem4 $T $I $T1 $T2 $T3 }. -notation "hvbox( ↑ [ term 46 d , break term 46 e ] break term 46 T )" +notation "hvbox( ↑* [ term 46 f ] break term 46 T )" non associative with precedence 46 - for @{ 'Lift $d $e $T }. + for @{ 'LiftStar $f $T }. notation "hvbox( T1 ⇨ break term 46 T2 )" non associative with precedence 45 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 deleted file mode 100644 index 4f5f26fc9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.etc +++ /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/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma new file mode 100644 index 000000000..aa2e587d8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma @@ -0,0 +1,141 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "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) /2 width=1 by length_pair/ +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 destruct +| #K1 #I1 #V1 #IH * + [ #L1 #L2 #_ >length_atom >length_pair + #H destruct + | #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 /2 width=1 by 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 >plus_n_Sm + #H elim (plus_xSy_x_false … H) +| #K1 #I1 #V1 #IH * + [ #L1 #L2 >append_pair >append_atom #H destruct + >length_pair >append_length >plus_n_Sm #H + lapply (discr_plus_x_xy … H) -H #H destruct + | #K2 #I2 #V2 #L1 #L2 >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_succ_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_succ_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 @(f_ind … length … L) -L #x #IHx * // -IH1 +#L #I #V #H destruct elim (lpair_ltail L I V) /4 width=1 by/ +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 1dbfd8f64..d33d4b452 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma @@ -29,14 +29,14 @@ interpretation "application to vector (term)" (* Basic properties *********************************************************) -lemma applv_nil: ∀T. Ⓐ ◊.T = T. +lemma applv_nil: ∀T. Ⓐ◊.T = T. // qed. -lemma applv_cons: ∀V,Vs,T. Ⓐ V@Vs.T = ⓐV.ⒶVs.T. +lemma applv_cons: ∀V,Vs,T. ⒶV@Vs.T = ⓐV.ⒶVs.T. // qed. -(* properties concerning simple terms ***************************************) +(* Properties with simple terms *********************************************) -lemma applv_simple: ∀T,Vs. 𝐒⦃T⦄ → 𝐒⦃ⒶVs.T⦄. +lemma applv_simple: ∀T,Vs. 𝐒⦃T⦄ → 𝐒⦃ⒶVs.T⦄. #T * // qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index 09d381cd8..1fc24f51e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -12,11 +12,12 @@ (* *) (**************************************************************************) +include "ground_2/relocation/rtmap_isfin.ma". include "basic_2/notation/relations/rdropstar_4.ma". include "basic_2/relocation/lreq.ma". include "basic_2/relocation/lifts.ma". -(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) +(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) (* Basic_1: includes: drop_skip_bind drop1_skip_bind *) (* Basic_2A1: includes: drop_atom drop_pair drop_drop drop_skip @@ -203,6 +204,13 @@ qed-. 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-. +(* forward lemmas with test for finite colength *****************************) + +lemma drops_fwd_isfin: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐅⦃f⦄. +#L1 #L2 #f #H elim H -L1 -L2 -f +/3 width=1 by isfin_next, isfin_push, isfin_isid/ +qed-. + (* Basic_2A1: removed theorems 14: drops_inv_nil drops_inv_cons d1_liftable_liftables drop_refl_atom_O2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma index 1e0ae189a..184716b90 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma @@ -14,9 +14,9 @@ include "basic_2/relocation/drops.ma". -(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) +(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) -(* Properties on context sensitive equivalence for terms ********************) +(* Properties with context-sensitive equivalence for terms ******************) lemma ceq_lift: d_liftable2 ceq. /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 8dec08adc..72d63a48a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma @@ -15,7 +15,7 @@ include "basic_2/relocation/lifts_lifts.ma". include "basic_2/relocation/drops_weight.ma". -(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) +(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma index b553a9c69..a5974d9c4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma @@ -12,11 +12,10 @@ (* *) (**************************************************************************) -include "ground_2/relocation/rtmap_isfin.ma". include "basic_2/grammar/lenv_length.ma". include "basic_2/relocation/drops.ma". -(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) +(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) (* Forward lemmas with length for local environments ************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma index f639424f4..9ebd8afe7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma @@ -14,9 +14,9 @@ include "basic_2/relocation/drops.ma". -(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) +(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) -(* Properties on general entrywise extension of context-sensitive relations *) +(* Properties with 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 → 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 cde181037..56f2fbf85 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma @@ -15,9 +15,9 @@ include "basic_2/relocation/drops_ceq.ma". include "basic_2/relocation/drops_lexs.ma". -(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) +(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) -(* Properties on ranged equivalence for local environments ******************) +(* Properties with ranged equivalence for local environments ****************) lemma lreq_dedropable: dedropable_sn lreq. @lexs_liftable_dedropable 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 0b1ef4ff2..411469458 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma @@ -16,9 +16,9 @@ include "ground_2/lib/lstar.ma". include "basic_2/relocation/lreq_lreq.ma". include "basic_2/relocation/drops.ma". -(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) +(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) -(* Properties on reflexive and transitive closure ***************************) +(* Properties with reflexive and transitive closure *************************) (* Basic_2A1: was: d_liftable_LTC *) lemma d2_liftable_LTC: ∀R. d_liftable2 R → d_liftable2 (LTC … R). diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_vector.ma index 9cf6e7c1f..f76942c5d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_vector.ma @@ -15,14 +15,14 @@ include "basic_2/relocation/lifts_vector.ma". include "basic_2/relocation/drops.ma". -(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) +(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) definition d_liftable1_all: relation2 lenv term → predicate bool ≝ λR,c. ∀L,K,f. ⬇*[c, f] L ≡ K → ∀Ts,Us. ⬆*[f] Ts ≡ Us → all … (R K) Ts → all … (R L) Us. -(* Properties on general relocation for term vectors ************************) +(* Properties with generic relocation for term vectors **********************) (* Basic_2A1: was: d1_liftables_liftables_all *) lemma d1_liftable_liftable_all: ∀R,c. d_liftable1 R c → d_liftable1_all R c. 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 2df6d9832..f0c5f355a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma @@ -16,9 +16,9 @@ include "basic_2/grammar/cl_restricted_weight.ma". include "basic_2/relocation/lifts_weight.ma". include "basic_2/relocation/drops.ma". -(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) +(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) -(* Forward lemmas on weight for local environments **************************) +(* Forward lemmas with weight for local environments ************************) (* Basic_2A1: includes: drop_fwd_lw *) lemma drops_fwd_lw: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}. @@ -40,7 +40,7 @@ lemma drops_fwd_lw_lt: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → ] qed-. -(* Forward lemmas on restricted weight for closures *************************) +(* Forward lemmas with restricted weight for closures ***********************) (* Basic_2A1: includes: drop_fwd_rfw *) lemma drops_pair2_fwd_rfw: ∀I,L,K,V,c,f. ⬇*[c, f] L ≡ K.ⓑ{I}V → ∀T. ♯{K, V} < ♯{L, T}. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_lreq.ma index d0231ec6a..a1f7ab05e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_lreq.ma @@ -17,7 +17,7 @@ include "basic_2/relocation/frees.ma". (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) -(* Properties on ranged equivalence for local environments ******************) +(* Properties with ranged equivalence for local environments ****************) lemma frees_lreq_conf: ∀L1,T,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → ∀L2. L1 ≡[f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f. #L1 #T #f #H elim H -L1 -T -f diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/freq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/freq.ma index c9a335348..0f3868536 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/freq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/freq.ma @@ -17,7 +17,7 @@ include "basic_2/grammar/genv.ma". include "basic_2/relocation/frees_weight.ma". include "basic_2/relocation/frees_lreq.ma". -(* LAZY EQUIVALENCE FOR CLOSURES ********************************************) +(* RANGED EQUIVALENCE FOR CLOSURES ******************************************) inductive freq (G) (L1) (T): relation3 genv lenv term ≝ | fleq_intro: ∀L2,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → L1 ≡[f] L2 → freq G L1 T G L2 T diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/freq_freq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/freq_freq.ma index dafa01768..d4d8f76de 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/freq_freq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/freq_freq.ma @@ -16,7 +16,7 @@ include "basic_2/relocation/lreq_lreq.ma". include "basic_2/relocation/frees_frees.ma". include "basic_2/relocation/freq.ma". -(* LAZY EQUIVALENCE FOR CLOSURES *******************************************) +(* RANGED EQUIVALENCE FOR CLOSURES *****************************************) (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index a79a3e4d9..753a62bc5 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 CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) +(* GENERIC 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_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma index 3f40c553c..1654342fd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma @@ -15,9 +15,9 @@ include "basic_2/grammar/lenv_length.ma". include "basic_2/relocation/lexs.ma". -(* GENERAL ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) +(* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) -(* Forward lemmas on length for local environments **************************) +(* Forward lemmas with length for local environments ************************) (* Basic_2A1: includes: lpx_sn_fwd_length *) lemma lexs_fwd_length: ∀RN,RP,L1,L2,f. L1 ⦻*[RN, RP, f] L2 → |L1| = |L2|. 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 a22e62c86..dbe74e5fd 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 CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) +(* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma index df090ce57..c39a162f7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma @@ -17,7 +17,7 @@ include "basic_2/relocation/lifts.ma". (* GENERIC RELOCATION FOR TERMS *********************************************) -(* Forward lemmas on simple terms *******************************************) +(* Forward lemmas with simple terms *****************************************) (* Basic_2A1: includes: lift_simple_dx *) lemma lifts_simple_dx: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma index 3c65cd7b9..5bfb660ae 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma @@ -17,7 +17,7 @@ include "basic_2/relocation/lifts.ma". (* GENERIC RELOCATION FOR TERMS *********************************************) -(* Forward lemmas on weight for terms ***************************************) +(* Forward lemmas with weight for terms *************************************) (* Basic_2A1: includes: lift_fwd_tw *) lemma lifts_fwd_tw: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → ♯{T1} = ♯{T2}. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma index 1b932c460..817360e99 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma @@ -17,7 +17,7 @@ include "basic_2/relocation/lreq.ma". (* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************) -(* Forward lemmas on length for local environments **************************) +(* Forward lemmas with length for local environments ************************) (* Basic_2A1: includes: lreq_fwd_length *) lemma lreq_fwd_length: ∀L1,L2,f. L1 ≡[f] L2 → |L1| = |L2|. 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 fd37f2b13..35da29879 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 @@ -31,10 +31,12 @@ for native type assignment. - Stage "A": "Extending the Applicability Condition" + Stage "A2": "Extending the Applicability Condition" λδ version 2A2 is started. + + Stage "A1": "Extending the Applicability Condition" λδ version 2A1 appears too complex and is dismissed. 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 fe54a52fe..b65bfda55 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 @@ -9,6 +9,7 @@ table { ] } ] +(* class "wine" [ { "examples" * } { [ { "terms with special features" * } { @@ -210,25 +211,7 @@ table { ] } ] - class "yellow" - [ { "multiple substitution" * } { - [ { "lazy equivalence" * } { - [ "fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )" "fleq_fleq" * ] - [ "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_lreq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ] - } - ] - [ { "lazy pointwise extension of a relation" * } { - [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_lreq" + "llpx_sn_drop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ] - } - ] - [ { "pointwise union for local environments" * } { - [ "llor ( ? ⋓[?,?] ? ≡ ? )" "llor_alt" + "llor_drop" * ] - } - ] - [ { "context-sensitive exclusion from free variables" * } { - [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_append" + "frees_lreq" + "frees_lift" * ] - } - ] + [ { "context-sensitive multiple rt-substitution" * } { [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ] } @@ -238,23 +221,18 @@ table { [ "fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_fqup" * ] } ] - [ { "iterated local env. slicing" * } { - [ "drops ( ⬇*[?,?] ? ≡ ? )" "drops_drop" + "drops_drops" * ] - } - ] - [ { "generic term relocation" * } { - [ "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lift_vector" * ] - [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ] + [ { "pointwise union for local environments" * } { + [ "llor ( ? ⋓[?,?] ? ≡ ? )" "llor_alt" + "llor_drop" * ] } ] [ { "support for multiple relocation" * } { [ "mr2 ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" "mr2_mr2" * ] } ] - } - ] - class "orange" - [ { "substitution" * } { + [ { "lazy pointwise extension of a relation" * } { + [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_lreq" + "llpx_sn_drop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ] + } + ] [ { "structural successor for closures" * } { [ "fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )" * ] [ "fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" * ] @@ -276,21 +254,50 @@ table { [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ] } ] - [ { "basic local env. slicing" * } { - [ "drop ( ⬇[?,?,?] ? ≡ ? )" "drop_append" + "drop_lreq" + "drop_drop" * ] + [ "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_lreq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ] +*) + class "yellow" + [ { "relocation" * } { + [ { "ranged equivalence for closures" * } { + [ "freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )" "freq_freq" * ] + } + ] + [ { "context-sensitive free variables" * } { + [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_lreq" + "frees_frees" * ] } ] - [ { "basic term relocation" * } { - [ "lift_vector ( ⬆[?,?] ? ≡ ? )" "lift_lift_vector" * ] - [ "lift ( ⬆[?,?] ? ≡ ? )" "lift_neq" + "lift_lift" * ] + [ { "generic slicing for local environments" * } { + [ "drops_vector ( ⬇*[?,?] ? ≡ ? )" * ] + [ "drops ( ⬇*[?,?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_ceq" + "drops_lexs" + "drops_lreq" + "drops_drops" * ] + } + ] + [ { "generic relocation for terms" * } { + [ "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lift_vector" * ] + [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_lifts" * ] + } + ] + [ { "ranged equivalence for local environments" * } { + [ "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ] + } + ] + [ { "generic entrywise extension of context-sensitive relations for terma" * } { + [ "lexs ( ? ⦻*[?,?,?] ? )" "lexs_length" + "lexs_lexs" * ] + } + ] + } + ] + class "orange" + [ { "" * } { + [ { "" * } { + [ * ] } ] } ] class "red" [ { "grammar" * } { - [ { "equivalence for local environments" * } { - [ "lreq ( ? ⩬[?,?] ? )" "lreq_lreq" * ] + [ { "context-sensitive equivalences for terms" * } { + [ "ceq" "ceq_ceq" * ] } ] [ { "same top term structure" * } {