From: Ferruccio Guidi Date: Tue, 3 May 2022 18:31:58 +0000 (+0200) Subject: update in delayed_updating X-Git-Tag: make_still_working~77 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eba13527cf74de399b7e5b958901962666d4cd25;p=helm.git update in delayed_updating + closed paths + updated notation for height + some parked files added --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift.etc new file mode 100644 index 000000000..a487fcf5a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift.etc @@ -0,0 +1,150 @@ +(**************************************************************************) +(* ___ *) +(* ||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_uni.ma". +include "ground/relocation/tr_pap_tls.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)) (⇂*[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 + | 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)), ⇂*[n]f, 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](⇂*[ninj n]f) = ↑[𝗱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 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/lift/lift_constructors.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_constructors.etc new file mode 100644 index 000000000..772c837fb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_constructors.etc @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lift/lift_id.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_id.etc new file mode 100644 index 000000000..1d8b45295 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_id.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_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/lift/lift_uni.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_uni.etc new file mode 100644 index 000000000..cd6c79533 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_uni.etc @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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 +tr_id_unfold #Hn + lapply (pippo … b … Hn) -Hn #Hn + @tr_compose_eq_repl + [