From: Ferruccio Guidi Date: Sat, 21 May 2022 18:23:22 +0000 (+0200) Subject: update in delayed_updating X-Git-Tag: make_still_working~69 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=97ff918432e878ab8314c72fe2b948a253b26e21;p=helm.git update in delayed_updating + unwind completed with an important result on lift --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind.etc new file mode 100644 index 000000000..3e76deece --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind.etc @@ -0,0 +1,187 @@ +(**************************************************************************) +(* ___ *) +(* ||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 new file mode 100644 index 000000000..4053fb84e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_fsubst.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/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 new file mode 100644 index 000000000..bc55294b7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm.etc @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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 new file mode 100644 index 000000000..e93a78e6e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm_eq.etc @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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 new file mode 100644 index 000000000..0f52a1858 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure.etc @@ -0,0 +1,269 @@ +(**************************************************************************) +(* ___ *) +(* ||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 +nsucc_inj #H0 + IH -IH // +| // +| nsucc_inj // +| // +| // +] +qed. + +lemma unwind_rmap_tls_eq (f) (p): + ⇂*[⧣p]f ≗ ⇂*[▼❘p❘]▼[p]⫯f. +(* +#f #p @(list_ind_rcons … p) -p // +#p * [ #n ] #IH // +(unwind2_path_eq_repl … (tr_compose_assoc …)) // +| <(unwind2_path_L_sn … f1) tr_compose_push_bi // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma new file mode 100644 index 000000000..642056c89 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unwind/unwind2_path_eq.ma". +include "delayed_updating/substitution/lift_eq.ma". +include "ground/relocation/tr_uni_compose.ma". + +(* UNWIND FOR PATH **********************************************************) + +(* Properties with lift_path ************************************************) + +lemma unwind2_lift_path_after (p) (f1) (f2): + ↑[f2]▼[f1]p = ▼[f2∘f1]p. +#p @(path_ind_unwind … p) -p // [ #n | #p ] #IH #f1 #f2 +[ tr_compose_push_bi // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma new file mode 100644 index 000000000..7cb6190b1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma @@ -0,0 +1,116 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unwind/unwind2_path.ma". +include "delayed_updating/unwind/unwind_gen_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 **********************************************************) + +(* Constructions with list_rcons ********************************************) + +lemma unwind2_path_d_dx (f) (p) (n) : + (⊗p)◖𝗱((▶[f](pᴿ))@⧣❨n❩) = ▼[f](p◖𝗱n). +#f #p #n unwind2_rmap_S_sn >reverse_rcons >structure_S_dx + @unwind2_term_grafted_sn // (**) (* auto fails *) +| /2 width=1 by unwind2_term_grafted_S_dx/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma new file mode 100644 index 000000000..4245a6638 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unwind/unwind2_prototerm_eq.ma". +include "delayed_updating/unwind/unwind2_path_structure.ma". +include "delayed_updating/substitution/fsubst.ma". +include "delayed_updating/syntax/preterm.ma". +include "delayed_updating/syntax/prototerm_proper.ma". + +(* UNWIND FOR PRETERM ******************************************************) + +(* Constructions with fsubst ************************************************) + +lemma unwind2_term_fsubst_sn (f) (t) (u) (p): u ϵ 𝐏 → + (▼[f]t)[⋔(⊗p)←▼[▶[f]pᴿ]u] ⊆ ▼[f](t[⋔p←u]). +#f #t #u #p #Hu #ql * * +[ #rl * #r #Hr #H1 #H2 destruct + >unwind2_path_append_proper_dx + /4 width=5 by in_comp_unwind2_path_term, in_ppc_comp_trans, or_introl, ex2_intro/ +| * #q #Hq #H1 #H0 + @(ex2_intro … H1) @or_intror @conj // * + [ tr_pushs_swap IH -IH IH -IH tr_compose_nap >tr_compose_push_bi // +qed. + +lemma tr_uni_xap_succ (n) (m): + ↑m + n = 𝐮❨n❩@❨↑m❩. +#n #m +tr_pushs_succ (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/unwind1/unwind_fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_fsubst.ma deleted file mode 100644 index 4053fb84e..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_fsubst.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/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/unwind1/unwind_prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm.ma deleted file mode 100644 index bc55294b7..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm.ma +++ /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/unwind1/unwind_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm_eq.ma deleted file mode 100644 index e93a78e6e..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm_eq.ma +++ /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/unwind1/unwind_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma deleted file mode 100644 index 0f52a1858..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma +++ /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 -nsucc_inj #H0 - IH -IH // -| // -| nsucc_inj // -| // -| // -] -qed. - -lemma unwind_rmap_tls_eq (f) (p): - ⇂*[⧣p]f ≗ ⇂*[▼❘p❘]▼[p]⫯f. -(* -#f #p @(list_ind_rcons … p) -p // -#p * [ #n ] #IH // -