From: Ferruccio Guidi Date: Sun, 21 Aug 2022 22:43:28 +0000 (+0200) Subject: partial update in delayed_updating X-Git-Tag: make_still_working~43 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b1c5b3370653db6e495bbf6b3799cba592746cdd;p=helm.git partial update in delayed_updating + syntax and substitution components updated + path_head parked and replaced by path_closed + balanced reductions introduced and main theorem proved + minor corrections to notation --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/downarrowright_2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/downarrowright_2.etc new file mode 100644 index 000000000..f086d72e2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/downarrowright_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( ↳[ break term 46 n ] break term 70 p )" + non associative with precedence 70 + for @{ 'DownArrowRight $n $p }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/lift_path_head.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/lift_path_head.etc new file mode 100644 index 000000000..21b70c57a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/lift_path_head.etc @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||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_path.ma". +include "delayed_updating/syntax/path_head.ma". +include "ground/relocation/xap.ma". + +(* LIFT FOR PATH ************************************************************) + +(* Constructions with head for path *****************************************) + +lemma lift_path_head_closed (f) (p) (q) (n): + q = ↳[n]q → + ↳[↑[p●q]f@❨n❩]↑[↑[p]f]q = ↑[↑[p]f]q. +#f #p #q elim q -q +[ #n #H0 + <(eq_inv_path_empty_head … H0) -H0 + nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn nsucc_unfold /2 width=1 by/ + | (IH … Hp Hq) in ⊢ (??%?); -IH -Hp -Hq + (IH … Hp Hq) in ⊢ (??%?); -IH -Hp -Hq // + | (IH … Hp Hq) in ⊢ (??%?); -IH -Hp -Hq // + | (IH … Hp Hq) in ⊢ (??%?); -IH -Hp -Hq // + | (IH … Hp Hq) in ⊢ (??%?); -IH -Hp -Hq // + ] +qed. + +lemma path_head_refl_append_sn (p) (q) (n): + q = ↳[n]q → q = ↳[n](p●q). +#p #q elim q -q +[ #n #Hn <(eq_inv_path_empty_head … Hn) -Hn // +| #l #q #IH #n @(nat_ind_succ … n) -n + [ #Hq | #n #_ cases l [ #k ] ] + [ lapply (eq_inv_path_head_zero_dx … Hq) -Hq #Hq destruct + | Hh in ⊢ (??%?); >path_head_structure_depth structure_L_sn + >H1k in ⊢ (??%?); >path_head_structure_depth list_append_rcons_dx >list_append_assoc + lapply (unwind2_rmap_append_pap_closed f … (p●𝗔◗b) … H1k) -H1k + unwind2_rmap_A_dx + /2 width=1 by tls_unwind2_rmap_closed/ + ] +(* Note: crux of the proof ends *) + | // + | /2 width=2 by ex_intro/ + | // + ] +] +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma new file mode 100644 index 000000000..f23728916 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma index a610cd323..d0dcf4eee 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma @@ -16,7 +16,6 @@ include "delayed_updating/substitution/fsubst.ma". include "delayed_updating/syntax/prototerm_constructors.ma". include "delayed_updating/syntax/prototerm_eq.ma". include "delayed_updating/syntax/path_head.ma". -include "delayed_updating/syntax/path_depth.ma". include "delayed_updating/notation/relations/black_rightarrow_df_3.ma". include "ground/xoa/ex_4_3.ma". 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 71a599326..b60bd708c 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma @@ -24,8 +24,6 @@ include "delayed_updating/substitution/lift_rmap_head.ma". (* Constructions with lift **************************************************) -(* ↑[↑[p◖𝗔◖𝗟]f]q *) - theorem dfr_lift_bi (f) (t1) (t2) (r): t1 ➡𝐝𝐟[r] t2 → ↑[f]t1 ➡𝐝𝐟[↑[f]r] ↑[f]t2. #f #t1 #t2 #r diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma new file mode 100644 index 000000000..b235cb481 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fsubst.ma". +include "delayed_updating/substitution/lift_prototerm.ma". +include "delayed_updating/syntax/prototerm_eq.ma". +include "delayed_updating/syntax/path_head.ma". +include "delayed_updating/syntax/path_balanced.ma". +include "delayed_updating/syntax/path_structure.ma". +include "delayed_updating/notation/relations/black_rightarrow_ibf_3.ma". +include "ground/relocation/tr_uni.ma". +include "ground/arith/nat_rplus.ma". +include "ground/xoa/ex_6_5.ma". + +(* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************) + +(**) (* explicit ninj because we cannot declare the expectd type of k *) +definition ibfr (r): relation2 prototerm prototerm ≝ + λt1,t2. + ∃∃p,b,q,h,k. p●𝗔◗b●𝗟◗q = r & + ⊗b ϵ 𝐁 & b = ↳[h]b & + (𝗟◗q) = ↳[ninj k](𝗟◗q) & r◖𝗱k ϵ t1 & + t1[⋔r←↑[𝐮❨k+h❩](t1⋔(p◖𝗦))] ⇔ t2 +. + +interpretation + "balanced focused reduction with immediate updating (prototerm)" + 'BlackRightArrowIBF t1 r t2 = (ibfr r t1 t2). diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_closed.ma new file mode 100644 index 000000000..b332b841f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_closed.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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_path.ma". +include "delayed_updating/syntax/path_closed.ma". +include "ground/relocation/xap.ma". + +(* LIFT FOR PATH ************************************************************) + +(* Constructions with pcc ***************************************************) + +lemma lift_path_closed (f) (q) (n): + q ϵ 𝐂❨n❩ → ↑[f]q ϵ 𝐂❨↑[q]f@❨n❩❩. +#f #q #n #Hq elim Hq -Hq // +#q #n [ #k ] #_ #IH +/2 width=1 by pcc_d_dx, pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/ +qed. + +lemma lift_path_rmap_closed (f) (p) (q) (n): + q ϵ 𝐂❨n❩ → ↑[↑[p]f]q ϵ 𝐂❨↑[p●q]f@❨n❩❩. +/2 width=1 by lift_path_closed/ +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_head.ma deleted file mode 100644 index 21b70c57a..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_head.ma +++ /dev/null @@ -1,61 +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/substitution/lift_path.ma". -include "delayed_updating/syntax/path_head.ma". -include "ground/relocation/xap.ma". - -(* LIFT FOR PATH ************************************************************) - -(* Constructions with head for path *****************************************) - -lemma lift_path_head_closed (f) (p) (q) (n): - q = ↳[n]q → - ↳[↑[p●q]f@❨n❩]↑[↑[p]f]q = ↑[↑[p]f]q. -#f #p #q elim q -q -[ #n #H0 - <(eq_inv_path_empty_head … H0) -H0 - nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn nsucc_unfold /2 width=1 by/ - | (IH … Hn2) -q1 // +| lapply (pcc_inv_A_dx … Hn2) -Hn2 #Hn2 + <(IH … Hn2) -q1 -n2 // +| lapply (pcc_inv_S_dx … Hn2) -Hn2 #Hn2 + <(IH … Hn2) -q1 -n2 // +] +qed-. + +theorem pcc_inj_L_sn (p1) (p2) (q1) (n): + q1 ϵ 𝐂❨n❩ → ∀q2. q2 ϵ 𝐂❨n❩ → + p1●𝗟◗q1 = p2●𝗟◗q2 → q1 = q2. +#p1 #p2 #q1 #n #Hq1 elim Hq1 -q1 -n +[|*: #q1 #n1 [ #k1 ] #_ #IH ] * // +[1,3,5,7,9,11: #l2 #q2 ] #Hq2 +tr_xap_ninj >(path_head_refl_append p … Hh) in ⊢ (??%?); +>tr_xap_ninj >(path_head_refl_append_sn p … Hh) in ⊢ (??%?); >(unwind2_rmap_head_xap_closed … Hh) -Hh