From: Ferruccio Guidi Date: Sun, 5 Mar 2017 17:08:20 +0000 (+0000) Subject: advances on cpxs and cnx (cnxa removed) ,,, X-Git-Tag: make_still_working~493 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e2b4ff64df523b4be9d7dc4e92386945846426e7;p=helm.git advances on cpxs and cnx (cnxa removed) ,,, --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_5.ma index 74444d815..680679e5f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬈ [ break term 46 h , break term 46 o ] 𝐒 ⦃ break term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬈ * [ break term 46 h , break term 46 o ] 𝐒 ⦃ break term 46 T ⦄ )" non associative with precedence 45 for @{ 'PRedTyStrong $h $o $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_5.ma deleted file mode 100644 index 207c25ded..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_5.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬊ ⬊ * [ break term 46 h , break term 46 o ] break term 46 T )" - non associative with precedence 45 - for @{ 'SNAlt $h $o $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma index f09fab54c..e13e044c3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma @@ -144,3 +144,5 @@ elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3 by cpxs_strap1, or3_intro1, or3_int lapply (cpxs_strap1 … HW1 … HW2) -W lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5 by or3_intro0, ex3_2_intro/ qed-. + +(* Basic_2A1: removed theorems 1: cpxs_neq_inv_step_sn *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.ma index 4f1d7ceee..74efaded1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.ma @@ -12,177 +12,81 @@ (* *) (**************************************************************************) -include "basic_2/reduction/lpx_drop.ma". -include "basic_2/computation/cpxs_lift.ma". +include "basic_2/rt_transition/cpx_lsubr.ma". +include "basic_2/rt_computation/cpxs.ma". -(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) (* Main properties **********************************************************) -theorem cpxs_trans: ∀h,o,G,L. Transitive … (cpxs h o G L). +theorem cpxs_trans: ∀h,G,L. Transitive … (cpxs h G L). normalize /2 width=3 by trans_TC/ qed-. -theorem cpxs_bind: ∀h,o,a,I,G,L,V1,V2,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈*[h, o] T2 → - ⦃G, L⦄ ⊢ V1 ⬈*[h, o] V2 → - ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2. -#h #o #a #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 +theorem cpxs_bind: ∀h,p,I,G,L,V1,V2,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈*[h] T2 → + ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 → + ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2. +#h #p #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /3 width=5 by cpxs_trans, cpxs_bind_dx/ qed. -theorem cpxs_flat: ∀h,o,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → - ⦃G, L⦄ ⊢ V1 ⬈*[h, o] V2 → - ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈*[h, o] ⓕ{I}V2.T2. -#h #o #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 +theorem cpxs_flat: ∀h,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → + ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 → + ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈*[h] ⓕ{I}V2.T2. +#h #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /3 width=5 by cpxs_trans, cpxs_flat_dx/ qed. -theorem cpxs_beta_rc: ∀h,o,a,G,L,V1,V2,W1,W2,T1,T2. - ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ W1 ⬈*[h, o] W2 → - ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ⬈*[h, o] ⓓ{a}ⓝW2.V2.T2. -#h #o #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cpxs_ind … H) -W2 +theorem cpxs_beta_rc: ∀h,p,G,L,V1,V2,W1,W2,T1,T2. + ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ W1 ⬈*[h] W2 → + ⦃G, L⦄ ⊢ ⓐV1.ⓛ{p}W1.T1 ⬈*[h] ⓓ{p}ⓝW2.V2.T2. +#h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cpxs_ind … H) -W2 /4 width=5 by cpxs_trans, cpxs_beta_dx, cpxs_bind_dx, cpx_pair_sn/ qed. -theorem cpxs_beta: ∀h,o,a,G,L,V1,V2,W1,W2,T1,T2. - ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ W1 ⬈*[h, o] W2 → ⦃G, L⦄ ⊢ V1 ⬈*[h, o] V2 → - ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ⬈*[h, o] ⓓ{a}ⓝW2.V2.T2. -#h #o #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cpxs_ind … H) -V2 +theorem cpxs_beta: ∀h,p,G,L,V1,V2,W1,W2,T1,T2. + ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ W1 ⬈*[h] W2 → ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 → + ⦃G, L⦄ ⊢ ⓐV1.ⓛ{p}W1.T1 ⬈*[h] ⓓ{p}ⓝW2.V2.T2. +#h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cpxs_ind … H) -V2 /4 width=5 by cpxs_trans, cpxs_beta_rc, cpxs_bind_dx, cpx_flat/ qed. -theorem cpxs_theta_rc: ∀h,o,a,G,L,V1,V,V2,W1,W2,T1,T2. - ⦃G, L⦄ ⊢ V1 ⬈[h, o] V → ⬆[0, 1] V ≡ V2 → - ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ W1 ⬈*[h, o] W2 → - ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ⬈*[h, o] ⓓ{a}W2.ⓐV2.T2. -#h #o #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H @(cpxs_ind … H) -W2 +theorem cpxs_theta_rc: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2. + ⦃G, L⦄ ⊢ V1 ⬈[h] V → ⬆*[1] V ≡ V2 → + ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ W1 ⬈*[h] W2 → + ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ⬈*[h] ⓓ{p}W2.ⓐV2.T2. +#h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H @(cpxs_ind … H) -W2 /3 width=5 by cpxs_trans, cpxs_theta_dx, cpxs_bind_dx/ qed. -theorem cpxs_theta: ∀h,o,a,G,L,V1,V,V2,W1,W2,T1,T2. - ⬆[0, 1] V ≡ V2 → ⦃G, L⦄ ⊢ W1 ⬈*[h, o] W2 → - ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ V1 ⬈*[h, o] V → - ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ⬈*[h, o] ⓓ{a}W2.ⓐV2.T2. -#h #o #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 +theorem cpxs_theta: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2. + ⬆*[1] V ≡ V2 → ⦃G, L⦄ ⊢ W1 ⬈*[h] W2 → + ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ V1 ⬈*[h] V → + ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ⬈*[h] ⓓ{p}W2.ⓐV2.T2. +#h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 /3 width=5 by cpxs_trans, cpxs_theta_rc, cpxs_flat_dx/ qed. (* Advanced inversion lemmas ************************************************) -lemma cpxs_inv_appl1: ∀h,o,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ⬈*[h, o] U2 → - ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h, o] V2 & ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 & - U2 = ⓐV2. T2 - | ∃∃a,W,T. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] ⓛ{a}W.T & ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V1.T ⬈*[h, o] U2 - | ∃∃a,V0,V2,V,T. ⦃G, L⦄ ⊢ V1 ⬈*[h, o] V0 & ⬆[0,1] V0 ≡ V2 & - ⦃G, L⦄ ⊢ T1 ⬈*[h, o] ⓓ{a}V.T & ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ⬈*[h, o] U2. -#h #o #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5 by or3_intro0, ex3_2_intro/ ] +lemma cpxs_inv_appl1: ∀h,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ⬈*[h] U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 & + U2 = ⓐV2.T2 + | ∃∃p,W,T. ⦃G, L⦄ ⊢ T1 ⬈*[h] ⓛ{p}W.T & ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V1.T ⬈*[h] U2 + | ∃∃p,V0,V2,V,T. ⦃G, L⦄ ⊢ V1 ⬈*[h] V0 & ⬆*[1] V0 ≡ V2 & + ⦃G, L⦄ ⊢ T1 ⬈*[h] ⓓ{p}V.T & ⦃G, L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] U2. +#h #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5 by or3_intro0, ex3_2_intro/ ] #U #U2 #_ #HU2 * * [ #V0 #T0 #HV10 #HT10 #H destruct elim (cpx_inv_appl1 … HU2) -HU2 * [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5 by cpxs_strap1, or3_intro0, ex3_2_intro/ - | #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct + | #p #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct lapply (cpxs_strap1 … HV10 … HV02) -V0 #HV12 lapply (lsubr_cpx_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 /5 width=5 by cpxs_bind, cpxs_flat_dx, cpx_cpxs, lsubr_beta, ex2_3_intro, or3_intro1/ - | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct + | #p #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct /5 width=10 by cpxs_flat_sn, cpxs_bind_dx, cpxs_strap1, ex4_5_intro, or3_intro2/ ] | /4 width=9 by cpxs_strap1, or3_intro1, ex2_3_intro/ | /4 width=11 by cpxs_strap1, or3_intro2, ex4_5_intro/ ] qed-. - -(* Properties on sn extended parallel reduction for local environments ******) - -lemma lpx_cpx_trans: ∀h,o,G. b_c_transitive … (cpx h o G) (λ_.lpx h o G). -#h #o #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2 -[ /2 width=3 by/ -| /3 width=2 by cpx_cpxs, cpx_st/ -| #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12 - elim (lpx_drop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H - elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct - /4 width=7 by cpxs_delta, cpxs_strap2/ -|4,9: /4 width=1 by cpxs_beta, cpxs_bind, lpx_pair/ -|5,7,8: /3 width=1 by cpxs_flat, cpxs_ct, cpxs_eps/ -| /4 width=3 by cpxs_zeta, lpx_pair/ -| /4 width=3 by cpxs_theta, cpxs_strap1, lpx_pair/ -] -qed-. - -lemma cpx_bind2: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → - ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈[h, o] T2 → - ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2. -/4 width=5 by lpx_cpx_trans, cpxs_bind_dx, lpx_pair/ qed. - -(* Advanced properties ******************************************************) - -lemma lpx_cpxs_trans: ∀h,o,G. b_rs_transitive … (cpx h o G) (λ_.lpx h o G). -#h #o #G @b_c_trans_LTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *) -qed-. - -lemma cpxs_bind2_dx: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → - ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h, o] T2 → - ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2. -/4 width=5 by lpx_cpxs_trans, cpxs_bind_dx, lpx_pair/ qed. - -(* Properties on supclosure *************************************************) - -lemma fqu_cpxs_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → (T2 = U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1) - #U2 #HVU2 @(ex3_intro … U2) - [1,3: /3 width=7 by fqu_drop, cpxs_delta, drop_pair, drop_drop/ - | #H destruct - lapply (lift_inv_lref2_be … HVU2 ? ?) -HVU2 // - ] -| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T)) - [1,3: /2 width=4 by fqu_pair_sn, cpxs_pair_sn/ - | #H0 destruct /2 width=1 by/ - ] -| #a #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓑ{a,I}V.T2)) - [1,3: /2 width=4 by fqu_bind_dx, cpxs_bind/ - | #H0 destruct /2 width=1 by/ - ] -| #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓕ{I}V.T2)) - [1,3: /2 width=4 by fqu_flat_dx, cpxs_flat/ - | #H0 destruct /2 width=1 by/ - ] -| #G #L #K #T1 #U1 #k #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (k+1)) - #U2 #HTU2 @(ex3_intro … U2) - [1,3: /2 width=10 by cpxs_lift, fqu_drop/ - | #H0 destruct /3 width=5 by lift_inj/ -] -qed-. - -lemma fquq_cpxs_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → (T2 = U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12 -[ #H12 elim (fqu_cpxs_trans_neq … H12 … HTU2 H) -T2 - /3 width=4 by fqu_fquq, ex3_intro/ -| * #HG #HL #HT destruct /3 width=4 by ex3_intro/ -] -qed-. - -lemma fqup_cpxs_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → (T2 = U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 -[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_neq … H12 … HTU2 H) -T2 - /3 width=4 by fqu_fqup, ex3_intro/ -| #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2 - #U1 #HTU1 #H #H12 elim (fqu_cpxs_trans_neq … H1 … HTU1 H) -T1 - /3 width=8 by fqup_strap2, ex3_intro/ -] -qed-. - -lemma fqus_cpxs_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → (T2 = U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12 -[ #H12 elim (fqup_cpxs_trans_neq … H12 … HTU2 H) -T2 - /3 width=4 by fqup_fqus, ex3_intro/ -| * #HG #HL #HT destruct /3 width=4 by ex3_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_etc.ma new file mode 100644 index 000000000..a28b01e54 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_etc.ma @@ -0,0 +1,100 @@ + +include "basic_2/reduction/lpx_drop.ma". +include "basic_2/computation/cpxs_lift.ma". +include "basic_2/rt_computation/cpxs_cpxs.ma". + +(* Properties on sn extended parallel reduction for local environments ******) + +lemma lpx_cpx_trans: ∀h,G. b_c_transitive … (cpx h G) (λ_.lpx h G). +#h #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2 +[ /2 width=3 by/ +| /3 width=2 by cpx_cpxs, cpx_st/ +| #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12 + elim (lpx_drop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H + elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct + /4 width=7 by cpxs_delta, cpxs_strap2/ +|4,9: /4 width=1 by cpxs_beta, cpxs_bind, lpx_pair/ +|5,7,8: /3 width=1 by cpxs_flat, cpxs_ct, cpxs_eps/ +| /4 width=3 by cpxs_zeta, lpx_pair/ +| /4 width=3 by cpxs_theta, cpxs_strap1, lpx_pair/ +] +qed-. + +lemma cpx_bind2: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈[h, o] T2 → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2. +/4 width=5 by lpx_cpx_trans, cpxs_bind_dx, lpx_pair/ qed. + +(* Advanced properties ******************************************************) + +lemma lpx_cpxs_trans: ∀h,o,G. b_rs_transitive … (cpx h o G) (λ_.lpx h o G). +#h #o #G @b_c_trans_LTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *) +qed-. + +lemma cpxs_bind2_dx: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h, o] T2 → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2. +/4 width=5 by lpx_cpxs_trans, cpxs_bind_dx, lpx_pair/ qed. + +(* Properties on supclosure *************************************************) + +lemma fqu_cpxs_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1) + #U2 #HVU2 @(ex3_intro … U2) + [1,3: /3 width=7 by fqu_drop, cpxs_delta, drop_pair, drop_drop/ + | #H destruct + lapply (lift_inv_lref2_be … HVU2 ? ?) -HVU2 // + ] +| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T)) + [1,3: /2 width=4 by fqu_pair_sn, cpxs_pair_sn/ + | #H0 destruct /2 width=1 by/ + ] +| #a #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓑ{a,I}V.T2)) + [1,3: /2 width=4 by fqu_bind_dx, cpxs_bind/ + | #H0 destruct /2 width=1 by/ + ] +| #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓕ{I}V.T2)) + [1,3: /2 width=4 by fqu_flat_dx, cpxs_flat/ + | #H0 destruct /2 width=1 by/ + ] +| #G #L #K #T1 #U1 #k #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (k+1)) + #U2 #HTU2 @(ex3_intro … U2) + [1,3: /2 width=10 by cpxs_lift, fqu_drop/ + | #H0 destruct /3 width=5 by lift_inj/ +] +qed-. + +lemma fquq_cpxs_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12 +[ #H12 elim (fqu_cpxs_trans_neq … H12 … HTU2 H) -T2 + /3 width=4 by fqu_fquq, ex3_intro/ +| * #HG #HL #HT destruct /3 width=4 by ex3_intro/ +] +qed-. + +lemma fqup_cpxs_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 +[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_neq … H12 … HTU2 H) -T2 + /3 width=4 by fqu_fqup, ex3_intro/ +| #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2 + #U1 #HTU1 #H #H12 elim (fqu_cpxs_trans_neq … H1 … HTU1 H) -T1 + /3 width=8 by fqup_strap2, ex3_intro/ +] +qed-. + +lemma fqus_cpxs_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12 +[ #H12 elim (fqup_cpxs_trans_neq … H12 … HTU2 H) -T2 + /3 width=4 by fqup_fqus, ex3_intro/ +| * #HG #HL #HT destruct /3 width=4 by ex3_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma index c3e2e2065..4960595ff 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma @@ -13,12 +13,14 @@ (**************************************************************************) include "basic_2/syntax/tdeq_tdeq.ma". -include "basic_2/rt_computation/cpxs.ma". -include "basic_2/rt_transition/cpx_lfdeq.ma". include "basic_2/rt_transition/lfpx_fqup.ma". +include "basic_2/rt_transition/lfpx_lfdeq.ma". +include "basic_2/rt_computation/cpxs.ma". (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) +(* Properties with degree-based equivalence for terms ***********************) + lemma tdeq_cpxs_trans: ∀h,o,U1,T1. U1 ≡[h, o] T1 → ∀G,L,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ∃∃U2. ⦃G, L⦄ ⊢ U1 ⬈*[h] U2 & U2 ≡[h, o] T2. #h #o #U1 #T1 #HUT1 #G #L #T2 #HT12 @(cpxs_ind … HT12) -T2 /2 width=3 by ex2_intro/ @@ -40,5 +42,3 @@ lemma cpxs_tdneq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ] ] qed-. - -(* Basic_2A1: removed theorems 1: cpxs_neq_inv_step_sn *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma index 3ba500020..5fe697558 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma @@ -28,11 +28,11 @@ interpretation (* Basic eliminators ********************************************************) lemma csx_ind: ∀h,o,G,L. ∀R:predicate term. - (∀T1. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T1⦄ → + (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 ) → - ∀T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄ → R T. + ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T. #h #o #G #L #R #H0 #T1 #H elim H -T1 /5 width=1 by SN_intro/ qed-. @@ -41,11 +41,11 @@ qed-. (* Basic_1: was just: sn3_pr2_intro *) lemma csx_intro: ∀h,o,G,L,T1. - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T2⦄) → - ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T1⦄. + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄) → + ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄. /4 width=1 by SN_intro/ qed. -lemma csx_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃⋆s⦄. +lemma csx_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃⋆s⦄. #h #o #G #L #s elim (deg_total h o s) #d generalize in match s; -s elim d -d [ #s1 #Hs1 @csx_intro #X #H #HX elim HX -HX @@ -60,8 +60,8 @@ qed. (* Basic forward lemmas *****************************************************) -fact csx_fwd_pair_sn_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃U⦄ → - ∀I,V,T. U = ②{I}V.T → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃V⦄. +fact csx_fwd_pair_sn_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ → + ∀I,V,T. U = ②{I}V.T → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄. #h #o #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csx_intro #V2 #HLV2 #HV2 @(IH (②{I}V2.T)) -IH /2 width=3 by cpx_pair_sn/ -HLV2 @@ -69,11 +69,11 @@ fact csx_fwd_pair_sn_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃U⦄ → qed-. (* Basic_1: was just: sn3_gen_head *) -lemma csx_fwd_pair_sn: ∀h,o,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃②{I}V.T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃V⦄. +lemma csx_fwd_pair_sn: ∀h,o,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃②{I}V.T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄. /2 width=5 by csx_fwd_pair_sn_aux/ qed-. -fact csx_fwd_bind_dx_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃U⦄ → - ∀p,I,V,T. U = ⓑ{p,I}V.T → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. +fact csx_fwd_bind_dx_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ → + ∀p,I,V,T. U = ⓑ{p,I}V.T → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. #h #o #G #L #U #H elim H -H #U0 #_ #IH #p #I #V #T #H destruct @csx_intro #T2 #HLT2 #HT2 @(IH (ⓑ{p,I}V.T2)) -IH /2 width=3 by cpx_bind/ -HLT2 @@ -81,11 +81,11 @@ fact csx_fwd_bind_dx_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃U⦄ → qed-. (* Basic_1: was just: sn3_gen_bind *) -lemma csx_fwd_bind_dx: ∀h,o,p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃ⓑ{p,I}V.T⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. +lemma csx_fwd_bind_dx: ∀h,o,p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓑ{p,I}V.T⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. /2 width=4 by csx_fwd_bind_dx_aux/ qed-. -fact csx_fwd_flat_dx_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃U⦄ → - ∀I,V,T. U = ⓕ{I}V.T → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. +fact csx_fwd_flat_dx_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ → + ∀I,V,T. U = ⓕ{I}V.T → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. #h #o #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csx_intro #T2 #HLT2 #HT2 @(IH (ⓕ{I}V.T2)) -IH /2 width=3 by cpx_flat/ -HLT2 @@ -93,15 +93,15 @@ fact csx_fwd_flat_dx_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃U⦄ → qed-. (* Basic_1: was just: sn3_gen_flat *) -lemma csx_fwd_flat_dx: ∀h,o,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃ⓕ{I}V.T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. +lemma csx_fwd_flat_dx: ∀h,o,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓕ{I}V.T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. /2 width=5 by csx_fwd_flat_dx_aux/ qed-. -lemma csx_fwd_bind: ∀h,o,p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃ⓑ{p,I}V.T⦄ → - ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. +lemma csx_fwd_bind: ∀h,o,p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓑ{p,I}V.T⦄ → + ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. /3 width=3 by csx_fwd_pair_sn, csx_fwd_bind_dx, conj/ qed-. -lemma csx_fwd_flat: ∀h,o,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃ⓕ{I}V.T⦄ → - ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃V⦄ ∧ ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. +lemma csx_fwd_flat: ∀h,o,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓕ{I}V.T⦄ → + ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ ∧ ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. /3 width=3 by csx_fwd_pair_sn, csx_fwd_flat_dx, conj/ qed-. (* Basic_1: removed theorems 14: @@ -110,3 +110,7 @@ lemma csx_fwd_flat: ∀h,o,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃ⓕ{I}V.T sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind *) +(* Basic_2A1: removed theorems 6: + csxa_ind csxa_intro csxa_cpxs_trans csxa_intro_cpx + csx_csxa csxa_csx +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_alt.ma deleted file mode 100644 index 0b9b29799..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_alt.ma +++ /dev/null @@ -1,107 +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/snalt_5.ma". -include "basic_2/computation/cpxs.ma". -include "basic_2/computation/csx.ma". - -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) - -(* alternative definition of csx *) -definition csxa: ∀h. sd h → relation3 genv lenv term ≝ - λh,o,G,L. SN … (cpxs h o G L) (eq …). - -interpretation - "context-sensitive extended strong normalization (term) alternative" - 'SNAlt h o G L T = (csxa h o G L T). - -(* Basic eliminators ********************************************************) - -lemma csxa_ind: ∀h,o,G,L. ∀R:predicate term. - (∀T1. ⦃G, L⦄ ⊢ ⬊⬊*[h, o] T1 → - (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1 - ) → - ∀T. ⦃G, L⦄ ⊢ ⬊⬊*[h, o] T → R T. -#h #o #G #L #R #H0 #T1 #H elim H -T1 /5 width=1 by SN_intro/ -qed-. - -(* Basic properties *********************************************************) - -lemma csx_intro_cpxs: ∀h,o,G,L,T1. - (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, o] T2) → - ⦃G, L⦄ ⊢ ⬊*[h, o] T1. -/4 width=1 by cpx_cpxs, csx_intro/ qed. - -(* Basic_1: was just: sn3_intro *) -lemma csxa_intro: ∀h,o,G,L,T1. - (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, o] T2) → - ⦃G, L⦄ ⊢ ⬊⬊*[h, o] T1. -/4 width=1 by SN_intro/ qed. - -fact csxa_intro_aux: ∀h,o,G,L,T1. ( - ∀T,T2. ⦃G, L⦄ ⊢ T ➡*[h, o] T2 → T1 = T → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, o] T2 - ) → ⦃G, L⦄ ⊢ ⬊⬊*[h, o] T1. -/4 width=3 by csxa_intro/ qed-. - -(* Basic_1: was just: sn3_pr3_trans (old version) *) -lemma csxa_cpxs_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬊⬊*[h, o] T1 → - ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → ⦃G, L⦄ ⊢ ⬊⬊*[h, o] T2. -#h #o #G #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 -@csxa_intro #T #HLT2 #HT2 -elim (eq_term_dec T1 T2) #HT12 -[ -IHT1 -HLT12 destruct /3 width=1 by/ -| -HT1 -HT2 /3 width=4 by/ -qed. - -(* Basic_1: was just: sn3_pr2_intro (old version) *) -lemma csxa_intro_cpx: ∀h,o,G,L,T1. ( - ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, o] T2 - ) → ⦃G, L⦄ ⊢ ⬊⬊*[h, o] T1. -#h #o #G #L #T1 #H -@csxa_intro_aux #T #T2 #H @(cpxs_ind_dx … H) -T -[ -H #H destruct #H - elim H // -| #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct - elim (eq_term_dec T0 T) #HT0 - [ -HLT1 -HLT2 -H /3 width=1 by/ - | -IHT -HT12 /4 width=3 by csxa_cpxs_trans/ - ] -] -qed. - -(* Main properties **********************************************************) - -theorem csx_csxa: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → ⦃G, L⦄ ⊢ ⬊⬊*[h, o] T. -#h #o #G #L #T #H @(csx_ind … H) -T /4 width=1 by csxa_intro_cpx/ -qed. - -theorem csxa_csx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬊⬊*[h, o] T → ⦃G, L⦄ ⊢ ⬊*[h, o] T. -#h #o #G #L #T #H @(csxa_ind … H) -T /4 width=1 by cpx_cpxs, csx_intro/ -qed. - -(* Basic_1: was just: sn3_pr3_trans *) -lemma csx_cpxs_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, o] T1 → - ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → ⦃G, L⦄ ⊢ ⬊*[h, o] T2. -#h #o #G #L #T1 #HT1 #T2 #H @(cpxs_ind … H) -T2 /2 width=3 by csx_cpx_trans/ -qed-. - -(* Main eliminators *********************************************************) - -lemma csx_ind_alt: ∀h,o,G,L. ∀R:predicate term. - (∀T1. ⦃G, L⦄ ⊢ ⬊*[h, o] T1 → - (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1 - ) → - ∀T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → R T. -#h #o #G #L #R #H0 #T1 #H @(csxa_ind … (csx_csxa … H)) -T1 /4 width=1 by csxa_csx/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma index 17d8633dc..8f9268fab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma @@ -20,5 +20,5 @@ include "basic_2/rt_computation/csx.ma". (* Properties with normal terms for uncounted parallel rt-transition ********) (* Basic_1: was just: sn3_nf2 *) -lemma cnx_csx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. +lemma cnx_csx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. /2 width=1 by NF_to_SN/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma new file mode 100644 index 000000000..1b4c9cb52 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||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_computation/cpxs_tdeq.ma". +include "basic_2/rt_computation/cpxs_cpxs.ma". +include "basic_2/rt_computation/csx_csx.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) + +(* Properties with uncounted context-sensitive rt-computation for terms *****) + +(* Basic_1: was just: sn3_intro *) +lemma csx_intro_cpxs: ∀h,o,G,L,T1. + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄) → + ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄. +/4 width=1 by cpx_cpxs, csx_intro/ qed-. + +(* Basic_1: was just: sn3_pr3_trans *) +lemma csx_cpxs_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → + ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄. +#h #o #G #L #T1 #HT1 #T2 #H @(cpxs_ind … H) -T2 +/2 width=3 by csx_cpx_trans/ +qed-. + +(* Eliminators with uncounted context-sensitive rt-computation for terms ****) + +lemma csx_ind_cpxs_tdeq: ∀h,o,G,L. ∀R:predicate term. + (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + ) → + ∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → + ∀T0. ⦃G, L⦄ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≡[h, o] T2 → R T2. +#h #o #G #L #R #IH #T1 #H @(csx_ind … H) -T1 +#T1 #HT1 #IH1 #T0 #HT10 #T2 #HT02 +@IH -IH /3 width=3 by csx_cpxs_trans, csx_tdeq_trans/ -HT1 #V2 #HTV2 #HnTV2 +lapply (tdeq_tdneq_trans … HT02 … HnTV2) -HnTV2 #H +elim (tdeq_cpxs_trans … HT02 … HTV2) -T2 #V0 #HTV0 #HV02 +lapply (tndeq_tdeq_canc_dx … H … HV02) -H #HnTV0 +elim (tdeq_dec h o T1 T0) #H +[ lapply (tdeq_tdneq_trans … H … HnTV0) -H -HnTV0 #Hn10 + lapply (cpxs_trans … HT10 … HTV0) -T0 #H10 + elim (cpxs_tdneq_inv_step_sn … H10 … Hn10) -H10 -Hn10 + /3 width=8 by tdeq_trans/ +| elim (cpxs_tdneq_inv_step_sn … HT10 … H) -HT10 -H #T #V #HT1 #HnT1 #HTV #HVT0 + elim (tdeq_cpxs_trans … HVT0 … HTV0) -T0 + /3 width=8 by cpxs_trans, tdeq_trans/ +] +qed-. + +lemma csx_ind_alt: ∀h,o,G,L. ∀R:predicate term. + (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + ) → + ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T. +#h #o #G #L #R #IH #T #HT +@(csx_ind_cpxs_tdeq … IH … HT) -IH -HT // (**) (* full auto fails *) +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 e1df7c029..628611eac 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 @@ -20,28 +20,28 @@ include "basic_2/rt_computation/csx.ma". (* Advanced properties ******************************************************) -lemma csx_tdeq_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T1⦄ → - ∀T2. T1 ≡[h, o] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T2⦄. +lemma csx_tdeq_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → + ∀T2. T1 ≡[h, o] T2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄. #h #o #G #L #T1 #H @(csx_ind … H) -T1 #T #_ #IH #T2 #HT2 @csx_intro #T1 #HT21 #HnT21 elim (tdeq_cpx_trans … HT2 … HT21) -HT21 /4 width=5 by tdeq_repl/ qed-. -lemma csx_cpx_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T1⦄ → - ∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T2⦄. +lemma csx_cpx_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → + ∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄. #h #o #G #L #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHT1 #T2 #HLT12 elim (tdeq_dec h o T1 T2) /3 width=4 by csx_tdeq_trans/ qed-. (* Basic_1: was just: sn3_cast *) -lemma csx_cast: ∀h,o,G,L,W. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃W⦄ → - ∀T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃ⓝW.T⦄. +lemma csx_cast: ∀h,o,G,L,W. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃W⦄ → + ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓝW.T⦄. #h #o #G #L #W #HW @(csx_ind … HW) -W #W #HW #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT @csx_intro #X #H1 #H2 elim (cpx_inv_cast1 … H1) -H1 [ * #W0 #T0 #HLW0 #HLT0 #H destruct - elim (tdeq_false_inv_pair … H2) -H2 + elim (tdneq_inv_pair … H2) -H2 [ -W -T #H elim H -H // | -HW -IHT /3 width=3 by csx_cpx_trans/ | -HW -HT -IHW /4 width=3 by csx_cpx_trans, cpx_pair_sn/ 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 deef34eac..556cb5704 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,2 +1,2 @@ -cpxs.ma -csx.ma csx_cnx.ma csx_csx.ma +cpxs.ma cpxs_tdeq.ma cpxs_cpxs.ma +csx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma index 4b077059d..6e08f7446 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma @@ -171,11 +171,11 @@ qed-. (* Negated inversion lemmas *************************************************) -lemma tdeq_false_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. - (②{I1}V1.T1 ≡[h, o] ②{I2}V2.T2 → ⊥) → - ∨∨ I1 = I2 → ⊥ - | V1 ≡[h, o] V2 → ⊥ - | (T1 ≡[h, o] T2 → ⊥). +lemma tdneq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. + (②{I1}V1.T1 ≡[h, o] ②{I2}V2.T2 → ⊥) → + ∨∨ I1 = I2 → ⊥ + | V1 ≡[h, o] V2 → ⊥ + | (T1 ≡[h, o] T2 → ⊥). #h #o #I1 #I2 #V1 #V2 #T1 #T2 #H12 elim (eq_item2_dec I1 I2) /3 width=1 by or3_intro0/ #H destruct elim (tdeq_dec h o V1 V2) /3 width=1 by or3_intro1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma index 9f47fd88f..af82e7cd7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma @@ -38,3 +38,13 @@ theorem tdeq_canc_dx: ∀h,o. right_cancellable … (tdeq h o). theorem tdeq_repl: ∀h,o,T1,T2. T1 ≡[h, o] T2 → ∀U1. T1 ≡[h, o] U1 → ∀U2. T2 ≡[h, o] U2 → U1 ≡[h, o] U2. /3 width=3 by tdeq_canc_sn, tdeq_trans/ qed-. + +(* Negated main properies ***************************************************) + +theorem tdeq_tdneq_trans: ∀h,o,T1,T. T1 ≡[h, o] T → ∀T2. (T ≡[h, o] T2 → ⊥) → + T1 ≡[h, o] T2 → ⊥. +/3 width=3 by tdeq_canc_sn/ qed-. + +theorem tndeq_tdeq_canc_dx: ∀h,o,T1,T. (T1 ≡[h, o] T → ⊥) → ∀T2. T2 ≡[h, o] T → + T1 ≡[h, o] T2 → ⊥. +/3 width=3 by tdeq_trans/ 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 267559ff5..03c104136 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 @@ -121,8 +121,8 @@ table { [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_lreq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] *) - [ "csx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐒⦃?⦄ )" "csx_cnx" + "csx_csx" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ] + [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx" + "csx_cpxs" + "csx_csx" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_cpxs" * ] } ] }