From 5224d5d0ff327a2360c9acd282af66ceed8788fc Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 3 Apr 2017 21:31:19 +0000 Subject: [PATCH] - lfsx started ... - advances to complete csx_aaa --- .../csx_aaa.ma => etc/csx_aaa.etc} | 44 +++---- .../{sn_6.ma => predtysnstrong_5.ma} | 4 +- .../lambdadelta/basic_2/relocation/lexs.ma | 11 ++ .../basic_2/rt_computation/cprs_aaa.ma | 29 +++++ .../basic_2/rt_computation/cpxs_aaa.ma | 17 ++- .../basic_2/rt_computation/lfsx.ma | 100 ++++++++++++++++ .../lfsx_fqus.ma} | 16 ++- .../lambdadelta/basic_2/rt_computation/lsx.ma | 109 ------------------ .../basic_2/rt_computation/partial.txt | 3 +- .../lambdadelta/basic_2/rt_transition/lfpx.ma | 4 +- .../lambdadelta/basic_2/static/lfdeq.ma | 4 +- .../lambdadelta/basic_2/static/lfxs.ma | 6 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 13 files changed, 194 insertions(+), 155 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/csx_aaa.ma => etc/csx_aaa.etc} (52%) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{sn_6.ma => predtysnstrong_5.ma} (87%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_aaa.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/snalt_6.ma => rt_computation/lfsx_fqus.ma} (69%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/csx_aaa.etc similarity index 52% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/csx_aaa.etc index 89f226a30..fb7dad498 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/csx_aaa.etc @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -include "basic_2/computation/gcp_aaa.ma". -include "basic_2/computation/cpxs_aaa.ma". -include "basic_2/computation/csx_theq_vector.ma". +include "basic_2/static/gcp_aaa.ma". +include "basic_2/rt_computation/cpxs_aaa.ma". +include "basic_2/rt_computation/csx_gcp.ma". +include "basic_2/rt_computation/csx_gcr.ma". -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) -(* Main properties on atomic arity assignment *******************************) +(* Main properties with atomic arity assignment *****************************) -theorem aaa_csx: ∀h,o,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, o] T. +theorem aaa_csx: ∀h,o,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. #h #o #G #L #T #A #H @(gcr_aaa … (csx_gcp h o) (csx_gcr h o) … H) qed. @@ -29,30 +30,31 @@ qed. fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term. (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 ) → - ∀T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → ⦃G, L⦄ ⊢ T ⁝ A → R T. + ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T. #h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/ qed-. lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term. (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 ) → ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T. /5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-. -fact aaa_ind_csx_alt_aux: ∀h,o,G,L,A. ∀R:predicate term. - (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1 - ) → - ∀T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → ⦃G, L⦄ ⊢ T ⁝ A → R T. -#h #o #G #L #A #R #IH #T #H @(csx_ind_alt … H) -T /4 width=5 by cpxs_aaa_conf/ +fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀R:predicate term. + (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + ) → + ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T. +#h #o #G #L #A #R #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/ qed-. -lemma aaa_ind_csx_alt: ∀h,o,G,L,A. ∀R:predicate term. - (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1 - ) → - ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T. -/5 width=9 by aaa_ind_csx_alt_aux, aaa_csx/ qed-. +(* Basic_2A1: was: aaa_ind_csx_alt *) +lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀R:predicate term. + (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + ) → + ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T. +/5 width=9 by aaa_ind_csx_cpxs_aux, aaa_csx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_5.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_5.ma index 14f27aab0..ea068dd8d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( G ⊢ ⬊ * [ break term 46 h , break term 46 o , break term 46 T , break term 46 f ] break term 46 L )" +notation "hvbox( G ⊢ ⬈ * [ break term 46 h , break term 46 o , break term 46 T ] 𝐒 ⦃ break term 46 L ⦄ )" non associative with precedence 45 - for @{ 'SN $h $o $T $f $G $L }. + for @{ 'PRedTySNStrong $h $o $T $G $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index 4e0c82132..9c009bbf2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -206,6 +206,17 @@ lemma lexs_co: ∀RN1,RP1,RN2,RP2. /3 width=1 by lexs_atom, lexs_next, lexs_push/ qed-. +lemma lexs_co_isid: ∀RN1,RP1,RN2,RP2. + (∀L1,T1,T2. RP1 L1 T1 T2 → RP2 L1 T1 T2) → + ∀f,L1,L2. L1 ⦻*[RN1, RP1, f] L2 → 𝐈⦃f⦄ → + L1 ⦻*[RN2, RP2, f] L2. +#RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 // +#f #I #K1 #K2 #V1 #V2 #_ #HV12 #IH #H +[ elim (isid_inv_next … H) -H // +| /4 width=3 by lexs_push, isid_inv_push/ +] +qed-. + lemma sle_lexs_trans: ∀RN,RP. (∀L,T1,T2. RN L T1 T2 → RP L T1 T2) → ∀f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 → ∀f1. f1 ⊆ f2 → L1 ⦻*[RN, RP, f1] L2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_aaa.ma new file mode 100644 index 000000000..2266edbad --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_aaa.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lpx_aaa.ma". +include "basic_2/computation/cpxs.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) + +(* Properties about atomic arity assignment on terms ************************) + +lemma cpxs_aaa_conf: ∀h,o,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → + ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +#h #o #G #L #T1 #A #HT1 #T2 #HT12 +@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=5 by cpx_aaa_conf/ +qed-. + +lemma cprs_aaa_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +/3 width=5 by cpxs_aaa_conf, cprs_cpxs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma index 2266edbad..3fa11c673 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma @@ -12,18 +12,15 @@ (* *) (**************************************************************************) -include "basic_2/reduction/lpx_aaa.ma". -include "basic_2/computation/cpxs.ma". +include "basic_2/rt_transition/lfpx_aaa.ma". +include "basic_2/rt_computation/cpxs.ma". -(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) -(* Properties about atomic arity assignment on terms ************************) +(* Properties with atomic arity assignment on terms *************************) -lemma cpxs_aaa_conf: ∀h,o,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → - ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. -#h #o #G #L #T1 #A #HT1 #T2 #HT12 +lemma cpxs_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → + ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +#h #G #L #T1 #A #HT1 #T2 #HT12 @(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=5 by cpx_aaa_conf/ qed-. - -lemma cprs_aaa_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. -/3 width=5 by cpxs_aaa_conf, cprs_cpxs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma new file mode 100644 index 000000000..51596c44e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma @@ -0,0 +1,100 @@ +(**************************************************************************) +(* ___ *) +(* ||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/predtysnstrong_5.ma". +include "basic_2/static/lfdeq.ma". +include "basic_2/rt_transition/lfpx.ma". + +(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****) + +definition lfsx: ∀h. sd h → relation3 term genv lenv ≝ + λh,o,T,G. SN … (lfpx h G T) (lfdeq h o T). + +interpretation + "strong normalization for uncounted context-sensitive parallel rt-transition on referred entries (local environment)" + 'PRedTySNStrong h o T G L = (lfsx h o T G L). + +(* Basic eliminators ********************************************************) + +(* Basic_2A1: was: lsx_ind *) +lemma lfsx_ind: ∀h,o,G,T. ∀R:predicate lenv. + (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → R L2) → + R L1 + ) → + ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L. +#h #o #G #T #R #H0 #L1 #H elim H -L1 +/5 width=1 by lfdeq_sym, SN_intro/ +qed-. + +(* Basic properties *********************************************************) + +(* Basic_2A1: was: lsx_intro *) +lemma lfsx_intro: ∀h,o,G,L1,T. + (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) → + G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄. +/5 width=1 by lfdeq_sym, SN_intro/ qed. +(* +lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄. +#h #o #G #L1 #s @lfsx_intro +#L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H * +[ #H1 #H2 destruct // +| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct + @lfdeq_sort +qed. + +lemma lfsx_gref: ∀h,o,G,L,l,p. G ⊢ ⬈*[h, o, §p, l] L. +#h #o #G #L1 #l #p @lfsx_intro +#L2 #HL12 #H elim H -H +/3 width=4 by lfpx_fwd_length, lfdeq_gref/ +qed. + +(* Basic forward lemmas *****************************************************) + +lemma lfsx_fwd_bind_sn: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a,I}V.T, l] L → + G ⊢ ⬈*[h, o, V, l] L. +#h #o #a #I #G #L #V #T #l #H @(lfsx_ind … H) -L +#L1 #_ #IHL1 @lfsx_intro +#L2 #HL12 #HV @IHL1 /3 width=4 by lfdeq_fwd_bind_sn/ +qed-. + +lemma lfsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L → + G ⊢ ⬈*[h, o, V, l] L. +#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L +#L1 #_ #IHL1 @lfsx_intro +#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_sn/ +qed-. + +lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L → + G ⊢ ⬈*[h, o, T, l] L. +#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L +#L1 #_ #IHL1 @lfsx_intro +#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_dx/ +qed-. + +lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ②{I}V.T, l] L → + G ⊢ ⬈*[h, o, V, l] L. +#h #o * /2 width=4 by lfsx_fwd_bind_sn, lfsx_fwd_flat_sn/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L → + G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, l] L. +/3 width=3 by lfsx_fwd_flat_sn, lfsx_fwd_flat_dx, conj/ qed-. + +(* Basic_2A1: removed theorems 5: + lsx_atom lsx_sort lsx_gref lsx_ge_up lsx_ge +*) +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqus.ma similarity index 69% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqus.ma index ce52c4ca3..789453aa9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqus.ma @@ -12,8 +12,16 @@ (* *) (**************************************************************************) -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) +include "basic_2/static/lfdeq_fqus.ma". +include "basic_2/rt_computation/lfsx.ma". -notation "hvbox( G ⊢ ⬊ ⬊ * [ break term 46 h , break term 46 o , break term 46 T , break term 46 f ] break term 46 L )" - non associative with precedence 45 - for @{ 'SNAlt $h $o $T $f $G $L }. +(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****) + +(* Advanced properties ******************************************************) + +(* Basic_2A1: was: lsx_atom *) +lemma lfsx_atom: ∀h,o,G,T. G ⊢ ⬈*[h, o, T] 𝐒⦃⋆⦄. +#h #o #G #T @lfsx_intro +#Y #H #HI lapply (lfpx_inv_atom_sn … H) -H +#H destruct elim HI -HI // +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx.ma deleted file mode 100644 index 7bb8aec4a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx.ma +++ /dev/null @@ -1,109 +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/sn_6.ma". -include "basic_2/multiple/lleq.ma". -include "basic_2/reduction/lpx.ma". - -(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) - -definition lsx: ∀h. sd h → relation4 ynat term genv lenv ≝ - λh,o,l,T,G. SN … (lpx h o G) (lleq l T). - -interpretation - "extended strong normalization (local environment)" - 'SN h o l T G L = (lsx h o T l G L). - -(* Basic eliminators ********************************************************) - -lemma lsx_ind: ∀h,o,G,T,l. ∀R:predicate lenv. - (∀L1. G ⊢ ⬊*[h, o, T, l] L1 → - (∀L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → (L1 ≡[T, l] L2 → ⊥) → R L2) → - R L1 - ) → - ∀L. G ⊢ ⬊*[h, o, T, l] L → R L. -#h #o #G #T #l #R #H0 #L1 #H elim H -L1 -/5 width=1 by lleq_sym, SN_intro/ -qed-. - -(* Basic properties *********************************************************) - -lemma lsx_intro: ∀h,o,G,L1,T,l. - (∀L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → (L1 ≡[T, l] L2 → ⊥) → G ⊢ ⬊*[h, o, T, l] L2) → - G ⊢ ⬊*[h, o, T, l] L1. -/5 width=1 by lleq_sym, SN_intro/ qed. - -lemma lsx_atom: ∀h,o,G,T,l. G ⊢ ⬊*[h, o, T, l] ⋆. -#h #o #G #T #l @lsx_intro -#X #H #HT lapply (lpx_inv_atom1 … H) -H -#H destruct elim HT -HT // -qed. - -lemma lsx_sort: ∀h,o,G,L,l,s. G ⊢ ⬊*[h, o, ⋆s, l] L. -#h #o #G #L1 #l #s @lsx_intro -#L2 #HL12 #H elim H -H -/3 width=4 by lpx_fwd_length, lleq_sort/ -qed. - -lemma lsx_gref: ∀h,o,G,L,l,p. G ⊢ ⬊*[h, o, §p, l] L. -#h #o #G #L1 #l #p @lsx_intro -#L2 #HL12 #H elim H -H -/3 width=4 by lpx_fwd_length, lleq_gref/ -qed. - -lemma lsx_ge_up: ∀h,o,G,L,T,U,lt,l,k. lt ≤ yinj l + yinj k → - ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, U, lt] L → G ⊢ ⬊*[h, o, U, l] L. -#h #o #G #L #T #U #lt #l #k #Hltlm #HTU #H @(lsx_ind … H) -L -/5 width=7 by lsx_intro, lleq_ge_up/ -qed-. - -lemma lsx_ge: ∀h,o,G,L,T,l1,l2. l1 ≤ l2 → - G ⊢ ⬊*[h, o, T, l1] L → G ⊢ ⬊*[h, o, T, l2] L. -#h #o #G #L #T #l1 #l2 #Hl12 #H @(lsx_ind … H) -L -/5 width=7 by lsx_intro, lleq_ge/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lsx_fwd_bind_sn: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ⓑ{a,I}V.T, l] L → - G ⊢ ⬊*[h, o, V, l] L. -#h #o #a #I #G #L #V #T #l #H @(lsx_ind … H) -L -#L1 #_ #IHL1 @lsx_intro -#L2 #HL12 #HV @IHL1 /3 width=4 by lleq_fwd_bind_sn/ -qed-. - -lemma lsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ⓕ{I}V.T, l] L → - G ⊢ ⬊*[h, o, V, l] L. -#h #o #I #G #L #V #T #l #H @(lsx_ind … H) -L -#L1 #_ #IHL1 @lsx_intro -#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_sn/ -qed-. - -lemma lsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ⓕ{I}V.T, l] L → - G ⊢ ⬊*[h, o, T, l] L. -#h #o #I #G #L #V #T #l #H @(lsx_ind … H) -L -#L1 #_ #IHL1 @lsx_intro -#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_dx/ -qed-. - -lemma lsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ②{I}V.T, l] L → - G ⊢ ⬊*[h, o, V, l] L. -#h #o * /2 width=4 by lsx_fwd_bind_sn, lsx_fwd_flat_sn/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -lemma lsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ⓕ{I}V.T, l] L → - G ⊢ ⬊*[h, o, V, l] L ∧ G ⊢ ⬊*[h, o, T, l] L. -/3 width=3 by lsx_fwd_flat_sn, lsx_fwd_flat_dx, conj/ 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 2ed89fa2f..4269b54d2 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,5 @@ -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 +cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma +lfsx.ma lfsx_fqup.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma index ad9f1e03f..0fc26a744 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma @@ -54,10 +54,10 @@ lemma lfpx_pair_repl_dx: ∀h,I,G,L1,L2,T,V,V1. (* Basic inversion lemmas ***************************************************) -lemma lfpx_inv_atom_sn: ∀h,I,G,Y2. ⦃G, ⋆⦄ ⊢ ⬈[h, ⓪{I}] Y2 → Y2 = ⋆. +lemma lfpx_inv_atom_sn: ∀h,G,Y2,T. ⦃G, ⋆⦄ ⊢ ⬈[h, T] Y2 → Y2 = ⋆. /2 width=3 by lfxs_inv_atom_sn/ qed-. -lemma lfpx_inv_atom_dx: ∀h,I,G,Y1. ⦃G, Y1⦄ ⊢ ⬈[h, ⓪{I}] ⋆ → Y1 = ⋆. +lemma lfpx_inv_atom_dx: ∀h,G,Y1,T. ⦃G, Y1⦄ ⊢ ⬈[h, T] ⋆ → Y1 = ⋆. /2 width=3 by lfxs_inv_atom_dx/ qed-. lemma lfpx_inv_sort: ∀h,G,Y1,Y2,s. ⦃G, Y1⦄ ⊢ ⬈[h, ⋆s] Y2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index e49ccbfbe..aa6484ace 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -105,10 +105,10 @@ lemma lfdeq_pair_repl_dx: ∀h,o,I,L1,L2.∀T:term.∀V,V1. (* Basic inversion lemmas ***************************************************) -lemma lfdeq_inv_atom_sn: ∀h,o,I,Y2. ⋆ ≡[h, o, ⓪{I}] Y2 → Y2 = ⋆. +lemma lfdeq_inv_atom_sn: ∀h,o,Y2. ∀T:term. ⋆ ≡[h, o, T] Y2 → Y2 = ⋆. /2 width=3 by lfxs_inv_atom_sn/ qed-. -lemma lfdeq_inv_atom_dx: ∀h,o,I,Y1. Y1 ≡[h, o, ⓪{I}] ⋆ → Y1 = ⋆. +lemma lfdeq_inv_atom_dx: ∀h,o,Y1. ∀T:term. Y1 ≡[h, o, T] ⋆ → Y1 = ⋆. /2 width=3 by lfxs_inv_atom_dx/ qed-. lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≡[h, o, #0] Y2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index 9f0a1a486..f754e46de 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -91,11 +91,11 @@ qed-. (* Basic inversion lemmas ***************************************************) -lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆. -#R #I #Y2 * /2 width=4 by lexs_inv_atom1/ +lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⦻*[R, T] Y2 → Y2 = ⋆. +#R #Y2 #T * /2 width=4 by lexs_inv_atom1/ qed-. -lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → Y1 = ⋆. +lemma lfxs_inv_atom_dx: ∀R,Y1,T. Y1 ⦻*[R, T] ⋆ → Y1 = ⋆. #R #I #Y1 * /2 width=4 by lexs_inv_atom2/ 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 c1b25de72..5019e8956 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 @@ -116,7 +116,7 @@ table { [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } ] } -- 2.39.2