From f8cbadc01cae834f65cf7e0c8fbb0992434e91ff Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 27 Apr 2022 19:41:11 +0200 Subject: [PATCH] update in delayed updating + new version of lift + corrected and updated notation --- .../functions/black_downtriangle_1.ma | 19 +++++++ .../functions/black_downtriangle_2.ma | 2 +- .../functions/black_righttriangle_1.ma | 19 +++++++ .../notation/functions/flat_1.ma | 19 +++++++ .../lambdadelta/delayed_updating/notes.txt | 4 ++ .../delayed_updating/substitution/lift.ma | 16 +++--- .../substitution/lift_after.ma | 9 +-- .../substitution/lift_constructors.ma | 20 +++---- .../delayed_updating/substitution/lift_eq.ma | 57 ++++++++++++++++--- .../substitution/lift_length.ma | 31 ++++++++++ .../substitution/lift_prototerm_eq.ma | 17 ++++++ .../substitution/lift_structure.ma | 35 ++++++++++++ .../delayed_updating/substitution/lift_uni.ma | 8 +-- 13 files changed, 215 insertions(+), 41 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_1.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_1.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/flat_1.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_length.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_1.ma new file mode 100644 index 000000000..03bfed51c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( ▼ term 70 t )" + non associative with precedence 70 + for @{ 'BlackDownTriangle $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_2.ma index 73cccf605..f1d2a0a78 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_2.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( ▼[ term 46 t1 ] break term 70 t2 )" +notation "hvbox( ▼[ term 46 t1 ] break term 70 t2 )" non associative with precedence 70 for @{ 'BlackDownTriangle $t1 $t2 }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_1.ma new file mode 100644 index 000000000..ee1a07589 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( ▶ term 70 t )" + non associative with precedence 70 + for @{ 'BlackRightTriangle $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/flat_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/flat_1.ma new file mode 100644 index 000000000..5d873910b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/flat_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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( ♭ term 70 p )" + non associative with precedence 70 + for @{ 'Flat $p }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt index d48321729..47d6b3600 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt @@ -9,3 +9,7 @@ lemma pr_pat_after_uni_tls (i2) (i1): . replace.sh . "/substitution/" "/unwind/" . replace.sh . ↑ ▼ + +266D;MUSIC FLAT SIGN;So;0;ON;;;;;N;FLAT;;;; +266E;MUSIC NATURAL SIGN;So;0;ON;;;;;N;NATURAL;;;; +266F;MUSIC SHARP SIGN;Sm;0;ON;;;;;N;SHARP;;;; diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma index a487fcf5a..5865fe6ad 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma @@ -15,8 +15,7 @@ include "delayed_updating/notation/functions/uparrow_4.ma". include "delayed_updating/notation/functions/uparrow_2.ma". include "delayed_updating/syntax/path.ma". -include "ground/relocation/tr_uni.ma". -include "ground/relocation/tr_pap_tls.ma". +include "ground/relocation/tr_id_pap.ma". (* LIFT FOR PATH ***********************************************************) @@ -28,7 +27,7 @@ match p with [ list_empty ⇒ k f (𝐞) | list_lcons l q ⇒ match l with - [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (⇂*[n]f) q + [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (𝐢) q | label_m ⇒ lift_gen (A) (λg,p. k g (𝗺◗p)) f q | label_L ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q | label_A ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q @@ -61,7 +60,7 @@ lemma lift_empty (A) (k) (f): // qed. lemma lift_d_sn (A) (k) (p) (n) (f): - ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), ⇂*[n]f, p❩ = ↑{A}❨k, f, 𝗱n◗p❩. + ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), 𝐢, p❩ = ↑{A}❨k, f, 𝗱n◗p❩. // qed. lemma lift_m_sn (A) (k) (p) (f): @@ -93,7 +92,7 @@ lemma lift_rmap_empty (f): // qed. lemma lift_rmap_d_sn (f) (p) (n): - ↑[p](⇂*[ninj n]f) = ↑[𝗱n◗p]f. + ↑[p]𝐢 = ↑[𝗱n◗p]f. // qed. lemma lift_rmap_m_sn (f) (p): @@ -117,7 +116,8 @@ lemma lift_rmap_S_sn (f) (p): lemma lift_rmap_append (p2) (p1) (f): ↑[p2]↑[p1]f = ↑[p1●p2]f. #p2 #p1 elim p1 -p1 // * [ #n ] #p1 #IH #f // -[ tr_compose_push_bi // -] +#p elim p -p [| * ] // #p #IH #f1 #f2 +tr_compose_push_bi // qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma index 772c837fb..3bd7b43bc 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/substitution/lift_prototerm_id.ma". +include "delayed_updating/substitution/lift_prototerm_eq.ma". include "delayed_updating/substitution/lift_uni.ma". include "delayed_updating/syntax/prototerm_constructors.ma". @@ -24,28 +24,24 @@ lemma lift_iref_bi (t1) (t2) (n): qed. lemma lift_iref_sn (f) (t:prototerm) (n:pnat): - (𝛗f@❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛗n.t). -#f #t #n #p * #q * #r #Hr #H1 #H2 destruct -@(ex2_intro … (𝗱n◗𝗺◗r)) + (𝛗f@❨n❩.t) ⊆ ↑[f](𝛗n.t). +#f #t #n #p * #q #Hq #H0 destruct +@(ex2_intro … (𝗱n◗𝗺◗q)) /2 width=1 by in_comp_iref/ qed-. lemma lift_iref_dx (f) (t) (n:pnat): - ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.↑[⇂*[n]f]t. + ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.t. #f #t #n #p * #q #Hq #H0 destruct elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct -/3 width=1 by in_comp_iref, in_comp_lift_bi/ +/2 width=1 by in_comp_iref/ qed-. lemma lift_iref (f) (t) (n:pnat): - (𝛗f@❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛗n.t). + (𝛗f@❨n❩.t) ⇔ ↑[f](𝛗n.t). /3 width=1 by conj, lift_iref_sn, lift_iref_dx/ qed. lemma lift_iref_uni (t) (m) (n): (𝛗(n+m).t) ⇔ ↑[𝐮❨m❩](𝛗n.t). -#t #m #n -@(subset_eq_trans … (lift_iref …)) -nsucc_pnpred list_length_lcons >list_length_lcons // +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma index fc3fb3fcf..55b271f8b 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma @@ -38,3 +38,20 @@ lemma lift_term_after (f1) (f2) (t): | @subset_equivalence_ext_f1_exteq /2 width=5/ ] qed. + +lemma lift_term_id_sn (t): + t ⊆ ↑[𝐢]t. +#t #p #Hp +>(lift_path_id p) +/2 width=1 by in_comp_lift_bi/ +qed-. + +lemma lift_term_id_dx (t): + ↑[𝐢]t ⊆ t. +#t #p * #q #Hq #H destruct // +qed-. + +lemma lift_term_id (t): + t ⇔ ↑[𝐢]t. +/3 width=2 by lift_term_id_dx, lift_term_id_sn, conj/ +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma new file mode 100644 index 000000000..86a425975 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||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_structure.ma". + +(* LIFT FOR PATH ***********************************************************) + +(* Constructions with structure ********************************************) + +lemma structure_lift (p) (f): + ⊗p = ⊗↑[f]p. +#p elim p -p // +* [ #n ] #p #IH #f // +[ nsucc_pnpred -