From: Ferruccio Guidi Date: Tue, 17 May 2022 15:51:39 +0000 (+0200) Subject: update in delayed_updating X-Git-Tag: make_still_working~73 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=dfcad1c1a698bac1b7fb6a5f59393b28f45182af update in delayed_updating + generic unwind for path + some old files parked --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/black_downtriangle_4.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/black_downtriangle_4.etc new file mode 100644 index 000000000..9235b7e10 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/black_downtriangle_4.etc @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation < "hvbox( ▼❨ term 46 k, break term 46 p, break term 46 f ❩ )" + non associative with precedence 70 + for @{ 'BlackDownTriangle $S $k $p $f }. + +notation > "hvbox( ▼❨ term 46 k, break term 46 p, break term 46 f ❩ )" + non associative with precedence 70 + for @{ 'BlackDownTriangle ? $k $p $f }. + +notation > "hvbox( ▼{ term 46 S }❨ break term 46 k, break term 46 p, break term 46 f ❩ )" + non associative with precedence 70 + for @{ 'BlackDownTriangle $S $k $p $f }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift.etc new file mode 100644 index 000000000..e6e1e661e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift.etc @@ -0,0 +1,158 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/functions/uparrow_4.ma". +include "delayed_updating/notation/functions/uparrow_2.ma". +include "delayed_updating/syntax/path.ma". +include "ground/relocation/tr_id_pap.ma". + +(* LIFT FOR PATH ***********************************************************) + +definition lift_continuation (A:Type[0]) ≝ + tr_map → path → A. + +rec definition lift_gen (A:Type[0]) (k:lift_continuation A) (f) (p) on p ≝ +match p with +[ list_empty ⇒ k f (𝐞) +| list_lcons l q ⇒ + match l with + [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (𝐢) q + | label_m ⇒ lift_gen (A) (λg,p. k g (𝗺◗p)) f q + | label_L ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q + | label_A ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q + | label_S ⇒ lift_gen (A) (λg,p. k g (𝗦◗p)) f q + ] +]. + +interpretation + "lift (gneric)" + 'UpArrow A k f p = (lift_gen A k f p). + +definition proj_path: lift_continuation … ≝ + λf,p.p. + +definition proj_rmap: lift_continuation … ≝ + λf,p.f. + +interpretation + "lift (path)" + 'UpArrow f p = (lift_gen ? proj_path f p). + +interpretation + "lift (relocation map)" + 'UpArrow p f = (lift_gen ? proj_rmap f p). + +(* Basic constructions ******************************************************) + +lemma lift_empty (A) (k) (f): + k f (𝐞) = ↑{A}❨k, f, 𝐞❩. +// qed. + +lemma lift_d_sn (A) (k) (p) (n) (f): + ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), 𝐢, p❩ = ↑{A}❨k, f, 𝗱n◗p❩. +// qed. + +lemma lift_m_sn (A) (k) (p) (f): + ↑❨(λg,p. k g (𝗺◗p)), f, p❩ = ↑{A}❨k, f, 𝗺◗p❩. +// qed. + +lemma lift_L_sn (A) (k) (p) (f): + ↑❨(λg,p. k g (𝗟◗p)), ⫯f, p❩ = ↑{A}❨k, f, 𝗟◗p❩. +// qed. + +lemma lift_A_sn (A) (k) (p) (f): + ↑❨(λg,p. k g (𝗔◗p)), f, p❩ = ↑{A}❨k, f, 𝗔◗p❩. +// qed. + +lemma lift_S_sn (A) (k) (p) (f): + ↑❨(λg,p. k g (𝗦◗p)), f, p❩ = ↑{A}❨k, f, 𝗦◗p❩. +// qed. + +(* Basic constructions with proj_path ***************************************) + +lemma lift_path_empty (f): + (𝐞) = ↑[f]𝐞. +// qed. + +(* Basic constructions with proj_rmap ***************************************) + +lemma lift_rmap_empty (f): + f = ↑[𝐞]f. +// qed. + +lemma lift_rmap_d_sn (f) (p) (n): + ↑[p]𝐢 = ↑[𝗱n◗p]f. +// qed. + +lemma lift_rmap_m_sn (f) (p): + ↑[p]f = ↑[𝗺◗p]f. +// qed. + +lemma lift_rmap_L_sn (f) (p): + ↑[p](⫯f) = ↑[𝗟◗p]f. +// qed. + +lemma lift_rmap_A_sn (f) (p): + ↑[p]f = ↑[𝗔◗p]f. +// qed. + +lemma lift_rmap_S_sn (f) (p): + ↑[p]f = ↑[𝗦◗p]f. +// qed. + +(* Advanced cinstructionswith proj_rmap and tr_id ***************************) + +lemma lift_rmap_id (p): + (𝐢) = ↑[p]𝐢. +#p elim p -p // +* [ #n ] #p #IH // +qed. + +(* Advanced constructions with proj_rmap and path_append ********************) + +lemma lift_rmap_append (p2) (p1) (f): + ↑[p2]↑[p1]f = ↑[p1●p2]f. +#p2 #p1 elim p1 -p1 // * [ #n ] #p1 #IH #f // +[ tr_compose_push_bi // +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_constructors.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_constructors.etc new file mode 100644 index 000000000..3bd7b43bc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_constructors.etc @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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_prototerm_eq.ma". +include "delayed_updating/substitution/lift_uni.ma". +include "delayed_updating/syntax/prototerm_constructors.ma". + +(* LIFT FOR PROTOTERM *******************************************************) + +lemma lift_iref_bi (t1) (t2) (n): + t1 ⇔ t2 → 𝛗n.t1 ⇔ 𝛗n.t2. +/2 width=1 by subset_equivalence_ext_f1_bi/ +qed. + +lemma lift_iref_sn (f) (t:prototerm) (n:pnat): + (𝛗f@❨n❩.t) ⊆ ↑[f](𝛗n.t). +#f #t #n #p * #q #Hq #H0 destruct +@(ex2_intro … (𝗱n◗𝗺◗q)) +/2 width=1 by in_comp_iref/ +qed-. + +lemma lift_iref_dx (f) (t) (n:pnat): + ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.t. +#f #t #n #p * #q #Hq #H0 destruct +elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct +/2 width=1 by in_comp_iref/ +qed-. + +lemma lift_iref (f) (t) (n:pnat): + (𝛗f@❨n❩.t) ⇔ ↑[f](𝛗n.t). +/3 width=1 by conj, lift_iref_sn, lift_iref_dx/ +qed. + +lemma lift_iref_uni (t) (m) (n): + (𝛗(n+m).t) ⇔ ↑[𝐮❨m❩](𝛗n.t). +// qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_eq.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_eq.etc new file mode 100644 index 000000000..1e9b2789b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_eq.etc @@ -0,0 +1,164 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground/relocation/tr_pap_eq.ma". +include "ground/relocation/tr_pn_eq.ma". + +(* LIFT FOR PATH ***********************************************************) + +definition lift_exteq (A): relation2 (lift_continuation A) (lift_continuation A) ≝ + λk1,k2. ∀f1,f2,p. f1 ≗ f2 → k1 f1 p = k2 f2 p. + +interpretation + "extensional equivalence (lift continuation)" + 'RingEq A k1 k2 = (lift_exteq A k1 k2). + +(* Constructions with lift_exteq ********************************************) + +lemma lift_eq_repl (A) (p) (k1) (k2): + k1 ≗{A} k2 → stream_eq_repl … (λf1,f2. ↑❨k1, f1, p❩ = ↑❨k2, f2, p❩). +#A #p elim p -p [| * [ #n ] #q #IH ] +#k1 #k2 #Hk #f1 #f2 #Hf +[ lift_lcons_alt // >lift_append_rcons_sn // +lift_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/lift1/lift_length.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_length.etc new file mode 100644 index 000000000..0576799af --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_length.etc @@ -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/substitution/lift_eq.ma". +include "ground/lib/list_length.ma". + +(* LIFT FOR PATH ***********************************************************) + +(* Constructions with list_length ******************************************) + +lemma lift_path_length (p) (f): + ❘p❘ = ❘↑[f]p❘. +#p elim p -p // * [ #n ] #p #IH #f // +[ list_length_lcons >list_length_lcons // +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_prototerm.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_prototerm.etc new file mode 100644 index 000000000..6555b5d9e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_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/substitution/lift.ma". +include "delayed_updating/syntax/prototerm.ma". +include "ground/lib/subset_ext.ma". + +(* LIFT FOR PROTOTERM *******************************************************) + +interpretation + "lift (prototerm)" + 'UpArrow f t = (subset_ext_f1 ? ? (lift_gen ? proj_path f) t). + +(* Basic constructions ******************************************************) + +lemma in_comp_lift_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/lift1/lift_prototerm_eq.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_prototerm_eq.etc new file mode 100644 index 000000000..55b271f8b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_prototerm_eq.etc @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/lift_after.ma". +include "delayed_updating/substitution/lift_prototerm.ma". + +(* LIFT FOR PROTOTERM *******************************************************) + +(* Constructions with subset_equivalence ************************************) + +lemma lift_term_eq_repl_sn (f1) (f2) (t): + f1 ≗ f2 → ↑[f1]t ⇔ ↑[f2]t. +/3 width=1 by subset_equivalence_ext_f1_exteq, lift_path_eq_repl/ +qed. + +lemma lift_term_eq_repl_dx (f) (t1) (t2): + t1 ⇔ t2 → ↑[f]t1 ⇔ ↑[f]t2. +/2 width=1 by subset_equivalence_ext_f1_bi/ +qed. + +lemma lift_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. + +lemma lift_term_id_sn (t): + t ⊆ ↑[𝐢]t. +#t #p #Hp +>(lift_path_id p) +/2 width=1 by in_comp_lift_bi/ +qed-. + +lemma lift_term_id_dx (t): + ↑[𝐢]t ⊆ t. +#t #p * #q #Hq #H destruct // +qed-. + +lemma lift_term_id (t): + t ⇔ ↑[𝐢]t. +/3 width=2 by lift_term_id_dx, lift_term_id_sn, conj/ +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_structure.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_structure.etc new file mode 100644 index 000000000..86a425975 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_structure.etc @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||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". + +(* LIFT FOR PATH ***********************************************************) + +(* Constructions with structure ********************************************) + +lemma structure_lift (p) (f): + ⊗p = ⊗↑[f]p. +#p elim p -p // +* [ #n ] #p #IH #f // +[ (list_length_inv_zero_sn … H0) -p // +| #k #IH * + [ #H0 elim (eq_inv_nsucc_zero … H0) + | * [ #n ] #p #H0 + lapply (eq_inv_nsucc_bi … H0) -H0 + [ cases p -p [ -IH | #l #p ] #H0 destruct // + (list_length_inv_zero_sn … H0) -p // +| #k #IH * + [ #n #H0 elim (eq_inv_nsucc_zero … H0) + | * [ #m ] #p #n #H0 + lapply (eq_inv_nsucc_bi … H0) -H0 + [ cases p -p [ -IH | #l #p ] #H0 destruct list_cons_shift tr_compose_pap // +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind2_rmap.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind2_rmap.etc new file mode 100644 index 000000000..9bb26750a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind2_rmap.etc @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unwind0/unwind1_rmap.ma". +include "delayed_updating/notation/functions/black_righttriangle_2.ma". + +(* EXTENDED UNWIND FOR RELOCATION MAP ***************************************) + +definition unwind2_rmap (f) (p): tr_map ≝ + (▶↑[f]p)∘(↑[p]f). + +interpretation + "extended unwind (relocation map)" + 'BlackRightTriangle f p = (unwind2_rmap f p). + +(* Basic constructions ******************************************************) + +lemma unwind2_rmap_unfold (f) (p): + (▶↑[f]p)∘(↑[p]f) = ▶[f]p. +// qed. + +lemma unwind2_rmap_m_sn (f) (p): + ▶[f]p = ▶[f](𝗺◗p). +#f #p +tr_compose_push_bi // -] -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_constructors.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_constructors.etc deleted file mode 100644 index 772c837fb..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_constructors.etc +++ /dev/null @@ -1,51 +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_prototerm_id.ma". -include "delayed_updating/substitution/lift_uni.ma". -include "delayed_updating/syntax/prototerm_constructors.ma". - -(* LIFT FOR PROTOTERM *******************************************************) - -lemma lift_iref_bi (t1) (t2) (n): - t1 ⇔ t2 → 𝛗n.t1 ⇔ 𝛗n.t2. -/2 width=1 by subset_equivalence_ext_f1_bi/ -qed. - -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_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 #H0 #Hp destruct -/3 width=1 by in_comp_iref, in_comp_lift_bi/ -qed-. - -lemma lift_iref (f) (t) (n:pnat): - (𝛗f@❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛗n.t). -/3 width=1 by conj, lift_iref_sn, lift_iref_dx/ -qed. - -lemma lift_iref_uni (t) (m) (n): - (𝛗(n+m).t) ⇔ ↑[𝐮❨m❩](𝛗n.t). -#t #m #n -@(subset_eq_trans … (lift_iref …)) -nsucc_pnpred lift_lcons_alt // >lift_append_rcons_sn // -lift_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/unwind3/lift_id.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_id.etc deleted file mode 100644 index 1d8b45295..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_id.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/substitution/lift_eq.ma". -include "ground/relocation/tr_id_pap.ma". -include "ground/relocation/tr_id_tls.ma". - -(* LIFT FOR PATH ***********************************************************) - -(* Constructions with tr_id ************************************************) - -lemma lift_path_id (p): - p = ↑[𝐢]p. -#p elim p -p // -* [ #n ] #p #IH // -[ (lift_path_id p) -/2 width=1 by in_comp_lift_bi/ -qed-. - -lemma lift_term_id_dx (t): - ↑[𝐢]t ⊆ t. -#t #p * #q #Hq #H destruct // -qed-. - -lemma lift_term_id (t): - t ⇔ ↑[𝐢]t. -/3 width=2 by lift_term_id_dx, lift_term_id_sn, conj/ -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_uni.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_uni.etc deleted file mode 100644 index cd6c79533..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_uni.etc +++ /dev/null @@ -1,28 +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_id.ma". -include "ground/relocation/tr_uni_pap.ma". -include "ground/relocation/tr_uni_tls.ma". - -(* LIFT FOR PATH ***********************************************************) - -(* Constructions with tr_uni ***********************************************) - -lemma lift_path_d_sn_uni (p) (m) (n): - (𝗱(n+m)◗p) = ↑[𝐮❨m❩](𝗱(n)◗p). -#p #m #n -nsucc_pnpred - "hvbox( ▼❨ term 46 k, break term 46 p, break term 46 f ❩ )" - non associative with precedence 70 - for @{ 'BlackDownTriangle ? $k $p $f }. - -notation > "hvbox( ▼{ term 46 S }❨ break term 46 k, break term 46 p, break term 46 f ❩ )" - non associative with precedence 70 - for @{ 'BlackDownTriangle $S $k $p $f }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma index e6e1e661e..a487fcf5a 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma @@ -15,7 +15,8 @@ include "delayed_updating/notation/functions/uparrow_4.ma". include "delayed_updating/notation/functions/uparrow_2.ma". include "delayed_updating/syntax/path.ma". -include "ground/relocation/tr_id_pap.ma". +include "ground/relocation/tr_uni.ma". +include "ground/relocation/tr_pap_tls.ma". (* LIFT FOR PATH ***********************************************************) @@ -27,7 +28,7 @@ match p with [ list_empty ⇒ k f (𝐞) | list_lcons l q ⇒ match l with - [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (𝐢) q + [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (⇂*[n]f) q | label_m ⇒ lift_gen (A) (λg,p. k g (𝗺◗p)) f q | label_L ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q | label_A ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q @@ -60,7 +61,7 @@ lemma lift_empty (A) (k) (f): // qed. lemma lift_d_sn (A) (k) (p) (n) (f): - ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), 𝐢, p❩ = ↑{A}❨k, f, 𝗱n◗p❩. + ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), ⇂*[n]f, p❩ = ↑{A}❨k, f, 𝗱n◗p❩. // qed. lemma lift_m_sn (A) (k) (p) (f): @@ -92,7 +93,7 @@ lemma lift_rmap_empty (f): // qed. lemma lift_rmap_d_sn (f) (p) (n): - ↑[p]𝐢 = ↑[𝗱n◗p]f. + ↑[p](⇂*[ninj n]f) = ↑[𝗱n◗p]f. // qed. lemma lift_rmap_m_sn (f) (p): @@ -111,21 +112,12 @@ lemma lift_rmap_S_sn (f) (p): ↑[p]f = ↑[𝗦◗p]f. // qed. -(* Advanced cinstructionswith proj_rmap and tr_id ***************************) - -lemma lift_rmap_id (p): - (𝐢) = ↑[p]𝐢. -#p elim p -p // -* [ #n ] #p #IH // -qed. - (* Advanced constructions with proj_rmap and path_append ********************) lemma lift_rmap_append (p2) (p1) (f): ↑[p2]↑[p1]f = ↑[p1●p2]f. #p2 #p1 elim p1 -p1 // * [ #n ] #p1 #IH #f // -[ tr_compose_push_bi // +#p elim p -p [| * ] // [ #n ] #p #IH #f1 #f2 +[ 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 3bd7b43bc..772c837fb 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/substitution/lift_prototerm_eq.ma". +include "delayed_updating/substitution/lift_prototerm_id.ma". include "delayed_updating/substitution/lift_uni.ma". include "delayed_updating/syntax/prototerm_constructors.ma". @@ -24,24 +24,28 @@ lemma lift_iref_bi (t1) (t2) (n): qed. lemma lift_iref_sn (f) (t:prototerm) (n:pnat): - (𝛗f@❨n❩.t) ⊆ ↑[f](𝛗n.t). -#f #t #n #p * #q #Hq #H0 destruct -@(ex2_intro … (𝗱n◗𝗺◗q)) + (𝛗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_dx (f) (t) (n:pnat): - ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.t. + ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.↑[⇂*[n]f]t. #f #t #n #p * #q #Hq #H0 destruct elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct -/2 width=1 by in_comp_iref/ +/3 width=1 by in_comp_iref, in_comp_lift_bi/ qed-. lemma lift_iref (f) (t) (n:pnat): - (𝛗f@❨n❩.t) ⇔ ↑[f](𝛗n.t). + (𝛗f@❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛗n.t). /3 width=1 by conj, lift_iref_sn, lift_iref_dx/ qed. lemma lift_iref_uni (t) (m) (n): (𝛗(n+m).t) ⇔ ↑[𝐮❨m❩](𝛗n.t). -// qed. +#t #m #n +@(subset_eq_trans … (lift_iref …)) +nsucc_pnpred list_length_lcons >list_length_lcons // -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 55b271f8b..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 @@ -38,20 +38,3 @@ lemma lift_term_after (f1) (f2) (t): | @subset_equivalence_ext_f1_exteq /2 width=5/ ] qed. - -lemma lift_term_id_sn (t): - t ⊆ ↑[𝐢]t. -#t #p #Hp ->(lift_path_id p) -/2 width=1 by in_comp_lift_bi/ -qed-. - -lemma lift_term_id_dx (t): - ↑[𝐢]t ⊆ t. -#t #p * #q #Hq #H destruct // -qed-. - -lemma lift_term_id (t): - t ⇔ ↑[𝐢]t. -/3 width=2 by lift_term_id_dx, lift_term_id_sn, conj/ -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma new file mode 100644 index 000000000..cc7569284 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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_prototerm_eq.ma". +include "delayed_updating/substitution/lift_id.ma". + +lemma lift_term_id_sn (t): + t ⊆ ↑[𝐢]t. +#t #p #Hp +>(lift_path_id p) +/2 width=1 by in_comp_lift_bi/ +qed-. + +lemma lift_term_id_dx (t): + ↑[𝐢]t ⊆ t. +#t #p * #q #Hq #H destruct // +qed-. + +lemma lift_term_id (t): + t ⇔ ↑[𝐢]t. +/3 width=2 by lift_term_id_dx, lift_term_id_sn, conj/ +qed. 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 86a425975..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma +++ /dev/null @@ -1,35 +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". - -(* LIFT FOR PATH ***********************************************************) - -(* Constructions with structure ********************************************) - -lemma structure_lift (p) (f): - ⊗p = ⊗↑[f]p. -#p elim p -p // -* [ #n ] #p #IH #f // -[ nsucc_pnpred +IH -IH tr_pushs_swap IH -IH (list_length_inv_zero_sn … H0) -p // -| #k #IH * - [ #H0 elim (eq_inv_nsucc_zero … H0) - | * [ #n ] #p #H0 - lapply (eq_inv_nsucc_bi … H0) -H0 - [ cases p -p [ -IH | #l #p ] #H0 destruct // - (list_length_inv_zero_sn … H0) -p // -| #k #IH * - [ #n #H0 elim (eq_inv_nsucc_zero … H0) - | * [ #m ] #p #n #H0 - lapply (eq_inv_nsucc_bi … H0) -H0 - [ cases p -p [ -IH | #l #p ] #H0 destruct list_cons_shift tr_compose_pap // -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_rmap.ma deleted file mode 100644 index 9bb26750a..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_rmap.ma +++ /dev/null @@ -1,59 +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/unwind0/unwind1_rmap.ma". -include "delayed_updating/notation/functions/black_righttriangle_2.ma". - -(* EXTENDED UNWIND FOR RELOCATION MAP ***************************************) - -definition unwind2_rmap (f) (p): tr_map ≝ - (▶↑[f]p)∘(↑[p]f). - -interpretation - "extended unwind (relocation map)" - 'BlackRightTriangle f p = (unwind2_rmap f p). - -(* Basic constructions ******************************************************) - -lemma unwind2_rmap_unfold (f) (p): - (▶↑[f]p)∘(↑[p]f) = ▶[f]p. -// qed. - -lemma unwind2_rmap_m_sn (f) (p): - ▶[f]p = ▶[f](𝗺◗p). -#f #p -"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; "⊃"; "⊐"; ] ; ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ;