From aa5c8c99c9f7ae285883cff133fc02b3d064888c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 18 Jan 2023 21:47:29 +0100 Subject: [PATCH] update in delayed_updating + new operator on update functions --- .../delayed_updating/relocation/tr_minus.ma | 40 +++++++++++++++++ .../relocation/tr_minus_eq.ma | 32 ++++++++++++++ .../relocation/tr_minus_pap.ma | 44 +++++++++++++++++++ .../relocation/tr_minus_pn.ma | 35 +++++++++++++++ 4 files changed, 151 insertions(+) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_eq.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pn.ma diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus.ma b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus.ma new file mode 100644 index 000000000..4232017c7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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/arith/pnat_minus.ma". +include "ground/arith/nat_minus.ma". +include "ground/relocation/tr_map.ma". + +(* RIGHT SUBTRACTION FOR TOTAL RELOCATION MAPS ******************************) + +corec definition tr_minus: nat → tr_map → tr_map. +* [ #f @f ] #q * #p #f +@((p-q)⨮(tr_minus (ninj (↑q)-ninj p) f)) +defined. + +interpretation + "right minus (total relocation maps)" + 'minus f n = (tr_minus n f). + +(* Basic constructions ******************************************************) + +lemma tr_minus_zero_dx (f): + f = f - 𝟎 . +* #f #p <(stream_unfold … ((f⨮p)-𝟎)) // +qed. + +lemma tr_minus_cons_inj (f) (p) (q): + (p-q)⨮(f-(ninj (↑q)-ninj p)) = (p⨮f)-(ninj q). +#f #p #q <(stream_unfold … ((p⨮f)-(ninj q))) // +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_eq.ma new file mode 100644 index 000000000..46a7696be --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_eq.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "delayed_updating/relocation/tr_minus.ma". +include "ground/lib/stream_eq.ma". + +(* RIGHT SUBTRACTION FOR TOTAL RELOCATION MAPS ******************************) + +(* Constructions with tr_eq *************************************************) + +corec lemma tr_minus_eq_repl (n): + stream_eq_repl … (λf1,f2. f1-n ≗ f2-n). +cases n -n +[ #f1 #f2 #Hf -tr_minus_eq_repl // +| #q * #p1 #f1 * #p2 #f2 #Hf + cases (stream_eq_inv_cons_bi … Hf) -Hf [|*: // ] * #Hf -p2 + cases tr_minus_cons_inj cases tr_minus_cons_inj + @stream_eq_cons // + @tr_minus_eq_repl // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma new file mode 100644 index 000000000..f27e43c65 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "delayed_updating/relocation/tr_minus_pn.ma". +include "ground/relocation/tr_pap_pn.ma". +include "ground/relocation/tr_pap_lt.ma". +include "ground/arith/nat_rplus_succ.ma". +include "ground/arith/pnat_le.ma". + +(* RIGHT SUBTRACTION FOR TOTAL RELOCATION MAPS ******************************) + +(* Constructions with tr_pap ************************************************) + +lemma tr_pap_minus_le (n) (p) (f): + f＠⧣❨p❩ ≤ p + n → + p = (f-n)＠⧣❨p❩. +#n @(nat_ind_succ … n) -n [| #n #IHn ] +[ #p #f #H1f + lapply (tr_pap_increasing f p) #H2f + >(ple_antisym … H2f H1f) in ⊢ (??%?); -H1f -H2f // +| #p elim p -p [| #p #IHp ] + #f elim (tr_map_split f) * #g #H0 destruct + [ // + |2,4: +