From 2bc0ba993e26ab77a792b38ba39da7a3dd03ad43 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 2 Jan 2022 19:07:48 +0100 Subject: [PATCH] update in delayed updating + some properties of lift --- matita/matita/contribs/lambdadelta/Makefile | 2 +- .../delayed_updating/etc/baruparrow_2.etc | 19 ++++ .../delayed_updating/etc/baruparrow_4.etc | 27 +++++ .../notation/functions/at_2.ma | 2 +- .../notation/functions/lamda_1.ma | 2 +- .../notation/functions/uparrow_2.ma | 2 +- .../notation/functions/uparrow_4.ma | 6 +- .../notation/relations/black_rightarrow_4.ma | 2 +- .../delayed_updating/reduction/dfr.ma | 1 - .../delayed_updating/substitution/lift.ma | 47 ++++----- .../delayed_updating/substitution/lift_eq.ma | 76 ++++++++++++++ .../substitution/lift_structure.ma | 98 +++++++++++++++++++ .../delayed_updating/syntax/path.ma | 4 +- .../delayed_updating/syntax/path_structure.ma | 69 +++++++++++-- .../functions/black_halfcircleleft_2.ma | 2 +- .../functions/black_halfcircleright_2.ma | 2 +- 16 files changed, 319 insertions(+), 42 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_2.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_4.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma rename matita/matita/contribs/lambdadelta/{delayed_updating => ground}/notation/functions/black_halfcircleleft_2.ma (94%) rename matita/matita/contribs/lambdadelta/{delayed_updating => ground}/notation/functions/black_halfcircleright_2.ma (94%) diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index dc13cc156..bee981cbd 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -26,7 +26,7 @@ TAGS := all names xoa orig elim deps top leaf stats tbls odeps trim clean \ pack-ground pack-2a pack-2b \ home up-home \ -PACKAGES := ground basic_2A static_2 basic_2 apps_2 alpha_1 +PACKAGES := ground basic_2A static_2 basic_2 apps_2 alpha_1 delayed_updating LDWS := $(shell find -name "*.ldw.xml") TBLS := $(shell find -name "*.tbl") diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_2.etc new file mode 100644 index 000000000..f6e1cf8ab --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_2.etc @@ -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 46 t1 ] break term 75 t2 )" + non associative with precedence 75 + for @{ 'BarUpArrow $t1 $t2 }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_4.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_4.etc new file mode 100644 index 000000000..425260d8f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_4.etc @@ -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 @{ 'BarUpArrow $S $k $p $f }. + +notation > "hvbox( ↥❨ term 46 k, break term 46 p, break term 46 f ❩ )" + non associative with precedence 75 + for @{ 'BarUpArrow ? $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 @{ 'BarUpArrow $S $k $p $f }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma index e08c4ea27..cf5c8f623 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( @ break term 76 u. break term 75 t )" +notation "hvbox( @ break term 76 u . break term 75 t )" non associative with precedence 75 for @{ 'At $u $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma index 379a9092d..6f8d020a9 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( 𝛌 . break term 75 t )" +notation "hvbox( 𝛌. break term 75 t )" non associative with precedence 75 for @{ 'Lamda $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma index ac803abae..c80ffe09f 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( ↑ [ term 46 t1 ] break term 75 t2 )" +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 index e9a85f9a6..1f35274c9 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma @@ -14,14 +14,14 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation < "hvbox( ↑ ❨ term 46 k, break term 46 p, break term 46 f ❩ )" +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 ❩ )" +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 ❩ )" +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 index 8622760f3..f27fa0bad 100644 --- 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 @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( t1 ➡ 'd' 'f' [ break term 46 p, break term 46 q ] break term 46 t2 )" +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 724168bdf..a99d8ca06 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -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". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma index 0b3dc7d5c..a396beb46 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma @@ -20,8 +20,11 @@ include "delayed_updating/notation/functions/uparrow_2.ma". (* LIFT FOR PATH ***********************************************************) +definition lift_continuation (A:Type[0]) ≝ + path → tr_map → A. + (* Note: inner numeric labels are not liftable, so they are removed *) -rec definition lift_gen (A:Type[0]) (k:?→?→A) (p) (f) on p ≝ +rec definition lift_gen (A:Type[0]) (k:lift_continuation A) (p) (f) on p ≝ match p with [ list_empty ⇒ k 𝐞 f | list_lcons l q ⇒ @@ -55,28 +58,26 @@ interpretation (* Basic constructions ******************************************************) -lemma lift_L (A) (k) (p) (f): +lemma lift_empty (A) (k) (f): + k 𝐞 f = ↑{A}❨k, 𝐞, f❩. +// qed. + +lemma lift_d_empty_sn (A) (k) (n) (f): + ↑❨(λp. k (𝗱❨f@❨n❩❩◗p)), 𝐞, f❩ = ↑{A}❨k, 𝗱❨n❩◗𝐞, f❩. +// qed. + +lemma lift_d_lcons_sn (A) (k) (p) (l) (n) (f): + ↑❨k, l◗p, f∘𝐮❨ninj n❩❩ = ↑{A}❨k, 𝗱❨n❩◗l◗p, f❩. +// qed. + +lemma lift_L_sn (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 +lemma lift_A_sn (A) (k) (p) (f): + ↑❨(λp. k (𝗔◗p)), p, f❩ = ↑{A}❨k, 𝗔◗p, f❩. +// qed. + +lemma lift_S_sn (A) (k) (p) (f): + ↑❨(λp. k (𝗦◗p)), p, f❩ = ↑{A}❨k, 𝗦◗p, f❩. +// qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma new file mode 100644 index 000000000..c0d7dcbf5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma @@ -0,0 +1,76 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". +include "ground/notation/relations/ringeq_3.ma". + +(* LIFT FOR PATH ***********************************************************) + +definition lift_exteq (A): relation2 (lift_continuation A) (lift_continuation A) ≝ + λk1,k2. ∀p,f. k1 p f = k2 p f. + +interpretation + "extensional equivalence (lift continuation)" + 'RingEq A k1 k2 = (lift_exteq A k1 k2). + +(* Constructions with lift_exteq ********************************************) + +lemma lift_eq_repl_sn (A) (p) (k1) (k2) (f): + k1 ≗{A} k2 → ↑❨k1, p, f❩ = ↑❨k2, p, f❩. +#A #p elim p -p +[ #k1 #k2 #f #Hk lift_lcons_alt >lift_append_rcons_sn + lift_lcons_alt >lift_append_rcons_sn + lift_lcons_alt >lift_append_rcons_sn + lift_lcons_alt >lift_append_rcons_sn + lift_lcons_alt