From 3ca651e49d422d9f9a2b793841ae526baf02065c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 30 Jun 2022 00:53:46 +0200 Subject: [PATCH] update in delayed_updating + bind condition simplified for ifr and dfr --- .../delayed_updating/reduction/dfr.ma | 2 +- .../delayed_updating/reduction/dfr_ifr.ma | 13 +++-- .../delayed_updating/reduction/dfr_lift.ma | 5 +- .../delayed_updating/reduction/ifr.ma | 2 +- .../delayed_updating/reduction/ifr_lift.ma | 5 +- .../delayed_updating/reduction/ifr_unwind.ma | 13 +++-- .../substitution/lift_path_head.ma | 29 +++++----- .../substitution/lift_rmap_head.ma | 44 ++++++++------- .../unwind/unwind2_rmap_head.ma | 54 +++++++++---------- 9 files changed, 77 insertions(+), 90 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma index 193136433..e0d17a691 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma @@ -25,7 +25,7 @@ include "delayed_updating/notation/relations/black_rightarrow_df_4.ma". definition dfr (p) (q): relation2 prototerm prototerm ≝ λt1,t2. ∃n:pnat. let r ≝ p●𝗔◗𝗟◗q in - ∧∧ (𝗟◗q)ᴿ = ↳[n](rᴿ) & r◖𝗱n ϵ t1 & + ∧∧ (𝗟◗q)ᴿ = ↳[n](𝗟◗q)ᴿ & r◖𝗱n ϵ t1 & t1[⋔r←𝛕n.(t1⋔(p◖𝗦))] ⇔ t2 . diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma index e54dd2678..2b15d3d52 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma @@ -41,13 +41,12 @@ theorem dfr_des_ifr (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 → @(ex_intro … (↑♭q)) @and3_intro [ -H0t1 -Ht1 -Ht2 >structure_L_sn >structure_reverse - >H1n >path_head_structure_depth H1n in ⊢ (??%?); >path_head_structure_depth list_append_rcons_sn in H1n; (list_append_rcons_sn … p) list_append_rcons_sn in H1n; list_append_rcons_sn unwind2_rmap_A_sn lift_path_L_sn - >list_append_rcons_sn in H1n; list_append_rcons_sn in H1n; #H1n >lift_rmap_A_dx - /2 width=1 by tls_lift_rmap_append_closed/ + /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/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma index 8be4493b7..765387b1c 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma @@ -24,7 +24,7 @@ include "delayed_updating/notation/relations/black_rightarrow_if_4.ma". definition ifr (p) (q): relation2 prototerm prototerm ≝ λt1,t2. ∃n:pnat. let r ≝ p●𝗔◗𝗟◗q in - ∧∧ (𝗟◗q)ᴿ = ↳[n](rᴿ) & r◖𝗱n ϵ t1 & + ∧∧ (𝗟◗q)ᴿ = ↳[n](𝗟◗q)ᴿ & r◖𝗱n ϵ t1 & t1[⋔r←↑[𝐮❨n❩](t1⋔(p◖𝗦))] ⇔ t2 . 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 6eb354905..0bf09b4aa 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma @@ -33,8 +33,7 @@ theorem ifr_lift_bi (f) (p) (q) (t1) (t2): @(ex_intro … ((↑[p●𝗔◗𝗟◗q]f)@⧣❨n❩)) @and3_intro [ -Ht1 -Ht2 lift_path_L_sn - >list_append_rcons_sn in H1n; list_append_rcons_sn in H1n; #H1n >lift_rmap_A_dx - /2 width=1 by tls_lift_rmap_append_closed/ + /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/ifr_unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma index 7d5769887..6a135ea2e 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma @@ -40,13 +40,12 @@ lemma ifr_unwind_bi (f) (p) (q) (t1) (t2): @(ex_intro … (↑♭q)) @and3_intro [ -H1t1 -H2t1 -Ht1 -Ht2 >structure_L_sn >structure_reverse - >H1n >path_head_structure_depth H1n in ⊢ (??%?); >path_head_structure_depth list_append_rcons_sn in H1n; (list_append_rcons_sn … p) list_append_rcons_sn in H1n; list_append_rcons_sn unwind2_rmap_A_sn tr_xap_succ_nap - lift_rmap_append tr_xap_succ_nap - tr_xap_succ_nap - tr_xap_succ_nap - tr_xap_succ_nap - nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn nsucc_unfold /2 width=1 by/ - | (reverse_reverse p) >(reverse_reverse q) +lemma tls_lift_rmap_closed (f) (q) (n): + qᴿ = ↳[n](qᴿ) → + f ≗ ⇂*[n]↑[q]f. +#f #q #n #H0 +>(reverse_reverse q) /2 width=1 by tls_plus_lift_rmap_reverse_closed/ qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma index cd21acf66..f6fbae181 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma @@ -24,38 +24,38 @@ include "ground/arith/nat_le_plus.ma". (* Constructions with path_head *********************************************) lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (k): - p = (↳[n]p)●q → k ≤ n → - (▶[f]p)@❨k❩ = (▶[f]↳[n]p)@❨k❩. + p = ↳[n]p → k ≤ n → + ▶[f](p●q)@❨k❩ = ▶[f]↳[n](p●q)@❨k❩. #f #p elim p -p -[ #q #n #k #Hq #Hk - elim (eq_inv_list_empty_append … Hq) -Hq * #_ // +[ #q #n #k #Hq + <(eq_inv_path_empty_head … Hq) -n #Hk + <(nle_inv_zero_dx … Hk) -k // | #l #p #IH #q #n @(nat_ind_succ … n) -n - [ #k #_ #Hk <(nle_inv_zero_dx … Hk) -k -IH - tr_xap_ninj >Hn in ⊢ (??%?); ->(unwind2_rmap_head_append_xap_closed … Hn) -Hn +>tr_xap_ninj >(path_head_refl_append q … Hn) in ⊢ (??%?); +>(unwind2_rmap_head_xap_closed … Hn) -Hn nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn