From 7008128d354c6e998a87bc2febe9f86ea714869c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 26 Oct 2022 23:42:31 +0200 Subject: [PATCH] update in delayed_updating + balanced reduction with main theorem proved + notation change for lift --- .../etc/balanced/dbfr_lift.etc | 51 ------------------ .../functions/righttrianglearrow_2.ma | 19 +++++++ .../{uparrow_2.ma => uptrianglearrow_2.ma} | 4 +- .../balanced/dbfr.etc => reduction/dbfr.ma} | 2 +- .../dbfr_ibfr.etc => reduction/dbfr_ibfr.ma} | 13 ++--- .../delayed_updating/reduction/dfr_lift.ma | 9 ++-- .../balanced/ibfr.etc => reduction/ibfr.ma} | 4 +- .../delayed_updating/reduction/ifr.ma | 2 +- .../delayed_updating/reduction/ifr_lift.ma | 4 +- .../substitution/fsubst_lift.ma | 6 +-- .../substitution/lift_constructors.ma | 10 ++-- .../substitution/lift_path.ma | 44 ++++++++-------- .../substitution/lift_path_after.ma | 2 +- .../substitution/lift_path_closed.ma | 8 +-- .../substitution/lift_path_eq.ma | 2 +- .../substitution/lift_path_id.ma | 2 +- .../substitution/lift_path_length.ma | 2 +- .../substitution/lift_path_proper.ma | 4 +- .../substitution/lift_path_structure.ma | 4 +- .../substitution/lift_path_uni.ma | 2 +- .../substitution/lift_prototerm.ma | 4 +- .../substitution/lift_prototerm_after.ma | 2 +- .../substitution/lift_prototerm_eq.ma | 12 ++--- .../substitution/lift_prototerm_id.ma | 6 +-- .../substitution/lift_prototerm_proper.ma | 4 +- .../substitution/lift_rmap.ma | 32 ++++++------ .../substitution/lift_rmap_after.ma | 2 +- .../substitution/lift_rmap_closed.ma | 6 +-- .../substitution/lift_rmap_eq.ma | 4 +- .../substitution/lift_rmap_id.ma | 2 +- .../substitution/lift_rmap_pap.ma | 2 +- .../substitution/prelift_label.ma | 26 +++++----- .../substitution/prelift_label_after.ma | 2 +- .../substitution/prelift_label_eq.ma | 2 +- .../substitution/prelift_label_id.ma | 2 +- .../substitution/prelift_rmap.ma | 14 ++--- .../substitution/prelift_rmap_after.ma | 2 +- .../substitution/prelift_rmap_eq.ma | 2 +- .../substitution/prelift_rmap_id.ma | 2 +- .../unwind/preunwind2_rmap_lift.ma | 2 +- .../unwind/unwind2_path_lift.ma | 4 +- .../unwind/unwind2_prototerm_lift.ma | 4 +- .../unwind/unwind2_rmap_closed.ma | 52 +++++++++++++++++-- .../unwind/unwind2_rmap_lift.ma | 4 +- 44 files changed, 195 insertions(+), 193 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_lift.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/righttrianglearrow_2.ma rename matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/{uparrow_2.ma => uptrianglearrow_2.ma} (91%) rename matita/matita/contribs/lambdadelta/delayed_updating/{etc/balanced/dbfr.etc => reduction/dbfr.ma} (95%) rename matita/matita/contribs/lambdadelta/delayed_updating/{etc/balanced/dbfr_ibfr.etc => reduction/dbfr_ibfr.ma} (91%) rename matita/matita/contribs/lambdadelta/delayed_updating/{etc/balanced/ibfr.etc => reduction/ibfr.ma} (91%) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_lift.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_lift.etc deleted file mode 100644 index f23728916..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_lift.etc +++ /dev/null @@ -1,51 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/reduction/dbfr.ma". - -include "delayed_updating/substitution/fsubst_lift.ma". -include "delayed_updating/substitution/fsubst_eq.ma". -include "delayed_updating/substitution/lift_constructors.ma". -include "delayed_updating/substitution/lift_path_head.ma". -include "delayed_updating/substitution/lift_rmap_head.ma". - -(* DELAYED BALANCED FOCUSED REDUCTION ***************************************) - -(* Constructions with lift **************************************************) - -theorem dfr_lift_bi (f) (t1) (t2) (r): - t1 ➡𝐝𝐛𝐟[r] t2 → ↑[f]t1 ➡𝐝𝐛𝐟[↑[f]r] ↑[f]t2. -#f #t1 #t2 #r -* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct -@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)＠⧣❨k❩)) -[ -H1k -Ht1 -Ht2 // -| -Ht1 -Ht2 - lift_path_L_sn - <(lift_path_head_closed … H1k) in ⊢ (??%?); -H1k // -| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1k - list_append_rcons_sn in H1k; #H1k >lift_rmap_A_dx - /2 width=1 by tls_lift_rmap_closed/ -(* Note: crux of the proof ends *) -] -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/righttrianglearrow_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/righttrianglearrow_2.ma new file mode 100644 index 000000000..38019a92d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/righttrianglearrow_2.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( 🠢[ break term 46 t1 ] break term 70 t2 )" + non associative with precedence 70 + for @{ 'RightTriangleArrow $t1 $t2 }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptrianglearrow_2.ma similarity index 91% rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptrianglearrow_2.ma index b3123df7b..e77ff4381 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptrianglearrow_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( ↑[ break term 46 t1 ] break term 70 t2 )" +notation "hvbox( 🠡[ break term 46 t1 ] break term 70 t2 )" non associative with precedence 70 - for @{ 'UpArrow $t1 $t2 }. + for @{ 'UpTriangleArrow $t1 $t2 }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr.etc b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma similarity index 95% rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr.etc rename to matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma index f82db8a73..b9b724633 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr.etc +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma @@ -27,7 +27,7 @@ include "ground/xoa/ex_6_5.ma". definition dbfr (r): relation2 prototerm prototerm ≝ λt1,t2. ∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r & - ⊗b ϵ 𝐁 & b ϵ 𝐂❨m❩ & q ϵ 𝐂❨n❩ & r◖𝗱↑n ϵ t1 & + ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓣ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 & t1[⋔r←𝛕↑(m+n).(t1⋔(p◖𝗦))] ⇔ t2 . diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_ibfr.etc b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma similarity index 91% rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_ibfr.etc rename to matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma index d7c16ca2b..fd62cdd78 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_ibfr.etc +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma @@ -45,11 +45,8 @@ theorem dbfr_des_ibfr (f) (t1) (t2) (r): t1 ϵ 𝐓 → /2 width=2 by path_closed_structure_depth/ | lapply (in_comp_unwind2_path_term f … Ht1) -H0t1 -Hb -Hm -Ht2 -Ht1 list_append_rcons_dx >list_append_assoc - unwind2_rmap_A_dx - /2 width=1 by tls_unwind2_rmap_closed/ + /2 width=2 by tls_succ_plus_unwind2_rmap_append_closed_bLq_dx/ ] -*) (* Note: crux of the proof ends *) | // | /2 width=2 by ex_intro/ diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma index 28b21e5e0..ed5778166 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma @@ -12,24 +12,23 @@ (* *) (**************************************************************************) +include "delayed_updating/reduction/dfr.ma". + include "delayed_updating/substitution/fsubst_lift.ma". include "delayed_updating/substitution/fsubst_eq.ma". include "delayed_updating/substitution/lift_constructors.ma". include "delayed_updating/substitution/lift_path_closed.ma". include "delayed_updating/substitution/lift_rmap_closed.ma". -(**) (* reverse include *) -include "delayed_updating/reduction/dfr.ma". - (* DELAYED FOCUSED REDUCTION ************************************************) (* Constructions with lift **************************************************) theorem dfr_lift_bi (f) (t1) (t2) (r): - t1 ➡𝐝𝐟[r] t2 → ↑[f]t1 ➡𝐝𝐟[↑[f]r] ↑[f]t2. + t1 ➡𝐝𝐟[r] t2 → 🠡[f]t1 ➡𝐝𝐟[🠡[f]r] 🠡[f]t2. #f #t1 #t2 #r * #p #q #n #Hr #Hn #Ht1 #Ht2 destruct -@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)＠§❨n❩)) +@(ex4_3_intro … (🠡[f]p) (🠡[🠢[f](p◖𝗔◖𝗟)]q) (🠢[f](p●𝗔◗𝗟◗q)＠§❨n❩)) [ -Hn -Ht1 -Ht2 // | -Ht1 -Ht2 /2 width=1 by lift_path_rmap_closed_L/ diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/ibfr.etc b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma similarity index 91% rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/ibfr.etc rename to matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma index dfa14ef98..869ad5754 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/ibfr.etc +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma @@ -28,8 +28,8 @@ include "ground/xoa/ex_6_5.ma". definition ibfr (r): relation2 prototerm prototerm ≝ λt1,t2. ∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r & - ⊗b ϵ 𝐁 & b ϵ 𝐂❨m❩ & q ϵ 𝐂❨n❩ & r◖𝗱↑n ϵ t1 & - t1[⋔r←↑[𝐮❨↑(m+n)❩](t1⋔(p◖𝗦))] ⇔ t2 + ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓣ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 & + t1[⋔r←🠡[𝐮❨↑(m+n)❩](t1⋔(p◖𝗦))] ⇔ t2 . interpretation diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma index 9bc8d994d..2a6553d9d 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma @@ -26,7 +26,7 @@ definition ifr (r): relation2 prototerm prototerm ≝ λt1,t2. ∃∃p,q,n. p●𝗔◗𝗟◗q = r & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 & - t1[⋔r←↑[𝐮❨↑n❩](t1⋔(p◖𝗦))] ⇔ t2 + t1[⋔r←🠡[𝐮❨↑n❩](t1⋔(p◖𝗦))] ⇔ t2 . interpretation diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma index 365447714..35a00a368 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma @@ -28,10 +28,10 @@ include "ground/relocation/tr_compose_eq.ma". (* Constructions with lift **************************************************) theorem ifr_lift_bi (f) (t1) (t2) (r): - t1 ➡𝐢𝐟[r] t2 → ↑[f]t1 ➡𝐢𝐟[↑[f]r] ↑[f]t2. + t1 ➡𝐢𝐟[r] t2 → 🠡[f]t1 ➡𝐢𝐟[🠡[f]r] 🠡[f]t2. #f #t1 #t2 #r * #p #q #n #Hr #Hn #Ht1 #Ht2 destruct -@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)＠§❨n❩)) +@(ex4_3_intro … (🠡[f]p) (🠡[🠢[f](p◖𝗔◖𝗟)]q) (🠢[f](p●𝗔◗𝗟◗q)＠§❨n❩)) [ -Hn -Ht1 -Ht2 // | -Ht1 -Ht2 /2 width=1 by lift_path_rmap_closed_L/ diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma index 383bc24f9..ad0de7230 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma @@ -20,7 +20,7 @@ include "delayed_updating/substitution/lift_prototerm_eq.ma". (* Constructions with lift for preterm **************************************) lemma lift_term_fsubst_sn (f) (t) (u) (p): - (↑[f]t)[⋔(↑[f]p)←↑[↑[p]f]u] ⊆ ↑[f](t[⋔p←u]). + (🠡[f]t)[⋔(🠡[f]p)←🠡[🠢[f]p]u] ⊆ 🠡[f](t[⋔p←u]). #f #t #u #p #ql * * [ #rl * #r #Hr #H1 #H2 destruct >lift_path_append @@ -32,7 +32,7 @@ lemma lift_term_fsubst_sn (f) (t) (u) (p): qed-. lemma lift_term_fsubst_dx (f) (t) (u) (p): - ↑[f](t[⋔p←u]) ⊆ (↑[f]t)[⋔(↑[f]p)←↑[↑[p]f]u]. + 🠡[f](t[⋔p←u]) ⊆ (🠡[f]t)[⋔(🠡[f]p)←🠡[🠢[f]p]u]. #f #t #u #p #ql * #q * * [ #r #Hu #H1 #H2 destruct @or_introl @ex2_intro @@ -47,5 +47,5 @@ lemma lift_term_fsubst_dx (f) (t) (u) (p): qed-. lemma lift_term_fsubst (f) (t) (u) (p): - (↑[f]t)[⋔(↑[f]p)←↑[↑[p]f]u] ⇔ ↑[f](t[⋔p←u]). + (🠡[f]t)[⋔(🠡[f]p)←🠡[🠢[f]p]u] ⇔ 🠡[f](t[⋔p←u]). /3 width=1 by lift_term_fsubst_sn, conj, lift_term_fsubst_dx/ 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 f263e2d14..56f7b178a 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma @@ -20,14 +20,14 @@ include "ground/relocation/nap.ma". (* LIFT FOR PROTOTERM *******************************************************) lemma lift_term_iref_pap_sn (f) (t:prototerm) (k:pnat): - (𝛕f＠⧣❨k❩.↑[⇂*[k]f]t) ⊆ ↑[f](𝛕k.t). + (𝛕f＠⧣❨k❩.🠡[⇂*[k]f]t) ⊆ 🠡[f](𝛕k.t). #f #t #k #p * #q * #r #Hr #H1 #H2 destruct @(ex2_intro … (𝗱k◗𝗺◗r)) /2 width=1 by in_comp_iref/ qed-. lemma lift_term_iref_pap_dx (f) (t) (k:pnat): - ↑[f](𝛕k.t) ⊆ 𝛕f＠⧣❨k❩.↑[⇂*[k]f]t. + 🠡[f](𝛕k.t) ⊆ 𝛕f＠⧣❨k❩.🠡[⇂*[k]f]t. #f #t #k #p * #q #Hq #H0 destruct elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct tr_pap_succ_nap // qed. lemma lift_term_iref_uni (t) (n) (k): - (𝛕(k+n).t) ⇔ ↑[𝐮❨n❩](𝛕k.t). + (𝛕(k+n).t) ⇔ 🠡[𝐮❨n❩](𝛕k.t). #t #n #k @(subset_eq_trans … (lift_term_iref_pap …)) nsucc_pnpred lift_rmap_L_dx #Hq1 diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_eq.ma index b9574e479..9de1d40d7 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_eq.ma @@ -21,7 +21,7 @@ include "delayed_updating/substitution/prelift_label_eq.ma". (* Constructions with path_eq ***********************************************) lemma lift_path_eq_repl (p): - stream_eq_repl … (λf1,f2. ↑[f1]p = ↑[f2]p). + stream_eq_repl … (λf1,f2. 🠡[f1]p = 🠡[f2]p). #p elim p -p // #l #p #IH #f1 #f2 #Hf nsucc_pnpred (lift_path_id p) /2 width=1 by in_comp_lift_path_term/ qed-. lemma lift_term_id_dx (t): - ↑[𝐢]t ⊆ t. + 🠡[𝐢]t ⊆ t. #t #p * #q #Hq #H destruct // qed-. lemma lift_term_id (t): - t ⇔ ↑[𝐢]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_prototerm_proper.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_proper.ma index 45d65b3ff..7e7236dbd 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_proper.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_proper.ma @@ -21,7 +21,7 @@ include "delayed_updating/syntax/prototerm_proper.ma". (* Constructions with proper condition for path *****************************) lemma lift_term_proper (f) (t): - t ϵ 𝐏 → ↑[f]t ϵ 𝐏. + t ϵ 𝐏 → 🠡[f]t ϵ 𝐏. #f #t #Ht #p * #q #Hq #H0 destruct @lift_path_proper @Ht -Ht // (**) (* auto fails *) qed. @@ -29,7 +29,7 @@ qed. (* Inversions with proper condition for path ********************************) lemma lift_term_inv_proper (f) (t): - ↑[f]t ϵ 𝐏 → t ϵ 𝐏. + 🠡[f]t ϵ 𝐏 → t ϵ 𝐏. #f #t #Ht #p #Hp @(lift_path_inv_proper f) @Ht -Ht @in_comp_lift_path_term // (**) (* auto fails *) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap.ma index 85f41d489..0e0bbb702 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap.ma @@ -20,72 +20,72 @@ include "delayed_updating/syntax/path.ma". rec definition lift_rmap (f) (p) on p: tr_map ≝ match p with [ list_empty ⇒ f -| list_lcons l q ⇒ ↑[l](lift_rmap f q) +| list_lcons l q ⇒ 🠢[lift_rmap f q]l ]. interpretation "lift (relocation map)" - 'UpArrow p f = (lift_rmap f p). + 'RightTriangleArrow f p = (lift_rmap f p). (* Basic constructions ******************************************************) lemma lift_rmap_empty (f): - f = ↑[𝐞]f. + f = 🠢[f]𝐞. // qed. lemma lift_rmap_rcons (f) (p) (l): - ↑[l]↑[p]f = ↑[p◖l]f. + 🠢[🠢[f]p]l = 🠢[f](p◖l). // qed. lemma lift_rmap_d_dx (f) (p) (k:pnat): - ⇂*[k](↑[p]f) = ↑[p◖𝗱k]f. + ⇂*[k](🠢[f]p) = 🠢[f](p◖𝗱k). // qed. lemma lift_rmap_m_dx (f) (p): - ↑[p]f = ↑[p◖𝗺]f. + 🠢[f]p = 🠢[f](p◖𝗺). // qed. lemma lift_rmap_L_dx (f) (p): - (⫯↑[p]f) = ↑[p◖𝗟]f. + (⫯🠢[f]p) = 🠢[f](p◖𝗟). // qed. lemma lift_rmap_A_dx (f) (p): - ↑[p]f = ↑[p◖𝗔]f. + 🠢[f]p = 🠢[f](p◖𝗔). // qed. lemma lift_rmap_S_dx (f) (p): - ↑[p]f = ↑[p◖𝗦]f. + 🠢[f]p = 🠢[f](p◖𝗦). // qed. (* Constructions with path_append *******************************************) lemma lift_rmap_append (p) (q) (f): - ↑[q]↑[p]f = ↑[p●q]f. + 🠢[🠢[f]p]q = 🠢[f](p●q). #p #q elim q -q // qed. (* Constructions with path_lcons ********************************************) lemma lift_rmap_lcons (f) (p) (l): - ↑[p]↑[l]f = ↑[l◗p]f. + 🠢[🠢[f]l]p = 🠢[f](l◗p). // qed. lemma lift_rmap_d_sn (f) (p) (k:pnat): - ↑[p](⇂*[k]f) = ↑[𝗱k◗p]f. + 🠢[⇂*[k]f]p = 🠢[f](𝗱k◗p). // qed. lemma lift_rmap_m_sn (f) (p): - ↑[p]f = ↑[𝗺◗p]f. + 🠢[f]p = 🠢[f](𝗺◗p). // qed. lemma lift_rmap_L_sn (f) (p): - ↑[p](⫯f) = ↑[𝗟◗p]f. + 🠢[⫯f]p = 🠢[f](𝗟◗p). // qed. lemma lift_rmap_A_sn (f) (p): - ↑[p]f = ↑[𝗔◗p]f. + 🠢[f]p = 🠢[f](𝗔◗p). // qed. lemma lift_rmap_S_sn (f) (p): - ↑[p]f = ↑[𝗦◗p]f. + 🠢[f]p = 🠢[f](𝗦◗p). // qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_after.ma index e209f97a7..e3dd359b0 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_after.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_after.ma @@ -20,7 +20,7 @@ include "delayed_updating/substitution/lift_path.ma". (* Constructions with tr_after **********************************************) lemma lift_rmap_after (g) (f) (p:path): - ↑[↑[f]p]g∘↑[p]f = ↑[p](g∘f). + 🠢[g]🠡[f]p∘🠢[f]p = 🠢[g∘f]p. #g #f #p elim p -p // #l #p #IH nrplus_inj_dx >nrplus_inj_sn // qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_id.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_id.ma index 98d4ab395..28eee66dc 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_id.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_id.ma @@ -20,6 +20,6 @@ include "delayed_updating/substitution/prelift_rmap_id.ma". (* Constructions with tr_id *************************************************) lemma lift_rmap_id (p): - (𝐢) = ↑[p]𝐢. + (𝐢) = 🠢[𝐢]p. #p elim p -p // qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_pap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_pap.ma index 6e1b39255..4239d0c44 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_pap.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_pap.ma @@ -20,5 +20,5 @@ include "ground/relocation/tr_pap_tls.ma". (* Constructions with tr_pap ************************************************) lemma lift_rmap_pap_d_dx (f) (p) (k) (h): - ↑[p]f＠⧣❨h+k❩ = ↑[p◖𝗱k]f＠⧣❨h❩+↑[p]f＠⧣❨k❩. + 🠢[f]p＠⧣❨h+k❩ = 🠢[f](p◖𝗱k)＠⧣❨h❩+🠢[f]p＠⧣❨k❩. // qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma index be57d8601..8dc8af8f8 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/notation/functions/uparrow_2.ma". +include "delayed_updating/notation/functions/uptrianglearrow_2.ma". include "delayed_updating/syntax/label.ma". include "ground/relocation/tr_pap_pap.ma". @@ -29,34 +29,34 @@ match l with interpretation "prelift (label)" - 'UpArrow f l = (prelift_label f l). + 'UpTriangleArrow f l = (prelift_label f l). (* Basic constructions ******************************************************) lemma prelift_label_d (f) (k): - (𝗱(f＠⧣❨k❩)) = ↑[f]𝗱k. + (𝗱(f＠⧣❨k❩)) = 🠡[f]𝗱k. // qed. lemma prelift_label_m (f): - (𝗺) = ↑[f]𝗺. + (𝗺) = 🠡[f]𝗺. // qed. lemma prelift_label_L (f): - (𝗟) = ↑[f]𝗟. + (𝗟) = 🠡[f]𝗟. // qed. lemma prelift_label_A (f): - (𝗔) = ↑[f]𝗔. + (𝗔) = 🠡[f]𝗔. // qed. lemma prelift_label_S (f): - (𝗦) = ↑[f]𝗦. + (𝗦) = 🠡[f]𝗦. // qed. (* Basic inversions *********************************************************) lemma prelift_label_inv_d_sn (f) (l) (k1): - (𝗱k1) = ↑[f]l → + (𝗱k1) = 🠡[f]l → ∃∃k2. k1 = f＠⧣❨k2❩ & 𝗱k2 = l. #f * [ #k ] #k1 [ (tr_pap_inj ???? Hk) -Hk // diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label_after.ma index 24720288b..f43f1b647 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label_after.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label_after.ma @@ -20,6 +20,6 @@ include "ground/relocation/tr_compose_pap.ma". (* Constructions with tr_after **********************************************) lemma prelift_label_after (g) (f) (l): - ↑[g]↑[f]l = ↑[g∘f]l. + 🠡[g]🠡[f]l = 🠡[g∘f]l. #g #f * [ #k ] // qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label_eq.ma index bccba6675..be012d6e0 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label_eq.ma @@ -20,7 +20,7 @@ include "ground/relocation/tr_pap_eq.ma". (* constructions with tr_map_eq *********************************************) lemma prelift_label_eq_repl (l): - stream_eq_repl … (λf1,f2. ↑[f1]l = ↑[f2]l). + stream_eq_repl … (λf1,f2. 🠡[f1]l = 🠡[f2]l). * // #k #f1 #f2 #Hf tr_compose_pap @@ -29,7 +29,7 @@ lemma lift_unwind2_path_after (g) (f) (p): qed. lemma unwind2_lift_path_after (g) (f) (p): - ▼[g]↑[f]p = ▼[g∘f]p. + ▼[g]🠡[f]p = ▼[g∘f]p. #g #f * // * [ #k ] #p [ tr_compose_pap diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma index 5b18cfb17..251d7ba72 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma @@ -23,7 +23,7 @@ include "delayed_updating/unwind/unwind2_prototerm.ma". (* Constructions with lift_prototerm ****************************************) lemma lift_unwind2_term_after (f1) (f2) (t): - ↑[f2]▼[f1]t ⇔ ▼[f2∘f1]t. + 🠡[f2]▼[f1]t ⇔ ▼[f2∘f1]t. #f1 #f2 #t @subset_eq_trans [| @subset_inclusion_ext_f1_compose ] @subset_equivalence_ext_f1_exteq #p @@ -31,7 +31,7 @@ lemma lift_unwind2_term_after (f1) (f2) (t): qed. lemma unwind2_lift_term_after (f1) (f2) (t): - ▼[f2]↑[f1]t ⇔ ▼[f2∘f1]t. + ▼[f2]🠡[f1]t ⇔ ▼[f2∘f1]t. #f1 #f2 #t @subset_eq_trans [| @subset_inclusion_ext_f1_compose ] @subset_equivalence_ext_f1_exteq #p diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma index 9dbc9ec50..0afdb349d 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma @@ -16,6 +16,7 @@ include "delayed_updating/unwind/unwind2_rmap_eq.ma". include "delayed_updating/syntax/path_closed.ma". include "delayed_updating/syntax/path_depth.ma". include "ground/relocation/xap.ma". +include "ground/lib/stream_tls_plus.ma". include "ground/lib/stream_eq_eq.ma". include "ground/arith/nat_le_plus.ma". include "ground/arith/nat_le_pred.ma". @@ -74,15 +75,32 @@ lemma unwind2_rmap_append_closed_Lq_dx_nap_depth (o) (f) (p) (q) (n): /2 width=2 by unwind2_rmap_push_closed_nap/ qed-. +lemma unwind2_rmap_append_closed_true_dx_xap_depth (f) (p) (q) (n): + q ϵ 𝐂❨Ⓣ,n❩ → ♭q = ▶[f](p●q)＠❨n❩. +#f #p #q #n #Hq elim Hq -q -n // +#q #n #k #Ho #_ #IH +Ho // nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold // -| nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold // +qed-. + +lemma tls_plus_unwind2_rmap_closed_true (f) (q) (n): + q ϵ 𝐂❨Ⓣ,n❩ → + ∀m. ⇂*[m]f ≗ ⇂*[m+n]▶[f]q. +#f #q #n #Hq elim Hq -q -n // +#q #n #k #Ho #_ #IH #m +>Ho // nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold +>nplus_succ_dx (unwind2_rmap_append_closed_true_dx_xap_depth f p … Hb) -Hb +>(unwind2_rmap_append_closed_Lq_dx_nap_plus … Hq) -Hq // +qed-. + +lemma tls_succ_plus_unwind2_rmap_append_closed_bLq_dx (o) (f) (p) (b) (q) (m) (n): + b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ → + ▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●b●𝗟◗q). +#o #f #p #b #q #m #n #Hb #Hq +>nplus_succ_dx