From 084fe5719d41ce13be068050fbade488d4a183ee Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 7 Aug 2022 19:36:15 +0200 Subject: [PATCH] update in delayed_updating + three old lemmas restored + some parked lemmas removed + minor renaming --- .../delayed_updating/etc/unwind1/unwind.etc | 187 ------------ .../etc/unwind1/unwind_constructors.etc | 37 --- .../etc/unwind1/unwind_depth.etc | 49 ---- .../etc/unwind1/unwind_eq.etc | 111 -------- .../etc/unwind1/unwind_eq_etc.etc | 15 - .../etc/unwind1/unwind_fsubst.etc | 61 ---- .../etc/unwind1/unwind_preterm_eq.etc | 68 ----- .../etc/unwind1/unwind_prototerm.etc | 30 -- .../etc/unwind1/unwind_prototerm_eq.etc | 41 --- .../etc/unwind1/unwind_structure.etc | 269 ------------------ .../etc/unwind1/unwind_structure_depth.etc | 31 -- .../delayed_updating/etc/unwind2/unwind.etc | 189 ------------ .../etc/unwind2/unwind_eq.etc | 122 -------- .../etc/unwind2/unwind_etc.etc | 10 - .../etc/unwind2/unwind_structure.etc | 269 ------------------ .../etc/unwind2/unwind_structure_depth.etc | 31 -- .../delayed_updating/etc/unwind3/unwind.etc | 189 ------------ .../etc/unwind3/unwind_constructors.etc | 44 --- .../etc/unwind3/unwind_eq.etc | 124 -------- .../etc/unwind3/unwind_fsubst.etc | 61 ---- .../etc/unwind3/unwind_lift.etc | 32 --- .../etc/unwind3/unwind_preterm_eq.etc | 68 ----- .../etc/unwind3/unwind_prototerm.etc | 30 -- .../etc/unwind3/unwind_prototerm_eq.etc | 41 --- .../etc/unwind3/unwind_structure.etc | 269 ------------------ .../etc/unwind3/unwind_structure_depth.etc | 31 -- .../unwind2_rmap_depth.ma} | 42 +-- .../unwind/unwind2_rmap_head.ma | 12 +- 28 files changed, 32 insertions(+), 2431 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_constructors.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_depth.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_eq.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_eq_etc.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_fsubst.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_preterm_eq.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm_eq.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure_depth.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_eq.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_etc.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_structure.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_structure_depth.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_constructors.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_eq.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_fsubst.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_lift.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_preterm_eq.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm_eq.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_structure.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_structure_depth.etc rename matita/matita/contribs/lambdadelta/delayed_updating/{etc/unwind2/unwind_depth.etc => unwind/unwind2_rmap_depth.ma} (60%) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind.etc deleted file mode 100644 index 3e76deece..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind.etc +++ /dev/null @@ -1,187 +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 "ground/relocation/tr_uni_pap.ma". -include "delayed_updating/syntax/path.ma". -include "delayed_updating/notation/functions/black_downtriangle_4.ma". -include "delayed_updating/notation/functions/black_downtriangle_2.ma". - -(* UNWIND FOR PATH **********************************************************) - -definition unwind_continuation (A:Type[0]) ≝ - tr_map → path → A. - -rec definition unwind_gen (A:Type[0]) (k:unwind_continuation A) (f) (p) on p ≝ -match p with -[ list_empty ⇒ k f (𝐞) -| list_lcons l q ⇒ - match l with - [ label_d n ⇒ - match q with - [ list_empty ⇒ unwind_gen (A) (λg,p. k g (𝗱(f@⧣❨n❩)◗p)) (𝐮❨f@⧣❨n❩❩) q - | list_lcons _ _ ⇒ unwind_gen (A) k (𝐮❨f@⧣❨n❩❩) q - ] - | label_m ⇒ unwind_gen (A) k f q - | label_L ⇒ unwind_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q - | label_A ⇒ unwind_gen (A) (λg,p. k g (𝗔◗p)) f q - | label_S ⇒ unwind_gen (A) (λg,p. k g (𝗦◗p)) f q - ] -]. - -interpretation - "unwind (gneric)" - 'BlackDownTriangle A k f p = (unwind_gen A k f p). - -definition proj_path: unwind_continuation … ≝ - λf,p.p. - -definition proj_rmap: unwind_continuation … ≝ - λf,p.f. - -interpretation - "unwind (path)" - 'BlackDownTriangle f p = (unwind_gen ? proj_path f p). - -interpretation - "unwind (relocation map)" - 'BlackDownTriangle p f = (unwind_gen ? proj_rmap f p). - -(* Basic constructions ******************************************************) - -lemma unwind_empty (A) (k) (f): - k f (𝐞) = ▼{A}❨k, f, 𝐞❩. -// qed. - -lemma unwind_d_empty (A) (k) (n) (f): - ▼❨(λg,p. k g (𝗱(f@⧣❨n❩)◗p)), 𝐮❨f@⧣❨n❩❩, 𝐞❩ = ▼{A}❨k, f, 𝗱n◗𝐞❩. -// qed. - -lemma unwind_d_lcons (A) (k) (p) (l) (n) (f): - ▼❨k, 𝐮❨f@⧣❨n❩❩, l◗p❩ = ▼{A}❨k, f, 𝗱n◗l◗p❩. -// qed. - -lemma unwind_m_sn (A) (k) (p) (f): - ▼❨k, f, p❩ = ▼{A}❨k, f, 𝗺◗p❩. -// qed. - -lemma unwind_L_sn (A) (k) (p) (f): - ▼❨(λg,p. k g (𝗟◗p)), ⫯f, p❩ = ▼{A}❨k, f, 𝗟◗p❩. -// qed. - -lemma unwind_A_sn (A) (k) (p) (f): - ▼❨(λg,p. k g (𝗔◗p)), f, p❩ = ▼{A}❨k, f, 𝗔◗p❩. -// qed. - -lemma unwind_S_sn (A) (k) (p) (f): - ▼❨(λg,p. k g (𝗦◗p)), f, p❩ = ▼{A}❨k, f, 𝗦◗p❩. -// qed. - -(* Basic constructions with proj_path ***************************************) - -lemma unwind_path_empty (f): - (𝐞) = ▼[f]𝐞. -// qed. - -lemma unwind_path_d_empty (f) (n): - 𝗱(f@⧣❨n❩)◗𝐞 = ▼[f](𝗱n◗𝐞). -// qed. - -lemma unwind_path_d_lcons (f) (p) (l) (n): - ▼[𝐮❨f@⧣❨n❩❩](l◗p) = ▼[f](𝗱n◗l◗p). -// qed. - -lemma unwind_path_m_sn (f) (p): - ▼[f]p = ▼[f](𝗺◗p). -// qed. - -(* Basic constructions with proj_rmap ***************************************) - -lemma unwind_rmap_empty (f): - f = ▼[𝐞]f. -// qed. - -lemma unwind_rmap_d_sn (f) (p) (n): - ▼[p](𝐮❨f@⧣❨n❩❩) = ▼[𝗱n◗p]f. -#f * // qed. - -lemma unwind_rmap_m_sn (f) (p): - ▼[p]f = ▼[𝗺◗p]f. -// qed. - -lemma unwind_rmap_L_sn (f) (p): - ▼[p](⫯f) = ▼[𝗟◗p]f. -// qed. - -lemma unwind_rmap_A_sn (f) (p): - ▼[p]f = ▼[𝗔◗p]f. -// qed. - -lemma unwind_rmap_S_sn (f) (p): - ▼[p]f = ▼[𝗦◗p]f. -// qed. - -(* Advanced constructions with proj_rmap and path_append ********************) - -lemma unwind_rmap_append (p2) (p1) (f): - ▼[p2]▼[p1]f = ▼[p1●p2]f. -#p2 #p1 elim p1 -p1 // * [ #n ] #p1 #IH #f // -[ (tr_pap_eq_repl … (▼[p]f) … (unwind_rmap_decompose …)) -unwind_lcons_alt // >unwind_append_rcons_sn // - unwind_lcons_alt >unwind_append_rcons_sn // - unwind_lcons_alt >unwind_append_rcons_sn // - unwind_lcons_alt nrplus_inj_dx -/2 width=1 by tr_tls_compose_uni_dx/ -qed. -*) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_fsubst.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_fsubst.etc deleted file mode 100644 index 4053fb84e..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_fsubst.etc +++ /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/unwind1/unwind_prototerm_eq.ma". -include "delayed_updating/unwind1/unwind_structure.ma". -include "delayed_updating/substitution/fsubst.ma". -include "delayed_updating/syntax/preterm.ma". -include "delayed_updating/syntax/prototerm_proper.ma". - -(* UNWIND FOR PROTOTERM *****************************************************) - -(* Constructions with fsubst ************************************************) - -lemma unwind_fsubst_sn (f) (t) (u) (p): u ϵ 𝐏 → - (▼[f]t)[⋔(⊗p)←▼[▼[p]f]u] ⊆ ▼[f](t[⋔p←u]). -#f #t #u #p #Hu #ql * * -[ #rl * #r #Hr #H1 #H2 destruct - >unwind_append_proper_dx - /4 width=5 by in_comp_unwind_bi, in_ppc_comp_trans, or_introl, ex2_intro/ -| * #q #Hq #H1 #H0 - @(ex2_intro … H1) @or_intror @conj // * - [ unwind_rmap_S_dx >structure_S_dx - @unwind_grafted_sn // -| /2 width=1 by unwind_grafted_S_dx/ -] -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm.etc deleted file mode 100644 index bc55294b7..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm.etc +++ /dev/null @@ -1,30 +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/unwind1/unwind.ma". -include "delayed_updating/syntax/prototerm.ma". -include "ground/lib/subset_ext.ma". - -(* UNWIND FOR PROTOTERM *****************************************************) - -interpretation - "unwind (prototerm)" - 'BlackDownTriangle f t = (subset_ext_f1 ? ? (unwind_gen ? proj_path f) t). - -(* Basic constructions ******************************************************) - -lemma in_comp_unwind_bi (f) (p) (t): - p ϵ t → ▼[f]p ϵ ▼[f]t. -/2 width=1 by subset_in_ext_f1_dx/ -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm_eq.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm_eq.etc deleted file mode 100644 index e93a78e6e..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm_eq.etc +++ /dev/null @@ -1,41 +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 "ground/lib/subset_ext_equivalence.ma". -include "delayed_updating/unwind1/unwind_eq.ma". -include "delayed_updating/unwind1/unwind_prototerm.ma". - -(* UNWIND FOR PROTOTERM *****************************************************) - -(* Constructions with subset_equivalence ************************************) - -lemma unwind_term_eq_repl_sn (f1) (f2) (t): - f1 ≗ f2 → ▼[f1]t ⇔ ▼[f2]t. -/3 width=1 by subset_equivalence_ext_f1_exteq, unwind_path_eq_repl/ -qed. - -lemma unwind_term_eq_repl_dx (f) (t1) (t2): - t1 ⇔ t2 → ▼[f]t1 ⇔ ▼[f]t2. -/2 width=1 by subset_equivalence_ext_f1_bi/ -qed. - -lemma unwind_term_after_id_sn (f) (t): - ▼[𝐢]▼[f]t ⇔ ▼[f]t. -#f #t @subset_eq_trans -[ -| @subset_inclusion_ext_f1_compose -| @subset_equivalence_ext_f1_exteq - #p @unwind_path_after_id_sn -] -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure.etc deleted file mode 100644 index 0f52a1858..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure.etc +++ /dev/null @@ -1,269 +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/unwind1/unwind_eq.ma". -include "delayed_updating/syntax/path_structure.ma". -include "delayed_updating/syntax/path_inner.ma". -include "delayed_updating/syntax/path_proper.ma". -include "ground/xoa/ex_4_2.ma". - -(* UNWIND FOR PATH *********************************************************) - -(* Basic constructions with structure **************************************) - -lemma structure_unwind (p) (f): - ⊗p = ⊗▼[f]p. -#p @(path_ind_unwind … p) -p // #p #IH #f -unwind_lcons_alt // >unwind_append_rcons_sn // - unwind_lcons_alt >unwind_append_rcons_sn // - unwind_lcons_alt >unwind_append_rcons_sn // - unwind_lcons_alt (unwind_path_eq_repl … (tr_compose_assoc …)) // -| tr_compose_push_bi // -] -qed. - -(* Advanced constructions with proj_rmap and stream_tls *********************) - -lemma unwind_rmap_tls_d_dx (f) (p) (m) (n): - ⇂*[m+n]▼[p]f ≗ ⇂*[m]▼[p◖𝗱n]f. -#f #p #m #n -nrplus_inj_dx -/2 width=1 by tr_tls_compose_uni_dx/ -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_etc.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_etc.etc deleted file mode 100644 index a9e563db6..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_etc.etc +++ /dev/null @@ -1,10 +0,0 @@ -include "delayed_updating/unwind2/unwind_depth.ma". -include "ground/relocation/tr_uni_compose.ma". - -lemma pippo (q) (p): - ▼[p]𝐢 ≗ ⇂*[↑❘q❘]▼[p●𝗟◗q]𝐢. -#q @(list_ind_rcons … q) -q // -#q * [ #n ] #IH #p // -list_cons_shift unwind_lcons_alt // >unwind_append_rcons_sn // - unwind_lcons_alt >unwind_append_rcons_sn // - unwind_lcons_alt >unwind_append_rcons_sn // - unwind_lcons_alt unwind_append_proper_dx - /4 width=5 by in_comp_unwind_bi, in_ppc_comp_trans, or_introl, ex2_intro/ -| * #q #Hq #H1 #H0 - @(ex2_intro … H1) @or_intror @conj // * - [ list_cons_shift unwind_rmap_S_dx >structure_S_dx - @unwind_grafted_sn // -| /2 width=1 by unwind_grafted_S_dx/ -] -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm.etc deleted file mode 100644 index c4a103b61..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm.etc +++ /dev/null @@ -1,30 +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/unwind3/unwind.ma". -include "delayed_updating/syntax/prototerm.ma". -include "ground/lib/subset_ext.ma". - -(* UNWIND FOR PROTOTERM *****************************************************) - -interpretation - "unwind (prototerm)" - 'BlackDownTriangle f t = (subset_ext_f1 ? ? (unwind_gen ? proj_path f) t). - -(* Basic constructions ******************************************************) - -lemma in_comp_unwind_bi (f) (p) (t): - p ϵ t → ▼[f]p ϵ ▼[f]t. -/2 width=1 by subset_in_ext_f1_dx/ -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm_eq.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm_eq.etc deleted file mode 100644 index 01d302f3e..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm_eq.etc +++ /dev/null @@ -1,41 +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 "ground/lib/subset_ext_equivalence.ma". -include "delayed_updating/unwind3/unwind_eq.ma". -include "delayed_updating/unwind3/unwind_prototerm.ma". - -(* UNWIND FOR PROTOTERM *****************************************************) - -(* Constructions with subset_equivalence ************************************) - -lemma unwind_term_eq_repl_sn (f1) (f2) (t): - f1 ≗ f2 → ▼[f1]t ⇔ ▼[f2]t. -/3 width=1 by subset_equivalence_ext_f1_exteq, unwind_path_eq_repl/ -qed. - -lemma unwind_term_eq_repl_dx (f) (t1) (t2): - t1 ⇔ t2 → ▼[f]t1 ⇔ ▼[f]t2. -/2 width=1 by subset_equivalence_ext_f1_bi/ -qed. - -lemma unwind_term_after_id_sn (f) (t): - ▼[𝐢]▼[f]t ⇔ ▼[f]t. -#f #t @subset_eq_trans -[ -| @subset_inclusion_ext_f1_compose -| @subset_equivalence_ext_f1_exteq - #p @unwind_path_after_id_sn -] -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_structure.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_structure.etc deleted file mode 100644 index c52a43871..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_structure.etc +++ /dev/null @@ -1,269 +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/unwind3/unwind_eq.ma". -include "delayed_updating/syntax/path_structure.ma". -include "delayed_updating/syntax/path_inner.ma". -include "delayed_updating/syntax/path_proper.ma". -include "ground/xoa/ex_4_2.ma". - -(* UNWIND FOR PATH *********************************************************) - -(* Basic constructions with structure **************************************) - -lemma structure_unwind (p) (f): - ⊗p = ⊗▼[f]p. -#p @(path_ind_unwind … p) -p // #p #IH #f -(tr_pap_eq_repl … (▼[p]f) … (unwind_rmap_decompose …)) -(tr_pap_eq_repl … (▶[f]p) … (unwind2_rmap_decompose …)) +unwind2_rmap_pap_le +*) +#f #p #n #Hn +>(tr_xap_eq_repl … (▶[f]p) … (unwind2_rmap_decompose …)) +tr_xap_ninj >(path_head_refl_append p … Hn) in ⊢ (??%?); ->(unwind2_rmap_head_xap_closed … Hn) -Hn +lemma unwind2_rmap_append_pap_closed (f) (p) (q) (h:pnat): + q = ↳[h]q → + ♭q = ninj (▶[f](p●q)@⧣❨h❩). +#f #p #q #h #Hh +>tr_xap_ninj >(path_head_refl_append p … Hh) in ⊢ (??%?); +>(unwind2_rmap_head_xap_closed … Hh) -Hh