From: Ferruccio Guidi Date: Tue, 3 May 2022 20:45:16 +0000 (+0200) Subject: update in delayed_updating X-Git-Tag: make_still_working~76 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2c68dcfee2c3fe819c8f92a9609620a85909ce8a;p=helm.git update in delayed_updating + conflicts solved --- 2c68dcfee2c3fe819c8f92a9609620a85909ce8a diff --cc matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift.etc index 000000000,000000000..a487fcf5a new file mode 100644 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift.etc @@@ -1,0 -1,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 --cc matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_constructors.etc index 000000000,000000000..772c837fb new file mode 100644 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_constructors.etc @@@ -1,0 -1,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 --cc matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_id.etc index 000000000,000000000..1d8b45295 new file mode 100644 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_id.etc @@@ -1,0 -1,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 --cc matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_uni.etc index 000000000,000000000..cd6c79533 new file mode 100644 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_uni.etc @@@ -1,0 -1,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 ++