From: Ferruccio Guidi Date: Tue, 21 Mar 2017 15:17:27 +0000 (+0000) Subject: we finally understood what tsts is, :) X-Git-Tag: make_still_working~474 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=69592aa1d0c0d122fb09f11cc53bf4c5a1532fdd we finally understood what tsts is, :) so we renamed it as theq --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma new file mode 100644 index 000000000..d8a6f77a3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma @@ -0,0 +1,103 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/theq_tdeq.ma". +include "basic_2/rt_computation/cpxs_lsubr.ma". +include "basic_2/rt_computation/cpxs_cnx.ma". +include "basic_2/rt_computation/lfpxs_cpxs.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) + +(* Forward lemmas with head equivalence for terms ***************************) + +lemma cpxs_fwd_sort: ∀h,o,G,L,U,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] U → + ⋆s ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⋆(next h s) ⬈*[h] U. +#h #o #G #L #U #s #H elim (cpxs_inv_sort1 … H) -H * +[ #H destruct /2 width=1 by or_introl/ +| #n #H destruct + @or_intror >iter_S <(iter_n_Sm … (next h)) // (**) +] +qed-. + +(* Note: probably this is an inversion lemma *) +(* Basic_2A1: was: cpxs_fwd_delta *) +lemma cpxs_fwd_delta_drops: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 → + ∀V2. ⬆*[⫯i] V1 ≡ V2 → + ∀U. ⦃G, L⦄ ⊢ #i ⬈*[h] U → + #i ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ V2 ⬈*[h] U. +#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H +elim (cpxs_inv_lref1_drops … H) -H /2 width=1 by or_introl/ +* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0 +lapply (drops_mono … HLK0 … HLK) -HLK0 #H destruct +elim (cpxs_lifts … HVU0 (Ⓣ) … L … HV12) -HVU0 -HV12 /2 width=3 by drops_isuni_fwd_drop2/ #X #H +<(lifts_mono … HU0 … H) -U0 -X /2 width=1 by or_intror/ +qed-. + +(* Basic_1: was just: pr3_iso_beta *) +lemma cpxs_fwd_beta: ∀h,o,p,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] U → + ⓐV.ⓛ{p}W.T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] U. +#h #o #p #G #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H * +[ #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ +| #b #W0 #T0 #HT0 #HU + elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct + lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 + /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/ +| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_ + elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct +] +qed-. + +lemma cpxs_fwd_theta: ∀h,o,p,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] U → + ∀V2. ⬆*[1] V1 ≡ V2 → ⓐV1.ⓓ{p}V.T ⩳[h, o] U ∨ + ⦃G, L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] U. +#h #o #p #G #L #V1 #V #T #U #H #V2 #HV12 +elim (cpxs_inv_appl1 … H) -H * +[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ +| #q #W #T0 #HT0 #HU + elim (cpxs_inv_abbr1 … HT0) -HT0 * + [ #V3 #T3 #_ #_ #H destruct + | #X #HT2 #H #H0 destruct + elim (lifts_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct + @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *) + @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{q}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T + @(cpxs_strap2 … (ⓐV1.ⓛ{q}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ] + /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ + ] +| #q #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU + @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *) + elim (cpxs_inv_abbr1 … HT0) -HT0 * + [ #V5 #T5 #HV5 #HT5 #H destruct + elim (cpxs_lifts … HV13 (Ⓣ) … (L.ⓓV) … HV12) -V1 /3 width=1 by drops_refl, drops_drop/ #X #H + <(lifts_mono … HV34 … H) -V3 -X /3 width=1 by cpxs_flat, cpxs_bind/ + | #X #HT1 #H #H0 destruct + elim (lifts_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct + elim (cpxs_lifts … HV13 (Ⓣ) … (L.ⓓV0) … HV12) -HV13 /3 width=1 by drops_refl, drops_drop/ #X #H + <(lifts_mono … HV34 … H) -V3 -X #HV24 + @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{q}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T + @(cpxs_strap2 … (ⓐV1.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V5 -T5 + @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/ + ] +] +qed-. + +lemma cpxs_fwd_cast: ∀h,o,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ⬈*[h] U → + ∨∨ ⓝW. T ⩳[h, o] U | ⦃G, L⦄ ⊢ T ⬈*[h] U | ⦃G, L⦄ ⊢ W ⬈*[h] U. +#h #o #G #L #W #T #U #H +elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ * +#W0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or3_intro0/ +qed-. + +lemma cpxs_fwd_cnx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → + ∀U. ⦃G, L⦄ ⊢ T ⬈*[h] U → T ⩳[h, o] U. +/3 width=4 by cpxs_inv_cnx1, tdeq_theq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma new file mode 100644 index 000000000..4d7cf8baf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma @@ -0,0 +1,192 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/theq_simple_vector.ma". +include "basic_2/relocation/lifts_vector.ma". +include "basic_2/rt_computation/cpxs_theq.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) + +(* Vector form of forward lemmas with head equivalence for terms ************) + +lemma cpxs_fwd_sort_vector: ∀h,o,G,L,s,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆s ⬈*[h] U → + ⒶVs.⋆s ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.⋆(next h s) ⬈*[h] U. +#h #o #G #L #s #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/ +#V #Vs #IHVs #U #H +elim (cpxs_inv_appl1 … H) -H * +[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ +| #p #W1 #T1 #HT1 #HU + elim (IHVs … HT1) -IHVs -HT1 #HT1 + [ elim (theq_inv_applv_bind_simple … HT1) // + | @or_intror (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV.ⓛ{p}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/ + ] +| #p #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU + elim (IHVs … HT1) -IHVs -HT1 #HT1 + [ elim (theq_inv_applv_bind_simple … HT1) // + | @or_intror (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV1.ⓓ{p}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/ + ] +] +qed-. + +(* Basic_2A1: was: cpxs_fwd_delta_vector *) +lemma cpxs_fwd_delta_drops_vector: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 → + ∀V2. ⬆*[⫯i] V1 ≡ V2 → + ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.#i ⬈*[h] U → + ⒶVs.#i ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.V2 ⬈*[h] U. +#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta_drops/ +#V #Vs #IHVs #U #H -K -V1 +elim (cpxs_inv_appl1 … H) -H * +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ +| #q #W0 #T0 #HT0 #HU + elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (theq_inv_applv_bind_simple … HT0) // + | @or_intror -i (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /3 width=1 by cpxs_flat_dx, cpx_beta/ + ] +| #q #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU + elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (theq_inv_applv_bind_simple … HT0) // + | @or_intror -i (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV0.ⓓ{q}V3.T0)) /3 width=3 by cpxs_flat, cpx_theta/ + ] +] +qed-. + +(* Basic_1: was just: pr3_iso_appls_beta *) +lemma cpxs_fwd_beta_vector: ∀h,o,p,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{p}W.T ⬈*[h] U → + ⒶVs.ⓐV.ⓛ{p}W. T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{p}ⓝW.V.T ⬈*[h] U. +#h #o #p #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/ +#V0 #Vs #IHVs #V #W #T #U #H +elim (cpxs_inv_appl1 … H) -H * +[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ +| #q #W1 #T1 #HT1 #HU + elim (IHVs … HT1) -IHVs -HT1 #HT1 + [ elim (theq_inv_applv_bind_simple … HT1) // + | @or_intror (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV0.ⓛ{q}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/ + ] +| #q #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU + elim (IHVs … HT1) -IHVs -HT1 #HT1 + [ elim (theq_inv_applv_bind_simple … HT1) // + | @or_intror (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV1.ⓓ{q}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/ + ] +] +qed-. + +(* Basic_1: was just: pr3_iso_appls_abbr *) +lemma cpxs_fwd_theta_vector: ∀h,o,G,L,V1b,V2b. ⬆*[1] V1b ≡ V2b → + ∀p,V,T,U. ⦃G, L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] U → + ⒶV1b.ⓓ{p}V.T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] U. +#h #o #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/ +#V1b #V2b #V1a #V2a #HV12a #HV12b #p +generalize in match HV12a; -HV12a +generalize in match V2a; -V2a +generalize in match V1a; -V1a +elim HV12b -V1b -V2b /2 width=1 by cpxs_fwd_theta/ +#V1b #V2b #V1b #V2b #HV12b #_ #IHV12b #V1a #V2a #HV12a #V #T #U #H +elim (cpxs_inv_appl1 … H) -H * +[ -IHV12b -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ +| #q #W0 #T0 #HT0 #HU + elim (IHV12b … HV12b … HT0) -IHV12b -HT0 #HT0 + [ -HV12a -HV12b -HU + elim (theq_inv_pair1 … HT0) #V1 #T1 #H destruct + | @or_intror -V1b (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + elim (cpxs_inv_abbr1 … HT0) -HT0 * + [ -HV12a #V1 #T1 #_ #_ #H destruct + | -V1b #X #HT1 #H #H0 destruct + elim (lifts_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct + @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{q}W1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b + @(cpxs_strap2 … (ⓐV1a.ⓛ{q}W0.T0)) + /4 width=7 by cpxs_beta_dx, cpx_zeta, lifts_bind, lifts_flat/ + ] + ] +| #q #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU + elim (IHV12b … HV12b … HT0) -HV12b -IHV12b -HT0 #HT0 + [ -HV12a -HV10a -HV0a -HU + elim (theq_inv_pair1 … HT0) #V1 #T1 #H destruct + | @or_intror -V1b -V1b (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + elim (cpxs_inv_abbr1 … HT0) -HT0 * + [ #V1 #T1 #HV1 #HT1 #H destruct + elim (cpxs_lifts … HV10a (Ⓣ) … (L.ⓓV) … HV12a) -V1a /3 width=1 by drops_refl, drops_drop/ #X #H + <(lifts_mono … HV0a … H) -V0a -X #HV2a + @(cpxs_trans … (ⓓ{p}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/ + | #X #HT1 #H #H0 destruct + elim (lifts_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct + elim (cpxs_lifts … HV10a (Ⓣ) … (L.ⓓV0) … HV12a) /3 width=1 by drops_refl, drops_drop/ #X #H + <(lifts_mono … HV0a … H) -V0a -X #HV2a + @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{q}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b + @(cpxs_strap2 … (ⓐV1a.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V1 -T1 + @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/ + ] + ] +] +qed-. + +(* Basic_1: was just: pr3_iso_appls_cast *) +lemma cpxs_fwd_cast_vector: ∀h,o,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ⬈*[h] U → + ∨∨ ⒶVs. ⓝW. T ⩳[h, o] U + | ⦃G, L⦄ ⊢ ⒶVs.T ⬈*[h] U + | ⦃G, L⦄ ⊢ ⒶVs.W ⬈*[h] U. +#h #o #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/ +#V #Vs #IHVs #W #T #U #H +elim (cpxs_inv_appl1 … H) -H * +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or3_intro0/ +| #q #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (theq_inv_applv_bind_simple … HT0) // + | @or3_intro1 -W (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ + | @or3_intro2 -T (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ + ] +| #q #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU + elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (theq_inv_applv_bind_simple … HT0) // + | @or3_intro1 -W (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ + | @or3_intro2 -T (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ + ] +] +qed-. + +(* Basic_1: was just: nf2_iso_appls_lref *) +lemma cpxs_fwd_cnx_vector: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → + ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ⬈*[h] U → ⒶVs.T ⩳[h, o] U. +#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *) +#V #Vs #IHVs #U #H +elim (cpxs_inv_appl1 … H) -H * +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair/ +| #p #W0 #T0 #HT0 #HU + lapply (IHVs … HT0) -IHVs -HT0 #HT0 + elim (theq_inv_applv_bind_simple … HT0) // +| #p #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU + lapply (IHVs … HT0) -IHVs -HT0 #HT0 + elim (theq_inv_applv_bind_simple … HT0) // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma deleted file mode 100644 index e7d1e9ed9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma +++ /dev/null @@ -1,103 +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 "basic_2/syntax/tsts_tdeq.ma". -include "basic_2/rt_computation/cpxs_lsubr.ma". -include "basic_2/rt_computation/cpxs_cnx.ma". -include "basic_2/rt_computation/lfpxs_cpxs.ma". - -(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) - -(* Forward lemmas with same top term structure ******************************) - -lemma cpxs_fwd_sort: ∀h,o,G,L,U,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] U → - ⋆s ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⋆(next h s) ⬈*[h] U. -#h #o #G #L #U #s #H elim (cpxs_inv_sort1 … H) -H * -[ #H destruct /2 width=1 by or_introl/ -| #n #H destruct - @or_intror >iter_S <(iter_n_Sm … (next h)) // (**) -] -qed-. - -(* Note: probably this is an inversion lemma *) -(* Basic_2A1: was: cpxs_fwd_delta *) -lemma cpxs_fwd_delta_drops: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 → - ∀V2. ⬆*[⫯i] V1 ≡ V2 → - ∀U. ⦃G, L⦄ ⊢ #i ⬈*[h] U → - #i ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ V2 ⬈*[h] U. -#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H -elim (cpxs_inv_lref1_drops … H) -H /2 width=1 by or_introl/ -* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0 -lapply (drops_mono … HLK0 … HLK) -HLK0 #H destruct -elim (cpxs_lifts … HVU0 (Ⓣ) … L … HV12) -HVU0 -HV12 /2 width=3 by drops_isuni_fwd_drop2/ #X #H -<(lifts_mono … HU0 … H) -U0 -X /2 width=1 by or_intror/ -qed-. - -(* Basic_1: was just: pr3_iso_beta *) -lemma cpxs_fwd_beta: ∀h,o,p,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] U → - ⓐV.ⓛ{p}W.T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] U. -#h #o #p #G #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H * -[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ -| #b #W0 #T0 #HT0 #HU - elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct - lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 - /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/ -| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_ - elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct -] -qed-. - -lemma cpxs_fwd_theta: ∀h,o,p,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] U → - ∀V2. ⬆*[1] V1 ≡ V2 → ⓐV1.ⓓ{p}V.T ⩳[h, o] U ∨ - ⦃G, L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] U. -#h #o #p #G #L #V1 #V #T #U #H #V2 #HV12 -elim (cpxs_inv_appl1 … H) -H * -[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ -| #q #W #T0 #HT0 #HU - elim (cpxs_inv_abbr1 … HT0) -HT0 * - [ #V3 #T3 #_ #_ #H destruct - | #X #HT2 #H #H0 destruct - elim (lifts_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct - @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *) - @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{q}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T - @(cpxs_strap2 … (ⓐV1.ⓛ{q}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ] - /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ - ] -| #q #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU - @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *) - elim (cpxs_inv_abbr1 … HT0) -HT0 * - [ #V5 #T5 #HV5 #HT5 #H destruct - elim (cpxs_lifts … HV13 (Ⓣ) … (L.ⓓV) … HV12) -V1 /3 width=1 by drops_refl, drops_drop/ #X #H - <(lifts_mono … HV34 … H) -V3 -X /3 width=1 by cpxs_flat, cpxs_bind/ - | #X #HT1 #H #H0 destruct - elim (lifts_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct - elim (cpxs_lifts … HV13 (Ⓣ) … (L.ⓓV0) … HV12) -HV13 /3 width=1 by drops_refl, drops_drop/ #X #H - <(lifts_mono … HV34 … H) -V3 -X #HV24 - @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{q}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T - @(cpxs_strap2 … (ⓐV1.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V5 -T5 - @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/ - ] -] -qed-. - -lemma cpxs_fwd_cast: ∀h,o,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ⬈*[h] U → - ∨∨ ⓝW. T ⩳[h, o] U | ⦃G, L⦄ ⊢ T ⬈*[h] U | ⦃G, L⦄ ⊢ W ⬈*[h] U. -#h #o #G #L #W #T #U #H -elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ * -#W0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/ -qed-. - -lemma cpxs_fwd_cnx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → - ∀U. ⦃G, L⦄ ⊢ T ⬈*[h] U → T ⩳[h, o] U. -/3 width=4 by cpxs_inv_cnx1, tdeq_tsts/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts_vector.ma deleted file mode 100644 index cf7cdba9d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts_vector.ma +++ /dev/null @@ -1,192 +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 "basic_2/syntax/tsts_simple_vector.ma". -include "basic_2/relocation/lifts_vector.ma". -include "basic_2/rt_computation/cpxs_tsts.ma". - -(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) - -(* Vector form of forward lemmas with same top term structure ***************) - -lemma cpxs_fwd_sort_vector: ∀h,o,G,L,s,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆s ⬈*[h] U → - ⒶVs.⋆s ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.⋆(next h s) ⬈*[h] U. -#h #o #G #L #s #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/ -#V #Vs #IHVs #U #H -elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ -| #p #W1 #T1 #HT1 #HU - elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tsts_inv_applv_bind_simple … HT1) // - | @or_intror (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV.ⓛ{p}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/ - ] -| #p #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU - elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tsts_inv_applv_bind_simple … HT1) // - | @or_intror (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV1.ⓓ{p}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/ - ] -] -qed-. - -(* Basic_2A1: was: cpxs_fwd_delta_vector *) -lemma cpxs_fwd_delta_drops_vector: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 → - ∀V2. ⬆*[⫯i] V1 ≡ V2 → - ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.#i ⬈*[h] U → - ⒶVs.#i ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.V2 ⬈*[h] U. -#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta_drops/ -#V #Vs #IHVs #U #H -K -V1 -elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ -| #q #W0 #T0 #HT0 #HU - elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tsts_inv_applv_bind_simple … HT0) // - | @or_intror -i (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /3 width=1 by cpxs_flat_dx, cpx_beta/ - ] -| #q #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU - elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tsts_inv_applv_bind_simple … HT0) // - | @or_intror -i (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓓ{q}V3.T0)) /3 width=3 by cpxs_flat, cpx_theta/ - ] -] -qed-. - -(* Basic_1: was just: pr3_iso_appls_beta *) -lemma cpxs_fwd_beta_vector: ∀h,o,p,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{p}W.T ⬈*[h] U → - ⒶVs.ⓐV.ⓛ{p}W. T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{p}ⓝW.V.T ⬈*[h] U. -#h #o #p #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/ -#V0 #Vs #IHVs #V #W #T #U #H -elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ -| #q #W1 #T1 #HT1 #HU - elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tsts_inv_applv_bind_simple … HT1) // - | @or_intror (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓛ{q}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/ - ] -| #q #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU - elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tsts_inv_applv_bind_simple … HT1) // - | @or_intror (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV1.ⓓ{q}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/ - ] -] -qed-. - -(* Basic_1: was just: pr3_iso_appls_abbr *) -lemma cpxs_fwd_theta_vector: ∀h,o,G,L,V1b,V2b. ⬆*[1] V1b ≡ V2b → - ∀p,V,T,U. ⦃G, L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] U → - ⒶV1b.ⓓ{p}V.T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] U. -#h #o #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/ -#V1b #V2b #V1a #V2a #HV12a #HV12b #p -generalize in match HV12a; -HV12a -generalize in match V2a; -V2a -generalize in match V1a; -V1a -elim HV12b -V1b -V2b /2 width=1 by cpxs_fwd_theta/ -#V1b #V2b #V1b #V2b #HV12b #_ #IHV12b #V1a #V2a #HV12a #V #T #U #H -elim (cpxs_inv_appl1 … H) -H * -[ -IHV12b -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ -| #q #W0 #T0 #HT0 #HU - elim (IHV12b … HV12b … HT0) -IHV12b -HT0 #HT0 - [ -HV12a -HV12b -HU - elim (tsts_inv_pair1 … HT0) #V1 #T1 #H destruct - | @or_intror -V1b (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - elim (cpxs_inv_abbr1 … HT0) -HT0 * - [ -HV12a #V1 #T1 #_ #_ #H destruct - | -V1b #X #HT1 #H #H0 destruct - elim (lifts_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct - @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{q}W1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b - @(cpxs_strap2 … (ⓐV1a.ⓛ{q}W0.T0)) - /4 width=7 by cpxs_beta_dx, cpx_zeta, lifts_bind, lifts_flat/ - ] - ] -| #q #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU - elim (IHV12b … HV12b … HT0) -HV12b -IHV12b -HT0 #HT0 - [ -HV12a -HV10a -HV0a -HU - elim (tsts_inv_pair1 … HT0) #V1 #T1 #H destruct - | @or_intror -V1b -V1b (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - elim (cpxs_inv_abbr1 … HT0) -HT0 * - [ #V1 #T1 #HV1 #HT1 #H destruct - elim (cpxs_lifts … HV10a (Ⓣ) … (L.ⓓV) … HV12a) -V1a /3 width=1 by drops_refl, drops_drop/ #X #H - <(lifts_mono … HV0a … H) -V0a -X #HV2a - @(cpxs_trans … (ⓓ{p}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/ - | #X #HT1 #H #H0 destruct - elim (lifts_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct - elim (cpxs_lifts … HV10a (Ⓣ) … (L.ⓓV0) … HV12a) /3 width=1 by drops_refl, drops_drop/ #X #H - <(lifts_mono … HV0a … H) -V0a -X #HV2a - @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{q}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b - @(cpxs_strap2 … (ⓐV1a.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V1 -T1 - @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/ - ] - ] -] -qed-. - -(* Basic_1: was just: pr3_iso_appls_cast *) -lemma cpxs_fwd_cast_vector: ∀h,o,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ⬈*[h] U → - ∨∨ ⒶVs. ⓝW. T ⩳[h, o] U - | ⦃G, L⦄ ⊢ ⒶVs.T ⬈*[h] U - | ⦃G, L⦄ ⊢ ⒶVs.W ⬈*[h] U. -#h #o #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/ -#V #Vs #IHVs #W #T #U #H -elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/ -| #q #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tsts_inv_applv_bind_simple … HT0) // - | @or3_intro1 -W (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ - | @or3_intro2 -T (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ - ] -| #q #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU - elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tsts_inv_applv_bind_simple … HT0) // - | @or3_intro1 -W (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ - | @or3_intro2 -T (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ - ] -] -qed-. - -(* Basic_1: was just: nf2_iso_appls_lref *) -lemma cpxs_fwd_cnx_vector: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → - ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ⬈*[h] U → ⒶVs.T ⩳[h, o] U. -#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *) -#V #Vs #IHVs #U #H -elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair/ -| #p #W0 #T0 #HT0 #HU - lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (tsts_inv_applv_bind_simple … HT0) // -| #p #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU - lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (tsts_inv_applv_bind_simple … HT0) // -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma index a9d3e4cae..89f226a30 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma @@ -14,7 +14,7 @@ include "basic_2/computation/gcp_aaa.ma". include "basic_2/computation/cpxs_aaa.ma". -include "basic_2/computation/csx_tsts_vector.ma". +include "basic_2/computation/csx_theq_vector.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma index da5803ae0..8caea5831 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/syntax/tsts_tsts.ma". include "basic_2/computation/cpxs_cpxs.ma". include "basic_2/computation/csx_alt.ma". include "basic_2/computation/csx_lift.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq.ma new file mode 100644 index 000000000..83c8fd43e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/theq_simple.ma". +include "basic_2/syntax/theq_theq.ma". +include "basic_2/rt_transition/cpx_simple.ma". +include "basic_2/rt_computation/cpxs.ma". +include "basic_2/rt_computation/csx_csx.ma". + +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) + +(* Properties with head equivalence for terms *******************************) + +(* Basic_1: was just: sn3_appl_appl *) +(* Basic_2A1: was: csx_appl_simple_tsts *) +lemma csx_appl_simple_theq: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T2⦄) → + 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T1⦄. +#h #o #G #L #V #H @(csx_ind … H) -V +#V #_ #IHV #T1 #H @(csx_ind … H) -T1 +#T1 #H1T1 #IHT1 #H2T1 #H3T1 +@csx_intro #X #HL #H +elim (cpx_inv_appl1_simple … HL) -HL // +#V0 #T0 #HLV0 #HLT10 #H0 destruct +elim (tdneq_inv_pair … H) -H +[ #H elim H -H // +| -IHT1 #HV0 + @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10 + @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ +| -IHV -H1T1 #H1T10 + @(csx_cpx_trans … (ⓐV.T0)) /2 width=1 by cpx_flat/ -HLV0 + elim (theq_dec h o T1 T0) #H2T10 + [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, theq_canc_sn, simple_theq_repl_dx/ + | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/ + ] +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma new file mode 100644 index 000000000..2c8dda2dc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma @@ -0,0 +1,128 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/gcp_cr.ma". +include "basic_2/computation/cpxs_theq_vector.ma". +include "basic_2/computation/csx_lpx.ma". +include "basic_2/computation/csx_vector.ma". + +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) + +(* Advanced properties ******************************************************) + +(* Basic_1: was just: sn3_appls_lref *) +lemma csx_applv_cnx: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → + ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Vs → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.T. +#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *) +#V #Vs #IHV #H +elim (csxv_inv_cons … H) -H #HV #HVs +@csx_appl_simple_theq /2 width=1 by applv_simple/ -IHV -HV -HVs +#X #H #H0 +lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H +elim (H0) -H0 // +qed. + +lemma csx_applv_sort: ∀h,o,G,L,s,Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Vs → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.⋆s. +#h #o #G #L #s elim (deg_total h o s) +#d generalize in match s; -s @(nat_ind_plus … d) -d [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ] +#d #IHd #s #Hkd lapply (deg_next_SO … Hkd) -Hkd +#Hkd #Vs elim Vs -Vs /2 width=1 by/ +#V #Vs #IHVs #HVVs +elim (csxv_inv_cons … HVVs) #HV #HVs +@csx_appl_simple_theq /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs +#X #H #H0 +elim (cpxs_fwd_sort_vector … H) -H #H +[ elim H0 -H0 // +| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h s))) /2 width=1 by cpxs_flat_dx/ +] +qed. + +(* Basic_1: was just: sn3_appls_beta *) +lemma csx_applv_beta: ∀h,o,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.ⓓ{a}ⓝW.V.T → + ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs. ⓐV.ⓛ{a}W.T. +#h #o #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/ +#V0 #Vs #IHV #V #W #T #H1T +lapply (csx_fwd_pair_sn … H1T) #HV0 +lapply (csx_fwd_flat_dx … H1T) #H2T +@csx_appl_simple_theq /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T +#X #H #H0 +elim (cpxs_fwd_beta_vector … H) -H #H +[ -H1T elim H0 -H0 // +| -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ +] +qed. + +lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇[i] L ≡ K.ⓑ{I}V1 → + ∀V2. ⬆[0, i + 1] V1 ≡ V2 → + ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, o] (ⒶVs.#i). +#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs +[ /4 width=12 by csx_inv_lift, csx_lref_bind, drop_fwd_drop2/ +| #V #Vs #IHV #H1T + lapply (csx_fwd_pair_sn … H1T) #HV + lapply (csx_fwd_flat_dx … H1T) #H2T + @csx_appl_simple_theq /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T + #X #H #H0 + elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H + [ -H1T elim H0 -H0 // + | -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ + ] +] +qed. + +(* Basic_1: was just: sn3_appls_abbr *) +lemma csx_applv_theta: ∀h,o,a,G,L,V1b,V2b. ⬆[0, 1] V1b ≡ V2b → + ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⓓ{a}V.ⒶV2b.T → + ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶV1b.ⓓ{a}V.T. +#h #o #a #G #L #V1b #V2b * -V1b -V2b /2 width=1 by/ +#V1b #V2b #V1 #V2 #HV12 #H +generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 +elim H -V1b -V2b /2 width=3 by csx_appl_theta/ +#V1b #V2b #V1 #V2 #HV12 #HV12b #IHV12b #W1 #W2 #HW12 #V #T #H +lapply (csx_appl_theta … HW12 … H) -H -HW12 #H +lapply (csx_fwd_pair_sn … H) #HW1 +lapply (csx_fwd_flat_dx … H) #H1 +@csx_appl_simple_theq /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2 +elim (cpxs_fwd_theta_vector … (V2@V2b) … H1) -H1 /2 width=1 by liftv_cons/ -HV12b -HV12 +[ -H #H elim H2 -H2 // +| -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ +] +qed. + +(* Basic_1: was just: sn3_appls_cast *) +lemma csx_applv_cast: ∀h,o,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.T → + ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.ⓝW.T. +#h #o #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/ +#V #Vs #IHV #W #T #H1W #H1T +lapply (csx_fwd_pair_sn … H1W) #HV +lapply (csx_fwd_flat_dx … H1W) #H2W +lapply (csx_fwd_flat_dx … H1T) #H2T +@csx_appl_simple_theq /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T +#X #H #H0 +elim (cpxs_fwd_cast_vector … H) -H #H +[ -H1W -H1T elim H0 -H0 // +| -H1W -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ +| -H1T -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ +] +qed. + +theorem csx_gcr: ∀h,o. gcr (cpx h o) (eq …) (csx h o) (csx h o). +#h #o @mk_gcr // +[ /3 width=1 by csx_applv_cnx/ +|2,3,6: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/ +| /2 width=7 by csx_applv_delta/ +| #G #L #V1b #V2b #HV12b #a #V #T #H #HV + @(csx_applv_theta … HV12b) -HV12b + @csx_abbr // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts.ma deleted file mode 100644 index d0c9837c7..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts.ma +++ /dev/null @@ -1,47 +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 "basic_2/syntax/tsts_simple.ma". -include "basic_2/syntax/tsts_tsts.ma". -include "basic_2/rt_transition/cpx_simple.ma". -include "basic_2/rt_computation/cpxs.ma". -include "basic_2/rt_computation/csx_csx.ma". - -(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) - -(* Properties with same top term structure **********************************) - -(* Basic_1: was just: sn3_appl_appl *) -lemma csx_appl_simple_tsts: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T2⦄) → - 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T1⦄. -#h #o #G #L #V #H @(csx_ind … H) -V -#V #_ #IHV #T1 #H @(csx_ind … H) -T1 -#T1 #H1T1 #IHT1 #H2T1 #H3T1 -@csx_intro #X #HL #H -elim (cpx_inv_appl1_simple … HL) -HL // -#V0 #T0 #HLV0 #HLT10 #H0 destruct -elim (tdneq_inv_pair … H) -H -[ #H elim H -H // -| -IHT1 #HV0 - @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10 - @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ -| -IHV -H1T1 #H1T10 - @(csx_cpx_trans … (ⓐV.T0)) /2 width=1 by cpx_flat/ -HLV0 - elim (tsts_dec h o T1 T0) #H2T10 - [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, tsts_canc_sn, simple_tsts_repl_dx/ - | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/ - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts_vector.ma deleted file mode 100644 index c8250d40c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts_vector.ma +++ /dev/null @@ -1,128 +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 "basic_2/computation/gcp_cr.ma". -include "basic_2/computation/cpxs_tsts_vector.ma". -include "basic_2/computation/csx_lpx.ma". -include "basic_2/computation/csx_vector.ma". - -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) - -(* Advanced properties ******************************************************) - -(* Basic_1: was just: sn3_appls_lref *) -lemma csx_applv_cnx: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → - ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Vs → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.T. -#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *) -#V #Vs #IHV #H -elim (csxv_inv_cons … H) -H #HV #HVs -@csx_appl_simple_tsts /2 width=1 by applv_simple/ -IHV -HV -HVs -#X #H #H0 -lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H -elim (H0) -H0 // -qed. - -lemma csx_applv_sort: ∀h,o,G,L,s,Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Vs → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.⋆s. -#h #o #G #L #s elim (deg_total h o s) -#d generalize in match s; -s @(nat_ind_plus … d) -d [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ] -#d #IHd #s #Hkd lapply (deg_next_SO … Hkd) -Hkd -#Hkd #Vs elim Vs -Vs /2 width=1 by/ -#V #Vs #IHVs #HVVs -elim (csxv_inv_cons … HVVs) #HV #HVs -@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs -#X #H #H0 -elim (cpxs_fwd_sort_vector … H) -H #H -[ elim H0 -H0 // -| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h s))) /2 width=1 by cpxs_flat_dx/ -] -qed. - -(* Basic_1: was just: sn3_appls_beta *) -lemma csx_applv_beta: ∀h,o,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.ⓓ{a}ⓝW.V.T → - ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs. ⓐV.ⓛ{a}W.T. -#h #o #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/ -#V0 #Vs #IHV #V #W #T #H1T -lapply (csx_fwd_pair_sn … H1T) #HV0 -lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T -#X #H #H0 -elim (cpxs_fwd_beta_vector … H) -H #H -[ -H1T elim H0 -H0 // -| -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ -] -qed. - -lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇[i] L ≡ K.ⓑ{I}V1 → - ∀V2. ⬆[0, i + 1] V1 ≡ V2 → - ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, o] (ⒶVs.#i). -#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs -[ /4 width=12 by csx_inv_lift, csx_lref_bind, drop_fwd_drop2/ -| #V #Vs #IHV #H1T - lapply (csx_fwd_pair_sn … H1T) #HV - lapply (csx_fwd_flat_dx … H1T) #H2T - @csx_appl_simple_tsts /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T - #X #H #H0 - elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H - [ -H1T elim H0 -H0 // - | -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ - ] -] -qed. - -(* Basic_1: was just: sn3_appls_abbr *) -lemma csx_applv_theta: ∀h,o,a,G,L,V1b,V2b. ⬆[0, 1] V1b ≡ V2b → - ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⓓ{a}V.ⒶV2b.T → - ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶV1b.ⓓ{a}V.T. -#h #o #a #G #L #V1b #V2b * -V1b -V2b /2 width=1 by/ -#V1b #V2b #V1 #V2 #HV12 #H -generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 -elim H -V1b -V2b /2 width=3 by csx_appl_theta/ -#V1b #V2b #V1 #V2 #HV12 #HV12b #IHV12b #W1 #W2 #HW12 #V #T #H -lapply (csx_appl_theta … HW12 … H) -H -HW12 #H -lapply (csx_fwd_pair_sn … H) #HW1 -lapply (csx_fwd_flat_dx … H) #H1 -@csx_appl_simple_tsts /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2 -elim (cpxs_fwd_theta_vector … (V2@V2b) … H1) -H1 /2 width=1 by liftv_cons/ -HV12b -HV12 -[ -H #H elim H2 -H2 // -| -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ -] -qed. - -(* Basic_1: was just: sn3_appls_cast *) -lemma csx_applv_cast: ∀h,o,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.T → - ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.ⓝW.T. -#h #o #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/ -#V #Vs #IHV #W #T #H1W #H1T -lapply (csx_fwd_pair_sn … H1W) #HV -lapply (csx_fwd_flat_dx … H1W) #H2W -lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T -#X #H #H0 -elim (cpxs_fwd_cast_vector … H) -H #H -[ -H1W -H1T elim H0 -H0 // -| -H1W -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ -| -H1T -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ -] -qed. - -theorem csx_gcr: ∀h,o. gcr (cpx h o) (eq …) (csx h o) (csx h o). -#h #o @mk_gcr // -[ /3 width=1 by csx_applv_cnx/ -|2,3,6: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/ -| /2 width=7 by csx_applv_delta/ -| #G #L #V1b #V2b #HV12b #a #V #T #H #HV - @(csx_applv_theta … HV12b) -HV12b - @csx_abbr // -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 0ff5a431f..5136af26a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,4 +1,4 @@ -cpxs.ma cpxs_tdeq.ma cpxs_tsts.ma cpxs_tsts_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma +cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma -csx.ma csx_simple.ma csx_tsts.ma csx_drops.ma csx_gcp.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma +csx.ma csx_simple.ma csx_theq.ma csx_drops.ma csx_gcp.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma csx_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/theq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq.ma new file mode 100644 index 000000000..a09a53533 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq.ma @@ -0,0 +1,177 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/topiso_4.ma". +include "basic_2/syntax/item_sd.ma". +include "basic_2/syntax/term.ma". + +(* HEAD EQUIVALENCE FOR TERMS ***********************************************) + +(* Basic_2A1: includes: tsts_atom tsts_pair *) +inductive theq (h) (o): relation term ≝ +| theq_sort: ∀s1,s2,d. deg h o s1 d → deg h o s2 d → theq h o (⋆s1) (⋆s2) +| theq_lref: ∀i. theq h o (#i) (#i) +| theq_gref: ∀l. theq h o (§l) (§l) +| theq_pair: ∀I,V1,V2,T1,T2. theq h o (②{I}V1.T1) (②{I}V2.T2) +. + +interpretation "head equivalence (term)" 'TopIso h o T1 T2 = (theq h o T1 T2). + +(* Basic inversion lemmas ***************************************************) + +fact theq_inv_sort1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀s1. X = ⋆s1 → + ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2. +#h #o #X #Y * -X -Y +[ #s1 #s2 #d #Hs1 #Hs2 #s #H destruct /2 width=5 by ex3_2_intro/ +| #i #s #H destruct +| #l #s #H destruct +| #I #V1 #V2 #T1 #T2 #s #H destruct +] +qed-. + +(* Basic_1: was just: iso_gen_sort *) +lemma theq_inv_sort1: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → + ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2. +/2 width=3 by theq_inv_sort1_aux/ qed-. + +fact theq_inv_lref1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀i. X = #i → Y = #i. +#h #o #X #Y * -X -Y // +[ #s1 #s2 #d #_ #_ #j #H destruct +| #I #V1 #V2 #T1 #T2 #j #H destruct +] +qed-. + +(* Basic_1: was: iso_gen_lref *) +lemma theq_inv_lref1: ∀h,o,Y,i. #i ⩳[h, o] Y → Y = #i. +/2 width=5 by theq_inv_lref1_aux/ qed-. + +fact theq_inv_gref1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀l. X = §l → Y = §l. +#h #o #X #Y * -X -Y // +[ #s1 #s2 #d #_ #_ #k #H destruct +| #I #V1 #V2 #T1 #T2 #k #H destruct +] +qed-. + +lemma theq_inv_gref1: ∀h,o,Y,l. §l ⩳[h, o] Y → Y = §l. +/2 width=5 by theq_inv_gref1_aux/ qed-. + +fact theq_inv_pair1_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → + ∀J,W1,U1. T1 = ②{J}W1.U1 → + ∃∃W2,U2. T2 = ②{J}W2.U2. +#h #o #T1 #T2 * -T1 -T2 +[ #s1 #s2 #d #_ #_ #J #W1 #U1 #H destruct +| #i #J #W1 #U1 #H destruct +| #l #J #W1 #U1 #H destruct +| #I #V1 #V2 #T1 #T2 #J #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/ +] +qed-. + +(* Basic_1: was: iso_gen_head *) +(* Basic_2A1: was: tsts_inv_pair1 *) +lemma theq_inv_pair1: ∀h,o,J,W1,U1,T2. ②{J}W1.U1 ⩳[h, o] T2 → + ∃∃W2,U2. T2 = ②{J}W2. U2. +/2 width=7 by theq_inv_pair1_aux/ qed-. + +fact theq_inv_pair2_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → + ∀J,W2,U2. T2 = ②{J}W2.U2 → + ∃∃W1,U1. T1 = ②{J}W1.U1. +#h #o #T1 #T2 * -T1 -T2 +[ #s1 #s2 #d #_ #_ #J #W2 #U2 #H destruct +| #i #J #W2 #U2 #H destruct +| #l #J #W2 #U2 #H destruct +| #I #V1 #V2 #T1 #T2 #J #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/ +] +qed-. + +(* Basic_2A1: was: tsts_inv_pair2 *) +lemma theq_inv_pair2: ∀h,o,J,T1,W2,U2. T1 ⩳[h, o] ②{J}W2.U2 → + ∃∃W1,U1. T1 = ②{J}W1.U1. +/2 width=7 by theq_inv_pair2_aux/ qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma theq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → ∀d. deg h o s1 d → + ∃∃s2. deg h o s2 d & Y = ⋆s2. +#h #o #Y #s1 #H #d #Hs1 elim (theq_inv_sort1 … H) -H +#s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/ +qed-. + +lemma theq_inv_sort_deg: ∀h,o,s1,s2. ⋆s1 ⩳[h, o] ⋆s2 → + ∀d1,d2. deg h o s1 d1 → deg h o s2 d2 → + d1 = d2. +#h #o #s1 #y #H #d1 #d2 #Hs1 #Hy +elim (theq_inv_sort1_deg … H … Hs1) -s1 #s2 #Hs2 #H destruct +<(deg_mono h o … Hy … Hs2) -s2 -d1 // +qed-. + +lemma theq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳[h, o] ②{I2}V2.T2 → + I1 = I2. +#h #o #I1 #I2 #V1 #V2 #T1 #T2 #H elim (theq_inv_pair1 … H) -H +#V0 #T0 #H destruct // +qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was: iso_refl *) +(* Basic_2A1: was: tsts_refl *) +lemma theq_refl: ∀h,o. reflexive … (theq h o). +#h #o * // +* /2 width=1 by theq_lref, theq_gref/ +#s elim (deg_total h o s) /2 width=3 by theq_sort/ +qed. + +(* Basic_2A1: was: tsts_sym *) +lemma theq_sym: ∀h,o. symmetric … (theq h o). +#h #o #T1 #T2 * -T1 -T2 /2 width=3 by theq_sort/ +qed-. + +(* Basic_2A1: was: tsts_dec *) +lemma theq_dec: ∀h,o,T1,T2. Decidable (T1 ⩳[h, o] T2). +#h #o * [ * #s1 | #I1 #V1 #T1 ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ] +[ elim (deg_total h o s1) #d1 #H1 + elim (deg_total h o s2) #d2 #H2 + elim (eq_nat_dec d1 d2) #Hd12 destruct /3 width=3 by theq_sort, or_introl/ + @or_intror #H + lapply (theq_inv_sort_deg … H … H1 H2) -H -H1 -H2 /2 width=1 by/ +|2,3,13: + @or_intror #H + elim (theq_inv_sort1 … H) -H #x1 #x2 #_ #_ #H destruct +|4,6,14: + @or_intror #H + lapply (theq_inv_lref1 … H) -H #H destruct +|5: + elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ + @or_intror #H + lapply (theq_inv_lref1 … H) -H #H destruct /2 width=1 by/ +|7,8,15: + @or_intror #H + lapply (theq_inv_gref1 … H) -H #H destruct +|9: + elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ + @or_intror #H + lapply (theq_inv_gref1 … H) -H #H destruct /2 width=1 by/ +|10,11,12: + @or_intror #H + elim (theq_inv_pair1 … H) -H #X1 #X2 #H destruct +|16: + elim (eq_item2_dec I1 I2) #HI12 destruct + [ /3 width=1 by theq_pair, or_introl/ ] + @or_intror #H + lapply (theq_inv_pair … H) -H /2 width=1 by/ +] +qed-. + +(* Basic_2A1: removed theorems 2: + tsts_inv_atom1 tsts_inv_atom2 +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_simple.ma new file mode 100644 index 000000000..a260edd75 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_simple.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/term_simple.ma". +include "basic_2/syntax/theq.ma". + +(* HEAD EQUIVALENCE FOR TERMS ***********************************************) + +(* Properies with simple (neutral) terms ************************************) + +(* Basic_2A1: was: simple_tsts_repl_dx *) +lemma simple_theq_repl_dx: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. +#h #o #T1 #T2 * -T1 -T2 // +#I #V1 #V2 #T1 #T2 #H +elim (simple_inv_pair … H) -H #J #H destruct // +qed-. + +(* Basic_2A1: was: simple_tsts_repl_sn *) +lemma simple_theq_repl_sn: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. +/3 width=5 by simple_theq_repl_dx, theq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_simple_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_simple_vector.ma new file mode 100644 index 000000000..a17c97090 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_simple_vector.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/term_vector.ma". +include "basic_2/syntax/theq_simple.ma". + +(* HEAD EQUIVALENCE FOR TERMS ***********************************************) + +(* Advanced inversion lemmas with simple (neutral) terms ********************) + +(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *) +(* Basic_2A1: was: tsts_inv_bind_applv_simple *) +lemma theq_inv_applv_bind_simple: ∀h,o,p,I,Vs,V2,T1,T2. ⒶVs.T1 ⩳[h, o] ⓑ{p,I}V2.T2 → + 𝐒⦃T1⦄ → ⊥. +#h #o #p #I #Vs #V2 #T1 #T2 #H elim (theq_inv_pair2 … H) -H +#V0 #T0 elim Vs -Vs normalize +[ #H destruct #H /2 width=5 by simple_inv_bind/ +| #V #Vs #_ #H destruct +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma new file mode 100644 index 000000000..2a111b40f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/tdeq.ma". +include "basic_2/syntax/theq.ma". + +(* HEAD EQUIVALENCE FOR TERMS ***********************************************) + +(* Properties with degree-based equivalence for terms ***********************) + +lemma tdeq_theq: ∀h,o,T1,T2. T1 ≡[h, o] T2 → T1 ⩳[h, o] T2. +#h #o #T1 #T2 * -T1 -T2 /2 width=3 by theq_sort, theq_pair/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_theq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_theq.ma new file mode 100644 index 000000000..88547d98e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_theq.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/theq.ma". + +(* HEAD EQUIVALENCE FOR TERMS ***********************************************) + +(* Main properties **********************************************************) + +(* Basic_1: was: iso_trans *) +(* Basic_2A1: was: tsts_trans *) +theorem theq_trans: ∀h,o. Transitive … (theq h o). +#h #o #T1 #T * -T1 -T +[ #s1 #s #d #Hs1 #Hs #X #H + elim (theq_inv_sort1_deg … H … Hs) -s /2 width=3 by theq_sort/ +| #i1 #i #H <(theq_inv_lref1 … H) -H // +| #l1 #l #H <(theq_inv_gref1 … H) -H // +| #I #V1 #V #T1 #T #X #H + elim (theq_inv_pair1 … H) -H #V2 #T2 #H destruct // +] +qed-. + +(* Basic_2A1: was: tsts_canc_sn *) +theorem theq_canc_sn: ∀h,o. left_cancellable … (theq h o). +/3 width=3 by theq_trans, theq_sym/ qed-. + +(* Basic_2A1: was: tsts_canc_dx *) +theorem theq_canc_dx: ∀h,o. right_cancellable … (theq h o). +/3 width=3 by theq_trans, theq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma deleted file mode 100644 index 6ea5dc782..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma +++ /dev/null @@ -1,172 +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 "basic_2/notation/relations/topiso_4.ma". -include "basic_2/syntax/item_sd.ma". -include "basic_2/syntax/term.ma". - -(* SAME TOP TERM STRUCTURE **************************************************) - -(* Basic_2A1: includes: tsts_atom *) -inductive tsts (h) (o): relation term ≝ -| tsts_sort: ∀s1,s2,d. deg h o s1 d → deg h o s2 d → tsts h o (⋆s1) (⋆s2) -| tsts_lref: ∀i. tsts h o (#i) (#i) -| tsts_gref: ∀l. tsts h o (§l) (§l) -| tsts_pair: ∀I,V1,V2,T1,T2. tsts h o (②{I}V1.T1) (②{I}V2.T2) -. - -interpretation "same top structure (term)" 'TopIso h o T1 T2 = (tsts h o T1 T2). - -(* Basic inversion lemmas ***************************************************) - -fact tsts_inv_sort1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀s1. X = ⋆s1 → - ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2. -#h #o #X #Y * -X -Y -[ #s1 #s2 #d #Hs1 #Hs2 #s #H destruct /2 width=5 by ex3_2_intro/ -| #i #s #H destruct -| #l #s #H destruct -| #I #V1 #V2 #T1 #T2 #s #H destruct -] -qed-. - -(* Basic_1: was just: iso_gen_sort *) -lemma tsts_inv_sort1: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → - ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2. -/2 width=3 by tsts_inv_sort1_aux/ qed-. - -fact tsts_inv_lref1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀i. X = #i → Y = #i. -#h #o #X #Y * -X -Y // -[ #s1 #s2 #d #_ #_ #j #H destruct -| #I #V1 #V2 #T1 #T2 #j #H destruct -] -qed-. - -(* Basic_1: was: iso_gen_lref *) -lemma tsts_inv_lref1: ∀h,o,Y,i. #i ⩳[h, o] Y → Y = #i. -/2 width=5 by tsts_inv_lref1_aux/ qed-. - -fact tsts_inv_gref1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀l. X = §l → Y = §l. -#h #o #X #Y * -X -Y // -[ #s1 #s2 #d #_ #_ #k #H destruct -| #I #V1 #V2 #T1 #T2 #k #H destruct -] -qed-. - -lemma tsts_inv_gref1: ∀h,o,Y,l. §l ⩳[h, o] Y → Y = §l. -/2 width=5 by tsts_inv_gref1_aux/ qed-. - -fact tsts_inv_pair1_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → - ∀J,W1,U1. T1 = ②{J}W1.U1 → - ∃∃W2,U2. T2 = ②{J}W2.U2. -#h #o #T1 #T2 * -T1 -T2 -[ #s1 #s2 #d #_ #_ #J #W1 #U1 #H destruct -| #i #J #W1 #U1 #H destruct -| #l #J #W1 #U1 #H destruct -| #I #V1 #V2 #T1 #T2 #J #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/ -] -qed-. - -(* Basic_1: was: iso_gen_head *) -lemma tsts_inv_pair1: ∀h,o,J,W1,U1,T2. ②{J}W1.U1 ⩳[h, o] T2 → - ∃∃W2,U2. T2 = ②{J}W2. U2. -/2 width=7 by tsts_inv_pair1_aux/ qed-. - -fact tsts_inv_pair2_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → - ∀J,W2,U2. T2 = ②{J}W2.U2 → - ∃∃W1,U1. T1 = ②{J}W1.U1. -#h #o #T1 #T2 * -T1 -T2 -[ #s1 #s2 #d #_ #_ #J #W2 #U2 #H destruct -| #i #J #W2 #U2 #H destruct -| #l #J #W2 #U2 #H destruct -| #I #V1 #V2 #T1 #T2 #J #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/ -] -qed-. - -lemma tsts_inv_pair2: ∀h,o,J,T1,W2,U2. T1 ⩳[h, o] ②{J}W2.U2 → - ∃∃W1,U1. T1 = ②{J}W1.U1. -/2 width=7 by tsts_inv_pair2_aux/ qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma tsts_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → ∀d. deg h o s1 d → - ∃∃s2. deg h o s2 d & Y = ⋆s2. -#h #o #Y #s1 #H #d #Hs1 elim (tsts_inv_sort1 … H) -H -#s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/ -qed-. - -lemma tsts_inv_sort_deg: ∀h,o,s1,s2. ⋆s1 ⩳[h, o] ⋆s2 → - ∀d1,d2. deg h o s1 d1 → deg h o s2 d2 → - d1 = d2. -#h #o #s1 #y #H #d1 #d2 #Hs1 #Hy -elim (tsts_inv_sort1_deg … H … Hs1) -s1 #s2 #Hs2 #H destruct -<(deg_mono h o … Hy … Hs2) -s2 -d1 // -qed-. - -lemma tsts_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳[h, o] ②{I2}V2.T2 → - I1 = I2. -#h #o #I1 #I2 #V1 #V2 #T1 #T2 #H elim (tsts_inv_pair1 … H) -H -#V0 #T0 #H destruct // -qed-. - -(* Basic properties *********************************************************) - -(* Basic_1: was: iso_refl *) -lemma tsts_refl: ∀h,o. reflexive … (tsts h o). -#h #o * // -* /2 width=1 by tsts_lref, tsts_gref/ -#s elim (deg_total h o s) /2 width=3 by tsts_sort/ -qed. - -lemma tsts_sym: ∀h,o. symmetric … (tsts h o). -#h #o #T1 #T2 * -T1 -T2 /2 width=3 by tsts_sort/ -qed-. - -lemma tsts_dec: ∀h,o,T1,T2. Decidable (T1 ⩳[h, o] T2). -#h #o * [ * #s1 | #I1 #V1 #T1 ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ] -[ elim (deg_total h o s1) #d1 #H1 - elim (deg_total h o s2) #d2 #H2 - elim (eq_nat_dec d1 d2) #Hd12 destruct /3 width=3 by tsts_sort, or_introl/ - @or_intror #H - lapply (tsts_inv_sort_deg … H … H1 H2) -H -H1 -H2 /2 width=1 by/ -|2,3,13: - @or_intror #H - elim (tsts_inv_sort1 … H) -H #x1 #x2 #_ #_ #H destruct -|4,6,14: - @or_intror #H - lapply (tsts_inv_lref1 … H) -H #H destruct -|5: - elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ - @or_intror #H - lapply (tsts_inv_lref1 … H) -H #H destruct /2 width=1 by/ -|7,8,15: - @or_intror #H - lapply (tsts_inv_gref1 … H) -H #H destruct -|9: - elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ - @or_intror #H - lapply (tsts_inv_gref1 … H) -H #H destruct /2 width=1 by/ -|10,11,12: - @or_intror #H - elim (tsts_inv_pair1 … H) -H #X1 #X2 #H destruct -|16: - elim (eq_item2_dec I1 I2) #HI12 destruct - [ /3 width=1 by tsts_pair, or_introl/ ] - @or_intror #H - lapply (tsts_inv_pair … H) -H /2 width=1 by/ -] -qed-. - -(* Basic_2A1: removed theorems 4: - tsts_inv_atom1 tsts_inv_atom2 -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple.ma deleted file mode 100644 index fe3613e8d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple.ma +++ /dev/null @@ -1,29 +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 "basic_2/syntax/term_simple.ma". -include "basic_2/syntax/tsts.ma". - -(* SAME TOP TERM STRUCTURE **************************************************) - -(* Properies with simple (neutral) terms ************************************) - -lemma simple_tsts_repl_dx: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. -#h #o #T1 #T2 * -T1 -T2 // -#I #V1 #V2 #T1 #T2 #H -elim (simple_inv_pair … H) -H #J #H destruct // -qed-. - -lemma simple_tsts_repl_sn: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. -/3 width=5 by simple_tsts_repl_dx, tsts_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple_vector.ma deleted file mode 100644 index 2320a0cf9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple_vector.ma +++ /dev/null @@ -1,31 +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 "basic_2/syntax/term_vector.ma". -include "basic_2/syntax/tsts_simple.ma". - -(* SAME TOP TERM STRUCTURE **************************************************) - -(* Advanced inversion lemmas with simple (neutral) terms ********************) - -(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *) -(* Basic_2A1: was: tsts_inv_bind_applv_simple *) -lemma tsts_inv_applv_bind_simple: ∀h,o,p,I,Vs,V2,T1,T2. ⒶVs.T1 ⩳[h, o] ⓑ{p,I}V2.T2 → - 𝐒⦃T1⦄ → ⊥. -#h #o #p #I #Vs #V2 #T1 #T2 #H elim (tsts_inv_pair2 … H) -H -#V0 #T0 elim Vs -Vs normalize -[ #H destruct #H /2 width=5 by simple_inv_bind/ -| #V #Vs #_ #H destruct -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tdeq.ma deleted file mode 100644 index 08e358784..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tdeq.ma +++ /dev/null @@ -1,24 +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 "basic_2/syntax/tdeq.ma". -include "basic_2/syntax/tsts.ma". - -(* SAME TOP TERM STRUCTURE **************************************************) - -(* Properties with degree-based equivalence for terms ***********************) - -lemma tdeq_tsts: ∀h,o,T1,T2. T1 ≡[h, o] T2 → T1 ⩳[h, o] T2. -#h #o #T1 #T2 * -T1 -T2 /2 width=3 by tsts_sort, tsts_pair/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tsts.ma deleted file mode 100644 index b3c790e53..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tsts.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 "basic_2/syntax/tsts.ma". - -(* SAME TOP TERM STRUCTURE **************************************************) - -(* Main properties **********************************************************) - -(* Basic_1: was: iso_trans *) -theorem tsts_trans: ∀h,o. Transitive … (tsts h o). -#h #o #T1 #T * -T1 -T -[ #s1 #s #d #Hs1 #Hs #X #H - elim (tsts_inv_sort1_deg … H … Hs) -s /2 width=3 by tsts_sort/ -| #i1 #i #H <(tsts_inv_lref1 … H) -H // -| #l1 #l #H <(tsts_inv_gref1 … H) -H // -| #I #V1 #V #T1 #T #X #H - elim (tsts_inv_pair1 … H) -H #V2 #T2 #H destruct // -] -qed-. - -theorem tsts_canc_sn: ∀h,o. left_cancellable … (tsts h o). -/3 width=3 by tsts_trans, tsts_sym/ qed-. - -theorem tsts_canc_dx: ∀h,o. right_cancellable … (tsts h o). -/3 width=3 by tsts_trans, tsts_sym/ qed-. 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 ed35813d2..efb95c8e3 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 @@ -89,7 +89,7 @@ table { [ { "strongly normalizing rt-computation" * } { [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ] [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )" "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ] - [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tsts_vector" + "csx_aaa" * ] + [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_theq_vector" + "csx_aaa" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lleq" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ] } ] @@ -114,9 +114,9 @@ table { [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ] *) [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ] - [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_tsts" + "csx_drops" + "csx_gcp" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] + [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_theq" + "csx_drops" + "csx_gcp" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } ] } @@ -233,8 +233,8 @@ table { [ "append ( ? @@ ? )" "append_length" * ] } ] - [ { "same top term structure" * } { - [ "tsts ( ? ⩳[?,?] ? )" "tsts_simple" + "tsts_tdeq" + "tsts_tsts" + "tsts_simple_vector" * ] + [ { "head equivalence for terms" * } { + [ "theq ( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ] } ] [ { "degree-based equivalence for terms" * } {