From: Ferruccio Guidi Date: Wed, 8 Jun 2022 22:43:41 +0000 (+0200) Subject: update in delayed_updating X-Git-Tag: make_still_working~62 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=00fca351072c2dba11b71c14b1169d303fd6836f;hp=6f1b6f85a78d4c8da42f035f433fe4b85962bd9b;p=helm.git 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 --- 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_id.ma deleted file mode 100644 index 1966c25f2..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_id.ma +++ /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 // -[ list_length_lcons >list_length_lcons // +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_structure.ma new file mode 100644 index 000000000..15d6e0933 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_structure.ma @@ -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_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/substitution/lift_prototerm_id.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma deleted file mode 100644 index b66b63f46..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma +++ /dev/null @@ -1,37 +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_eq.ma". -include "delayed_updating/substitution/lift_path_id.ma". - -(* LIFT FOR PROTOTERM *******************************************************) - -(* Constructions with tr_id *************************************************) - -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/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 // * [