From: Ferruccio Guidi Date: Tue, 20 Dec 2022 00:10:07 +0000 (+0100) Subject: update in delayed_updating X-Git-Tag: make_still_working~18 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ea71486fd1aab2eae2bab42729a66ae775c7f248;p=helm.git update in delayed_updating + excess added to closure condition for path + height for path restored --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_closed_height.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_closed_height.etc deleted file mode 100644 index 72b6dead7..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_closed_height.etc +++ /dev/null @@ -1,34 +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/syntax/path_closed.ma". -include "delayed_updating/syntax/path_height.ma". -include "delayed_updating/syntax/path_depth.ma". - -(* CLOSED CONDITION FOR PATH ************************************************) - -(* Destructions with height and depth ***************************************) - -lemma path_closed_des_depth (o) (q) (n): - q ϵ 𝐂❨o,n❩ → ♯q + n = ♭q. -#o #q #n #Hq elim Hq -q -n // -#q #n #_ #IH nplus_succ_dx Ho -Ho // Ho2 // @@ -182,9 +192,9 @@ qed. (* Inversions with path_append **********************************************) -lemma pcc_false_inv_append_bi (x) (m) (n): - x ϵ 𝐂❨Ⓕ,m+n❩ → - ∃∃p,q. p ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & p●q = x. +lemma pcc_false_zero_dx_inv_append_bi (x) (m) (n): + x ϵ 𝐂❨Ⓕ,m+n,𝟎❩ → + ∃∃p,q. p ϵ 𝐂❨Ⓕ,m,𝟎❩ & q ϵ 𝐂❨Ⓕ,n,𝟎❩ & p●q = x. #x #m #n #Hx @(insert_eq_1 … (m+n) … Hx) -Hx #y #Hy generalize in match n; -n @@ -212,39 +222,39 @@ qed-. (* Constructions with path_lcons ********************************************) -lemma pcc_m_sn (o) (q) (n): - q ϵ 𝐂❨o,n❩ → (𝗺◗q) ϵ 𝐂❨o,n❩. -#o #q #n #Hq -lapply (pcc_append_bi (Ⓣ) … (𝐞◖𝗺) … Hq) -Hq +lemma pcc_m_sn (o) (e) (q) (n): + q ϵ 𝐂❨o,n,e❩ → (𝗺◗q) ϵ 𝐂❨o,n,e❩. +#o #e #q #n #Hq +lapply (pcc_append_bi (Ⓣ) … (𝟎) e … (𝐞◖𝗺) … Hq) -Hq /2 width=3 by pcc_m_dx/ qed. -lemma pcc_L_sn (o) (q) (n): - q ϵ 𝐂❨o,n❩ → (𝗟◗q) ϵ 𝐂❨o,↑n❩. -#o #q #n #Hq -lapply (pcc_append_bi (Ⓣ) … (𝐞◖𝗟) … Hq) -Hq +lemma pcc_L_sn (o) (e) (q) (n): + q ϵ 𝐂❨o,n,e❩ → (𝗟◗q) ϵ 𝐂❨o,↑n,e❩. +#o #e #q #n #Hq +lapply (pcc_append_bi (Ⓣ) … (𝟎) e … (𝐞◖𝗟) … Hq) -Hq /2 width=3 by pcc_L_dx/ qed. -lemma pcc_A_sn (o) (q) (n): - q ϵ 𝐂❨o,n❩ → (𝗔◗q) ϵ 𝐂❨o,n❩. -#o #q #n #Hq -lapply (pcc_append_bi (Ⓣ) … (𝐞◖𝗔) … Hq) -Hq +lemma pcc_A_sn (o) (e) (q) (n): + q ϵ 𝐂❨o,n,e❩ → (𝗔◗q) ϵ 𝐂❨o,n,e❩. +#o #e #q #n #Hq +lapply (pcc_append_bi (Ⓣ) … (𝟎) e … (𝐞◖𝗔) … Hq) -Hq /2 width=3 by pcc_A_dx/ qed. -lemma pcc_S_sn (o) (q) (n): - q ϵ 𝐂❨o,n❩ → (𝗦◗q) ϵ 𝐂❨o,n❩. -#o #q #n #Hq -lapply (pcc_append_bi (Ⓣ) … (𝐞◖𝗦) … Hq) -Hq +lemma pcc_S_sn (o) (e) (q) (n): + q ϵ 𝐂❨o,n,e❩ → (𝗦◗q) ϵ 𝐂❨o,n,e❩. +#o #e #q #n #Hq +lapply (pcc_append_bi (Ⓣ) … (𝟎) e … (𝐞◖𝗦) … Hq) -Hq /2 width=3 by pcc_S_dx/ qed. (* Main inversions **********************************************************) -theorem pcc_mono (o1) (o2) (q) (n1): - q ϵ 𝐂❨o1,n1❩ → ∀n2. q ϵ 𝐂❨o2,n2❩ → n1 = n2. -#o1 #o2 #q1 #n1 #Hn1 elim Hn1 -q1 -n1 +theorem pcc_mono (o1) (o2) (e) (q) (n1): + q ϵ 𝐂❨o1,n1,e❩ → ∀n2. q ϵ 𝐂❨o2,n2,e❩ → n1 = n2. +#o1 #o2 #e #q1 #n1 #Hn1 elim Hn1 -q1 -n1 [|*: #q1 #n1 [ #k1 #_ ] #_ #IH ] #n2 #Hn2 [ <(pcc_inv_empty … Hn2) -n2 // | lapply (pcc_des_d_dx … Hn2) -Hn2 #Hn2 @@ -261,15 +271,15 @@ theorem pcc_mono (o1) (o2) (q) (n1): ] qed-. -theorem pcc_inj_L_sn (o1) (o2) (p1) (p2) (q1) (n): - q1 ϵ 𝐂❨o1,n❩ → ∀q2. q2 ϵ 𝐂❨o2,n❩ → +theorem pcc_zero_dx_inj_L_sn (o1) (o2) (p1) (p2) (q1) (n): + q1 ϵ 𝐂❨o1,n,𝟎❩ → ∀q2. q2 ϵ 𝐂❨o2,n,𝟎❩ → p1●𝗟◗q1 = p2●𝗟◗q2 → q1 = q2. #o1 #o2 #p1 #p2 #q1 #n #Hq1 elim Hq1 -q1 -n [|*: #q1 #n1 [ #k1 #_ ] #_ #IH ] * // [1,3,5,7,9,11: #l2 #q2 ] #Hq2 (nplus_zero_dx (♭q)) +<(path_closed_des_depth … Hq) -Hq +(nplus_zero_sn n) @@ -62,7 +62,7 @@ lemma nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n): qed-. lemma tls_succ_plus_unwind2_rmap_push_closed (o) (f) (q) (n): - q ϵ 𝐂❨o,n❩ → + q ϵ 𝐂❨o,n,𝟎❩ → ∀m. ⇂*[m]f ≗ ⇂*[↑(m+n)]▶[⫯f]q. #o #f #q #n #Hn elim Hn -q -n // #q #n #k #_ #_ #IH #m @@ -71,21 +71,21 @@ lemma tls_succ_plus_unwind2_rmap_push_closed (o) (f) (q) (n): qed-. lemma tls_succ_unwind2_rmap_push_closed (o) (f) (q) (n): - q ϵ 𝐂❨o,n❩ → + q ϵ 𝐂❨o,n,𝟎❩ → f ≗ ⇂*[↑n]▶[⫯f]q. #o #f #q #n #Hn /2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/ qed-. lemma tls_succ_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n): - q ϵ 𝐂❨o,n❩ → + q ϵ 𝐂❨o,n,𝟎❩ → ∀m. ⇂*[m]▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●𝗟◗q). #o #f #p #q #n #Hn #m /2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/ qed-. lemma tls_succ_unwind2_rmap_closed (f) (q) (n): - q ϵ 𝐂❨Ⓕ,n❩ → + q ϵ 𝐂❨Ⓕ,n,𝟎❩ → ⇂f ≗ ⇂*[↑n]▶[f]q. #f #q #n #Hn @(stream_eq_canc_dx … (stream_tls_eq_repl …)) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma index 32bc5f594..a5127cc45 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma @@ -20,7 +20,7 @@ include "delayed_updating/unwind/unwind2_rmap_closed.ma". (* Note: crux of the commutation between unwind and balanced focused reduction *) lemma unwind2_rmap_uni_crux (f) (p) (b) (q) (m) (n): - b ϵ 𝐂❨Ⓕ,m❩ → q ϵ 𝐂❨Ⓕ,n❩ → + b ϵ 𝐂❨Ⓕ,m,𝟎❩ → q ϵ 𝐂❨Ⓕ,n,𝟎❩ → (𝐮❨↑(♭b+♭q)❩ ∘ ▶[f]p ≗ ▶[f](p●𝗔◗b●𝗟◗q) ∘ 𝐮❨↑(m+n)❩). #f #p #b #q #m #n #Hm #Hn list_append_assoc @@ -34,7 +34,7 @@ lemma unwind2_rmap_uni_crux (f) (p) (b) (q) (m) (n): [ nsucc_unfold >nplus_succ_dx >nplus_succ_dx tr_nap_plus_dx stream_tls_succ