From 713673ecf863cb6187291f016ed4490b12a03ac0 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 16 Apr 2013 19:45:41 +0000 Subject: [PATCH] - we commit just the components before "reducibility" - reaxiomatized substitution and reduction now commute with respect to subclosure - delift and thin removed for now --- .../cpr/aaa_ltpss_dx.etc} | 0 .../cpr/aaa_ltpss_sn.etc} | 0 .../lambdadelta/basic_2/etc/cpr/cpr.etc | 111 ++++++++ .../lambdadelta/basic_2/etc/cpr/cpr_lift.etc | 180 ++++++++++++ .../lambdadelta/basic_2/etc/cpr/ltpr.etc | 67 +++++ .../basic_2/etc/cpr/ltpr_ldrop.etc | 45 +++ .../lambdadelta/basic_2/etc/cpr/ltpr_ltpr.etc | 29 ++ .../ltpss_dx.ma => etc/cpr/ltpss_dx.etc} | 0 .../cpr/ltpss_dx_ldrop.etc} | 0 .../cpr/ltpss_dx_ltpss_dx.etc} | 0 .../cpr/ltpss_dx_tps.etc} | 0 .../cpr/ltpss_dx_tpss.etc} | 0 .../ltpss_sn.ma => etc/cpr/ltpss_sn.etc} | 0 .../cpr/ltpss_sn_alt.etc} | 0 .../cpr/ltpss_sn_ldrop.etc} | 0 .../cpr/ltpss_sn_ltpss_sn.etc} | 0 .../cpr/ltpss_sn_tps.etc} | 0 .../cpr/ltpss_sn_tpss.etc} | 0 .../cpr/ssta_ltpss_dx.etc} | 0 .../cpr/ssta_ltpss_sn.etc} | 0 .../cpr/sstas_ltpss_dx.etc} | 0 .../cpr/sstas_ltpss_sn.etc} | 0 .../lambdadelta/basic_2/etc/cpr/tpr.etc | 242 ++++++++++++++++ .../lambdadelta/basic_2/etc/cpr/tpr_lift.etc | 121 ++++++++ .../lambdadelta/basic_2/etc/cpr/tpr_tpr.etc | 261 ++++++++++++++++++ .../{substitution/tps.ma => etc/cpr/tps.etc} | 0 .../tps_lift.ma => etc/cpr/tps_lift.etc} | 0 .../tps_tps.ma => etc/cpr/tps_tps.etc} | 0 .../{unfold/tpss.ma => etc/cpr/tpss.etc} | 0 .../tpss_alt.ma => etc/cpr/tpss_alt.etc} | 0 .../tpss_lift.ma => etc/cpr/tpss_lift.etc} | 0 .../tpss_tpss.ma => etc/cpr/tpss_tpss.etc} | 0 .../delift.ma => etc/delift/delift.etc} | 0 .../delift/delift_alt.etc} | 0 .../delift/delift_delift.etc} | 0 .../delift/delift_lift.etc} | 0 .../delift/delift_ltpss.etc} | 0 .../delift/delift_tpss.etc} | 0 .../{unfold/thin.ma => etc/delift/thin.etc} | 0 .../delift/thin_delift.etc} | 0 .../delift/thin_ldrop.etc} | 0 .../lambdadelta/basic_2/grammar/lenv_px_sn.ma | 47 +++- .../contribs/lambdadelta/basic_2/notation.ma | 16 +- .../lambdadelta/basic_2/restricted/cpqs.ma | 3 +- .../lambdadelta/basic_2/restricted/lpqs.ma | 11 +- .../basic_2/restricted/lpqs_cpqs.ma | 4 +- .../basic_2/restricted/lpqs_lpqs.ma | 2 +- .../lambdadelta/basic_2/static/aaa_lpss.ma | 54 ++++ .../lambdadelta/basic_2/static/ssta_lpss.ma | 81 ++++++ .../{etc/fsup/fsups.etc => unfold/fsups.ma} | 5 +- .../fsups_fsups.etc => unfold/fsups_fsups.ma} | 2 +- .../lambdadelta/basic_2/unfold/lpss.ma | 12 +- .../lambdadelta/basic_2/unfold/lpss_cpss.ma | 4 +- .../lambdadelta/basic_2/unwind/sstas_lpss.ma | 39 +++ .../lambdadelta/basic_2/web/basic_2.ldw.xml | 5 + .../lambdadelta/basic_2/web/basic_2_src.tbl | 30 +- matita/matita/predefined_virtuals.ml | 4 +- 57 files changed, 1325 insertions(+), 50 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{static/aaa_ltpss_dx.ma => etc/cpr/aaa_ltpss_dx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{static/aaa_ltpss_sn.ma => etc/cpr/aaa_ltpss_sn.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_lift.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_ldrop.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_ltpr.etc rename matita/matita/contribs/lambdadelta/basic_2/{unfold/ltpss_dx.ma => etc/cpr/ltpss_dx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/ltpss_dx_ldrop.ma => etc/cpr/ltpss_dx_ldrop.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/ltpss_dx_ltpss_dx.ma => etc/cpr/ltpss_dx_ltpss_dx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/ltpss_dx_tps.ma => etc/cpr/ltpss_dx_tps.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/ltpss_dx_tpss.ma => etc/cpr/ltpss_dx_tpss.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/ltpss_sn.ma => etc/cpr/ltpss_sn.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/ltpss_sn_alt.ma => etc/cpr/ltpss_sn_alt.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/ltpss_sn_ldrop.ma => etc/cpr/ltpss_sn_ldrop.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/ltpss_sn_ltpss_sn.ma => etc/cpr/ltpss_sn_ltpss_sn.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/ltpss_sn_tps.ma => etc/cpr/ltpss_sn_tps.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/ltpss_sn_tpss.ma => etc/cpr/ltpss_sn_tpss.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{static/ssta_ltpss_dx.ma => etc/cpr/ssta_ltpss_dx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{static/ssta_ltpss_sn.ma => etc/cpr/ssta_ltpss_sn.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unwind/sstas_ltpss_dx.ma => etc/cpr/sstas_ltpss_dx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unwind/sstas_ltpss_sn.ma => etc/cpr/sstas_ltpss_sn.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpr.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpr_lift.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpr_tpr.etc rename matita/matita/contribs/lambdadelta/basic_2/{substitution/tps.ma => etc/cpr/tps.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/tps_lift.ma => etc/cpr/tps_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/tps_tps.ma => etc/cpr/tps_tps.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/tpss.ma => etc/cpr/tpss.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/tpss_alt.ma => etc/cpr/tpss_alt.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/tpss_lift.ma => etc/cpr/tpss_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/tpss_tpss.ma => etc/cpr/tpss_tpss.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/delift.ma => etc/delift/delift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/delift_alt.ma => etc/delift/delift_alt.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/delift_delift.ma => etc/delift/delift_delift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/delift_lift.ma => etc/delift/delift_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/delift_ltpss.ma => etc/delift/delift_ltpss.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/delift_tpss.ma => etc/delift/delift_tpss.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/thin.ma => etc/delift/thin.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/thin_delift.ma => etc/delift/thin_delift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/thin_ldrop.ma => etc/delift/thin_ldrop.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/aaa_lpss.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/ssta_lpss.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc/fsup/fsups.etc => unfold/fsups.ma} (99%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/fsup/fsups_fsups.etc => unfold/fsups_fsups.ma} (97%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lpss.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/aaa_ltpss_dx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/static/aaa_ltpss_dx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/aaa_ltpss_dx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/aaa_ltpss_sn.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/static/aaa_ltpss_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/aaa_ltpss_sn.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr.etc new file mode 100644 index 000000000..d82299c38 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr.etc @@ -0,0 +1,111 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/unfold/tpss.ma". +include "basic_2/reducibility/tpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) + +(* Basic_1: includes: pr2_delta1 *) +definition cpr: lenv → relation term ≝ + λL,T1,T2. ∃∃T. T1 ➡ T & L ⊢ T ▶* [0, |L|] T2. + +interpretation + "context-sensitive parallel reduction (term)" + 'PRed L T1 T2 = (cpr L T1 T2). + +(* Basic properties *********************************************************) + +lemma cpr_intro: ∀L,T1,T,T2,d,e. T1 ➡ T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ➡ T2. +/3 width=5/ qed-. + +(* Basic_1: was by definition: pr2_free *) +lemma cpr_tpr: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ T1 ➡ T2. +/2 width=3/ qed. + +lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ➡ T2. +/3 width=5/ qed. + +lemma cpr_refl: ∀L,T. L ⊢ T ➡ T. +/2 width=1/ qed. + +(* Note: new property *) +(* Basic_1: was only: pr2_thin_dx *) +lemma cpr_flat: ∀I,L,V1,V2,T1,T2. + L ⊢ V1 ➡ V2 → L ⊢ T1 ➡ T2 → L ⊢ ⓕ{I} V1. T1 ➡ ⓕ{I} V2. T2. +#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/ +qed. + +lemma cpr_cast: ∀L,V,T1,T2. + L ⊢ T1 ➡ T2 → L ⊢ ⓝV. T1 ➡ T2. +#L #V #T1 #T2 * /3 width=3/ +qed. + +(* Note: it does not hold replacing |L1| with |L2| *) +(* Basic_1: was only: pr2_change *) +lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 → + ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2. +#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 +lapply (tpss_lsubr_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/ +qed. + +(* Basic inversion lemmas ***************************************************) + +(* Basic_1: was: pr2_gen_csort *) +lemma cpr_inv_atom: ∀T1,T2. ⋆ ⊢ T1 ➡ T2 → T1 ➡ T2. +#T1 #T2 * #T #HT normalize #HT2 +<(tpss_inv_refl_O2 … HT2) -HT2 // +qed-. + +(* Basic_1: was: pr2_gen_sort *) +lemma cpr_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ➡ T2 → T2 = ⋆k. +#L #T2 #k * #X #H +>(tpr_inv_atom1 … H) -H #H +>(tpss_inv_sort1 … H) -H // +qed-. + +(* Basic_1: was: pr2_gen_cast *) +lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ ⓝV1. T1 ➡ U2 → ( + ∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ T1 ➡ T2 & + U2 = ⓝV2. T2 + ) ∨ L ⊢ T1 ➡ U2. +#L #V1 #T1 #U2 * #X #H #HU2 +elim (tpr_inv_cast1 … H) -H /3 width=3/ +* #V #T #HV1 #HT1 #H destruct +elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/ +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma cpr_fwd_bind1_minus: ∀I,L,V1,T1,T. L ⊢ -ⓑ{I}V1.T1 ➡ T → ∀b. + ∃∃V2,T2. L ⊢ ⓑ{b,I}V1.T1 ➡ ⓑ{b,I}V2.T2 & + T = -ⓑ{I}V2.T2. +#I #L #V1 #T1 #T * #X #H1 #H2 #b +elim (tpr_fwd_bind1_minus … H1 b) -H1 #V0 #T0 #HT10 #H destruct +elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/ +qed-. + +lemma cpr_fwd_shift1: ∀L,L1,T1,T. L ⊢ L1 @@ T1 ➡ T → + ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. +#L #L1 #T1 #T * #X #H1 #H2 +elim (tpr_fwd_shift1 … H1) -H1 #L0 #T0 #HL10 #H destruct +elim (tpss_fwd_shift1 … H2) -H2 #L2 #T2 #HL02 #H destruct /2 width=4/ +qed-. + +(* Basic_1: removed theorems 6: + pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans + pr2_gen_ctail pr2_ctail + Basic_1: removed local theorems 3: + pr2_free_free pr2_free_delta pr2_delta_delta +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_lift.etc new file mode 100644 index 000000000..0a7afddab --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_lift.etc @@ -0,0 +1,180 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/unfold/tpss_lift.ma". +include "basic_2/reducibility/tpr_lift.ma". +include "basic_2/reducibility/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) + +(* Advanced properties ******************************************************) + +lemma cpr_cdelta: ∀L,K,V1,W1,W2,i. + ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 ▶* [0, |L| - i - 1] W1 → + ⇧[0, i + 1] W1 ≡ W2 → L ⊢ #i ➡ W2. +#L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12 +lapply (ldrop_fwd_ldrop2_length … HLK) #Hi +@ex2_intro [2: // | skip | @tpss_subst /width=6/ ] (**) (* /3 width=6/ is too slow *) +qed. + +lemma cpr_abst: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡ T2 → + ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡ ⓑ{a,I}V2. T2. +#L #V1 #V2 * #V0 #HV10 #HV02 #V #T1 #T2 * #T0 #HT10 #HT02 #a #I +lapply (tpss_inv_S2 … HT02 L V ?) -HT02 // #HT02 +lapply (tpss_lsubr_trans … HT02 (L.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02 +@(ex2_intro … (ⓑ{a,I}V0.T0)) /2 width=1/ (* explicit constructors *) +qed. + +lemma cpr_beta: ∀a,L,V1,V2,W,T1,T2. + L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛ{a}W.T1 ➡ ⓓ{a}V2.T2. +#a #L #V1 #V2 #W #T1 #T2 * #V #HV1 #HV2 * #T #HT1 #HT2 +lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2 +lapply (tpss_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2 +@(ex2_intro … (ⓓ{a}V.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too slow *) +qed. + +lemma cpr_beta_dx: ∀a,L,V1,V2,W,T1,T2. + V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛ{a}W.T1 ➡ ⓓ{a}V2.T2. +/3 width=1/ qed. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was: pr2_gen_lref *) +lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ➡ T2 → + T2 = #i ∨ + ∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 & + K ⊢ V1 ▶* [0, |L| - i - 1] T1 & + ⇧[0, i + 1] T1 ≡ T2 & + i < |L|. +#L #T2 #i * #X #H +>(tpr_inv_atom1 … H) -H #H +elim (tpss_inv_lref1 … H) -H /2 width=1/ +* /3 width=6/ +qed-. + +(* Basic_1: was pr2_gen_abbr *) +lemma cpr_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1. T1 ➡ U2 → + (∃∃V,V2,T2. V1 ➡ V & L ⊢ V ▶* [O, |L|] V2 & + L. ⓓV ⊢ T1 ➡ T2 & + U2 = ⓓ{a}V2. T2 + ) ∨ + ∃∃T2. L.ⓓV1 ⊢ T1 ➡ T2 & ⇧[0,1] U2 ≡ T2 & a = true. +#a #L #V1 #T1 #Y * #X #H1 #H2 +elim (tpr_inv_abbr1 … H1) -H1 * +[ #V #T #T0 #HV1 #HT1 #HT0 #H destruct + elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT02 #H destruct + lapply (tps_lsubr_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0 + lapply (tps_weak_full … HT0) -HT0 #HT0 + lapply (tpss_lsubr_trans … HT02 (L. ⓓV) ?) -HT02 /2 width=1/ #HT02 + lapply (tpss_weak_full … HT02) -HT02 #HT02 + lapply (tpss_strap2 … HT0 HT02) -T0 /4 width=7/ +| #T2 #HT12 #HXT2 #H destruct + elim (lift_total Y 0 1) #Z #HYZ + lapply (tpss_lift_ge … H2 (L.ⓓV1) … HXT2 … HYZ) -X // /2 width=1/ #H + lapply (cpr_intro … HT12 … H) -T2 /3 width=3/ +] +qed-. + +(* Basic_1: was: pr2_gen_abst *) +lemma cpr_inv_abst1: ∀a,L,V1,T1,U2. L ⊢ ⓛ{a}V1. T1 ➡ U2 → ∀I,W. + ∃∃V2,T2. L ⊢ V1 ➡ V2 & L. ⓑ{I} W ⊢ T1 ➡ T2 & U2 = ⓛ{a}V2. T2. +#a #L #V1 #T1 #Y * #X #H1 #H2 #I #W +elim (tpr_inv_abst1 … H1) -H1 #V #T #HV1 #HT1 #H destruct +elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct +lapply (tpss_lsubr_trans … HT2 (L. ⓑ{I} W) ?) -HT2 /2 width=1/ /4 width=5/ +qed-. + +(* Basic_1: was pr2_gen_appl *) +lemma cpr_inv_appl1: ∀L,V1,U0,U2. L ⊢ ⓐV1. U0 ➡ U2 → + ∨∨ ∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ U0 ➡ T2 & + U2 = ⓐV2. T2 + | ∃∃a,V2,W,T1,T2. L ⊢ V1 ➡ V2 & L. ⓓV2 ⊢ T1 ➡ T2 & + U0 = ⓛ{a}W. T1 & + U2 = ⓓ{a}V2. T2 + | ∃∃a,V2,V,W1,W2,T1,T2. L ⊢ V1 ➡ V2 & L ⊢ W1 ➡ W2 & L. ⓓW2 ⊢ T1 ➡ T2 & + ⇧[0,1] V2 ≡ V & + U0 = ⓓ{a}W1. T1 & + U2 = ⓓ{a}W2. ⓐV. T2. +#L #V1 #U0 #Y * #X #H1 #H2 +elim (tpr_inv_appl1 … H1) -H1 * +[ #V #U #HV1 #HU0 #H destruct + elim (tpss_inv_flat1 … H2) -H2 #V2 #U2 #HV2 #HU2 #H destruct /4 width=5/ +| #a #V #W #T0 #T #HV1 #HT0 #H #H1 destruct + elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct + lapply (tpss_weak … HT2 0 (|L|+1) ? ?) -HT2 // /4 width=9/ +| #a #V0 #V #W #W0 #T #T0 #HV10 #HW0 #HT0 #HV0 #H #H1 destruct + elim (tpss_inv_bind1 … H2) -H2 #W2 #X #HW02 #HX #HY destruct + elim (tpss_inv_flat1 … HX) -HX #V2 #T2 #HV2 #HT2 #H destruct + elim (tpss_inv_lift1_ge … HV2 … HV0 ?) -V // [3: /2 width=1/ |2: skip ] #V shift_append_assoc normalize #H + elim (tpr_inv_bind1 … H) -H * + [ #V0 #T0 #X0 #_ #HT10 #H0 #H destruct + elim (IH … HT10) -IH -T1 #L #T #HL1 #H destruct + elim (tps_fwd_shift1 … H0) -T #L2 #T2 #HL2 #H destruct + >append_length >HL1 >HL2 -L1 -L + @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *) + | #T #_ #_ #H destruct + ] +] +qed-. + +(* Basic_1: removed theorems 3: + pr0_subst0_back pr0_subst0_fwd pr0_subst0 +*) +(* Basic_1: removed local theorems: 1: pr0_delta_tau *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpr_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpr_lift.etc new file mode 100644 index 000000000..8d6b0363a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpr_lift.etc @@ -0,0 +1,121 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/substitution/tps_lift.ma". +include "basic_2/reducibility/tpr.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) + +(* Relocation properties ****************************************************) + +(* Basic_1: was: pr0_lift *) +lemma tpr_lift: t_liftable tpr. +#T1 #T2 #H elim H -T1 -T2 +[ * #i #U1 #d #e #HU1 #U2 #HU2 + lapply (lift_mono … HU1 … HU2) -HU1 #H destruct + [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct // + | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct // + | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct // + ] +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #X1 #d #e #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct + elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct /3 width=4/ +| #a #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #X1 #d #e #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct + elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct + elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct /3 width=4/ +| #a #I #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV12 #IHT1 #X1 #d #e #HX1 #X2 #HX2 + elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct + elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct + elim (lift_total T (d + 1) e) #U #HTU + @tpr_delta + [4: @(tps_lift_le … HT2 … HTU HTU0 ?) /2 width=1/ |1: skip |2: /2 width=4/ |3: /2 width=4/ ] (**) (*/3. is too slow *) +| #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #X1 #d #e #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct + elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct + elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct + elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct + elim (lift_trans_ge … HV2 … HV3 ?) -V // /3 width=4/ +| #V #T1 #T #T2 #_ #HT2 #IHT1 #X #d #e #H #U2 #HTU2 + elim (lift_inv_bind1 … H) -H #V3 #T3 #_ #HT13 #H destruct -V + elim (lift_conf_O1 … HTU2 … HT2) -T2 /3 width=4/ +| #V #T1 #T2 #_ #IHT12 #X #d #e #HX #T #HT2 + elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct /3 width=4/ +] +qed. + +(* Basic_1: was: pr0_gen_lift *) +lemma tpr_inv_lift1: t_deliftable_sn tpr. +#T1 #T2 #H elim H -T1 -T2 +[ * #i #X #d #e #HX + [ lapply (lift_inv_sort2 … HX) -HX #H destruct /2 width=3/ + | lapply (lift_inv_lref2 … HX) -HX * * #Hid #H destruct /3 width=3/ + | lapply (lift_inv_gref2 … HX) -HX #H destruct /2 width=3/ + ] +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #X #d #e #HX + elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct + elim (IHV12 … HV01) -V1 + elim (IHT12 … HT01) -T1 /3 width=5/ +| #a #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #X #d #e #HX + elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct + elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct + elim (IHV12 … HV01) -V1 + elim (IHT12 … HT01) -T1 /3 width=5/ +| #a #I #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV12 #IHT1 #X #d #e #HX + elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct + elim (IHV12 … HWV1) -V1 #W2 #HWV2 #HW12 + elim (IHT1 … HUT1) -T1 #U #HUT #HU1 + elim (tps_inv_lift1_le … HT2 … HUT ?) -T // [3: /2 width=5/ |2: skip ] #U2 #HU2 #HUT2 + @ex2_intro [2: /2 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /3 width=5/ is slow *) +| #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #X #d #e #HX + elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct + elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct + elim (IHV12 … HV01) -V1 #V3 #HV32 #HV03 + elim (IHW12 … HW01) -W1 #W3 #HW32 #HW03 + elim (IHT12 … HT01) -T1 #T3 #HT32 #HT03 + elim (lift_trans_le … HV32 … HV2 ?) -V2 // #V2 #HV32 #HV2 + @ex2_intro [2: /3 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *) +| #V #T1 #T #T2 #_ #HT2 #IHT1 #X #d #e #HX + elim (lift_inv_bind2 … HX) -HX #V3 #T3 #_ #HT31 #H destruct + elim (IHT1 … HT31) -T1 #T1 #HT1 #HT31 + elim (lift_div_le … HT2 … HT1 ?) -T // /3 width=5/ +| #V #T1 #T2 #_ #IHT12 #X #d #e #HX + elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct + elim (IHT12 … HT01) -T1 /3 width=3/ +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was pr0_gen_abst *) +lemma tpr_inv_abst1: ∀a,V1,T1,U2. ⓛ{a}V1. T1 ➡ U2 → + ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛ{a}V2. T2. +#a #V1 #T1 #U2 #H elim (tpr_inv_bind1 … H) -H * +[ #V2 #T #T2 #HV12 #HT1 #HT2 + lapply (tps_inv_refl_SO2 … HT2 ???) -HT2 // /2 width=5/ +| #T2 #_ #_ #_ #H destruct +] +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma tpr_fwd_abst1: ∀a,V1,T1,U2. ⓛ{a}V1.T1 ➡ U2 → ∀b,I,W. + ∃∃V2,T2. ⓑ{b,I}W.T1 ➡ ⓑ{b,I}W.T2 & + U2 = ⓛ{a}V2.T2. +#a #V1 #T1 #U2 #H #b #I #W elim (tpr_inv_bind1 … H) -H * +[ #V2 #T #T2 #HV12 #HT1 #HT2 + lapply (tps_inv_refl_SO2 … HT2 ???) -HT2 // /3 width=4/ +| #T2 #_ #_ #_ #H destruct +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpr_tpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpr_tpr.etc new file mode 100644 index 000000000..a733345bf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpr_tpr.etc @@ -0,0 +1,261 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/reducibility/ltpr_tpss.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) + +(* Confluence lemmas ********************************************************) + +fact tpr_conf_atom_atom: ∀I. ∃∃X. ⓪{I} ➡ X & ⓪{I} ➡ X. +/2 width=3/ qed. + +fact tpr_conf_flat_flat: + ∀I,V0,V1,T0,T1,V2,T2. ( + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → + ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → + ∃∃X. X1 ➡ X & X2 ➡ X + ) → + V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 → + ∃∃T0. ⓕ{I} V1. T1 ➡ T0 & ⓕ{I} V2. T2 ➡ T0. +#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 +elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2 +elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=5/ +qed. + +fact tpr_conf_flat_beta: + ∀a,V0,V1,T1,V2,W0,U0,T2. ( + ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{U0} + 1) + 1 → + ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → + ∃∃X. X1 ➡ X & X2 ➡ X + ) → + V0 ➡ V1 → V0 ➡ V2 → + U0 ➡ T2 → ⓛ{a}W0. U0 ➡ T1 → + ∃∃X. ⓐV1. T1 ➡ X & ⓓ{a}V2. T2 ➡ X. +#a #V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H +elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct +elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 +elim (IH … HT02 … HU01) -HT02 -HU01 -IH /2 width=1/ /3 width=5/ +qed. + +(* Basic-1: was: + pr0_cong_upsilon_refl pr0_cong_upsilon_zeta + pr0_cong_upsilon_cong pr0_cong_upsilon_delta +*) +fact tpr_conf_flat_theta: + ∀a,V0,V1,T1,V2,V,W0,W2,U0,U2. ( + ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{U0} + 1) + 1 → + ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → + ∃∃X. X1 ➡ X & X2 ➡ X + ) → + V0 ➡ V1 → V0 ➡ V2 → ⇧[O,1] V2 ≡ V → + W0 ➡ W2 → U0 ➡ U2 → ⓓ{a}W0. U0 ➡ T1 → + ∃∃X. ⓐV1. T1 ➡ X & ⓓ{a}W2. ⓐV. U2 ➡ X. +#a #V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H +elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #VV #HVV1 #HVV2 +elim (lift_total VV 0 1) #VVV #HVV +lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV +elim (tpr_inv_abbr1 … H) -H * +(* case 1: delta *) +[ -HV2 -HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct + elim (IH … HW02 … HWW2) -HW02 -HWW2 /2 width=1/ #W #HW02 #HWW2 + elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH /2 width=1/ #U #HU2 #HUUU2 + elim (tpr_tps_conf_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1 + @ex2_intro + [2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ] + |1:skip + |3: @tpr_delta [3: @tpr_flat |1: skip ] /2 width=5/ + ] (**) (* /5 width=14/ is too slow *) +(* case 3: zeta *) +| -HV2 -HW02 -HVV2 #U1 #HU01 #HTU1 + elim (IH … HU01 … HU02) -HU01 -HU02 -IH // -U0 #U #HU1 #HU2 + elim (tpr_inv_lift1 … HU1 … HTU1) -U1 #UU #HUU #HT1UU #H destruct + @(ex2_intro … (ⓐVV.UU)) /2 width=1/ /3 width=5/ (**) (* /4 width=9/ is too slow *) +] +qed. + +fact tpr_conf_flat_cast: + ∀X2,V0,V1,T0,T1. ( + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → + ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → + ∃∃X. X1 ➡ X & X2 ➡ X + ) → + V0 ➡ V1 → T0 ➡ T1 → T0 ➡ X2 → + ∃∃X. ⓝV1. T1 ➡ X & X2 ➡ X. +#X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02 +elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=3/ +qed. + +fact tpr_conf_beta_beta: + ∀a. ∀W0:term. ∀V0,V1,T0,T1,V2,T2. ( + ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{T0} + 1) + 1 → + ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → + ∃∃X. X1 ➡ X & X2 ➡ X + ) → + V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 → + ∃∃X. ⓓ{a}V1. T1 ➡X & ⓓ{a}V2. T2 ➡ X. +#a #W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 +elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ +elim (IH … HT01 … HT02) -HT01 -HT02 -IH /2 width=1/ /3 width=5/ +qed. + +(* Basic_1: was: pr0_cong_delta pr0_delta_delta *) +fact tpr_conf_delta_delta: + ∀a,I1,V0,V1,T0,T1,TT1,V2,T2,TT2. ( + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → + ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → + ∃∃X. X1 ➡ X & X2 ➡ X + ) → + V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 → + ⋆. ⓑ{I1} V1 ⊢ T1 ▶ [O, 1] TT1 → + ⋆. ⓑ{I1} V2 ⊢ T2 ▶ [O, 1] TT2 → + ∃∃X. ⓑ{a,I1} V1. TT1 ➡ X & ⓑ{a,I1} V2. TT2 ➡ X. +#a #I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2 +elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2 +elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2 +elim (tpr_tps_conf_bind … HV1 HT1 … HTT1) -T1 #U1 #TTU1 #HTU1 +elim (tpr_tps_conf_bind … HV2 HT2 … HTT2) -T2 #U2 #TTU2 #HTU2 +elim (tps_conf_eq … HTU1 … HTU2) -T #U #HU1 #HU2 +@ex2_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *) +qed. + +fact tpr_conf_delta_zeta: + ∀X2,V0,V1,T0,T1,TT1,T2. ( + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → + ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → + ∃∃X. X1 ➡ X & X2 ➡ X + ) → + V0 ➡ V1 → T0 ➡ T1 → ⋆. ⓓV1 ⊢ T1 ▶ [O,1] TT1 → + T0 ➡ T2 → ⇧[O, 1] X2 ≡ T2 → + ∃∃X. +ⓓV1. TT1 ➡ X & X2 ➡ X. +#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HT02 #HXT2 +elim (IH … HT01 … HT02) -IH -HT01 -HT02 // -V0 -T0 #T #HT1 #HT2 +elim (tpr_tps_conf_bind ? ? V1 … HT1 HTT1) -T1 // #TT #HTT1 #HTT +elim (tpr_inv_lift1 … HT2 … HXT2) -T2 #X #HXT #HX2 +lapply (tps_inv_lift1_eq … HTT … HXT) -HTT #H destruct /3 width=3/ +qed. + +(* Basic_1: was: pr0_upsilon_upsilon *) +fact tpr_conf_theta_theta: + ∀a,VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. ( + ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{T0} + 1) + 1 → + ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → + ∃∃X. X1 ➡ X & X2 ➡ X + ) → + V0 ➡ V1 → V0 ➡ V2 → W0 ➡ W1 → W0 ➡ W2 → T0 ➡ T1 → T0 ➡ T2 → + ⇧[O, 1] V1 ≡ VV1 → ⇧[O, 1] V2 ≡ VV2 → + ∃∃X. ⓓ{a}W1. ⓐVV1. T1 ➡ X & ⓓ{a}W2. ⓐVV2. T2 ➡ X. +#a #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2 +elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 +elim (IH … HW01 … HW02) -HW01 -HW02 /2 width=1/ #W #HW1 #HW2 +elim (IH … HT01 … HT02) -HT01 -HT02 -IH /2 width=1/ #T #HT1 #HT2 +elim (lift_total V 0 1) #VV #HVV +lapply (tpr_lift … HV1 … HVV1 … HVV) -V1 #HVV1 +lapply (tpr_lift … HV2 … HVV2 … HVV) -V2 -HVV #HVV2 +@ex2_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *) +qed. + +fact tpr_conf_zeta_zeta: + ∀V0:term. ∀X2,TT0,T0,T1,TT2. ( + ∀X0:term. ♯{X0} < ♯{V0} + ♯{TT0} + 1 → + ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → + ∃∃X. X1 ➡ X & X2 ➡ X + ) → + TT0 ➡ T0 → ⇧[O, 1] T1 ≡ T0 → + TT0 ➡ TT2 → ⇧[O, 1] X2 ≡ TT2 → + ∃∃X. T1 ➡ X & X2 ➡ X. +#V0 #X2 #TT0 #T0 #T1 #TT2 #IH #HTT0 #HT10 #HTT02 #HXTT2 +elim (IH … HTT0 … HTT02) -IH -HTT0 -HTT02 // -V0 -TT0 #T #HT0 #HTT2 +elim (tpr_inv_lift1 … HT0 … HT10) -T0 #T0 #HT0 #HT10 +elim (tpr_inv_lift1 … HTT2 … HXTT2) -TT2 #TT2 #HTT2 #HXTT2 +lapply (lift_inj … HTT2 … HT0) -HTT2 #H destruct /2 width=3/ +qed. + +fact tpr_conf_tau_tau: + ∀V0,T0:term. ∀X2,T1. ( + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → + ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → + ∃∃X. X1 ➡ X & X2 ➡ X + ) → + T0 ➡ T1 → T0 ➡ X2 → + ∃∃X. T1 ➡ X & X2 ➡ X. +#V0 #T0 #X2 #T1 #IH #HT01 #HT02 +elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /2 width=3/ +qed. + +(* Confluence ***************************************************************) + +(* Basic_1: was: pr0_confluence *) +theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ➡ T1 → T0 ➡ T2 → + ∃∃T. T1 ➡ T & T2 ➡ T. +#T0 @(f_ind … tw … T0) -T0 #n #IH * +[ #I #_ #X1 #X2 #H1 #H2 -n + >(tpr_inv_atom1 … H1) -X1 + >(tpr_inv_atom1 … H2) -X2 +(* case 1: atom, atom *) + // +| * [ #a ] #I #V0 #T0 #Hn #X1 #X2 #H1 #H2 + [ elim (tpr_inv_bind1 … H1) -H1 * + [ #V1 #T1 #U1 #HV01 #HT01 #HTU1 #H1 + | #T1 #HT01 #HXT1 #H11 #H12 + ] + elim (tpr_inv_bind1 … H2) -H2 * + [1,3: #V2 #T2 #U2 #HV02 #HT02 #HTU2 #H2 + |2,4: #T2 #HT02 #HXT2 #H21 #H22 + ] destruct +(* case 2: delta, delta *) + [ /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *) +(* case 3: zeta, delta (repeated) *) + | @ex2_commute /3 width=10 by tpr_conf_delta_zeta/ +(* case 4: delta, zeta *) + | /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *) +(* case 5: zeta, zeta *) + | /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *) + ] + | elim (tpr_inv_flat1 … H1) -H1 * + [ #V1 #T1 #HV01 #HT01 #H1 + | #b1 #V1 #W1 #U1 #T1 #HV01 #HUT1 #H11 #H12 #H13 + | #b1 #V1 #Y1 #W1 #Z1 #U1 #T1 #HV01 #HWZ1 #HUT1 #HVY1 #H11 #H12 #H13 + | #HX1 #H1 + ] + elim (tpr_inv_flat1 … H2) -H2 * + [1,5,9,13: #V2 #T2 #HV02 #HT02 #H2 + |2,6,10,14: #b2 #V2 #W2 #U2 #T2 #HV02 #HUT2 #H21 #H22 #H23 + |3,7,11,15: #b2 #V2 #Y2 #W2 #Z2 #U2 #T2 #HV02 #HWZ2 #HUT2 #HVY2 #H21 #H22 #H23 + |4,8,12,16: #HX2 #H2 + ] destruct +(* case 6: flat, flat *) + [ /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *) +(* case 7: beta, flat (repeated) *) + | @ex2_commute /3 width=8 by tpr_conf_flat_beta/ +(* case 8: theta, flat (repeated) *) + | @ex2_commute /3 width=11 by tpr_conf_flat_theta/ +(* case 9: tau, flat (repeated) *) + | @ex2_commute /3 width=6 by tpr_conf_flat_cast/ +(* case 10: flat, beta *) + | /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *) +(* case 11: beta, beta *) + | /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *) +(* case 12: flat, theta *) + | /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *) +(* case 13: theta, theta *) + | /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *) +(* case 14: flat, tau *) + | /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *) +(* case 15: tau, tau *) + | /3 width=5 by tpr_conf_tau_tau/ + ] + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tps.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tps.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tps_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tps_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tps_tps.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tps_tps.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpss.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpss.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpss_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpss_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpss_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpss_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpss_tpss.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpss_tpss.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_delift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/delift_delift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_delift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_ltpss.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_ltpss.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/delift_ltpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_ltpss.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_tpss.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/delift_tpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_tpss.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/thin.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/thin.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/thin.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/delift/thin.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/thin_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/thin_delift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/thin_delift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/delift/thin_delift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/thin_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/thin_ldrop.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/thin_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/delift/thin_ldrop.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma index e3f661cfc..e746586ae 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma @@ -23,15 +23,14 @@ inductive lpx_sn (R:lenv→relation term): relation lenv ≝ lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) . -definition lpx_sn_confluent: predicate (lenv→relation term) ≝ λR. - ∀L0,T0,T1. R L0 T0 T1 → ∀T2. R L0 T0 T2 → - ∀L1. lpx_sn R L0 L1 → ∀L2. lpx_sn R L0 L2 → - ∃∃T. R L1 T1 T & R L2 T2 T. - -definition lpx_sn_transitive: predicate (lenv→relation term) ≝ λR. - ∀L1,T1,T. R L1 T1 T → ∀L2. lpx_sn R L1 L2 → - ∀T2. R L2 T T2 → R L1 T1 T2. +definition lpx_sn_confluent: relation (lenv→relation term) ≝ λR1,R2. + ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → + ∀L1. lpx_sn R1 L0 L1 → ∀L2. lpx_sn R2 L0 L2 → + ∃∃T. R1 L1 T1 T & R2 L2 T2 T. +definition lpx_sn_transitive: relation (lenv→relation term) ≝ λR1,R2. + ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn R1 L1 L2 → + ∀T2. R2 L2 T T2 → R1 L1 T1 T2. (* Basic inversion lemmas ***************************************************) @@ -85,6 +84,32 @@ lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|. #R #L1 #L2 #H elim H -L1 -L2 normalize // qed-. +(* Advanced forward lemmas **************************************************) + +lemma lpx_sn_fwd_append1: ∀R,L1,K1,L. lpx_sn R (K1 @@ L1) L → + ∃∃K2,L2. lpx_sn R K1 K2 & L = K2 @@ L2. +#R #L1 elim L1 -L1 +[ #K1 #K2 #HK12 + @(ex2_2_intro … K2 (⋆)) // (* explicit constructor, /2 width=4/ does not work *) +| #L1 #I #V1 #IH #K1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct + elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #H destruct + @(ex2_2_intro … (L2.ⓑ{I}V2) HK12) // (* explicit constructor, /2 width=4/ does not work *) +] +qed-. + +lemma lpx_sn_fwd_append2: ∀R,L2,K2,L. lpx_sn R L (K2 @@ L2) → + ∃∃K1,L1. lpx_sn R K1 K2 & L = K1 @@ L1. +#R #L2 elim L2 -L2 +[ #K2 #K1 #HK12 + @(ex2_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=4/ does not work *) +| #L2 #I #V2 #IH #K2 #X #H + elim (lpx_sn_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct + elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #H destruct + @(ex2_2_intro … (L1.ⓑ{I}V1) HK12) // (* explicit constructor, /2 width=4/ does not work *) +] +qed-. + (* Basic properties *********************************************************) lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R). @@ -97,13 +122,15 @@ lemma lpx_sn_append: ∀R. l_appendable_sn R → #R #HR #K1 #K2 #H elim H -K1 -K2 // /3 width=1/ qed-. -lemma lpx_sn_trans: ∀R. lpx_sn_transitive R → Transitive … (lpx_sn R). +(* Advanced properties ******************************************************) + +lemma lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn R). #R #HR #L1 #L #H elim H -L1 -L // #I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5/ qed-. -lemma lpx_sn_conf: ∀R. lpx_sn_confluent R → confluent … (lpx_sn R). +lemma lpx_sn_conf: ∀R. lpx_sn_confluent R R → confluent … (lpx_sn R). #R #HR #L0 @(f_ind … length … L0) -L0 #n #IH * [ #_ #X1 #H1 #X2 #H2 -n >(lpx_sn_inv_atom1 … H1) -X1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index 5e730aec2..689d6edc2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -306,17 +306,17 @@ notation "hvbox( L ⊢ break 𝐇𝐍 ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'HdNormal $L $T }. -notation "hvbox( T1 ➡ break term 46 T2 )" - non associative with precedence 45 - for @{ 'PRed $T1 $T2 }. - notation "hvbox( L ⊢ break term 46 T1 ➡ break term 46 T2 )" non associative with precedence 45 for @{ 'PRed $L $T1 $T2 }. -notation "hvbox( ⦃ term 46 L1 ⦄ ➡ break ⦃ term 46 L2 ⦄ )" +notation "hvbox( L1 ⊢ ➡ break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedSn $L1 $L2 }. + +notation "hvbox( L1 ⊢ ➡ ➡ break term 46 L2 )" non associative with precedence 45 - for @{ 'FocalizedPRed $L1 $L2 }. + for @{ 'PRedSnAlt $L1 $L2 }. notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ➡ break ⦃ term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 @@ -326,10 +326,6 @@ notation "hvbox( L ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ➡ break ⦃ non associative with precedence 45 for @{ 'FocalizedPRed $L $L1 $T1 $L2 $T2 }. -notation "hvbox( ⦃ term 46 L1 ⦄ ➡ ➡ break ⦃ term 46 L2 ⦄ )" - non associative with precedence 45 - for @{ 'FocalizedPRedAlt $L1 $L2 }. - (* Computation **************************************************************) notation "hvbox( T1 ➡ * break term 46 T2 )" diff --git a/matita/matita/contribs/lambdadelta/basic_2/restricted/cpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/restricted/cpqs.ma index 9d5983292..4992de0b0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/restricted/cpqs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/restricted/cpqs.ma @@ -48,9 +48,8 @@ lemma cpqs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➤* T2 → elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi (cpss_inv_sort1 … H) -H // +| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12 + elim (cpss_inv_lref1 … H) -H + [ #H destruct + elim (lpss_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2 + elim (lpss_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/ + | * #Y #Z #V2 #H #HV12 #HV2 + lapply (ldrop_mono … H … HLK1) -H #H destruct + elim (lpss_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2 + elim (lpss_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -V0 /3 width=7/ + ] +| #a #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (cpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=2/ +| #a #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (cpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=1/ +| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (cpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=3/ +| #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (cpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=1/ +] +qed-. + +lemma aaa_cpss_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ▶* T2 → L ⊢ T2 ⁝ A. +/2 width=5 by aaa_cpss_lpss_conf/ qed-. + +lemma aaa_lpss_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ▶* L2 → L2 ⊢ T ⁝ A. +/2 width=5 by aaa_cpss_lpss_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lpss.ma new file mode 100644 index 000000000..0aacb2b63 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lpss.ma @@ -0,0 +1,81 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/unfold/lpss_ldrop.ma". +include "basic_2/static/ssta_lift.ma". + +(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************) + +(* Properties about sn parallel unfold **************************************) + +(* Note: apparently this was missing in basic_1 *) +lemma ssta_tpss_lpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → + ∀T2. L1 ⊢ T1 ▶* T2 → ∀L2. L1 ⊢ ▶* L2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L1 ⊢ U1 ▶* U2. +#h #g #L1 #T1 #U1 #l #H elim H -L1 -T1 -U1 -l +[ #L1 #k1 #l1 #Hkl1 #X #H + >(cpss_inv_sort1 … H) -H /3 width=3/ +| #L1 #K1 #V1 #W1 #U1 #i #l #HLK1 #_ #HWU1 #IHVW1 #X #H #L2 #HL12 + elim (cpss_inv_lref1 … H) -H + [ #H destruct + elim (lpss_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 + elim (lpss_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 #HLK1 + elim (IHVW1 … HV12 … HK12) -IHVW1 -HV12 -HK12 #W2 #HVW2 #HW12 + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (cpss_lift … HW12 … HLK1 … HWU1 … HWU2) -HW12 -HLK1 -HWU1 /3 width=6/ + | * #Y #Z #V2 #H #HV12 #HV2 + lapply (ldrop_mono … H … HLK1) -H #H destruct + elim (lpss_ldrop_conf … HLK1 … HL12) -HL12 #Z #H #HLK2 + elim (lpss_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -V0 #HLK2 + lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 #HLK1 + elim (IHVW1 … HV12 … HK12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12 + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (ssta_lift … HVW2 … HLK2 … HV2 … HWU2) -HVW2 -HLK2 -HV2 + lapply (cpss_lift … HW12 … HLK1 … HWU1 … HWU2) -HW12 -HLK1 -HWU1 -HWU2 /3 width=3/ + ] +| #L1 #K1 #W1 #V1 #U1 #i #l #HLK1 #_ #HWU1 #IHWV1 #X #H #L2 #HL12 + elim (cpss_inv_lref1 … H) -H [ | -IHWV1 -HWU1 -HL12 ] + [ #H destruct + elim (lpss_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 + elim (lpss_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 #HLK1 + elim (IHWV1 … HW12 … HK12) -IHWV1 -HK12 #V2 #HWV2 #_ + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (cpss_lift … HW12 … HLK1 … HWU1 … HWU2) -HW12 -HLK1 -HWU1 /3 width=6/ + | * #K2 #V2 #W2 #HLK2 #_ #_ + lapply (ldrop_mono … HLK2 … HLK1) -HLK1 -HLK2 #H destruct + ] +| #a #I #L1 #V1 #T1 #U1 #l #_ #IHTU1 #X #H #L2 #HL12 + elim (cpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + elim (IHTU1 … HT12 (L2.ⓑ{I}V2)) -IHTU1 -HT12 /2 width=1/ -HL12 /3 width=5/ +| #L1 #V1 #T1 #U1 #l #_ #IHTU1 #X #H #L2 #HL12 + elim (cpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + elim (IHTU1 … HT12 … HL12) -IHTU1 -HT12 -HL12 /3 width=5/ +| #L1 #W1 #T1 #U1 #l #_ #IHTU1 #X #H #L2 #HL12 + elim (cpss_inv_flat1 … H) -H #W2 #T2 #HW12 #HT12 #H destruct + elim (IHTU1 … HT12 … HL12) -IHTU1 -HT12 -HL12 /3 width=3/ +] +qed-. + +lemma ssta_cpss_conf: ∀h,g,L,T1,U1,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l, U1⦄ → + ∀T2. L ⊢ T1 ▶* T2 → + ∃∃U2. ⦃h, L⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L ⊢ U1 ▶* U2. +/2 width=3 by ssta_tpss_lpss_conf/ qed-. + +lemma ssta_lpss_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ → + ∀L2. L1 ⊢ ▶* L2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ & L1 ⊢ U1 ▶* U2. +/2 width=3 by ssta_tpss_lpss_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups.etc b/matita/matita/contribs/lambdadelta/basic_2/unfold/fsups.ma similarity index 99% rename from matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups.etc rename to matita/matita/contribs/lambdadelta/basic_2/unfold/fsups.ma index c7867e1f8..bee55674d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/fsups.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/grammar/fsupp.ma". +include "basic_2/unfold/fsupp.ma". (* STAR-ITERATED SUPCLOSURE *************************************************) @@ -70,7 +70,7 @@ lemma fsups_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄ → ♯{L2, T #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2 // /4 width=3 by fsup_fwd_cw, lt_to_le_to_lt, lt_to_le/ (**) (* slow even with trace *) qed-. - +(* (* Advanced inversion lemmas on plus-iterated supclosure ********************) lemma fsupp_inv_bind1_fsups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⊃+ ⦃L2, T2⦄ → @@ -90,3 +90,4 @@ lemma fsupp_inv_flat1_fsups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⊃+ ⦃L2, | #L #T #L2 #T2 #_ #HT2 * /3 width=4/ ] qed-. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups_fsups.etc b/matita/matita/contribs/lambdadelta/basic_2/unfold/fsups_fsups.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups_fsups.etc rename to matita/matita/contribs/lambdadelta/basic_2/unfold/fsups_fsups.ma index e2f893f24..1c4b366c4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups_fsups.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/fsups_fsups.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/grammar/fsups.ma". +include "basic_2/unfold/fsups.ma". (* STAR-ITERATED SUPCLOSURE *************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss.ma index 7d3145367..d0c856b9f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss.ma @@ -29,7 +29,7 @@ lemma lpss_inv_atom1: ∀L2. ⋆ ⊢ ▶* L2 → L2 = ⋆. /2 width=4 by lpx_sn_inv_atom1_aux/ qed-. lemma lpss_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ▶* L2 → - ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2. + ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2. /2 width=3 by lpx_sn_inv_pair1_aux/ qed-. lemma lpss_inv_atom2: ∀L1. L1 ⊢ ▶* ⋆ → L1 = ⋆. @@ -54,6 +54,16 @@ lemma lpss_append: ∀K1,K2. K1 ⊢ ▶* K2 → ∀L1,L2. L1 ⊢ ▶* L2 → lemma lpss_fwd_length: ∀L1,L2. L1 ⊢ ▶* L2 → |L1| = |L2|. /2 width=2 by lpx_sn_fwd_length/ qed-. +(* Advanced forward lemmas **************************************************) + +lemma lpss_fwd_append1: ∀K1,L1,L. K1 @@ L1 ⊢ ▶* L → + ∃∃K2,L2. K1 ⊢ ▶* K2 & L = K2 @@ L2. +/2 width=2 by lpx_sn_fwd_append1/ qed-. + +lemma lpss_fwd_append2: ∀L,K2,L2. L ⊢ ▶* K2 @@ L2 → + ∃∃K1,L1. K1 ⊢ ▶* K2 & L = K1 @@ L1. +/2 width=2 by lpx_sn_fwd_append2/ qed-. + (* Basic_1: removed theorems 28: csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma index 0e23bfce5..6c060f88f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma @@ -109,7 +109,7 @@ elim (IH … HV01 … HV02 … HL01 … HL02) // elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/ qed-. -theorem cpss_conf_lpss: lpx_sn_confluent cpss. +theorem cpss_conf_lpss: lpx_sn_confluent cpss cpss. #L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*] [ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpss_inv_atom1 … H1) -H1 @@ -139,7 +139,7 @@ qed-. theorem cpss_conf: ∀L. confluent … (cpss L). /2 width=6 by cpss_conf_lpss/ qed-. -theorem cpss_trans_lpss: lpx_sn_transitive cpss. +theorem cpss_trans_lpss: lpx_sn_transitive cpss cpss. #L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*] [ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct elim (cpss_inv_atom1 … H1) -H1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lpss.ma new file mode 100644 index 000000000..cd16c5847 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lpss.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/static/ssta_lpss.ma". +include "basic_2/unwind/sstas.ma". + +(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************) + +(* Properties about sn parallel unfold **************************************) + +lemma sstas_tpss_lpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → + ∀T2. L1 ⊢ T1 ▶* T2 → ∀L2. L1 ⊢ ▶* L2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U1 ▶* U2. +#h #g #L1 #T1 #U1 #H @(sstas_ind_dx … H) -T1 /2 width=3/ +#T0 #U0 #l0 #HTU0 #_ #IHU01 #T #HT0 #L2 #HL12 +elim (ssta_tpss_lpss_conf … HTU0 … HT0 … HL12) -HTU0 -HT0 #U #HTU #HU0 +elim (IHU01 … HU0 … HL12) -IHU01 -U0 -HL12 /3 width=4/ +qed-. + +lemma sstas_tpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*[g] U1 → + ∀T2. L ⊢ T1 ▶* T2 → + ∃∃U2. ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U1 ▶* U2. +/2 width=3 by sstas_tpss_lpss_conf/ qed-. + +lemma sstas_lpss_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*[g] U1 → + ∀L2. L1 ⊢ ▶* L2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T •*[g] U2 & L1 ⊢ U1 ▶* U2. +/2 width=3 by sstas_tpss_lpss_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index d8206ed98..1c4a0bef5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -33,6 +33,11 @@ Extended context-sensitive strong normalization for simply typed terms. + + Reaxiomatized substitution and reduction + commute with respect to subclosure + (anniversary milestone). + Mutual recursive preservation of stratified native validity for hyper computation on closures. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 239a44fe7..8ed310e1e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -133,6 +133,11 @@ table { [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ] } ] + [ { "revised context-sensitive reduction" * } { + [ "lpr ( ? ⊢ ➡ ? )" "lpr_ldrop" + "lpr_cpr" + "lpr_lpr" * ] + [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" * ] + } + ] [ { "context-sensitive reduction" * } { [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_tpss" + "cpr_ltpss_dx" + "cpr_ltpss_sn" + "cpr_delift" + "cpr_aaa" + "cpr_ltpr" + "cpr_cpr" * ] } @@ -158,13 +163,13 @@ table { [ "lpqs ( ? ⊢ ➤* ? )" "lpqs_ldrop" + "lpqs_cpqs" + "lpqs_lpqs" * ] [ "cpqs ( ? ⊢ ? ➤* ? )" "cpqs_lift" * ] } - ] + ] } ] class "green" [ { "unwind" * } { [ { "iterated stratified static type assignment" * } { - [ "sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )" "sstas_lift" + "sstas_ltpss_dx" + "sstas_ltpss_sn" + "sstas_aaa" + "sstas_sstas" * ] + [ "sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )" "sstas_lift" + "sstas_lpss" + "sstas_aaa" + "sstas_sstas" * ] } ] } @@ -172,7 +177,7 @@ table { class "grass" [ { "static typing" * } { [ { "stratified static type assignment" * } { - [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_ltpss_dx" + "ssta_ltpss_sn" + "ssta_aaa" + "ssta_ssta" * ] + [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_lpss" + "ssta_aaa" + "ssta_ssta" * ] } ] [ { "local env. ref. for atomic arity assignment" * } { @@ -180,7 +185,7 @@ table { } ] [ { "atomic arity assignment" * } { - [ "aaa ( ? ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_ltpss_dx" + "aaa_ltpss_sn" + "aaa_aaa" * ] + [ "aaa ( ? ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_lpss" + "aaa_aaa" * ] } ] [ { "parameters" * } { @@ -191,7 +196,8 @@ table { ] class "yellow" [ { "unfold" * } { - [ { "basic local env. thinning" * } { +(* + [ { "basic local env. thinning" * } { [ "thin ( ? ▼*[?,?] ≡ ? )" "thin_ldrop" + "thin_delift" * ] } ] @@ -199,18 +205,14 @@ table { [ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" + "delift_tpss" + "delift_ltpss" + "delift_delift" * ] } ] - [ { "revised parallel substitution" * } { +*) + [ { "parallel substitution" * } { [ "lpss ( ? ⊢ ▶* ? )" "lpss_ldrop" + "lpss_cpss" + "lpss_lpss" * ] [ "cpss ( ? ⊢ ? ▶* ? )" "cpss_lift" * ] } ] - [ { "partial unfold" * } { - [ "ltpss_sn ( ? ⊢ ▶*[?,?] ? )" "ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )" "ltpss_sn_ldrop" + "ltpss_sn_tps" + "ltpss_sn_tpss" + "ltpss_sn_ltpss_sn" * ] - [ "ltpss_dx ( ? ▶*[?,?] ? )" "ltpss_dx_ldrop" + "ltpss_dx_tps" + "ltpss_dx_tpss" + "ltpss_dx_ltpss_dx" * ] - [ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ] - } - ] [ { "iterated structural successor for closures" * } { + [ "fsups ( ⦃?,?⦄ ⊃* ⦃?,?⦄ )" "fsups_fsups" * ] [ "fsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ )" "fsupp_fsupp" * ] } ] @@ -231,10 +233,6 @@ table { ] class "orange" [ { "substitution" * } { - [ { "parallel substitution" * } { - [ "tps ( ? ⊢ ? ▶[?,?] ? )" "tps_lift" + "tps_tps" * ] - } - ] [ { "structural successor for closures" * } { [ "fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ )" * ] } diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 225fe64bf..d8da251bb 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1509,7 +1509,7 @@ let predefined_classes = [ ["#"; "♯"; "⌘"; ]; ["-"; "÷"; "⊢"; "⊩"; ]; ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ]; - ["→"; "↦"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; + ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "➤"; "➸"; "⇉"; "⥰"; ] ; ["^"; "↑"; ] ; ["⇑"; "⇧"; "⬆"; ] ; @@ -1527,7 +1527,7 @@ let predefined_classes = [ ["□"; "◽"; "▪"; "◾"; ]; ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ; [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ; - ["≥"; "≽"; "⥸"; ]; + ["≥"; "⪀"; "≽"; "⥸"; ]; ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ; ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ; ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ; -- 2.39.2