From 33d0a7a9029859be79b25b5a495e0f30dab11f37 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 29 Oct 2021 20:11:28 +0200 Subject: [PATCH] update in ground + total relocation restarted --- .../ground/etc/relocation/pstream.etc | 2 - .../ground/notation/functions/element_t_1.ma | 19 +++++++++ .../ground/relocation/pr_compose.ma | 2 +- .../ground/relocation/pr_nexts_eq.ma | 23 +++++++++- .../lambdadelta/ground/relocation/tr_eq.ma | 39 +++++++++++++++++ .../lambdadelta/ground/relocation/tr_map.ma | 42 +++++++++++++++++++ .../lambdadelta/ground/relocation/tr_nexts.ma | 30 +++++++++++++ .../tr_pat.ma} | 31 +++++++------- .../lambdadelta/ground/web/ground_src.tbl | 4 ++ 9 files changed, 174 insertions(+), 18 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground/notation/functions/element_t_1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_map.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_nexts.ma rename matita/matita/contribs/lambdadelta/ground/{etc/relocation/pstream_istot.etc => relocation/tr_pat.ma} (82%) 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/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 #_ ] +[ apply_S1 >apply_S1 /3 width=1 by eq_f2/ +>tr_pat_S1 >tr_pat_S1 /3 width=1 by eq_f2/ qed. -lemma apply_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩). +lemma tr_pat_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. +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 - lapply (Hf (𝟏)) >apply_O1 >apply_O1 #H destruct - lapply (Hf (↑i)) >apply_S1 >apply_S1 #H + 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" * ] -- 2.39.2