From 632dfd0a57c9951d0efbd769d6f433c4ef68a314 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 18 Dec 2021 23:42:38 +0100 Subject: [PATCH] update in ground + positive application for total relocation maps completed --- .../ground/etc/relocation/pstream.etc | 18 ------- .../lambdadelta/ground/lib/stream_eq.ma | 1 + .../lambdadelta/ground/relocation/tr_ist.ma | 24 +++++++++ .../lambdadelta/ground/relocation/tr_pap.ma | 47 ------------------ .../ground/relocation/tr_pap_eq.ma | 42 ++++++++++++++++ .../ground/relocation/tr_pap_pap.ma | 22 +++++++++ .../ground/relocation/tr_pap_pn.ma | 26 ++++++++++ .../lambdadelta/ground/relocation/tr_pn.ma | 49 +++++++++++++++++++ .../lambdadelta/ground/web/ground_src.tbl | 5 +- 9 files changed, 167 insertions(+), 67 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_ist.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc index cc8863b59..8827703c5 100644 --- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc +++ b/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc @@ -18,24 +18,6 @@ include "ground/arith/pnat.ma". (* RELOCATION P-STREAM ******************************************************) -definition gr_push: gr_map → gr_map ≝ λf. 𝟏⨮f. - -interpretation "push (pstream)" 'UpSpoon f = (gr_push f). - -definition gr_next: gr_map → gr_map. -* #p #f @(↑p⨮f) -defined. - -interpretation "next (pstream)" 'UpArrow f = (gr_next f). - -(* Basic properties *********************************************************) - -lemma gr_push_unfold: ∀f. 𝟏⨮f = ⫯f. -// qed. - -lemma gr_next_unfold: ∀f,p. (↑p)⨮f = ↑(p⨮f). -// qed. - (* Basic inversion lemmas ***************************************************) lemma eq_inv_gr_push_bi: injective ? ? gr_push. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma index 1e1320776..47f441dd0 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma @@ -55,6 +55,7 @@ lemma stream_eq_repl_sym (A) (R): (* Basic inversions *********************************************************) +(*** eq_inv_seq_aux *) lemma stream_eq_inv_cons_bi (A): ∀t1,t2. t1 ≗{A} t2 → ∀u1,u2,b1,b2. b1⨮u1 = t1 → b2⨮u2 = t2 → diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_ist.ma new file mode 100644 index 000000000..e06bdf828 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_ist.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/pr_ist.ma". +include "ground/relocation/tr_pap_pat.ma". + +(* TOTAL RELOCATION MAPS ****************************************************) + +(* Constructions with pr_ist ************************************************) + +(*** at_istot *) +lemma tr_ist (f): 𝐓❨𝐭❨f❩❩. +/2 width=2 by ex_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma index 67231de44..ac2d3fb38 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma @@ -42,50 +42,3 @@ lemma tr_pap_unit (f): lemma tr_pap_succ (f): ∀p,i. f@❨i❩+p = (p⨮f)@❨↑i❩. // qed. -(* -(*** apply_S2 *) -lemma tr_pap_next (f): - ∀i. ↑(f@❨i❩) = (↑f)@❨i❩. -* #p #f * // -qed. - - - -(*** apply_eq_repl *) -lemma apply_eq_repl (i): - ∀f1,f2. f1 ≗ f2 → f1@❨i❩ = f2@❨i❩. - - -(i): pr_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩). -#i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H -elim (eq_inv_seq_aux … H) -H #Hp #Hf // ->apply_S1 >apply_S1 /3 width=1 by eq_f2/ -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-. - -(* -include "ground/relocation/pstream_eq.ma". -*) - -(* -include "ground/relocation/rtmap_istot.ma". - -lemma at_istot: ∀f. 𝐓❨f❩. -/2 width=2 by ex_intro/ qed. -*) -*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma new file mode 100644 index 000000000..0373fbd09 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lib/stream_eq.ma". +include "ground/relocation/tr_pap.ma". + +(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************) + +(* Main constructions with stream_eq ****************************************) + +(* Note: a better statement would be: tr_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩) *) +(*** apply_eq_repl *) +theorem apply_eq_repl (i): + ∀f1,f2. f1 ≗ f2 → f1@❨i❩ = f2@❨i❩. +#i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H +elim (stream_eq_inv_cons_bi … H) -H [1,8: |*: // ] #Hp #Hf // +