From: Ferruccio Guidi Date: Fri, 17 Mar 2017 18:54:16 +0000 (+0000) Subject: advances on csx towards strong normalization of rt-computation ,,, X-Git-Tag: make_still_working~475 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=2f00c2224c66757d00883602cfd0bbd2448eb3ca advances on csx towards strong normalization of rt-computation ,,, --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma index afb3e127a..6f0cef9d0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma @@ -49,6 +49,14 @@ definition deliftable2_sn: predicate (relation term) ≝ λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≡ U1 → ∃∃T2. ⬆*[f] T2 ≡ U2 & R T1 T2. +definition liftable2_bi: predicate (relation term) ≝ + λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⬆*[f] T1 ≡ U1 → + ∀U2. ⬆*[f] T2 ≡ U2 → R U1 U2. + +definition deliftable2_bi: predicate (relation term) ≝ + λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≡ U1 → + ∀T2. ⬆*[f] T2 ≡ U2 → R T1 T2. + (* Basic inversion lemmas ***************************************************) fact lifts_inv_sort1_aux: ∀f,X,Y. ⬆*[f] X ≡ Y → ∀s. X = ⋆s → Y = ⋆s. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma index f679a756d..381c1c96c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma @@ -116,3 +116,15 @@ lemma lifts_mono: ∀f,T,U1. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 #f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐈𝐝 … f) /3 width=6 by lifts_conf, lifts_fwd_isid/ qed-. + +lemma liftable2_sn_bi: ∀R. liftable2 R → liftable2_bi R. +#R #HR #T1 #T2 #HT12 #f #U1 #HTU1 #U2 #HTU2 +elim (HR … HT12 … HTU1) -HR -T1 #X #HTX #HUX +<(lifts_mono … HTX … HTU2) -T2 -U2 -f // +qed-. + +lemma deliftable2_sn_bi: ∀R. deliftable2_sn R → deliftable2_bi R. +#R #HR #U1 #U2 #HU12 #f #T1 #HTU1 #T2 #HTU2 +elim (HR … HU12 … HTU1) -HR -U1 #X #HUX #HTX +<(lifts_inj … HUX … HTU2) -U2 -T2 -f // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma index 205514ce6..e581cc538 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/syntax/tdeq.ma". -include "basic_2/relocation/lifts.ma". +include "basic_2/relocation/lifts_lifts.ma". (* GENERIC RELOCATION FOR TERMS *********************************************) @@ -38,6 +38,9 @@ lemma tdeq_lifts: ∀h,o. liftable2 (tdeq h o). ] qed-. +lemma tdeq_lifts_bi: ∀h,o. liftable2_bi (tdeq h o). +/3 width=6 by tdeq_lifts, liftable2_sn_bi/ qed-. + (* Inversion lemmas with degree-based equivalence for terms *****************) lemma tdeq_inv_lifts: ∀h,o. deliftable2_sn (tdeq h o). @@ -58,3 +61,6 @@ lemma tdeq_inv_lifts: ∀h,o. deliftable2_sn (tdeq h o). /3 width=5 by lifts_flat, tdeq_pair, ex2_intro/ ] qed-. + +lemma tdeq_inv_lifts_bi: ∀h,o. deliftable2_bi (tdeq h o). +/3 width=6 by tdeq_inv_lifts, deliftable2_sn_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma index 628611eac..b675ddec7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma @@ -14,7 +14,7 @@ include "basic_2/syntax/tdeq_tdeq.ma". include "basic_2/rt_transition/lfpx_lfdeq.ma". -include "basic_2/rt_computation/csx.ma". +include "basic_2/rt_computation/csx_drops.ma". (* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) @@ -49,3 +49,27 @@ lemma csx_cast: ∀h,o,G,L,W. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃W⦄ → |*: /3 width=3 by csx_cpx_trans/ ] qed. + +(* Basic_1: was just: sn3_abbr *) +(* Basic_2A1: was: csx_lref_bind *) +lemma csx_lref_drops: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V → + ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄. +#h #o #I #G #L #K #V #i #HLK #HV +@csx_intro #X #H #Hi elim (cpx_inv_lref1_drops … H) -H +[ #H destruct elim Hi // +| -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1 + lapply (drops_mono … HLK0 … HLK) -HLK #H destruct + /3 width=8 by csx_lifts, csx_cpx_trans, drops_isuni_fwd_drop2/ +] +qed. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was: sn3_gen_def *) +(* Basic_2A1: was: csx_inv_lref_bind *) +lemma csx_inv_lref_drops: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V → + ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄ → ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄. +#h #o #I #G #L #K #V #i #HLK #Hi +elim (lifts_total V (𝐔❴⫯i❵)) +/4 width=9 by csx_inv_lifts, csx_cpx_trans, cpx_delta_drops, drops_isuni_fwd_drop2/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma new file mode 100644 index 000000000..f934707bb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/lifts_tdeq.ma". +include "basic_2/rt_transition/cpx_drops.ma". +include "basic_2/rt_computation/csx.ma". + +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) + +(* Properties with generic relocation ***************************************) + +(* Basic_1: was just: sn3_lift *) +(* Basic_2A1: was just: csx_lift *) +lemma csx_lifts: ∀h,o,G. d_liftable1 … (csx h o G). +#h #o #G #K #T #H @(csx_ind … H) -T +#T1 #_ #IH #b #f #L #HLK #U1 #HTU1 +@csx_intro #U2 #HU12 #HnU12 +elim (cpx_inv_lifts … HU12 … HLK … HTU1) -HU12 +/4 width=7 by tdeq_lifts_bi/ +qed-. + +(* Inversion lemmas with generic slicing ************************************) + +(* Basic_1: was just: sn3_gen_lift *) +(* Basic_2A1: was just: csx_inv_lift *) +lemma csx_inv_lifts: ∀h,o,G. d_deliftable1 … (csx h o G). +#h #o #G #L #U #H @(csx_ind … H) -U +#U1 #_ #IH #b #f #K #HLK #T1 #HTU1 +@csx_intro #T2 #HT12 #HnT12 +elim (cpx_lifts … HT12 … HLK … HTU1) -HT12 +/4 width=7 by tdeq_inv_lifts_bi/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma new file mode 100644 index 000000000..4ea05ba43 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma @@ -0,0 +1,28 @@ +lemma csx_fqu_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/2 width=8 by csx_inv_lref_bind, csx_inv_lift, csx_fwd_flat_dx, csx_fwd_bind_dx, csx_fwd_pair_sn/ +qed-. + +lemma csx_fquq_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #H elim (fquq_inv_gen … H12) -H12 +[ /2 width=5 by csx_fqu_conf/ +| * #HG #HL #HT destruct // +] +qed-. + +lemma csx_fqup_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +/3 width=5 by csx_fqu_conf/ +qed-. + +lemma csx_fqus_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #H elim (fqus_inv_gen … H12) -H12 +[ /2 width=5 by csx_fqup_conf/ +| * #HG #HL #HT destruct // +] +qed-. + diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma new file mode 100644 index 000000000..a5bfe6cdf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/gcp.ma". +include "basic_2/rt_transition/cnx_drops.ma". +include "basic_2/rt_computation/csx_drops.ma". + +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) + +(* Main properties **********************************************************) + +theorem csx_gcp: ∀h,o. gcp (cpx h) (tdeq h o) (csx h o). +#h #o @mk_gcp +[ normalize /3 width=13 by cnx_lifts/ +| #G #L elim (deg_total h o 0) /3 width=8 by cnx_sort_iter, ex_intro/ +| /2 width=8 by csx_lifts/ +| /2 width=3 by csx_fwd_flat_dx/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lift.ma deleted file mode 100644 index bfabc34bf..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lift.ma +++ /dev/null @@ -1,119 +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/reduction/cnx_lift.ma". -include "basic_2/computation/gcp.ma". -include "basic_2/computation/csx.ma". - -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) - -(* Relocation properties ****************************************************) - -(* Basic_1: was just: sn3_lift *) -lemma csx_lift: ∀h,o,G,L2,L1,T1,b,l,k. ⦃G, L1⦄ ⊢ ⬊*[h, o] T1 → - ∀T2. ⬇[b, l, k] L2 ≡ L1 → ⬆[l, k] T1 ≡ T2 → ⦃G, L2⦄ ⊢ ⬊*[h, o] T2. -#h #o #G #L2 #L1 #T1 #b #l #k #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12 -@csx_intro #T #HLT2 #HT2 -elim (cpx_inv_lift1 … HLT2 … HL21 … HT12) -HLT2 #T0 #HT0 #HLT10 -@(IHT1 … HLT10) // -L1 -L2 #H destruct ->(lift_mono … HT0 … HT12) in HT2; -T1 /2 width=1 by/ -qed. - -(* Basic_1: was just: sn3_gen_lift *) -lemma csx_inv_lift: ∀h,o,G,L2,L1,T1,b,l,k. ⦃G, L1⦄ ⊢ ⬊*[h, o] T1 → - ∀T2. ⬇[b, l, k] L1 ≡ L2 → ⬆[l, k] T2 ≡ T1 → ⦃G, L2⦄ ⊢ ⬊*[h, o] T2. -#h #o #G #L2 #L1 #T1 #b #l #k #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21 -@csx_intro #T #HLT2 #HT2 -elim (lift_total T l k) #T0 #HT0 -lapply (cpx_lift … HLT2 … HL12 … HT21 … HT0) -HLT2 #HLT10 -@(IHT1 … HLT10) // -L1 -L2 #H destruct ->(lift_inj … HT0 … HT21) in HT2; -T1 /2 width=1 by/ -qed. - -(* Advanced inversion lemmas ************************************************) - -(* Basic_1: was: sn3_gen_def *) -lemma csx_inv_lref_bind: ∀h,o,I,G,L,K,V,i. ⬇[i] L ≡ K.ⓑ{I}V → - ⦃G, L⦄ ⊢ ⬊*[h, o] #i → ⦃G, K⦄ ⊢ ⬊*[h, o] V. -#h #o #I #G #L #K #V #i #HLK #Hi -elim (lift_total V 0 (i+1)) -/4 width=9 by csx_inv_lift, csx_cpx_trans, cpx_delta, drop_fwd_drop2/ -qed-. - -(* Advanced properties ******************************************************) - -(* Basic_1: was just: sn3_abbr *) -lemma csx_lref_bind: ∀h,o,I,G,L,K,V,i. ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ ⬊*[h, o] V → ⦃G, L⦄ ⊢ ⬊*[h, o] #i. -#h #o #I #G #L #K #V #i #HLK #HV -@csx_intro #X #H #Hi -elim (cpx_inv_lref1 … H) -H -[ #H destruct elim Hi // -| -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1 - lapply (drop_mono … HLK0 … HLK) -HLK #H destruct - /3 width=8 by csx_lift, csx_cpx_trans, drop_fwd_drop2/ -] -qed. - -lemma csx_appl_simple: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, o] V → ∀T1. - (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → (T1 = 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 #IHT1 #HT1 -@csx_intro #X #H1 #H2 -elim (cpx_inv_appl1_simple … H1) // -H1 -#V0 #T0 #HLV0 #HLT10 #H destruct -elim (eq_false_inv_tpair_dx … H2) -H2 -[ -IHV -HT1 /4 width=3 by csx_cpx_trans, cpx_pair_sn/ -| -HLT10 * #H #HV0 destruct - @IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ (**) (* full auto 17s *) -] -qed. - -lemma csx_fqu_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬊*[h, o] T2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/2 width=8 by csx_inv_lref_bind, csx_inv_lift, csx_fwd_flat_dx, csx_fwd_bind_dx, csx_fwd_pair_sn/ -qed-. - -lemma csx_fquq_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬊*[h, o] T2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #H elim (fquq_inv_gen … H12) -H12 -[ /2 width=5 by csx_fqu_conf/ -| * #HG #HL #HT destruct // -] -qed-. - -lemma csx_fqup_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬊*[h, o] T2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -/3 width=5 by csx_fqu_conf/ -qed-. - -lemma csx_fqus_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬊*[h, o] T2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #H elim (fqus_inv_gen … H12) -H12 -[ /2 width=5 by csx_fqup_conf/ -| * #HG #HL #HT destruct // -] -qed-. - -(* Main properties **********************************************************) - -theorem csx_gcp: ∀h,o. gcp (cpx h o) (eq …) (csx h o). -#h #o @mk_gcp -[ normalize /3 width=13 by cnx_lift/ -| #G #L elim (deg_total h o 0) /3 width=8 by cnx_sort_iter, ex_intro/ -| /2 width=8 by csx_lift/ -| /2 width=3 by csx_fwd_flat_dx/ -] -qed. 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 1c239f8f8..da5803ae0 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 @@ -116,23 +116,3 @@ qed-. lemma csx_appl_theta: ∀h,o,a,V1,V2. ⬆[0, 1] V1 ≡ V2 → ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓐV1.ⓓ{a}V.T. /2 width=5 by csx_appl_theta_aux/ qed. - -(* 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, o] T2 → (T1 ≂ 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 (eq_false_inv_tpair_sn … 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 -HLV0 * #H #H1T10 destruct - elim (tsts_dec T1 T0) #H2T10 - [ @IHT1 -IHT1 /4 width=3 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_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma new file mode 100644 index 000000000..d6d1c1094 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpx_simple.ma". +include "basic_2/rt_computation/csx_csx.ma". + +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) + +(* Properties with simple terms *********************************************) + +lemma csx_appl_simple: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ∀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 #IHT1 #HT1 +@csx_intro #X #H1 #H2 +elim (cpx_inv_appl1_simple … H1) // -H1 +#V0 #T0 #HLV0 #HLT10 #H destruct +elim (tdneq_inv_pair … H2) -H2 +[ #H elim H -H // +| #HV0 @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10 + @(IHV … HLV0 … HV0) -HV0 /4 width=5 by csx_cpx_trans, cpx_pair_sn/ (**) (* full auto too slow *) +| -IHV -HT1 /4 width=3 by csx_cpx_trans, cpx_pair_sn/ +] +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 new file mode 100644 index 000000000..d0c9837c7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 68c8d4eac..0ff5a431f 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 lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma -csx.ma csx_cnx.ma csx_cpxs.ma csx_csx.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_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt deleted file mode 100644 index 18ddd3c3d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ /dev/null @@ -1,9 +0,0 @@ -cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma -cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma cpx_lfxs.ma cpx_lfdeq.ma -lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_lfdeq.ma lfpx_aaa.ma lfpx_lfpx.ma -cnx.ma cnx_simple.ma cnx_drops.ma cnx_cnx.ma -cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_lfxs.ma cpm_cpx.ma -cpr.ma cpr_drops.ma -lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fquq.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma -fpb.ma fpb_lfdeq.ma -fpbq.ma fpbq_aaa.ma 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 7df4abf0a..ed35813d2 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 @@ -114,7 +114,7 @@ table { [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ] *) [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ] - [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx" + "csx_cpxs" + "csx_csx" * ] + [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_tsts" + "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" * ] }