From: Ferruccio Guidi Date: Fri, 29 Oct 2021 18:11:28 +0000 (+0200) Subject: update in ground X-Git-Tag: make_still_working~133^2~1 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=33d0a7a9029859be79b25b5a495e0f30dab11f37;hp=835d26af0fdaa835b6aa1b35765cb22fb3590c4b;p=helm.git update in ground + total relocation restarted --- diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc index b641364f7..90626a1d5 100644 --- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc +++ b/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc @@ -18,8 +18,6 @@ include "ground/arith/pnat.ma". (* RELOCATION P-STREAM ******************************************************) -definition gr_map: Type[0] ≝ stream pnat. - definition gr_push: gr_map → gr_map ≝ λf. 𝟏⨮f. interpretation "push (pstream)" 'UpSpoon f = (gr_push f). diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_istot.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_istot.etc deleted file mode 100644 index 584154dfa..000000000 --- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_istot.etc +++ /dev/null @@ -1,122 +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/notation/functions/apply_2.ma". -include "ground/arith/pnat_le_plus.ma". -include "ground/relocation/pstream_eq.ma". -include "ground/relocation/rtmap_istot.ma". - -(* RELOCATION P-STREAM ******************************************************) - -rec definition apply (i: pnat) on i: gr_map → pnat. -* #p #f cases i -i -[ @p -| #i lapply (apply i f) -apply -i -f - #i @(i+p) -] -defined. - -interpretation "functional application (nstream)" - 'Apply f i = (apply i f). - -(* Properties on at (specific) ************************************************) - -lemma at_O1: ∀i2,f. @❪𝟏, i2⨮f❫ ≘ i2. -#i2 elim i2 -i2 /2 width=5 by gr_pat_refl, gr_pat_next/ -qed. - -lemma at_S1: ∀p,f,i1,i2. @❪i1, f❫ ≘ i2 → @❪↑i1, p⨮f❫ ≘ i2+p. -#p elim p -p /3 width=7 by gr_pat_push, gr_pat_next/ -qed. - -lemma at_total: ∀i1,f. @❪i1, f❫ ≘ f@❨i1❩. -#i1 elim i1 -i1 -[ * // | #i #IH * /3 width=1 by at_S1/ ] -qed. - -lemma at_istot: ∀f. 𝐓❪f❫. -/2 width=2 by ex_intro/ qed. - -lemma at_plus2: ∀f,i1,i,p,q. @❪i1, p⨮f❫ ≘ i → @❪i1, (p+q)⨮f❫ ≘ i+q. -#f #i1 #i #p #q #H elim q -q -/2 width=5 by gr_pat_next/ -qed. - -(* Inversion lemmas on at (specific) ******************************************) - -lemma at_inv_O1: ∀f,p,i2. @❪𝟏, p⨮f❫ ≘ i2 → p = i2. -#f #p elim p -p /2 width=6 by gr_pat_inv_unit_push/ -#p #IH #i2 #H elim (gr_pat_inv_next … H) -H [|*: // ] -#j2 #Hj * -i2 /3 width=1 by eq_f/ -qed-. - -lemma at_inv_S1: ∀f,p,j1,i2. @❪↑j1, p⨮f❫ ≘ i2 → - ∃∃j2. @❪j1, f❫ ≘ j2 & j2+p = i2. -#f #p elim p -p /2 width=5 by gr_pat_inv_succ_push/ -#p #IH #j1 #i2 #H elim (gr_pat_inv_next … H) -H [|*: // ] -#j2 #Hj * -i2 elim (IH … Hj) -IH -Hj -#i2 #Hi * -j2 /2 width=3 by ex2_intro/ -qed-. - -lemma at_inv_total: ∀f,i1,i2. @❪i1, f❫ ≘ i2 → f@❨i1❩ = i2. -/2 width=6 by fr2_nat_mono/ qed-. - -(* Forward lemmas on at (specific) *******************************************) - -lemma at_increasing_plus: ∀f,p,i1,i2. @❪i1, p⨮f❫ ≘ i2 → i1 + p ≤ ↑i2. -#f #p * -[ #i2 #H <(at_inv_O1 … H) -i2 // -| #i1 #i2 #H elim (at_inv_S1 … H) -H - #j1 #Ht * -i2 apply_S1 >apply_S1 /3 width=1 by eq_f2/ -qed. - -lemma apply_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩). -* #p #f * // -qed. - -(* Main inversion lemmas ****************************************************) - -theorem apply_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2. -/2 width=4 by gr_pat_inj/ qed-. - -corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2. -* #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons -[ @(Hf (𝟏)) -| @nstream_eq_inv_ext -nstream_eq_inv_ext #i - lapply (Hf (𝟏)) >apply_O1 >apply_O1 #H destruct - lapply (Hf (↑i)) >apply_S1 >apply_S1 #H - /3 width=2 by eq_inv_pplus_bi_dx, eq_inv_psucc_bi/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/element_t_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_t_1.ma new file mode 100644 index 000000000..7e136deb6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_t_1.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 *) +(* *) +(**************************************************************************) + +(* GROUND NOTATION **********************************************************) + +notation "hvbox( 𝐭❨ break term 46 a ❩ )" + non associative with precedence 75 + for @{ 'ElementT $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma index 4cd185f2a..12ce1a69c 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma @@ -28,7 +28,7 @@ interpretation "functional composition (partial relocation maps)" 'compose f2 f1 = (pr_compose f2 f1). -(* Basic constructions (specific) *******************************************) +(* Basic constructions ******************************************************) lemma pr_compose_unfold_refl (f2) (f1): ⫯(f2∘f1) = (⫯f2)∘(⫯f1). #f2 #f1 diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma index ca6a8d5ac..3ca8053d8 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/relocation/pr_eq.ma". +include "ground/relocation/pr_tl_eq.ma". include "ground/relocation/pr_nexts.ma". (* ITERATED NEXT FOR PARTIAL RELOCATION MAPS ********************************) @@ -25,3 +25,24 @@ lemma pr_nexts_eq_repl (n): #n @(nat_ind_succ … n) -n /3 width=5 by pr_eq_next/ qed. + +(* Inversions with pr_eq ****************************************************) + +lemma pr_eq_inv_nexts_push_bi (f1) (f2) (n1) (n2): + ↑*[n1] ⫯f1 ≡ ↑*[n2] ⫯f2 → + ∧∧ n1 = n2 & f1 ≡ f2. +#f1 #f2 +#n1 @(nat_ind_succ … n1) -n1 [| #n1 #IH ] +#n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ] +[ tr_pat_S1 >tr_pat_S1 /3 width=1 by eq_f2/ +qed. + +lemma tr_pat_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩). +* #p #f * // +qed. + +(* Main inversion lemmas ****************************************************) + +theorem tr_pat_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2. +/2 width=4 by gr_pat_inj/ qed-. + +corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2. +* #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons +[ @(Hf (𝟏)) +| @nstream_eq_inv_ext -nstream_eq_inv_ext #i + ltr_pat (Hf (𝟏)) >tr_pat_O1 >tr_pat_O1 #H destruct + ltr_pat (Hf (↑i)) >tr_pat_S1 >tr_pat_S1 #H + /3 width=2 by eq_inv_pplus_bi_dx, eq_inv_psucc_bi/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl index da49c6c48..1aee10f42 100644 --- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl @@ -29,6 +29,10 @@ table { [ "fr2_map ( ◊ ) ( ❨?,?❩;? )" * ] } ] + [ { "total relocation" * } { + [ "tr_map ( 𝐭❨?❩ )" "tr_nexts" "tr_eq" * ] + } + ] [ { "partial relocation" * } { [ "pr_sor ( ? ⋓ ? ≘ ? )" "pr_sor_eq" "pr_sor_tls" "pr_sor_isi" "pr_sor_fcla" "pr_sor_isf" "pr_sor_coafter_ist_isf" "pr_sor_sle" "pr_sor_sor" "pr_sor_sor_sle" * ] [ "pr_sand ( ? ⋒ ? ≘ ? )" "pr_sand_eq" * ]