From: Ferruccio Guidi Date: Thu, 24 Mar 2022 20:08:45 +0000 (+0100) Subject: update in delayed_updating X-Git-Tag: make_still_working~81 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b15b3e2d9e333bf94677ff2731c825da3566c9ec;p=helm.git update in delayed_updating + lift + two versions of unwind + some renaming, additions and corrections --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc new file mode 100644 index 000000000..b568c322a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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/prototerm_constructors.ma". +include "delayed_updating/syntax/prototerm_equivalence.ma". +include "delayed_updating/substitution/fsubst.ma". +include "delayed_updating/substitution/unwind.ma". +include "delayed_updating/syntax/path_structure.ma". +include "delayed_updating/syntax/path_balanced.ma". +include "delayed_updating/syntax/path_depth.ma". +include "delayed_updating/notation/relations/black_rightarrow_df_4.ma". +include "ground/xoa/ex_1_2.ma". +include "ground/xoa/and_4.ma". + +(* DELAYED FOCUSED REDUCTION ************************************************) + +definition dfr (p) (q): relation2 prototerm prototerm ≝ + λt1,t2. ∃∃b,n. + let r ≝ p●𝗔◗b●𝗟◗q in + ∧∧ ⊗b ϵ 𝐁 & ∀f. ↑❘q❘ = (↑[q]⫯f)@❨n❩ & r◖𝗱n ϵ t1 & + t1[⋔r←𝛗(n+❘b❘).(t1⋔(p◖𝗦))] ⇔ t2 +. + +interpretation + "focused balanced reduction with delayed updating (prototerm)" + 'BlackRightArrowDF t1 p q t2 = (dfr p q t1 t2). diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc new file mode 100644 index 000000000..069415421 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc @@ -0,0 +1,106 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dfr.ma". +include "delayed_updating/reduction/ifr.ma". +include "delayed_updating/substitution/fsubst_unwind.ma". +include "delayed_updating/substitution/fsubst_eq.ma". +include "delayed_updating/substitution/unwind_constructors.ma". +include "delayed_updating/substitution/unwind_preterm_eq.ma". +include "delayed_updating/substitution/unwind_structure_depth.ma". +include "delayed_updating/substitution/unwind_depth.ma". +include "delayed_updating/syntax/prototerm_proper_constructors.ma". +include "delayed_updating/syntax/path_structure_depth.ma". +include "ground/relocation/tr_uni_compose.ma". +include "ground/relocation/tr_pap_pushs.ma". + +(* DELAYED FOCUSED REDUCTION ************************************************) + +lemma tr_uni_eq_repl (n1) (n2): + n1 = n2 → 𝐮❨n1❩ ≗ 𝐮❨n2❩. +// qed. + +axiom pippo (b) (q) (n): + ↑❘q❘ = (↑[q]𝐢)@❨n❩ → + ↑❘q❘+❘b❘= (↑[b●𝗟◗q]𝐢)@❨n+❘b❘❩. + +lemma unwind_rmap_tls_eq_id (p) (n): + ❘p❘ = ↑[p]𝐢@❨n❩ → + (𝐢) ≗ ⇂*[n]↑[p]𝐢. +#p @(list_ind_rcons … p) -p +[ #n tr_pushs_swap tr_id_unfold #Hn + lapply (pippo … b … Hn) -Hn #Hn + @tr_compose_eq_repl + [ lift_append_proper_dx - /4 width=5 by in_comp_lift_bi, in_ppc_comp_trans, or_introl, ex2_intro/ -| * #q #Hq #H1 #H0 - @(ex2_intro … H1) @or_intror @conj // * - [ (tr_pap_eq_repl … (↑[p]f) … (lift_rmap_decompose …)) -lift_rmap_S_dx >structure_S_dx - @lift_grafted_sn // -| /2 width=1 by lift_grafted_S_dx/ -] -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_structure.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_structure.etc deleted file mode 100644 index 2a219e0ff..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_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/substitution/lift_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". - -(* LIFT FOR PATH ***********************************************************) - -(* Basic constructions with structure **************************************) - -lemma structure_lift (p) (f): - ⊗p = ⊗↑[f]p. -#p @(path_ind_lift … p) -p // #p #IH #f -nsucc_inj #H0 - IH -IH // -| // -| nsucc_inj // -| // -| // -] -qed. - -lemma lift_rmap_tls_eq (f) (p): - ⇂*[⧣p]f ≗ ⇂*[↑❘p❘]↑[p]⫯f. -(* -#f #p @(list_ind_rcons … p) -p // -#p * [ #n ] #IH // -tr_pushs_swap tr_id_unfold #Hn lapply (pippo … b … Hn) -Hn #Hn @tr_compose_eq_repl - [ lift_append_proper_dx - /4 width=5 by in_comp_lift_bi, in_ppc_comp_trans, or_introl, ex2_intro/ -| * #q #Hq #H1 #H0 - @(ex2_intro … H1) @or_intror @conj // * - [ tr_compose_push_bi // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma index 89ef40e91..31f4bbc14 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma @@ -17,26 +17,21 @@ include "delayed_updating/syntax/prototerm_constructors.ma". (* LIFT FOR PROTOTERM *******************************************************) -lemma lift_iref_after_sn (f) (t:prototerm) (n:pnat): - ↑[f∘𝐮❨n❩]t ⊆ ↑[f](𝛗n.t). -#f #t #n #p * #q #Hq #H0 destruct -@(ex2_intro … (𝗱n◗𝗺◗q)) +lemma lift_iref_sn (f) (t:prototerm) (n:pnat): + (𝛗f@❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛗n.t). +#f #t #n #p * #q * #r #Hr #H1 #H2 destruct +@(ex2_intro … (𝗱n◗𝗺◗r)) /2 width=1 by in_comp_iref/ qed-. -lemma lift_iref_after_dx (f) (t) (n:pnat): - ↑[f](𝛗n.t) ⊆ ↑[f∘𝐮❨n❩]t. +lemma lift_iref_dx (f) (t) (n:pnat): + ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.↑[⇂*[n]f]t. #f #t #n #p * #q #Hq #H0 destruct -elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct -/2 width=1 by in_comp_lift_bi/ +elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct +/3 width=1 by in_comp_iref, in_comp_lift_bi/ qed-. -lemma lift_iref_after (f) (t) (n:pnat): - ↑[f∘𝐮❨n❩]t ⇔ ↑[f](𝛗n.t). -/3 width=1 by conj, lift_iref_after_sn, lift_iref_after_dx/ -qed. - lemma lift_iref (f) (t) (n:pnat): - ↑[f]↑[𝐮❨n❩]t ⇔ ↑[f](𝛗n.t). -/3 width=3 by lift_term_after, subset_eq_trans/ + (𝛗f@❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛗n.t). +/3 width=1 by conj, lift_iref_sn, lift_iref_dx/ qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma deleted file mode 100644 index bf6831e80..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma +++ /dev/null @@ -1,48 +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.ma". -include "delayed_updating/syntax/path_depth.ma". -include "ground/relocation/tr_id_compose.ma". -include "ground/relocation/tr_compose_compose.ma". -include "ground/relocation/tr_compose_pn.ma". -include "ground/relocation/tr_compose_eq.ma". -include "ground/relocation/tr_pn_eq.ma". -include "ground/lib/stream_eq_eq.ma". - -(* LIFT FOR PATH ***********************************************************) - -(* Constructions with depth ************************************************) - -lemma lift_rmap_decompose (p) (f): - ↑[p]f ≗ (⫯*[❘p❘]f)∘(↑[p]𝐢). -#p @(list_ind_rcons … p) -p -[ #f (tr_pap_eq_repl … (↑[p]f) … (lift_rmap_decompose …)) -lift_lcons_alt // >lift_append_rcons_sn // - lift_lcons_alt >lift_append_rcons_sn // - lift_lcons_alt >lift_append_rcons_sn // - lift_lcons_alt // >lift_append_rcons_sn // +lift_lcons_alt (lift_path_eq_repl … (tr_compose_assoc …)) // -| tr_compose_push_bi // -] -qed. +(* COMMENT (* Advanced constructions with proj_rmap and stream_tls *********************) @@ -120,3 +120,4 @@ lemma lift_rmap_tls_d_dx (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/substitution/lift_preterm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm_eq.ma deleted file mode 100644 index d2bbd15be..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm_eq.ma +++ /dev/null @@ -1,81 +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_equivalence.ma". -include "delayed_updating/syntax/preterm.ma". -include "delayed_updating/substitution/lift_structure.ma". -include "delayed_updating/substitution/lift_prototerm.ma". - -lemma pippo (p): - ⊗p ϵ 𝐈. -#p @(list_ind_rcons … p) -p -[ lift_rmap_S_dx >structure_S_dx - @lift_grafted_sn // -| /2 width=1 by lift_grafted_S_dx/ -] -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma index 24a3dbc60..fc3fb3fcf 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground/lib/subset_ext_equivalence.ma". -include "delayed_updating/substitution/lift_eq.ma". +include "delayed_updating/substitution/lift_after.ma". include "delayed_updating/substitution/lift_prototerm.ma". (* LIFT FOR PROTOTERM *******************************************************) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma deleted file mode 100644 index 2a219e0ff..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_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/substitution/lift_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". - -(* LIFT FOR PATH ***********************************************************) - -(* Basic constructions with structure **************************************) - -lemma structure_lift (p) (f): - ⊗p = ⊗↑[f]p. -#p @(path_ind_lift … p) -p // #p #IH #f -nsucc_inj #H0 - IH -IH // -| // -| nsucc_inj // -| // -| // -] -qed. - -lemma lift_rmap_tls_eq (f) (p): - ⇂*[⧣p]f ≗ ⇂*[↑❘p❘]↑[p]⫯f. -(* -#f #p @(list_ind_rcons … p) -p // -#p * [ #n ] #IH // -(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 new file mode 100644 index 000000000..4053fb84e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_fsubst.ma @@ -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/unwind1/unwind_prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm.ma new file mode 100644 index 000000000..bc55294b7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm.ma @@ -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/unwind1/unwind_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm_eq.ma new file mode 100644 index 000000000..e93a78e6e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm_eq.ma @@ -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/unwind1/unwind_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma new file mode 100644 index 000000000..27d369219 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma @@ -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 // +(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 (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/unwind2/unwind_fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_fsubst.ma new file mode 100644 index 000000000..fedc665fb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_fsubst.ma @@ -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/unwind2/unwind_prototerm_eq.ma". +include "delayed_updating/unwind2/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 // * + [ 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 // +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/unwind2/unwind_prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_prototerm.ma new file mode 100644 index 000000000..1a5d46b77 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_prototerm.ma @@ -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/unwind2/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/unwind2/unwind_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_prototerm_eq.ma new file mode 100644 index 000000000..15b8cdb2c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_prototerm_eq.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unwind2/unwind_eq.ma". +include "delayed_updating/unwind2/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 (f1) (f2) (t): + ▼[f2]▼[f1]t ⇔ ▼[f2∘f1]t. +#f1 #f2 #t @subset_eq_trans +[ +| @subset_inclusion_ext_f1_compose +| @subset_equivalence_ext_f1_exteq /2 width=5/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_structure.ma new file mode 100644 index 000000000..b5d92a577 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_structure.ma @@ -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/unwind2/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 +