From 503500ff9a6d9cca363a42b5fe7f3f5de69239f9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 28 Dec 2021 00:38:37 +0100 Subject: [PATCH] update in delayed_updating + updated notation for lists + WIP on lift --- .../delayed_updating/etc/path_etc.etc | 35 ++++++++ .../{comma_2.ma => black_halfcircleleft_2.ma} | 6 +- ...icolon_2.ma => black_halfcircleright_2.ma} | 4 +- .../functions/uparrow_2.ma} | 19 +---- .../notation/functions/uparrow_4.ma | 27 ++++++ .../notation/relations/black_rightarrow_4.ma | 19 +++++ .../delayed_updating/reduction/dfr.ma | 15 ++-- .../delayed_updating/substitution/fsubst.ma | 4 +- .../delayed_updating/substitution/lift.ma | 82 +++++++++++++++++++ .../delayed_updating/syntax/bdd_term.ma | 28 +++---- .../delayed_updating/syntax/path.ma | 12 +-- .../delayed_updating/syntax/path_balanced.ma | 6 +- .../delayed_updating/syntax/path_structure.ma | 6 +- .../delayed_updating/syntax/preterm.ma | 4 +- .../syntax/preterm_constructors.ma | 16 ++-- matita/matita/predefined_virtuals.ml | 2 +- 16 files changed, 217 insertions(+), 68 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/path_etc.etc rename matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/{comma_2.ma => black_halfcircleleft_2.ma} (90%) rename matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/{semicolon_2.ma => black_halfcircleright_2.ma} (93%) rename matita/matita/contribs/lambdadelta/delayed_updating/{substitution/path_dephi.ma => notation/functions/uparrow_2.ma} (68%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/path_etc.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/path_etc.etc new file mode 100644 index 000000000..e6a2ce59c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/path_etc.etc @@ -0,0 +1,35 @@ +notation "hvbox( l1 ● break l2 )" + right associative with precedence 47 + for @{ 'DoubleSemicolon $l1 $l2 }. + +notation "hvbox( hd ◗ break tl )" + right associative with precedence 47 + for @{ 'Semicolon $hd $tl }. + +notation "hvbox( hd ◖ break tl )" + left associative with precedence 47 + for @{ 'Comma $hd $tl }. + +lemma tmp1 (l1) (l2) (p): l1 ◗ l2 ◗ p = l1 ◗ (l2 ◗ p). +// qed. + +lemma tmp2 (p) (l1) (l2): p ◖ l1 ◖ l2 = (p ◖ l1) ◖ l2. +// qed. + +lemma tmp3 (p1) (p2) (p3): p1 ● p2 ● p3 = p1 ● (p2 ● p3). +// qed. + +lemma tmp4 (l1) (p) (l2): l1 ◗ p ◖ l2 = l1 ◗ (p ◖ l2). +// qed. + +lemma tmp5 (p1) (l) (p2): p1 ◖ l ● p2 = (p1 ◖ l) ● p2. +// qed. + +lemma tmp6 (p1) (p2) (l): p1 ● p2 ◖ l = p1 ● (p2 ◖ l). +// qed. + +lemma tmp7 (l) (p1) (p2): l ◗ p1 ● p2 = l ◗ (p1 ● p2). +// qed. + +lemma tmp8 (p1) (l) (p2): p1 ● l ◗ p2 = p1 ● (l ◗ p2). +// qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/comma_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_halfcircleleft_2.ma similarity index 90% rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/comma_2.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_halfcircleleft_2.ma index f2f318da5..fe9683834 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/comma_2.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_halfcircleleft_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( hd , break tl )" - right associative with precedence 50 - for @{ 'Comma $hd $tl }. +notation "hvbox( hd ◖ break tl )" + left associative with precedence 47 + for @{ 'BlackHalfCircleLeft $hd $tl }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/semicolon_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_halfcircleright_2.ma similarity index 93% rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/semicolon_2.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_halfcircleright_2.ma index 81c475923..c58a18653 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/semicolon_2.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_halfcircleright_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( hd ; break tl )" +notation "hvbox( hd ◗ break tl )" right associative with precedence 47 - for @{ 'Semicolon $hd $tl }. + for @{ 'BlackHalfCircleRight $hd $tl }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/path_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma similarity index 68% rename from matita/matita/contribs/lambdadelta/delayed_updating/substitution/path_dephi.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma index f51295ecf..ac803abae 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/path_dephi.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma @@ -12,19 +12,8 @@ (* *) (**************************************************************************) -include "ground/relocation/tr_pap.ma". -include "delayed_updating/syntax/path.ma". +(* NOTATION FOR DELAYED UPDATING ********************************************) -(* DEPHI FOR PATH ***********************************************************) - -rec definition path_dephi (f) (p) on p ≝ -match p with -[ list_empty ⇒ 𝐞 -| list_lcons l q ⇒ - match l with - [ label_node_d n ⇒ 𝗱❨f@❨n❩❩;path_dephi f q - | label_edge_L ⇒ 𝗟;path_dephi (𝟏⨮f) q - | label_edge_A ⇒ 𝗔;path_dephi f q - | label_edge_S ⇒ 𝗦;path_dephi f q - ] -]. +notation "hvbox( ↑ [ term 46 t1 ] break term 75 t2 )" + non associative with precedence 75 + for @{ 'UpArrow $t1 $t2 }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma new file mode 100644 index 000000000..e9a85f9a6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 46 k, break term 46 p, break term 46 f ❩ )" + non associative with precedence 75 + for @{ 'UpArrow $S $k $p $f }. + +notation > "hvbox( ↑ ❨ term 46 k, break term 46 p, break term 46 f ❩ )" + non associative with precedence 75 + for @{ 'UpArrow ? $k $p $f }. + +notation > "hvbox( ↑ { term 46 S } ❨ break term 46 k, break term 46 p, break term 46 f ❩ )" + non associative with precedence 75 + for @{ 'UpArrow $S $k $p $f }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma new file mode 100644 index 000000000..8622760f3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.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( t1 ➡ 'd' 'f' [ break term 46 p, break term 46 q ] break term 46 t2 )" + non associative with precedence 45 + for @{ 'BlackRightArrow $t1 $p $q $t2 }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma index f0b3f5f31..724168bdf 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma @@ -16,19 +16,16 @@ include "ground/xoa/ex_3_1.ma". include "delayed_updating/syntax/path_structure.ma". include "delayed_updating/syntax/path_balanced.ma". include "delayed_updating/substitution/fsubst.ma". -(* -include "delayed_updating/notation/functions/pitchforkleftarrow_3.ma". -*) +include "delayed_updating/notation/relations/black_rightarrow_4.ma". (* DELAYED FOCALIZED REDUCTION **********************************************) inductive dfr (p) (q) (t): predicate preterm ≝ | dfr_beta (b) (n): - let r ≝ p;;(𝗔;b;;(𝗟;q,𝗱❨n❩)) in - r ϵ t → ⊓⊗b → dfr p q t (t[⋔r←t⋔p,𝗦]) + let r ≝ p●𝗔◗b●𝗟◗q◖𝗱❨n❩ in + r ϵ t → ⊓⊗b → dfr p q t (t[⋔r←t⋔(p◖𝗦)]) . -(* + interpretation - "focalized substitution (preterm)" - 'PitchforkLeftArrow t p u = (fsubst p u t). -*) + "delayed focalized reduction (preterm)" + 'BlackRightArrow t1 p q t2 = (dfr p q t1 t2). diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma index 0ff05222b..53f18be31 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma @@ -20,8 +20,8 @@ include "delayed_updating/notation/functions/pitchforkleftarrow_3.ma". definition fsubst (p) (u): preterm → preterm ≝ λt,q. - ∨∨ ∃∃r. r ϵ u & p ϵ ▵t & p;;r = q - | ∧∧ q ϵ t & (∀r. p;;r = q → ⊥) + ∨∨ ∃∃r. r ϵ u & p ϵ ▵t & p●r = q + | ∧∧ q ϵ t & (∀r. p●r = q → ⊥) . interpretation diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma new file mode 100644 index 000000000..0b3dc7d5c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma @@ -0,0 +1,82 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tr_compose.ma". +include "ground/relocation/tr_uni.ma". +include "delayed_updating/syntax/path.ma". +include "delayed_updating/notation/functions/uparrow_4.ma". +include "delayed_updating/notation/functions/uparrow_2.ma". + +(* LIFT FOR PATH ***********************************************************) + +(* Note: inner numeric labels are not liftable, so they are removed *) +rec definition lift_gen (A:Type[0]) (k:?→?→A) (p) (f) on p ≝ +match p with +[ list_empty ⇒ k 𝐞 f +| list_lcons l q ⇒ + match l with + [ label_node_d n ⇒ + match q with + [ list_empty ⇒ lift_gen (A) (λp. k (𝗱❨f@❨n❩❩◗p)) q f + | list_lcons _ _ ⇒ lift_gen (A) k q (f∘𝐮❨n❩) + ] + | label_edge_L ⇒ lift_gen (A) (λp. k (𝗟◗p)) q (⫯f) + | label_edge_A ⇒ lift_gen (A) (λp. k (𝗔◗p)) q f + | label_edge_S ⇒ lift_gen (A) (λp. k (𝗦◗p)) q f + ] +]. + +interpretation + "lift (gneric)" + 'UpArrow A k p f = (lift_gen A k p f). + +definition proj_path (p:path) (f:tr_map) ≝ p. + +definition proj_rmap (p:path) (f:tr_map) ≝ f. + +interpretation + "lift (path)" + 'UpArrow f p = (lift_gen ? proj_path p f). + +interpretation + "lift (relocation map)" + 'UpArrow p f = (lift_gen ? proj_rmap p f). + +(* Basic constructions ******************************************************) + +lemma lift_L (A) (k) (p) (f): + ↑❨(λp. k (𝗟◗p)), p, ⫯f❩ = ↑{A}❨k, 𝗟◗p, f❩. +// qed. + +(* Basic constructions with proj_path ***************************************) + +lemma lift_append (p) (f) (q): + q●↑[f]p = ↑❨(λp. proj_path (q●p)), p, f❩. +#p elim p -p +[ // +| #l #p #IH #f #q cases l + [ + | (list_append_rcons_sn ? q) in ⊢ (???(??(λ_.%)??)); + + IH + | // + +(* Constructions with append ************************************************) + +theorem lift_append_A (p2) (p1) (f): + (↑[f]p1)●𝗔◗↑[↑[p1]f]p2 = ↑[f](p1●𝗔◗p2). +#p2 #p1 elim p1 -p1 +[ #f normalize 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 26fb80e56..1f8dfd1b5 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma @@ -39,11 +39,11 @@ interpretation lemma bdd_inv_in_comp_gen: ∀t,p. t ϵ 𝐃𝛗 → p ϵ t → - ∨∨ ∃∃n. #n ⇔ t & 𝗱❨n❩;𝐞 = p - | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t & 𝗱❨n❩;q = p - | ∃∃u,q. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t & 𝗟;q = p - | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t & 𝗔;q = p - | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t & 𝗦;q = p + ∨∨ ∃∃n. #n ⇔ t & 𝗱❨n❩◗𝐞 = p + | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t & 𝗱❨n❩◗q = p + | ∃∃u,q. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t & 𝗟◗q = p + | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t & 𝗔◗q = p + | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t & 𝗦◗q = p . #t #p #H elim H -H [ #n * /3 width=3 by or5_intro0, ex2_intro/ @@ -62,7 +62,7 @@ lemma bdd_inv_in_comp_gen: qed-. lemma bdd_inv_in_comp_d: - ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ t → + ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩◗q ϵ t → ∨∨ ∧∧ #n ⇔ t & 𝐞 = q | ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t . @@ -77,7 +77,7 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq * qed-. lemma bdd_inv_in_root_d: - ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ ▵t → + ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩◗q ϵ ▵t → ∨∨ ∧∧ #n ⇔ t & 𝐞 = q | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛗n.u ⇔ t . @@ -92,7 +92,7 @@ elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq * qed-. lemma bdd_inv_in_comp_L: - ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ t → + ∀t,q. t ϵ 𝐃𝛗 → 𝗟◗q ϵ t → ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t . #t #q #Ht #Hq @@ -106,7 +106,7 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq * qed-. lemma bdd_inv_in_root_L: - ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ ▵t → + ∀t,q. t ϵ 𝐃𝛗 → 𝗟◗q ϵ ▵t → ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛌.u ⇔ t. #t #q #Ht * #r #Hq elim (bdd_inv_in_comp_L … Ht Hq) -Ht -Hq @@ -115,7 +115,7 @@ elim (bdd_inv_in_comp_L … Ht Hq) -Ht -Hq qed-. lemma bdd_inv_in_comp_A: - ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ t → + ∀t,q. t ϵ 𝐃𝛗 → 𝗔◗q ϵ t → ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t . #t #q #Ht #Hq @@ -129,7 +129,7 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq * qed-. lemma bdd_inv_in_root_A: - ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ ▵t → + ∀t,q. t ϵ 𝐃𝛗 → 𝗔◗q ϵ ▵t → ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵u & @v.u ⇔ t . #t #q #Ht * #r #Hq @@ -139,7 +139,7 @@ elim (bdd_inv_in_comp_A … Ht Hq) -Ht -Hq qed-. lemma bdd_inv_in_comp_S: - ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ t → + ∀t,q. t ϵ 𝐃𝛗 → 𝗦◗q ϵ t → ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t . #t #q #Ht #Hq @@ -153,7 +153,7 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq * qed-. lemma bdd_inv_in_root_S: - ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ ▵t → + ∀t,q. t ϵ 𝐃𝛗 → 𝗦◗q ϵ ▵t → ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵v & @v.u ⇔ t . #t #q #Ht * #r #Hq @@ -165,7 +165,7 @@ qed-. (* Advanced inversions ******************************************************) lemma bbd_mono_in_root_d: - ∀l,n,p,t. t ϵ 𝐃𝛗 → p,𝗱❨n❩ ϵ ▵t → p,l ϵ ▵t → 𝗱❨n❩ = l. + ∀l,n,p,t. t ϵ 𝐃𝛗 → p◖𝗱❨n❩ ϵ ▵t → p◖l ϵ ▵t → 𝗱❨n❩ = l. #l #n #p elim p -p [ #t #Ht