From: Ferruccio Guidi Date: Mon, 14 Feb 2022 23:23:15 +0000 (+0100) Subject: update in delayed_updating X-Git-Tag: make_still_working~88 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e0c91d8a4422da0b39aca790e5826dc8a617b303;p=helm.git update in delayed_updating + update count for paths + minor additions and corrections --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/circled_times_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/circled_times_1.ma index ac8c482a9..8c39289b5 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/circled_times_1.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/circled_times_1.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( ⊗ term 60 p )" - non associative with precedence 60 +notation "hvbox( ⊗ term 70 p )" + non associative with precedence 70 for @{ 'CircledTimes $p }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_1.ma index 9369e0840..ccd9bef9c 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_1.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_1.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( # break term 90 n )" +notation "hvbox( ⧣ break term 90 n )" non associative with precedence 70 for @{ 'Hash $n }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma index 17fcd8598..84e271530 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma @@ -43,7 +43,7 @@ lemma dfr_lift_bi (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 → @(subset_eq_trans … (lift_fsubst …)) [ tr_compose_push_bi // ] qed. + +(* Advanced constructions with proj_rmap and stream_tls *********************) + +lemma lift_rmap_tls_d_dx (f) (p) (m) (n): + ⇂*[m+n]↑[p]f ≗ ⇂*[m]↑[p◖𝗱n]f. +#f #p #m #n +nrplus_inj_dx +/2 width=1 by tr_tls_compose_uni_dx/ +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_update.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_update.ma new file mode 100644 index 000000000..999b0e188 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_update.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/lift_eq.ma". +include "delayed_updating/syntax/path_update.ma". +include "delayed_updating/syntax/path_depth.ma". +include "ground/lib/stream_eq_eq.ma". + +(* LIFT FOR PATH ***********************************************************) + +(* Constructions with update ***********************************************) + +axiom arith1 (p,q:pnat) (n:nat): + nrplus (pplus p q) n = pplus p (nrplus q n). + +lemma pippo (f) (p) (m:pnat): + ⇂*[ninj (m+⧣p)]f ≗ ⇂*[ninj (m+❘p❘)]↑[p]f. +#f #p @(list_ind_rcons … p) -p [ // ] +#p * [ #n ] #IH #m +[ nsucc_inj // +| // +| // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma index 897773a42..8d514e0d7 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma @@ -24,7 +24,7 @@ include "ground/xoa/ex_5_3.ma". (* BY-DEPTH DELAYED (BDD) TERM **********************************************) inductive bdd: 𝒫❨prototerm❩ ≝ -| bdd_oref: ∀n. bdd (#n) +| bdd_oref: ∀n. bdd (⧣n) | bdd_iref: ∀t,n. bdd t → bdd (𝛗n.t) | bdd_abst: ∀t. bdd t → bdd (𝛌.t) | bdd_appl: ∀u,t. bdd u → bdd t → bdd (@u.t) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma index a85d74ef1..cdf24943a 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma @@ -55,10 +55,10 @@ lemma depth_A_sn (q): ❘q❘ = ❘𝗔◗q❘. lemma depth_S_sn (q): ❘q❘ = ❘𝗦◗q❘. // qed. -(* Advanced constructions with nplus ****************************************) +(* Main constructions *******************************************************) -lemma depth_plus (p1) (p2): - ❘p2❘+❘p1❘ = ❘p1●p2❘. +theorem depth_append (p1) (p2): + ❘p2❘+❘p1❘ = ❘p1●p2❘. #p1 elim p1 -p1 // * [ #n ] #p1 #IH #p2