From 00fca351072c2dba11b71c14b1169d303fd6836f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 9 Jun 2022 00:43:41 +0200 Subject: [PATCH] update in delayed_updating + lift changed to lift after unwind in ifr + notion of lift swapped again + some additions to prove a side condition of ifr_unwind_bi --- .../delayed_updating/reduction/dfr_ifr.ma | 14 ++++---- .../delayed_updating/reduction/ifr.ma | 4 +-- .../delayed_updating/reduction/ifr_unwind.ma | 32 ++++++++--------- .../delayed_updating/substitution/lift.ma | 24 ++++++++----- .../substitution/lift_constructors.ma | 20 +++++------ .../delayed_updating/substitution/lift_eq.ma | 35 +++++++++++-------- .../substitution/lift_path_after.ma | 9 ++--- .../{lift_path_id.ma => lift_path_length.ma} | 19 +++++----- ...prototerm_id.ma => lift_path_structure.ma} | 34 +++++++++--------- .../substitution/lift_path_uni.ma | 8 ++--- .../substitution/lift_prototerm_eq.ma | 17 +++++++++ .../syntax/path_inner_proper.ma | 26 ++++++++++++++ .../delayed_updating/syntax/path_proper.ma | 7 +++- .../syntax/prototerm_proper.ma | 11 +++--- .../syntax/prototerm_proper_inner.ma | 26 ++++++++++++++ .../unwind/unwind2_path_inner.ma | 28 +++++++++++++++ .../unwind/unwind2_preterm_fsubst.ma | 4 +-- .../unwind/unwind2_prototerm_inner.ma | 28 +++++++++++++++ 18 files changed, 239 insertions(+), 107 deletions(-) rename matita/matita/contribs/lambdadelta/delayed_updating/substitution/{lift_path_id.ma => lift_path_length.ma} (78%) rename matita/matita/contribs/lambdadelta/delayed_updating/substitution/{lift_prototerm_id.ma => lift_path_structure.ma} (65%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner_proper.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_inner.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_inner.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma index 8403b7781..be7f3b3d3 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma @@ -18,11 +18,9 @@ include "delayed_updating/reduction/ifr.ma". include "delayed_updating/unwind/unwind2_constructors.ma". include "delayed_updating/unwind/unwind2_preterm_fsubst.ma". include "delayed_updating/unwind/unwind2_preterm_eq.ma". -include "delayed_updating/unwind/unwind2_prototerm_lift.ma". include "delayed_updating/unwind/unwind2_rmap_head.ma". include "delayed_updating/substitution/fsubst_eq.ma". -include "delayed_updating/substitution/lift_prototerm_eq.ma". include "delayed_updating/syntax/prototerm_proper_constructors.ma". include "delayed_updating/syntax/path_head_structure.ma". @@ -38,12 +36,12 @@ theorem dfr_des_ifr (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 → t1 ➡𝐝𝐟[p,q] t2 → ▼[f]t1 ➡𝐟[⊗p,⊗q] ▼[f]t2. #f #p #q #t1 #t2 #H0t1 * #n * #H1n #Ht1 #Ht2 -@(ex_intro … (↑♭⊗q)) @and3_intro +@(ex_intro … (↑♭q)) @and3_intro [ -H0t1 -Ht1 -Ht2 >structure_L_sn >structure_reverse >H1n >path_head_structure_depth list_append_rcons_sn in H1n; list_append_rcons_sn in H1n; nrplus_inj_dx in ⊢ (???%); structure_L_sn >structure_reverse >H1n >path_head_structure_depth list_append_rcons_sn in H1n; list_append_rcons_sn in H1n; nrplus_inj_dx in ⊢ (???%); nsucc_pnpred nrplus_inj_dx /2 width=1 by tr_tls_compose_uni_dx/ qed. - *) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_after.ma index 869d680fe..938d21534 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_after.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_after.ma @@ -15,7 +15,6 @@ 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 ************************************************************) @@ -23,9 +22,7 @@ include "ground/relocation/tr_compose_tls.ma". lemma lift_path_after (p) (f1) (f2): ↑[f2]↑[f1]p = ↑[f2∘f1]p. -#p elim p -p [| * ] // [ #n ] #p #IH #f1 #f2 -[ tr_compose_push_bi // -] +#p elim p -p [| * ] // #p #IH #f1 #f2 +tr_compose_push_bi // qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_id.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_length.ma similarity index 78% rename from matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_id.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_length.ma index 1966c25f2..f384cf746 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_id.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_length.ma @@ -13,18 +13,19 @@ (**************************************************************************) include "delayed_updating/substitution/lift_eq.ma". -include "ground/relocation/tr_id_pap.ma". -include "ground/relocation/tr_id_tls.ma". +include "ground/lib/list_length.ma". (* LIFT FOR PATH ************************************************************) -(* Constructions with tr_id *************************************************) +(* Constructions with list_length *******************************************) -lemma lift_path_id (p): - p = ↑[𝐢]p. -#p elim p -p // -* [ #n ] #p #IH // -[ list_length_lcons >list_length_lcons // qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_structure.ma similarity index 65% rename from matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_structure.ma index b66b63f46..15d6e0933 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_structure.ma @@ -12,26 +12,24 @@ (* *) (**************************************************************************) -include "delayed_updating/substitution/lift_prototerm_eq.ma". -include "delayed_updating/substitution/lift_path_id.ma". +include "delayed_updating/substitution/lift_eq.ma". +include "delayed_updating/syntax/path_structure.ma". -(* LIFT FOR PROTOTERM *******************************************************) +(* LIFT FOR PATH ************************************************************) -(* Constructions with tr_id *************************************************) +(* Constructions with structure *********************************************) -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 structure_lift_path (p) (f): + ⊗p = ⊗↑[f]p. +#p elim p -p // +* [ #n ] #p #IH #f // +[ 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/syntax/path_inner_proper.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner_proper.ma new file mode 100644 index 000000000..042df447b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner_proper.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/path_inner.ma". +include "delayed_updating/syntax/path_proper.ma". + +(* INNER CONDITION FOR PATH *************************************************) + +(* Destructions with proper condition for path ******************************) + +lemma path_des_outer_proper (p): + p ⧸ϵ 𝐈 → p ϵ 𝐏. +#p #H1 #H2 destruct +@H1 -H1 // (**) (* auto fails *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma index 9cab60b87..ff6a53c39 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma @@ -30,7 +30,12 @@ interpretation (* Basic constructions ******************************************************) lemma ppc_lcons (l) (q): l◗q ϵ 𝐏. -#l #p #H destruct +#l #q #H0 destruct +qed. + +lemma ppc_rcons (l) (q): q◖l ϵ 𝐏. +#l #q #H +elim (eq_inv_list_empty_rcons ??? H) qed. (* Basic inversions ********************************************************) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper.ma index b2bb92cf8..31fa1ca4a 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper.ma @@ -30,13 +30,16 @@ lemma tpc_i (t): #H elim (Ht H) qed. -(* Basic inversions *********************************************************) +(* Basic destructions *******************************************************) -lemma in_ppc_comp_trans (t) (p): +lemma in_comp_tpc_trans (t) (p): p ϵ t → t ϵ 𝐏 → p ϵ 𝐏. #t #p #Hp #Ht @(Ht … Hp) qed-. -lemma tpc_e (t): 𝐞 ϵ t → t ϵ 𝐏 → ⊥. -/2 width=5 by in_ppc_comp_trans/ qed-. +(* Basic inversions *********************************************************) + +lemma tpc_inv_empty (t): + (𝐞) ϵ t → t ϵ 𝐏 → ⊥. +/2 width=5 by in_comp_tpc_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_inner.ma new file mode 100644 index 000000000..e3665476b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_inner.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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_proper.ma". +include "delayed_updating/syntax/path_inner_proper.ma". +include "ground/lib/subset_overlap.ma". + +(* PROPER CONDITION FOR PROTOTERM *******************************************) + +(* Constructions with inner condition for prototerm *************************) + +lemma term_proper_outer (t): + t ⧸≬ 𝐈 → t ϵ 𝐏. +/4 width=3 by path_des_outer_proper, subset_ol_i/ +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_inner.ma new file mode 100644 index 000000000..2ec01a2f6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_inner.ma @@ -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/unwind/unwind2_path_structure.ma". +include "delayed_updating/syntax/path_inner.ma". + +(* UNWIND FOR PATH **********************************************************) + +(* Destructions with inner condition for path *******************************) + +lemma unwind2_path_des_inner (f) (p): + ▼[f]p ϵ 𝐈 → p ϵ 𝐈. +#f #p @(list_ind_rcons … p) -p // +#p * [ #n ] #_ // +unwind2_path_append_proper_dx - /4 width=5 by in_comp_unwind2_path_term, in_ppc_comp_trans, or_introl, ex2_intro/ + /4 width=5 by in_comp_unwind2_path_term, in_comp_tpc_trans, or_introl, ex2_intro/ | * #q #Hq #H1 #H0 @(ex2_intro … H1) @or_intror @conj // * [