From 255976c0e9096f1f6931fdfc15bae04b5af96c0c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 8 Jun 2022 19:14:49 +0200 Subject: [PATCH] update in delayed_updating + some files parked --- .../etc/{lift1 => lift_k}/lift.etc | 26 ++++-------- .../{lift1 => lift_k}/lift_constructors.etc | 22 ++++++---- .../etc/{lift1 => lift_k}/lift_eq.etc | 39 +++++++---------- .../lift_path_after.etc} | 13 +++--- .../lift_path_id.etc} | 21 +++++----- .../etc/lift_k/lift_path_proper.etc | 42 +++++++++++++++++++ .../lift_uni.etc => lift_k/lift_path_uni.etc} | 12 ++++-- .../etc/{lift1 => lift_k}/lift_prototerm.etc | 0 .../{lift1 => lift_k}/lift_prototerm_eq.etc | 19 +-------- .../lift_prototerm_id.etc} | 34 ++++++++------- .../etc/lift_k/lift_prototerm_proper.etc | 36 ++++++++++++++++ .../delayed_updating/etc/prototerm_inner.etc | 37 ++++++++++++++++ 12 files changed, 198 insertions(+), 103 deletions(-) rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{lift1 => lift_k}/lift.etc (88%) rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{lift1 => lift_k}/lift_constructors.etc (74%) rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{lift1 => lift_k}/lift_eq.etc (88%) rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{lift1/lift_after.etc => lift_k/lift_path_after.etc} (84%) rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{lift1/lift_length.etc => lift_k/lift_path_id.etc} (76%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_path_proper.etc rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{lift1/lift_uni.etc => lift_k/lift_path_uni.etc} (86%) rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{lift1 => lift_k}/lift_prototerm.etc (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{lift1 => lift_k}/lift_prototerm_eq.etc (82%) rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{lift1/lift_structure.etc => lift_k/lift_prototerm_id.etc} (63%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_prototerm_proper.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/prototerm_inner.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift.etc similarity index 88% rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift.etc rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift.etc index e6e1e661e..b873ed303 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift.etc +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift.etc @@ -15,9 +15,10 @@ 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 ***********************************************************) +(* LIFT FOR PATH ************************************************************) definition lift_continuation (A:Type[0]) ≝ tr_map → path → A. @@ -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 // -[ nsucc_pnpred 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_after.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_path_after.etc similarity index 84% rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_after.etc rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_path_after.etc index 02b2c6ee1..869d680fe 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_after.etc +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_path_after.etc @@ -15,14 +15,17 @@ include "delayed_updating/substitution/lift_eq.ma". include "ground/relocation/tr_compose_pap.ma". include "ground/relocation/tr_compose_pn.ma". +include "ground/relocation/tr_compose_tls.ma". -(* LIFT FOR PATH ***********************************************************) +(* LIFT FOR PATH ************************************************************) -(* Constructions with tr_after *********************************************) +(* Constructions with tr_after **********************************************) lemma lift_path_after (p) (f1) (f2): ↑[f2]↑[f1]p = ↑[f2∘f1]p. -#p elim p -p [| * ] // #p #IH #f1 #f2 -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/etc/lift1/lift_length.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_path_id.etc similarity index 76% rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_length.etc rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_path_id.etc index 0576799af..1966c25f2 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_length.etc +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_path_id.etc @@ -13,19 +13,18 @@ (**************************************************************************) include "delayed_updating/substitution/lift_eq.ma". -include "ground/lib/list_length.ma". +include "ground/relocation/tr_id_pap.ma". +include "ground/relocation/tr_id_tls.ma". -(* LIFT FOR PATH ***********************************************************) +(* LIFT FOR PATH ************************************************************) -(* Constructions with list_length ******************************************) +(* Constructions with tr_id *************************************************) -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/lift_k/lift_path_proper.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_path_proper.etc new file mode 100644 index 000000000..0eef97896 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_path_proper.etc @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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_proper.ma". + +(* LIFT FOR PATH ************************************************************) + +(* Constructions with proper condition for path *****************************) + +lemma lift_path_proper (f) (p): + p ϵ 𝐏 → ↑[f]p ϵ 𝐏. +#f * +[ #H0 elim (ppc_inv_empty … H0) +| * [ #n ] #p #_ + [ nsucc_pnpred +(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/lift_k/lift_prototerm_id.etc similarity index 63% rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_structure.etc rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_prototerm_id.etc index 86a425975..b66b63f46 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_structure.etc +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_prototerm_id.etc @@ -12,24 +12,26 @@ (* *) (**************************************************************************) -include "delayed_updating/substitution/lift_eq.ma". -include "delayed_updating/syntax/path_structure.ma". +include "delayed_updating/substitution/lift_prototerm_eq.ma". +include "delayed_updating/substitution/lift_path_id.ma". -(* LIFT FOR PATH ***********************************************************) +(* LIFT FOR PROTOTERM *******************************************************) -(* Constructions with structure ********************************************) +(* Constructions with tr_id *************************************************) -lemma structure_lift (p) (f): - ⊗p = ⊗↑[f]p. -#p elim p -p // -* [ #n ] #p #IH #f // -[ (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_structure (p) (f): - ⊗p = ↑[f]⊗p. -#p elim p -p // -* [ #n ] #p #IH #f // +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_k/lift_prototerm_proper.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_prototerm_proper.etc new file mode 100644 index 000000000..a9b16219f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_k/lift_prototerm_proper.etc @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". +include "delayed_updating/substitution/lift_path_proper.ma". +include "delayed_updating/syntax/prototerm_proper.ma". + +(* LIFT FOR PROTOTERM *******************************************************) + +(* Constructions with proper condition for path *****************************) + +lemma lift_term_proper (f) (t): + t ϵ 𝐏 → ↑[f]t ϵ 𝐏. +#f #t #Ht #p * #q #Hq #H0 destruct +@lift_path_proper @Ht -Ht // (**) (* auto fails *) +qed. + +(* Inversions with proper condition for path ********************************) + +lemma lift_term_inv_proper (f) (t): + ↑[f]t ϵ 𝐏 → t ϵ 𝐏. +#f #t #Ht #p #Hp +@(lift_path_inv_proper f) +@Ht -Ht @in_comp_lift_bi // (**) (* auto fails *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/prototerm_inner.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/prototerm_inner.etc new file mode 100644 index 000000000..b2095a752 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/prototerm_inner.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.ma". +include "delayed_updating/syntax/path_inner.ma". +include "ground/lib/subset_ext_equivalence.ma". + +(* INNER CONDITION FOR PROTOTERM ********************************************) + +interpretation + "inner condition (prototerm)" + 'ClassI = (subset_ext_p1 path pic). + +(* Basic destructions *******************************************************) + +lemma in_comp_tic_trans (t) (p): + p ϵ t → t ϵ 𝐈 → p ϵ 𝐈. +#t #p #Hp #Ht +@(Ht … Hp) +qed-. + +(* Basic inversions *********************************************************) + +lemma tic_inv_d_dx (t) (p) (n): + p◖𝗱n ϵ t → t ϵ 𝐈 → ⊥. +/2 width=7 by in_comp_tic_trans/ qed-. -- 2.39.2