From: Ferruccio Guidi Date: Sat, 13 Jul 2013 15:08:58 +0000 (+0000) Subject: partial commit of the components before "conversion" X-Git-Tag: make_still_working~1130 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ef49e0e7f5f298c299afdd3cbfdc2404ecb93879;p=helm.git partial commit of the components before "conversion" - some work on extended reduction and computation - some renaming --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma index 0e63d954c..4ad5ffb5e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma @@ -17,35 +17,31 @@ include "basic_2/substitution/ldrops.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) definition CP1 ≝ λRR:lenv→relation term. λRS:relation term. - ∀L,k. NF … (RR L) RS (⋆k). + ∀L. ∃k. NF … (RR L) RS (⋆k). definition CP2 ≝ λRR:lenv→relation term. λRS:relation term. - ∀L,K,W,i. ⇩[0,i] L ≡ K. ⓛW → NF … (RR L) RS (#i). - -definition CP3 ≝ λRR:lenv→relation term. λRP:lenv→predicate term. - ∀L,V,k. RP L (ⓐ⋆k.V) → RP L V. - -definition CP4 ≝ λRR:lenv→relation term. λRS:relation term. ∀L0,L,T,T0,d,e. NF … (RR L) RS T → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR L0) RS T0. -definition CP4s ≝ λRR:lenv→relation term. λRS:relation term. +definition CP2s ≝ λRR:lenv→relation term. λRS:relation term. ∀L0,L,des. ⇩*[des] L0 ≡ L → ∀T,T0. ⇧*[des] T ≡ T0 → NF … (RR L) RS T → NF … (RR L0) RS T0. +definition CP3 ≝ λRP:lenv→predicate term. + ∀L,V,k. RP L (ⓐ⋆k.V) → RP L V. + (* requirements for abstract computation properties *) record acp (RR:lenv->relation term) (RS:relation term) (RP:lenv→predicate term) : Prop ≝ { cp1: CP1 RR RS; cp2: CP2 RR RS; - cp3: CP3 RR RP; - cp4: CP4 RR RS + cp3: CP3 RP }. (* Basic properties *********************************************************) (* Basic_1: was: nf2_lift1 *) -lemma acp_lifts: ∀RR,RS. CP4 RR RS → CP4s RR RS. +lemma acp_lifts: ∀RR,RS. CP2 RR RS → CP2s RR RS. #RR #RS #HRR #L1 #L2 #des #H elim H -L1 -L2 -des [ #L #T1 #T2 #H #HT1 <(lifts_inv_nil … H) -H // diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma index b23563f14..5e5d699e9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma @@ -32,7 +32,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. [ #L #k #L0 #des #HL0 #X #H #L2 #HL20 >(lifts_inv_sort1 … H) -H lapply (aacr_acr … H1RP H2RP (⓪)) #HAtom - @(s2 … HAtom … ◊) // /2 width=2/ + @(s4 … HAtom … ◊) // | #I #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20 lapply (aacr_acr … H1RP H2RP B) #HB elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct @@ -43,27 +43,24 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. elim (lsubc_ldrop_O1_trans … HL20 … HL0) -HL0 #X #HLK2 #H elim (lsubc_inv_pair2 … H) -H * [ #K2 #HK20 #H destruct - generalize in match HLK2; generalize in match I; -HLK2 -I * #HLK2 - [ elim (lift_total V0 0 (i0 +1)) #V #HV0 - elim (lifts_lift_trans … Hi0 … Hdes0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2 - @(s4 … HB … ◊ … HV0 HLK2) /3 width=7/ (* uses IHB HL20 V2 HV0 *) - | @(s2 … HB … ◊) // /2 width=3/ - ] + elim (lift_total V0 0 (i0 +1)) #V #HV0 + elim (lifts_lift_trans … Hi0 … Hdes0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2 + @(s5 … HB … ◊ … HV0 HLK2) /3 width=7/ (* uses IHB HL20 V2 HV0 *) | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0 #K2 #V2 #A2 #HKV2A #HKV0A #_ #H1 #H2 destruct lapply (ldrop_fwd_ldrop2 … HLK2) #HLK2b lapply (aaa_lifts … HK01 … HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B >(aaa_mono … HKV0A … HKV0B) in HKV2A; -HKV0A -HKV0B #HKV2B elim (lift_total V2 0 (i0 +1)) #V #HV2 - @(s4 … HB … ◊ … HV2 HLK2) - @(s7 … HB … HKV2B) // + @(s5 … HB … ◊ … HV2 HLK2) + @(s8 … HB … HKV2B) // ] | #a #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (aacr_acr … H1RP H2RP A) #HA lapply (aacr_acr … H1RP H2RP B) #HB lapply (s1 … HB) -HB #HB - @(s5 … HA … ◊ ◊) // /3 width=5/ + @(s6 … HA … ◊ ◊) // /3 width=5/ | #a #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02 elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct @(aacr_abst … H1RP H2RP) @@ -84,7 +81,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (aacr_acr … H1RP H2RP A) #HA lapply (s1 … HA) #H - @(s6 … HA … ◊) /2 width=5/ /3 width=5/ + @(s7 … HA … ◊) /2 width=5/ /3 width=5/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma index a452a9073..a91a9f318 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma @@ -33,21 +33,24 @@ definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→p definition S3 ≝ λRP,C:lenv→predicate term. ∀a,L,Vs,V,T,W. C L (ⒶVs. ⓓ{a}V. T) → RP L W → C L (ⒶVs. ⓐV. ⓛ{a}W. T). -definition S4 ≝ λRP,C:lenv→predicate term. ∀L,K,Vs,V1,V2,i. +definition S4 ≝ λRP,C:lenv→predicate term. + ∀L,Vs. all … (RP L) Vs → ∀k. C L (ⒶVs.⋆k). + +definition S5 ≝ λRP,C:lenv→predicate term. ∀I,L,K,Vs,V1,V2,i. C L (ⒶVs. V2) → ⇧[0, i + 1] V1 ≡ V2 → - ⇩[0, i] L ≡ K. ⓓV1 → C L (Ⓐ Vs. #i). + ⇩[0, i] L ≡ K. ⓑ{I}V1 → C L (Ⓐ Vs. #i). -definition S5 ≝ λRP,C:lenv→predicate term. +definition S6 ≝ λRP,C:lenv→predicate term. ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → ∀a,V,T. C (L. ⓓV) (ⒶV2s. T) → RP L V → C L (ⒶV1s. ⓓ{a}V. T). -definition S6 ≝ λRP,C:lenv→predicate term. +definition S7 ≝ λRP,C:lenv→predicate term. ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. ⓝW. T). -definition S7 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e. +definition S8 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e. C L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2. -definition S7s ≝ λC:lenv→predicate term. +definition S8s ≝ λC:lenv→predicate term. ∀L1,L2,des. ⇩*[des] L2 ≡ L1 → ∀T1,T2. ⇧*[des] T1 ≡ T2 → C L1 T1 → C L2 T2. @@ -59,7 +62,8 @@ record acr (RR:lenv->relation term) (RS:relation term) (RP,C:lenv→predicate te s4: S4 RP C; s5: S5 RP C; s6: S6 RP C; - s7: S7 C + s7: S7 RP C; + s8: S8 C }. (* the abstract candidate of reducibility associated to an atomic arity *) @@ -77,7 +81,7 @@ interpretation (* Basic properties *********************************************************) (* Basic_1: was: sc3_lift1 *) -lemma acr_lifts: ∀C. S7 C → S7s C. +lemma acr_lifts: ∀C. S8 C → S8s C. #C #HC #L1 #L2 #des #H elim H -L1 -L2 -des [ #L #T1 #T2 #H #HT1 <(lifts_inv_nil … H) -H // @@ -91,7 +95,7 @@ lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) → RP L V → RP L0 V0. #RR #RS #RP #HRP #des #L0 #L #V #V0 #HL0 #HV0 #HV @acr_lifts /width=6/ -@(s7 … HRP) +@(s8 … HRP) qed. (* Basic_1: was only: sns3_lifts1 *) @@ -111,10 +115,11 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → #RR #RS #RP #H1RP #H2RP #A elim A -A normalize // #B #A #IHB #IHA @mk_acr normalize [ #L #T #H - lapply (H ? (⋆0) ? ⟠ ? ? ?) -H + elim (cp1 … H1RP L) #k #HK + lapply (H ? (⋆k) ? ⟠ ? ? ?) -H [1,3: // |2,4: skip - | @(s2 … IHB … ◊) // /2 width=2/ - | #H @(cp3 … H1RP … 0) @(s1 … IHA) // + | @(s2 … IHB … ◊) // + | #H @(cp3 … H1RP … k) @(s1 … IHA) // ] | #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct @@ -125,7 +130,12 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct @(s3 … IHA … (V0 @ V0s)) /2 width=6 by rp_lifts/ /4 width=5/ -| #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H +| #L #Vs #HVs #k #L0 #V0 #X #hdes #HB #HL0 #H + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + >(lifts_inv_sort1 … HY) -Y + lapply (s1 … IHB … HB) #HV0 + @(s4 … IHA … (V0 @ V0s)) /3 width=6/ +| #I #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct elim (ldrops_ldrop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0 @@ -134,15 +144,15 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → elim (lift_total W1 0 (i0 + 1)) #W2 #HW12 elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2 >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2 - @(s4 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4/ + @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4/ | #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct elim (lift_total V10 0 1) #V20 #HV120 elim (liftv_total 0 1 V10s) #V20s #HV120s - @(s5 … IHA … (V10 @ V10s) (V20 @ V20s)) /2 width=1/ /2 width=6 by rp_lifts/ + @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /2 width=1/ /2 width=6 by rp_lifts/ @(HA … (des + 1)) /2 width=1/ - [ @(s7 … IHB … HB … HV120) /2 width=1/ + [ @(s8 … IHB … HB … HV120) /2 width=1/ | @lifts_applv // elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s >(liftv_mono … HV12s … HV10s) -V1s // @@ -150,7 +160,7 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → | #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct - @(s6 … IHA … (V0 @ V0s)) /2 width=6 by rp_lifts/ /3 width=4/ + @(s7 … IHA … (V0 @ V0s)) /2 width=6 by rp_lifts/ /3 width=4/ | /3 width=7/ ] qed. @@ -167,7 +177,7 @@ lapply (aacr_acr … H1RP H2RP B) #HCB elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct lapply (s1 … HCB) -HCB #HCB @(s3 … HCA … ◊) /2 width=6 by rp_lifts/ -@(s5 … HCA … ◊ ◊) // /2 width=1/ /2 width=3/ +@(s6 … HCA … ◊ ◊) // /2 width=1/ /2 width=3/ qed. (* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma index f1f6495bd..1b3bcf666 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reduction/cnf.ma". +include "basic_2/reduction/cnr.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) @@ -168,7 +168,7 @@ elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3/ * qed-. (* Basic_1: was: nf2_pr3_unfold *) -lemma cprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U. +lemma cprs_inv_cnr1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U. #L #T #U #H @(cprs_ind_dx … H) -T // #T0 #T #H1T0 #_ #IHT #H2T0 lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma deleted file mode 100644 index faeb6a633..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma +++ /dev/null @@ -1,25 +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/lpx_aaa.ma". -include "basic_2/computation/cprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) - -(* Properties about atomic arity assignment on terms ************************) - -lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ⁝ A. -#L #T1 #A #HT1 #T2 #HT12 -@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=3 by aaa_cpr_conf/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lpss.ma index 271094919..9887fa77c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lpss.ma @@ -89,4 +89,4 @@ elim (lpss_cpss_conf_dx … HU12 … HL12) -L1 #U #HU1 #HU2 elim (cpss_conf … HU1 … HUT1) -U1 #U1 #HU1 #HTU1 lapply (cpss_trans … HU2 … HU1) -U lapply (cprs_cpss_trans … HT21 … HTU1) -T1 /2 width=3/ -qed-. \ No newline at end of file +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc.ma deleted file mode 100644 index 143079b0c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc.ma +++ /dev/null @@ -1,91 +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/grammar/tstc.ma". -include "basic_2/computation/lprs_cprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) - -(* Forward lemmas involving same top term constructor ***********************) - -lemma cprs_fwd_cnf: ∀L,T. L ⊢ 𝐍⦃T⦄ → ∀U. L ⊢ T ➡* U → T ≃ U. -#L #T #HT #U #H ->(cprs_inv_cnf1 … H HT) -L -T // -qed-. - -(* Basic_1: was: pr3_iso_beta *) -lemma cprs_fwd_beta: ∀a,L,V,W,T,U. L ⊢ ⓐV. ⓛ{a}W. T ➡* U → - ⓐV. ⓛ{a}W. T ≃ U ∨ L ⊢ ⓓ{a}V. T ➡* U. -#a #L #V #W #T #U #H -elim (cprs_inv_appl1 … H) -H * -[ #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #b #V0 #W0 #T0 #HV0 #HT0 #HU - elim (cprs_fwd_abst1 … HT0 Abbr V) -HT0 #W1 #T1 #_ #HT1 #H destruct -W1 - @or_intror -W - @(cprs_trans … HU) -U /2 width=1/ (**) (* explicit constructor *) -| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_ - elim (cprs_fwd_abst1 … HT1 Abbr V) -HT1 #W2 #T2 #_ #_ #H destruct -] -qed-. - -(* Note: probably this is an inversion lemma *) -lemma cprs_fwd_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 → - ∀V2. ⇧[0, i + 1] V1 ≡ V2 → - ∀U. L ⊢ #i ➡* U → - #i ≃ U ∨ L ⊢ V2 ➡* U. -#L #K #V1 #i #HLK #V2 #HV12 #U #H -elim (cprs_inv_lref1 … H) -H /2 width=1/ -* #K0 #V0 #U0 #HLK0 #HVU0 #HU0 -lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct -lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=9/ -qed-. - -lemma cprs_fwd_theta: ∀a,L,V1,V,T,U. L ⊢ ⓐV1. ⓓ{a}V. T ➡* U → - ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1. ⓓ{a}V. T ≃ U ∨ - L ⊢ ⓓ{a}V. ⓐV2. T ➡* U. -#a #L #V1 #V #T #U #H #V2 #HV12 -elim (cprs_inv_appl1 … H) -H * -[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #b #V0 #W #T0 #HV10 #HT0 #HU - elim (cprs_inv_abbr1 … HT0) -HT0 * - [ #V3 #T3 #_ #_ #H destruct - | #X #HT2 #H #H0 destruct - elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct - @or_intror @(cprs_trans … HU) -U (**) (* explicit constructor *) - @(cprs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1/ ] -T - @(cprs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [ /5 width=7/ ] -V -V2 -W2 -T2 - @(cprs_strap2 … (ⓓ{b}V1.T0)) [ /3 width=1/ ] -W /2 width=1/ - ] -| #b #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU - @or_intror @(cprs_trans … HU) -U (**) (* explicit constructor *) - elim (cprs_inv_abbr1 … HT0) -HT0 * - [ #V5 #T5 #HV5 #HT5 #H destruct - lapply (cprs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3 /2 width=1/ - /3 width=1/ - | #X #HT1 #H #H0 destruct - elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct - lapply (cprs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=1/ #HV24 - @(cprs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1/ ] -T - @(cprs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V5 -T5 - @(cprs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/ - ] -] -qed-. - -lemma cprs_fwd_tau: ∀L,W,T,U. L ⊢ ⓝW. T ➡* U → - ⓝW. T ≃ U ∨ L ⊢ T ➡* U. -#L #W #T #U #H -elim (cprs_inv_cast1 … H) -H /2 width=1/ * -#W0 #T0 #_ #_ #H destruct /2 width=1/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma deleted file mode 100644 index 46377da57..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma +++ /dev/null @@ -1,157 +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/grammar/tstc_vector.ma". -include "basic_2/relocation/lift_vector.ma". -include "basic_2/computation/cprs_tstc.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) - -(* Vector form of forward lemmas involving same top term constructor ********) - -(* Basic_1: was just: nf2_iso_appls_lref *) -lemma cprs_fwd_cnf_vector: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ∀Vs,U. L ⊢ ⒶVs.T ➡* U → ⒶVs.T ≃ U. -#L #T #H1T #H2T #Vs elim Vs -Vs [ @(cprs_fwd_cnf … H2T) ] (**) (* /2 width=3 by cprs_fwd_cnf/ does not work *) -#V #Vs #IHVs #U #H -elim (cprs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #a #V0 #W0 #T0 #HV0 #HT0 #HU - lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (tstc_inv_bind_appls_simple … HT0 ?) // -| #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU - lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (tstc_inv_bind_appls_simple … HT0 ?) // -] -qed-. - -(* Basic_1: was: pr3_iso_appls_beta *) -lemma cprs_fwd_beta_vector: ∀a,L,Vs,V,W,T,U. L ⊢ ⒶVs. ⓐV. ⓛ{a}W. T ➡* U → - ⒶVs. ⓐV. ⓛ{a}W. T ≃ U ∨ L ⊢ ⒶVs. ⓓ{a}V. T ➡* U. -#a #L #Vs elim Vs -Vs /2 width=1 by cprs_fwd_beta/ -#V0 #Vs #IHVs #V #W #T #U #H -elim (cprs_inv_appl1 … H) -H * -[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1/ -| #b #V1 #W1 #T1 #HV01 #HT1 #HU - elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_appls_simple … HT1 ?) // - | @or_intror -W (**) (* explicit constructor *) - @(cprs_trans … HU) -U - @(cprs_strap1 … (ⓐV1.ⓛ{b}W1.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=1/ - ] -| #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU - elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_appls_simple … HT1 ?) // - | @or_intror -W (**) (* explicit constructor *) - @(cprs_trans … HU) -U - @(cprs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=3/ - ] -] -qed-. - -lemma cprs_fwd_delta_vector: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 → - ∀V2. ⇧[0, i + 1] V1 ≡ V2 → - ∀Vs,U. L ⊢ ⒶVs.#i ➡* U → - ⒶVs.#i ≃ U ∨ L ⊢ ⒶVs.V2 ➡* U. -#L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=4 by cprs_fwd_delta/ -#V #Vs #IHVs #U #H -K -V1 -elim (cprs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #b #V0 #W0 #T0 #HV0 #HT0 #HU - elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_appls_simple … HT0 ?) // - | @or_intror -i (**) (* explicit constructor *) - @(cprs_trans … HU) -U - @(cprs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=1/ - ] -| #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU - elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_appls_simple … HT0 ?) // - | @or_intror -i (**) (* explicit constructor *) - @(cprs_trans … HU) -U - @(cprs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=3/ - ] -] -qed-. - -(* Basic_1: was: pr3_iso_appls_abbr *) -lemma cprs_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → - ∀a,V,T,U. L ⊢ ⒶV1s. ⓓ{a}V. T ➡* U → - ⒶV1s. ⓓ{a}V. T ≃ U ∨ L ⊢ ⓓ{a}V. ⒶV2s. T ➡* U. -#L #V1s #V2s * -V1s -V2s /3 width=1/ -#V1s #V2s #V1a #V2a #HV12a #HV12s #a -generalize in match HV12a; -HV12a -generalize in match V2a; -V2a -generalize in match V1a; -V1a -elim HV12s -V1s -V2s /2 width=1 by cprs_fwd_theta/ -#V1s #V2s #V1b #V2b #HV12b #_ #IHV12s #V1a #V2a #HV12a #V #T #U #H -elim (cprs_inv_appl1 … H) -H * -[ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #b #V0a #W0 #T0 #HV10a #HT0 #HU - elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0 - [ -HV12a -HV12b -HV10a -HU - elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct - | @or_intror -V1s (**) (* explicit constructor *) - @(cprs_trans … HU) -U - elim (cprs_inv_abbr1 … HT0) -HT0 * - [ -HV12a -HV12b -HV10a #V1 #T1 #_ #_ #H destruct - | -V1b #X #HT1 #H #H0 destruct - elim (lift_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct - @(cprs_trans … (+ⓓV.ⓐV2a.ⓛ{b}W1.T1)) [ /3 width=1/ ] -T -V2b -V2s - @(cprs_strap2 … (ⓐV1a.ⓛ{b}W0.T0)) [ /5 width=7/ ] -V -V2a -W1 -T1 - @(cprs_strap2 … (ⓓ{b}V1a.T0)) [ /3 width=1/ ] -W0 /2 width=1/ - ] - ] -| #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU - elim (IHV12s … HV12b … HT0) -HV12b -IHV12s -HT0 #HT0 - [ -HV12a -HV10a -HV0a -HU - elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct - | @or_intror -V1s -V1b (**) (* explicit constructor *) - @(cprs_trans … HU) -U - elim (cprs_inv_abbr1 … HT0) -HT0 * - [ #V1 #T1 #HV1 #HT1 #H destruct - lapply (cprs_lift … HV10a (L.ⓓV) … HV12a … HV0a) -V1a -V0a [ /2 width=1/ ] #HV2a - @(cprs_trans … (ⓓ{a}V.ⓐV2a.T1)) [ /3 width=1/ ] -T -V2b -V2s /3 width=1/ - | #X #HT1 #H #H0 destruct - elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct - lapply (cprs_lift … HV10a (L.ⓓV0) … HV12a … HV0a) -V0a [ /2 width=1/ ] #HV2a - @(cprs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1/ ] -T -V2b -V2s - @(cprs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V1 -T1 - @(cprs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/ - ] - ] -] -qed-. - -(* Basic_1: was: pr3_iso_appls_cast *) -lemma cprs_fwd_tau_vector: ∀L,Vs,W,T,U. L ⊢ ⒶVs. ⓝW. T ➡* U → - ⒶVs. ⓝW. T ≃ U ∨ L ⊢ ⒶVs. T ➡* U. -#L #Vs elim Vs -Vs /2 width=1 by cprs_fwd_tau/ -#V #Vs #IHVs #W #T #U #H -elim (cprs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ -| #b #V0 #W0 #T0 #HV0 #HT0 #HU - elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_appls_simple … HT0 ?) // - | @or_intror -W (**) (* explicit constructor *) - @(cprs_trans … HU) -U - @(cprs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=1/ - ] -| #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU - elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_appls_simple … HT0 ?) // - | @or_intror -W (**) (* explicit constructor *) - @(cprs_trans … HU) -U - @(cprs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=3/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma index 202d14d14..ba775d00d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) -include "basic_2/reduction/cpx.ma". +include "basic_2/reduction/cnx.ma". include "basic_2/computation/cprs.ma". -(* EXTENDED CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS *****************) +(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) definition cpxs: ∀h. sd h → lenv → relation term ≝ λh,g. LTC … (cpx h g). @@ -147,3 +147,9 @@ lemma cpxs_inv_cast1: ∀h,g,L,W1,T1,U2. ⦃h, L⦄ ⊢ ⓝW1.T1 ➡*[g] U2 → elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3/ * #W2 #T2 #HW2 #HT2 #H destruct /4 width=5/ qed-. + +lemma cpxs_inv_cnx1: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T ➡*[g] U → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → T = U. +#h #g #L #T #U #H @(cpxs_ind_dx … H) -T // +#T0 #T #H1T0 #_ #IHT #H2T0 +lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_aaa.ma new file mode 100644 index 000000000..ed2329c54 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_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 aaa_cpxs_conf: ∀h,g,L,T1,A. L ⊢ T1 ⁝ A → + ∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → L ⊢ T2 ⁝ A. +#h #g #L #T1 #A #HT1 #T2 #HT12 +@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=5 by aaa_cpx_conf/ +qed-. + +lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ⁝ A. +/3 width=5 by aaa_cpxs_conf, cprs_cpxs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma new file mode 100644 index 000000000..08696ac93 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma @@ -0,0 +1,107 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ldrop.ma". +include "basic_2/computation/cpxs_lift.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) + +(* Main properties **********************************************************) + +theorem cpxs_trans: ∀h,g,L. Transitive … (cpxs h g L). +#h #g #L #T1 #T #HT1 #T2 @trans_TC @HT1 qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *) + +theorem cpxs_bind: ∀h,g,a,I,L,V1,V2,T1,T2. ⦃h, L.ⓑ{I}V1⦄ ⊢ T1 ➡*[g] T2 → + ⦃h, L⦄ ⊢ V1 ➡*[g] V2 → + ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2. +#h #g #a #I #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/ +#V #V2 #_ #HV2 #IHV1 +@(cpxs_trans … IHV1) -V1 /2 width=1/ +qed. + +theorem cpxs_flat: ∀h,g,I,L,V1,V2,T1,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → + ⦃h, L⦄ ⊢ V1 ➡*[g] V2 → + ⦃h, L⦄ ⊢ ⓕ{I} V1.T1 ➡*[g] ⓕ{I} V2.T2. +#h #g #I #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/ +#V #V2 #_ #HV2 #IHV1 +@(cpxs_trans … IHV1) -IHV1 /2 width=1/ +qed. + +theorem cpxs_beta: ∀h,g,a,L,V1,V2,W,T1,T2. + ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ V1 ➡*[g] V2 → + ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W.T1 ➡*[g] ⓓ{a}V2.T2. +#h #g #a #L #V1 #V2 #W #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/ +#V #V2 #_ #HV2 #IHV1 +@(cpxs_trans … IHV1) /2 width=1/ +qed. + +theorem cpxs_theta_rc: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2. + ⦃h, L⦄ ⊢ V1 ➡[g] V → ⇧[0, 1] V ≡ V2 → + ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 → + ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2. +#h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 /2 width=3/ +#W #W2 #_ #HW2 #IHW1 +@(cpxs_trans … IHW1) /2 width=1/ +qed. + +theorem cpxs_theta: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2. + ⇧[0, 1] V ≡ V2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 → + ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ V1 ➡*[g] V → + ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2. +#h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 /2 width=3/ +#V1 #V0 #HV10 #_ #IHV0 +@(cpxs_trans … IHV0) /2 width=1/ +qed. + +(* Properties on sn extended parallel reduction for local environments ******) + +lemma lpx_cpx_trans: ∀h,g. s_r_trans … (cpx h g) (lpx h g). +#h #g #L2 #T1 #T2 #HT12 elim HT12 -L2 -T1 -T2 +[ /2 width=3/ +| /3 width=2/ +| #I #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12 + elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H + elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct + lapply (IHV02 … HK12) -K2 #HV02 + lapply (cpxs_strap2 … HV10 … HV02) -V0 /2 width=7/ +| #a #I #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12 + lapply (IHT12 (L1.ⓑ{I}V1) ?) -IHT12 /2 width=1/ /3 width=1/ +|5,7: /3 width=1/ +| #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12 + lapply (IHT1 (L1.ⓓV2) ?) -IHT1 /2 width=1/ /2 width=3/ +| #a #L2 #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12 + lapply (IHT12 (L1.ⓛW) ?) -IHT12 /2 width=1/ /3 width=1/ +| #a #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12 + lapply (IHT12 (L1.ⓓW1) ?) -IHT12 /2 width=1/ /3 width=3/ +] +qed-. + +lemma cpx_bind2: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 → + ∀I,T1,T2. ⦃h, L.ⓑ{I}V2⦄ ⊢ T1 ➡[g] T2 → + ∀a. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2. +#h #g #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 +lapply (lpx_cpx_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/ +qed. + +(* Advanced properties ******************************************************) + +lemma lpx_cpxs_trans: ∀h,g. s_rs_trans … (cpx h g) (lpx h g). +/3 width=5 by s_r_trans_TC1, lpx_cpx_trans/ qed-. + +lemma cpxs_bind2_dx: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 → + ∀I,T1,T2. ⦃h, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[g] T2 → + ∀a. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2. +#h #g #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 +lapply (lpx_cpxs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma index 52aff988f..2e86e82f4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/substitution/fsups_fsups.ma". include "basic_2/reduction/cpx_lift.ma". include "basic_2/computation/cpxs.ma". @@ -47,19 +48,15 @@ qed-. (* Relocation properties ****************************************************) -(* Basic_1: was: pr3_lift *) lemma cpxs_lift: ∀h,g. l_liftable (cpxs h g). /3 width=9/ qed. -(* Basic_1: was: pr3_gen_lift *) lemma cpxs_inv_lift1: ∀h,g. l_deliftable_sn (cpxs h g). /3 width=5 by l_deliftable_sn_LTC, cpx_inv_lift1/ qed-. (* Properties on supclosure *************************************************) -include "basic_2/substitution/fsups.ma". - lemma fsupq_cpxs_trans: ∀h,g,L1,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 ➡*[g] U2 → ∀T1. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ → ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡*[g] U1 & ⦃L1, U1⦄ ⊃* ⦃L2, U2⦄. @@ -69,6 +66,16 @@ elim (fsupq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2 elim (IHTU2 … HT2) -T2 /3 width=3/ qed-. +lemma fsups_cpxs_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄ → + ∀U2. ⦃h, L2⦄ ⊢ T2 ➡*[g] U2 → + ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡*[g] U1 & ⦃L1, U1⦄ ⊃* ⦃L2, U2⦄. +#h #g #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2 [ /2 width=3/ ] +#L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2 +elim (fsupq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2 +elim (IHT1 … HT2) -T #T #HT1 #HT2 +lapply (fsups_trans … HT2 … HTU2) -L -T2 /2 width=3/ +qed-. + lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ → ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma new file mode 100644 index 000000000..e8478aa84 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma @@ -0,0 +1,92 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/tstc.ma". +include "basic_2/computation/lpxs_cpxs.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) + +(* Forward lemmas involving same top term constructor ***********************) + +lemma cpxs_fwd_cnx: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ∀U. ⦃h, L⦄ ⊢ T ➡*[g] U → T ≃ U. +#h #g #L #T #HT #U #H +>(cpxs_inv_cnx1 … H HT) -L -T // +qed-. + +(* Basic_1: was just: pr3_iso_beta *) +lemma cpxs_fwd_beta: ∀h,g,a,L,V,W,T,U. ⦃h, L⦄ ⊢ ⓐV.ⓛ{a}W.T ➡*[g] U → + ⓐV.ⓛ{a}W.T ≃ U ∨ + ∃∃T0. ⦃h, L.ⓛW⦄ ⊢ T ➡*[g] T0 & ⦃h, L⦄ ⊢ ⓓ{a}V.T0 ➡*[g] U. +#h #g #a #L #V #W #T #U #H +elim (cpxs_inv_appl1 … H) -H * +[ #V0 #T0 #_ #_ #H destruct /2 width=1/ +| #b #V0 #W0 #T0 #HV0 #HT0 #HU + elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #_ #HT1 #H destruct -W1 + @or_intror @(ex2_intro … HT1) -W (**) (* explicit constructors *) + @(cpxs_trans … HU) -U /2 width=1/ +| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_ + elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct +] +qed-. + +(* Note: probably this is an inversion lemma *) +lemma cpxs_fwd_delta: ∀h,g,I,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 → + ∀V2. ⇧[0, i + 1] V1 ≡ V2 → + ∀U. ⦃h, L⦄ ⊢ #i ➡*[g] U → + #i ≃ U ∨ ⦃h, L⦄ ⊢ V2 ➡*[g] U. +#h #g #I #L #K #V1 #i #HLK #V2 #HV12 #U #H +elim (cpxs_inv_lref1 … H) -H /2 width=1/ +* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0 +lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct +lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=9/ +qed-. + +lemma cpxs_fwd_theta: ∀h,g,a,L,V1,V,T,U. ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[g] U → + ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≃ U ∨ + ⦃h, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[g] U. +#h #g #a #L #V1 #V #T #U #H #V2 #HV12 +elim (cpxs_inv_appl1 … H) -H * +[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1/ +| #b #V0 #W #T0 #HV10 #HT0 #HU + elim (cpxs_inv_abbr1 … HT0) -HT0 * + [ #V3 #T3 #_ #_ #H destruct + | #X #HT2 #H #H0 destruct + elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct + @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *) + @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1/ ] -T + @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [ /5 width=7/ ] -V -V2 -W2 -T2 + @(cpxs_strap2 … (ⓓ{b}V1.T0)) [ /3 width=1/ ] -W /2 width=1/ + ] +| #b #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 + lapply (cpxs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3 /2 width=1/ + /3 width=1/ + | #X #HT1 #H #H0 destruct + elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct + lapply (cpxs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=1/ #HV24 + @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1/ ] -T + @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V5 -T5 + @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/ + ] +] +qed-. + +lemma cpxs_fwd_tau: ∀h,g,L,W,T,U. ⦃h, L⦄ ⊢ ⓝW.T ➡*[g] U → + ⓝW. T ≃ U ∨ ⦃h, L⦄ ⊢ T ➡*[g] U. +#h #g #L #W #T #U #H +elim (cpxs_inv_cast1 … H) -H /2 width=1/ * +#W0 #T0 #_ #_ #H destruct /2 width=1/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma new file mode 100644 index 000000000..dffa50fba --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma @@ -0,0 +1,162 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/tstc_vector.ma". +include "basic_2/relocation/lift_vector.ma". +include "basic_2/computation/cpxs_tstc.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) + +(* Vector form of forward lemmas involving same top term constructor ********) + +(* Basic_1: was just: nf2_iso_appls_lref *) +lemma cpxs_fwd_cnx_vector: ∀h,g,L,T. 𝐒⦃T⦄ → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → + ∀Vs,U. ⦃h, L⦄ ⊢ ⒶVs.T ➡*[g] U → ⒶVs.T ≃ U. +#h #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/ +| #a #V0 #W0 #T0 #HV0 #HT0 #HU + lapply (IHVs … HT0) -IHVs -HT0 #HT0 + elim (tstc_inv_bind_appls_simple … HT0) // +| #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU + lapply (IHVs … HT0) -IHVs -HT0 #HT0 + elim (tstc_inv_bind_appls_simple … HT0) // +] +qed-. + +(* Basic_1: was just: pr3_iso_appls_beta *) +lemma cpxs_fwd_beta_vector: ∀h,g,a,L,Vs,V,W,T,U. ⦃h, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[g] U → + ⒶVs. ⓐV. ⓛ{a}W. T ≃ U ∨ + ∃∃T0.⦃h, L.ⓛW⦄ ⊢ T ➡*[g] T0 & ⦃h, L⦄ ⊢ ⒶVs.ⓓ{a}V.T0 ➡*[g] U. +#h #g #a #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/ +| #b #V1 #W1 #T1 #HV01 #HT1 #HU + elim (IHVs … HT1) -IHVs -HT1 + [ #HT1 elim (tstc_inv_bind_appls_simple … HT1) // + | * #T0 #HT0 #HT01 + @or_intror @(ex2_intro … HT0) -W (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV1.ⓛ{b}W1.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=1/ + ] +| #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU + elim (IHVs … HT1) -IHVs -HT1 + [ #HT1 elim (tstc_inv_bind_appls_simple … HT1) // + | * #T0 #HT0 #HT01 + @or_intror @(ex2_intro … HT0) -W (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=3/ + ] +] +qed-. + +lemma cpxs_fwd_delta_vector: ∀h,g,I,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 → + ∀V2. ⇧[0, i + 1] V1 ≡ V2 → + ∀Vs,U. ⦃h, L⦄ ⊢ ⒶVs.#i ➡*[g] U → + ⒶVs.#i ≃ U ∨ ⦃h, L⦄ ⊢ ⒶVs.V2 ➡*[g] U. +#h #g #I #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta/ +#V #Vs #IHVs #U #H -K -V1 +elim (cpxs_inv_appl1 … H) -H * +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ +| #b #V0 #W0 #T0 #HV0 #HT0 #HU + elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (tstc_inv_bind_appls_simple … HT0) // + | @or_intror -i (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=1/ + ] +| #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU + elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (tstc_inv_bind_appls_simple … HT0) // + | @or_intror -i (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=3/ + ] +] +qed-. + +(* Basic_1: was just: pr3_iso_appls_abbr *) +lemma cpxs_fwd_theta_vector: ∀h,g,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀a,V,T,U. ⦃h, L⦄ ⊢ ⒶV1s.ⓓ{a}V.T ➡*[g] U → + ⒶV1s. ⓓ{a}V. T ≃ U ∨ ⦃h, L⦄ ⊢ ⓓ{a}V.ⒶV2s.T ➡*[g] U. +#h #g #L #V1s #V2s * -V1s -V2s /3 width=1/ +#V1s #V2s #V1a #V2a #HV12a #HV12s #a +generalize in match HV12a; -HV12a +generalize in match V2a; -V2a +generalize in match V1a; -V1a +elim HV12s -V1s -V2s /2 width=1 by cpxs_fwd_theta/ +#V1s #V2s #V1b #V2b #HV12b #_ #IHV12s #V1a #V2a #HV12a #V #T #U #H +elim (cpxs_inv_appl1 … H) -H * +[ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1/ +| #b #V0a #W0 #T0 #HV10a #HT0 #HU + elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0 + [ -HV12a -HV12b -HV10a -HU + elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct + | @or_intror -V1s (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + elim (cpxs_inv_abbr1 … HT0) -HT0 * + [ -HV12a -HV12b -HV10a #V1 #T1 #_ #_ #H destruct + | -V1b #X #HT1 #H #H0 destruct + elim (lift_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct + @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{b}W1.T1)) [ /3 width=1/ ] -T -V2b -V2s + @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0)) [ /5 width=7/ ] -V -V2a -W1 -T1 + @(cpxs_strap2 … (ⓓ{b}V1a.T0)) [ /3 width=1/ ] -W0 /2 width=1/ + ] + ] +| #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU + elim (IHV12s … HV12b … HT0) -HV12b -IHV12s -HT0 #HT0 + [ -HV12a -HV10a -HV0a -HU + elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct + | @or_intror -V1s -V1b (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + elim (cpxs_inv_abbr1 … HT0) -HT0 * + [ #V1 #T1 #HV1 #HT1 #H destruct + lapply (cpxs_lift … HV10a (L.ⓓV) … HV12a … HV0a) -V1a -V0a [ /2 width=1/ ] #HV2a + @(cpxs_trans … (ⓓ{a}V.ⓐV2a.T1)) [ /3 width=1/ ] -T -V2b -V2s /3 width=1/ + | #X #HT1 #H #H0 destruct + elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct + lapply (cpxs_lift … HV10a (L.ⓓV0) … HV12a … HV0a) -V0a [ /2 width=1/ ] #HV2a + @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1/ ] -T -V2b -V2s + @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V1 -T1 + @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/ + ] + ] +] +qed-. + +(* Basic_1: was just: pr3_iso_appls_cast *) +lemma cpxs_fwd_tau_vector: ∀h,g,L,Vs,W,T,U. ⦃h, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[g] U → + ⒶVs. ⓝW. T ≃ U ∨ ⦃h, L⦄ ⊢ ⒶVs.T ➡*[g] U. +#h #g #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_tau/ +#V #Vs #IHVs #W #T #U #H +elim (cpxs_inv_appl1 … H) -H * +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/ +| #b #V0 #W0 #T0 #HV0 #HT0 #HU + elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (tstc_inv_bind_appls_simple … HT0) // + | @or_intror -W (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=1/ + ] +| #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU + elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (tstc_inv_bind_appls_simple … HT0) // + | @or_intror -W (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=3/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma index 9a3154784..92719458e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma @@ -12,93 +12,99 @@ (* *) (**************************************************************************) -include "basic_2/reduction/cnf.ma". +include "basic_2/reduction/cnx.ma". -(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) -definition csn: lenv → predicate term ≝ λL. SN … (cpr L) (eq …). +definition csn: ∀h. sd h → lenv → predicate term ≝ + λh,g,L. SN … (cpx h g L) (eq …). interpretation - "context-sensitive strong normalization (term)" - 'SN L T = (csn L T). + "context-sensitive extended strong normalization (term)" + 'SN h g L T = (csn h g L T). (* Basic eliminators ********************************************************) -lemma csn_ind: ∀L. ∀R:predicate term. - (∀T1. L ⊢ ⬊* T1 → - (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → R T2) → +lemma csn_ind: ∀h,g,L. ∀R:predicate term. + (∀T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 → + (∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → - ∀T. L ⊢ ⬊* T → R T. -#L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1 + ∀T. ⦃h, L⦄ ⊢ ⬊*[g] T → R T. +#h #g #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1 @H0 -H0 /3 width=1/ -IHT1 /4 width=1/ qed-. (* Basic properties *********************************************************) -(* Basic_1: was: sn3_pr2_intro *) -lemma csn_intro: ∀L,T1. - (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬊* T2) → L ⊢ ⬊* T1. +(* Basic_1: was just: sn3_pr2_intro *) +lemma csn_intro: ∀h,g,L,T1. + (∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊*[g] T2) → + ⦃h, L⦄ ⊢ ⬊*[g] T1. /4 width=1/ qed. -(* Basic_1: was: sn3_nf2 *) -lemma csn_cnf: ∀L,T. L ⊢ 𝐍⦃T⦄ → L ⊢ ⬊* T. +(* Basic_1: was just: sn3_nf2 *) +lemma cnx_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ⦃h, L⦄ ⊢ ⬊*[g] T. /2 width=1/ qed. -lemma csn_cpr_trans: ∀L,T1. L ⊢ ⬊* T1 → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ ⬊* T2. -#L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 +lemma csn_cpx_trans: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 → + ∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] T2. +#h #g #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 @csn_intro #T #HLT2 #HT2 elim (term_eq_dec T1 T2) #HT12 [ -IHT1 -HLT12 destruct /3 width=1/ | -HT1 -HT2 /3 width=4/ qed-. -(* Basic_1: was: sn3_cast *) -lemma csn_cast: ∀L,W. L ⊢ ⬊* W → ∀T. L ⊢ ⬊* T → L ⊢ ⬊* ⓝW. T. -#L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT +(* Basic_1: was just: sn3_cast *) +lemma csn_cast: ∀h,g,L,W. ⦃h, L⦄ ⊢ ⬊*[g] W → + ∀T. ⦃h, L⦄ ⊢ ⬊*[g] T → ⦃h, L⦄ ⊢ ⬊*[g] ⓝW.T. +#h #g #L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT @csn_intro #X #H1 #H2 -elim (cpr_inv_cast1 … H1) -H1 +elim (cpx_inv_cast1 … H1) -H1 [ * #W0 #T0 #HLW0 #HLT0 #H destruct elim (eq_false_inv_tpair_sn … H2) -H2 - [ /3 width=3 by csn_cpr_trans/ + [ /3 width=3 by csn_cpx_trans/ | -HLW0 * #H destruct /3 width=1/ ] -| /3 width=3 by csn_cpr_trans/ +| /3 width=3 by csn_cpx_trans/ ] qed. (* Basic forward lemmas *****************************************************) -fact csn_fwd_pair_sn_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ②{I} V. T → L ⊢ ⬊* V. -#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct +fact csn_fwd_pair_sn_aux: ∀h,g,L,U. ⦃h, L⦄ ⊢ ⬊*[g] U → + ∀I,V,T. U = ②{I}V.T → ⦃h, L⦄ ⊢ ⬊*[g] V. +#h #g #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csn_intro #V2 #HLV2 #HV2 -@(IH (②{I} V2. T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/ +@(IH (②{I}V2.T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/ qed-. -(* Basic_1: was: sn3_gen_head *) -lemma csn_fwd_pair_sn: ∀I,L,V,T. L ⊢ ⬊* ②{I} V. T → L ⊢ ⬊* V. +(* Basic_1: was just: sn3_gen_head *) +lemma csn_fwd_pair_sn: ∀h,g,I,L,V,T. ⦃h, L⦄ ⊢ ⬊*[g] ②{I}V.T → ⦃h, L⦄ ⊢ ⬊*[g] V. /2 width=5 by csn_fwd_pair_sn_aux/ qed-. -fact csn_fwd_bind_dx_aux: ∀L,U. L ⊢ ⬊* U → - ∀a,I,V,T. U = ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T. -#L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct +fact csn_fwd_bind_dx_aux: ∀h,g,L,U. ⦃h, L⦄ ⊢ ⬊*[g] U → + ∀a,I,V,T. U = ⓑ{a,I}V.T → ⦃h, L.ⓑ{I}V⦄ ⊢ ⬊*[g] T. +#h #g #L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct @csn_intro #T2 #HLT2 #HT2 @(IH (ⓑ{a,I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ qed-. -(* Basic_1: was: sn3_gen_bind *) -lemma csn_fwd_bind_dx: ∀a,I,L,V,T. L ⊢ ⬊* ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T. +(* Basic_1: was just: sn3_gen_bind *) +lemma csn_fwd_bind_dx: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊢ ⬊*[g] ⓑ{a,I}V.T → ⦃h, L.ⓑ{I}V⦄ ⊢ ⬊*[g] T. /2 width=4 by csn_fwd_bind_dx_aux/ qed-. -fact csn_fwd_flat_dx_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬊* T. -#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct +fact csn_fwd_flat_dx_aux: ∀h,g,L,U. ⦃h, L⦄ ⊢ ⬊*[g] U → + ∀I,V,T. U = ⓕ{I}V.T → ⦃h, L⦄ ⊢ ⬊*[g] T. +#h #g #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csn_intro #T2 #HLT2 #HT2 -@(IH (ⓕ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ -qed. +@(IH (ⓕ{I}V.T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ +qed-. -(* Basic_1: was: sn3_gen_flat *) -lemma csn_fwd_flat_dx: ∀I,L,V,T. L ⊢ ⬊* ⓕ{I} V. T → L ⊢ ⬊* T. -/2 width=5/ qed-. +(* Basic_1: was just: sn3_gen_flat *) +lemma csn_fwd_flat_dx: ∀h,g,I,L,V,T. ⦃h, L⦄ ⊢ ⬊*[g] ⓕ{I}V.T → ⦃h, L⦄ ⊢ ⬊*[g] T. +/2 width=5 by csn_fwd_flat_dx_aux/ qed-. (* Basic_1: removed theorems 14: sn3_cdelta diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma index eb10f0981..d300affdf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma @@ -12,55 +12,59 @@ (* *) (**************************************************************************) -include "basic_2/computation/cprs.ma". +include "basic_2/computation/cpxs.ma". include "basic_2/computation/csn.ma". -(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) (* alternative definition of csn *) -definition csna: lenv → predicate term ≝ λL. SN … (cprs L) (eq …). +definition csna: ∀h. sd h → lenv → predicate term ≝ + λh,g,L. SN … (cpxs h g L) (eq …). interpretation - "context-sensitive strong normalization (term) alternative" - 'SNAlt L T = (csna L T). + "context-sensitive extended strong normalization (term) alternative" + 'SNAlt h g L T = (csna h g L T). (* Basic eliminators ********************************************************) -lemma csna_ind: ∀L. ∀R:predicate term. - (∀T1. L ⊢ ⬊⬊* T1 → - (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → R T2) → R T1 +lemma csna_ind: ∀h,g,L. ∀R:predicate term. + (∀T1. ⦃h, L⦄ ⊢ ⬊⬊*[g] T1 → + (∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → - ∀T. L ⊢ ⬊⬊* T → R T. -#L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1 + ∀T. ⦃h, L⦄ ⊢ ⬊⬊*[g] T → R T. +#h #g #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1 @H0 -H0 /3 width=1/ -IHT1 /4 width=1/ qed-. (* Basic properties *********************************************************) -(* Basic_1: was: sn3_intro *) -lemma csna_intro: ∀L,T1. - (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → L ⊢ ⬊⬊* T2) → L ⊢ ⬊⬊* T1. +(* Basic_1: was just: sn3_intro *) +lemma csna_intro: ∀h,g,L,T1. + (∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T2) → + ⦃h, L⦄ ⊢ ⬊⬊*[g] T1. /4 width=1/ qed. -fact csna_intro_aux: ∀L,T1. - (∀T,T2. L ⊢ T ➡* T2 → T1 = T → (T1 = T2 → ⊥) → L ⊢ ⬊⬊* T2) → L ⊢ ⬊⬊* T1. +fact csna_intro_aux: ∀h,g,L,T1. ( + ∀T,T2. ⦃h, L⦄ ⊢ T ➡*[g] T2 → T1 = T → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T2 + ) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T1. /4 width=3/ qed-. -(* Basic_1: was: sn3_pr3_trans (old version) *) -lemma csna_cprs_trans: ∀L,T1. L ⊢ ⬊⬊* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬊⬊* T2. -#L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 +(* Basic_1: was just: sn3_pr3_trans (old version) *) +lemma csna_cpxs_trans: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊⬊*[g] T1 → + ∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊⬊*[g] T2. +#h #g #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 @csna_intro #T #HLT2 #HT2 elim (term_eq_dec T1 T2) #HT12 [ -IHT1 -HLT12 destruct /3 width=1/ | -HT1 -HT2 /3 width=4/ qed. -(* Basic_1: was: sn3_pr2_intro (old version) *) -lemma csna_intro_cpr: ∀L,T1. - (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬊⬊* T2) → - L ⊢ ⬊⬊* T1. -#L #T1 #H -@csna_intro_aux #T #T2 #H @(cprs_ind_dx … H) -T +(* Basic_1: was just: sn3_pr2_intro (old version) *) +lemma csna_intro_cpx: ∀h,g,L,T1. ( + ∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T2 + ) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T1. +#h #g #L #T1 #H +@csna_intro_aux #T #T2 #H @(cpxs_ind_dx … H) -T [ -H #H destruct #H elim (H ?) // | #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct @@ -73,26 +77,27 @@ qed. (* Main properties **********************************************************) -theorem csn_csna: ∀L,T. L ⊢ ⬊* T → L ⊢ ⬊⬊* T. -#L #T #H @(csn_ind … H) -T /4 width=1/ +theorem csn_csna: ∀h,g,L,T. ⦃h, L⦄ ⊢ ⬊*[g] T → ⦃h, L⦄ ⊢ ⬊⬊*[g] T. +#h #g #L #T #H @(csn_ind … H) -T /4 width=1/ qed. -theorem csna_csn: ∀L,T. L ⊢ ⬊⬊* T → L ⊢ ⬊* T. -#L #T #H @(csna_ind … H) -T /4 width=1/ +theorem csna_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ ⬊⬊*[g] T → ⦃h, L⦄ ⊢ ⬊*[g] T. +#h #g #L #T #H @(csna_ind … H) -T /4 width=1/ qed. -(* Basic_1: was: sn3_pr3_trans *) -lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬊* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬊* T2. -#L #T1 #HT1 #T2 #H @(cprs_ind … H) -T2 // /2 width=3 by csn_cpr_trans/ +(* Basic_1: was just: sn3_pr3_trans *) +lemma csn_cpxs_trans: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 → + ∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] T2. +#h #g #L #T1 #HT1 #T2 #H @(cpxs_ind … H) -T2 // /2 width=3 by csn_cpx_trans/ qed-. (* Main eliminators *********************************************************) -lemma csn_ind_alt: ∀L. ∀R:predicate term. - (∀T1. L ⊢ ⬊* T1 → - (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → R T2) → R T1 +lemma csn_ind_alt: ∀h,g,L. ∀R:predicate term. + (∀T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 → + (∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → - ∀T. L ⊢ ⬊* T → R T. -#L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1 + ∀T. ⦃h, L⦄ ⊢ ⬊*[g] T → R T. +#h #g #L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1 @H0 -H0 /2 width=1/ -HT1 /3 width=1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma index 14da31097..21d97b774 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma @@ -12,77 +12,66 @@ (* *) (**************************************************************************) -include "basic_2/reduction/cnf_lift.ma". +include "basic_2/reduction/cnx_lift.ma". include "basic_2/computation/acp.ma". include "basic_2/computation/csn.ma". -(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) (* Relocation properties ****************************************************) -(* Basic_1: was: sn3_lift *) -lemma csn_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬊* T1 → - ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → L2 ⊢ ⬊* T2. -#L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12 +(* Basic_1: was just: sn3_lift *) +lemma csn_lift: ∀h,g,L2,L1,T1,d,e. ⦃h, L1⦄ ⊢ ⬊*[g] T1 → + ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → ⦃h, L2⦄ ⊢ ⬊*[g] T2. +#h #g #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12 @csn_intro #T #HLT2 #HT2 -elim (cpr_inv_lift1 … HLT2 … HL21 … HT12) -HLT2 #T0 #HT0 #HLT10 +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/ qed. -(* Basic_1: was: sn3_gen_lift *) -lemma csn_inv_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬊* T1 → - ∀T2. ⇩[d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → L2 ⊢ ⬊* T2. -#L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21 +(* Basic_1: was just: sn3_gen_lift *) +lemma csn_inv_lift: ∀h,g,L2,L1,T1,d,e. ⦃h, L1⦄ ⊢ ⬊*[g] T1 → + ∀T2. ⇩[d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → ⦃h, L2⦄ ⊢ ⬊*[g] T2. +#h #g #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21 @csn_intro #T #HLT2 #HT2 elim (lift_total T d e) #T0 #HT0 -lapply (cpr_lift … HLT2 … HL12 … HT21 … HT0) -HLT2 #HLT10 +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/ qed. (* Advanced properties ******************************************************) -(* Basic_1: was: sn3_abbr *) -lemma csn_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → K ⊢ ⬊* V → L ⊢ ⬊* #i. -#L #K #V #i #HLK #HV +(* Basic_1: was just: sn3_abbr *) +lemma csn_lref_bind: ∀h,g,I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃h, K⦄ ⊢ ⬊*[g] V → ⦃h, L⦄ ⊢ ⬊*[g] #i. +#h #g #I #L #K #V #i #HLK #HV @csn_intro #X #H #Hi -elim (cpr_inv_lref1 … H) -H -[ #H destruct elim (Hi ?) // -| -Hi * #K0 #V0 #V1 #HLK0 #HV01 #HV1 +elim (cpx_inv_lref1 … H) -H +[ #H destruct elim Hi // +| -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1 lapply (ldrop_mono … HLK0 … HLK) -HLK #H destruct lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #HLK @(csn_lift … HLK HV1) -HLK -HV1 - @(csn_cpr_trans … HV) -HV // + @(csn_cpx_trans … HV) -HV // ] qed. -lemma csn_abst: ∀a,L,W. L ⊢ ⬊* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬊* T → L ⊢ ⬊* ⓛ{a}W. T. -#a #L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT +lemma csn_appl_simple: ∀h,g,L,V. ⦃h, L⦄ ⊢ ⬊*[g] V → ∀T1. + (∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.T2) → + 𝐒⦃T1⦄ → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.T1. +#h #g #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1 @csn_intro #X #H1 #H2 -elim (cpr_fwd_abst1 … H1 I V) -H1 -#W0 #T0 #HLW0 #HLT0 #H destruct -elim (eq_false_inv_tpair_sn … H2) -H2 -[ /3 width=5 by csn_cpr_trans/ -| -HLW0 * #H destruct /3 width=1/ -] -qed. - -lemma csn_appl_simple: ∀L,V. L ⊢ ⬊* V → ∀T1. - (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) → - 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1. -#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1 -@csn_intro #X #H1 #H2 -elim (cpr_inv_appl1_simple … H1 ?) // -H1 +elim (cpx_inv_appl1_simple … H1) // -H1 #V0 #T0 #HLV0 #HLT10 #H destruct elim (eq_false_inv_tpair_dx … H2) -H2 [ -IHV -HT1 #HT10 - @(csn_cpr_trans … (ⓐV.T0)) /2 width=1/ -HLV0 + @(csn_cpx_trans … (ⓐV.T0)) /2 width=1/ -HLV0 @IHT1 -IHT1 // /2 width=1/ | -HLT10 * #H #HV0 destruct @IHV -IHV // -HT1 /2 width=1/ -HV0 #T2 #HLT02 #HT02 - @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0 + @(csn_cpx_trans … (ⓐV.T2)) /2 width=1/ -HLV0 @IHT1 -IHT1 // -HLT02 /2 width=1/ ] qed. @@ -90,21 +79,22 @@ qed. (* Advanced inversion lemmas ************************************************) (* Basic_1: was: sn3_gen_def *) -lemma csn_inv_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → L ⊢ ⬊* #i → K ⊢ ⬊* V. -#L #K #V #i #HLK #Hi +lemma csn_inv_lref_bind: ∀h,g,I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → + ⦃h, L⦄ ⊢ ⬊*[g] #i → ⦃h, K⦄ ⊢ ⬊*[g] V. +#h #g #I #L #K #V #i #HLK #Hi elim (lift_total V 0 (i+1)) #V0 #HV0 lapply (ldrop_fwd_ldrop2 … HLK) #H0LK @(csn_inv_lift … H0LK … HV0) -H0LK -@(csn_cpr_trans … Hi) -Hi /2 width=6/ +@(csn_cpx_trans … Hi) -Hi /2 width=7/ qed-. (* Main properties **********************************************************) -theorem csn_acp: acp cpr (eq …) (csn …). -@mk_acp -[ /2 width=1/ -| /2 width=3/ -| /2 width=5/ -| @cnf_lift +theorem csn_acp: ∀h,g. acp (cpx h g) (eq …) (csn h g). +#h #g @mk_acp +[ #L elim (deg_total h g 0) + #l #Hl lapply (cnx_sort_iter … L … Hl) /2 width=2/ +| @cnx_lift +| /2 width=3 by csn_fwd_flat_dx/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma deleted file mode 100644 index b406fa3f1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma +++ /dev/null @@ -1,141 +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/grammar/tstc_tstc.ma". -include "basic_2/computation/cprs_cprs.ma". -include "basic_2/computation/csn_alt.ma". -include "basic_2/computation/csn_lift.ma". - -(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) - -(* Advanced properties ******************************************************) - -lemma csn_lpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬊* T → L2 ⊢ ⬊* T. -#L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT -@csn_intro #T0 #HLT0 #HT0 -@IHT /2 width=2/ -IHT -HT0 /2 width=3 by lpr_cpr_trans/ -qed. - -lemma csn_abbr: ∀a,L,V. L ⊢ ⬊* V → ∀T. L. ⓓV ⊢ ⬊* T → L ⊢ ⬊* ⓓ{a}V. T. -#a #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT -@csn_intro #X #H1 #H2 -elim (cpr_inv_abbr1 … H1) -H1 * -[ #V1 #T1 #HLV1 #HLT1 #H destruct - elim (eq_false_inv_tpair_sn … H2) -H2 - [ #HV1 @IHV // /2 width=1/ -HV1 - @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3 by csn_cpr_trans/ - | -IHV -HLV1 * #H destruct /3 width=1/ - ] -| -IHV -IHT -H2 #T0 #HLT0 #HT0 - lapply (csn_cpr_trans … HT … HLT0) -T #HLT0 - lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/ -] -qed. - -fact csn_appl_beta_aux: ∀a,L,W. L ⊢ ⬊* W → ∀U. L ⊢ ⬊* U → - ∀V,T. U = ⓓ{a}V. T → L ⊢ ⬊* ⓐV. ⓛ{a}W. T. -#a #L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct -lapply (csn_fwd_pair_sn … HVT) #HV -lapply (csn_fwd_bind_dx … HVT) #HT -HVT -@csn_intro #X #H #H2 -elim (cpr_inv_appl1 … H) -H * -[ #V0 #Y #HLV0 #H #H0 destruct - elim (cpr_fwd_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct - elim (eq_false_inv_beta … H2) -H2 - [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0 - @csn_abbr /2 width=3 by csn_cpr_trans/ -HV - @(csn_lpr_conf (L.ⓓV)) /2 width=1/ -V0 /2 width=3 by csn_cpr_trans/ - | -IHW -HLW0 -HV -HT * #H #HVT0 destruct - @(IHVT … HVT0) -IHVT -HVT0 // /3 width=1/ - ] -| -IHW -IHVT -H2 #b #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct - lapply (cpr_lsubr_trans … HLT01 (L.ⓓV) ?) -HLT01 /2 width=1/ #HLT01 - @csn_abbr /2 width=3 by csn_cpr_trans/ -HV - @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3 by csn_cpr_trans/ -| -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct -] -qed-. - -(* Basic_1: was: sn3_beta *) -lemma csn_appl_beta: ∀a,L,W. L ⊢ ⬊* W → ∀V,T. L ⊢ ⬊* ⓓ{a}V. T → - L ⊢ ⬊* ⓐV. ⓛ{a}W. T. -/2 width=3 by csn_appl_beta_aux/ qed. - -fact csn_appl_theta_aux: ∀a,L,U. L ⊢ ⬊* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀V,T. U = ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T. -#a #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct -lapply (csn_fwd_pair_sn … HVT) #HV -lapply (csn_fwd_bind_dx … HVT) -HVT #HVT -@csn_intro #X #HL #H -elim (cpr_inv_appl1 … HL) -HL * -[ -HV #V0 #Y #HLV10 #HL #H0 destruct - elim (cpr_inv_abbr1 … HL) -HL * - [ #V3 #T3 #HV3 #HLT3 #H0 destruct - elim (lift_total V0 0 1) #V4 #HV04 - elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3)) - [ -IHVT #H0 destruct - elim (eq_false_inv_tpair_sn … H) -H - [ -HLV10 -HV3 -HLT3 -HVT - >(lift_inj … HV12 … HV04) -V4 - #H elim H // - | * #_ #H elim H // - ] - | -H -HVT #H - lapply (cpr_lift … HLV10 (L. ⓓV) … HV12 … HV04) -HLV10 -HV12 /2 width=1/ #HV24 - @(IHVT … H … HV04) -IHVT // -H -HV04 /4 width=1/ - ] - | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct - lapply (csn_cpr_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0 - lapply (csn_inv_lift L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY - @(csn_cpr_trans … HVY) /2 width=1/ - ] -| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct -| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct - lapply (cpr_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23 - @csn_abbr /2 width=3 by csn_cpr_trans/ -HV - @(csn_lpr_conf (L. ⓓW0)) /2 width=1/ -W1 - @(csn_cprs_trans … HVT) -HVT /3 width=1/ -] -qed-. - -lemma csn_appl_theta: ∀a,V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀L,V,T. L ⊢ ⬊* ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T. -/2 width=5 by csn_appl_theta_aux/ qed. - -(* Basic_1: was only: sn3_appl_appl *) -lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬊* V → ∀T1. - L ⊢ ⬊* T1 → - (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) → - 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1. -#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 -@csn_intro #X #HL #H -elim (cpr_inv_appl1_simple … HL ?) -HL // -#V0 #T0 #HLV0 #HLT10 #H0 destruct -elim (eq_false_inv_tpair_sn … H) -H -[ -IHT1 #HV0 - @(csn_cpr_trans … (ⓐV0.T1)) /2 width=1/ -HLT10 - @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0 - #T2 #HLT12 #HT12 - @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0 - @H2T1 -H2T1 // -HLT12 /2 width=1/ -| -IHV -H1T1 -HLV0 * #H #H1T10 destruct - elim (tstc_dec T1 T0) #H2T10 - [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1 - #T2 #HLT02 #HT02 - @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/ - | -IHT1 -H3T1 -H1T10 - @H2T1 -H2T1 /2 width=1/ - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma new file mode 100644 index 000000000..7fcc3fa0e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma @@ -0,0 +1,164 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/tstc_tstc.ma". +include "basic_2/computation/cpxs_cpxs.ma". +include "basic_2/computation/csn_alt.ma". +include "basic_2/computation/csn_lift.ma". + +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) + +(* Advanced properties ******************************************************) + +lemma csn_lpx_conf: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → + ∀T. ⦃h, L1⦄ ⊢ ⬊*[g] T → ⦃h, L2⦄ ⊢ ⬊*[g] T. +#h #g #L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT +@csn_intro #T0 #HLT0 #HT0 +@IHT /2 width=2/ -IHT -HT0 /2 width=3 by lpx_cpx_trans/ +qed. + +lemma csn_abst: ∀h,g,a,L,W. ⦃h, L⦄ ⊢ ⬊*[g] W → + ∀T. ⦃h, L.ⓛW⦄ ⊢ ⬊*[g] T → ⦃h, L⦄ ⊢ ⬊*[g] ⓛ{a}W.T. +#h #g #a #L #W #HW @(csn_ind … HW) -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT +@csn_intro #X #H1 #H2 +elim (cpx_inv_abst1 … H1) -H1 +#W0 #T0 #HLW0 #HLT0 #H destruct +elim (eq_false_inv_tpair_sn … H2) -H2 +[ -IHT #H lapply (csn_cpx_trans … HLT0) // -HT + #HT0 lapply (csn_lpx_conf … (L.ⓛW0) … HT0) -HT0 /2 width=1/ /3 width=1/ +| -IHW -HLW0 -HT * #H destruct /3 width=1/ +] +qed. + +lemma csn_abbr: ∀h,g,a,L,V. ⦃h, L⦄ ⊢ ⬊*[g] V → + ∀T. ⦃h, L.ⓓV⦄ ⊢ ⬊*[g] T → ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V. T. +#h #g #a #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT +@csn_intro #X #H1 #H2 +elim (cpx_inv_abbr1 … H1) -H1 * +[ #V1 #T1 #HLV1 #HLT1 #H destruct + elim (eq_false_inv_tpair_sn … H2) -H2 + [ #HV1 @IHV // /2 width=1/ -HV1 + @(csn_lpx_conf … (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3 by csn_cpx_trans/ + | -IHV -HLV1 * #H destruct /3 width=1/ + ] +| -IHV -IHT -H2 #T0 #HLT0 #HT0 + lapply (csn_cpx_trans … HT … HLT0) -T #HLT0 + lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/ +] +qed. + +fact csn_appl_beta_aux: ∀h,g,a,L,U1. ⦃h, L⦄ ⊢ ⬊*[g] U1 → ∀V. ⦃h, L⦄ ⊢ ⬊*[g] V → + ∀W,T1. U1 = ⓛ{a}W.T1 → ( + ∀T2. ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V.T2 + ) → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.ⓛ{a}W.T1. +#h #g #a #L #X1 #H @(csn_ind … H) -X1 +#X1 #HT1 #IHT1 #X2 #H @(csn_ind … H) -X2 +#V #HV #IHV #W #T1 #H1 #IHT2 destruct +@csn_intro #X #H1 #H2 +elim (cpx_inv_appl1 … H1) -H1 * +[ #V0 #Y #HLV0 #H #H0 destruct + elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct + elim (eq_false_inv_tpair_dx … H2) -H2 + [ lapply (csn_cpx_trans … HV … HLV0) -HV #HV0 #HWT0 + @IHT1 -IHT1 [4,5: // |1: skip |2,3: /2 width=1/ ] -HWT0 -HV0 #T2 #HT02 + lapply (lpx_cpxs_trans … HT02 (L.ⓛW) ?) [ /2 width=1/ ] -W0 #HT02 + lapply (cpxs_strap2 … HLT0 … HT02) -T0 #HT12 + lapply (IHT2 … HT12) -T1 #HT2 + @(csn_cpx_trans … HT2) -HT2 /2 width=1/ + | -HV -HT1 -IHT1 -HLW0 -HLT0 * #H #HV0 destruct + @IHV -IHV [1,3: // |2: /2 width=1/ ] -HV0 #T2 #HT02 + lapply (IHT2 … HT02) -IHT2 -HT02 #HT2 + @(csn_cpx_trans … HT2) -HT2 /2 width=1/ + ] +| -HT1 -IHT1 -HV -IHV -H2 #b #V0 #W0 #T0 #T3 #HLV0 #HLT01 #H1 #H2 destruct + lapply (IHT2 T3 ?) [ /2 width=1/ ] -IHT2 -HLT01 #HT3 + @(csn_cpx_trans … HT3) -HT3 /2 width=1/ +| -HT1 -IHT1 -HV -IHV -IHT2 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct +] +qed-. + +(* Basic_1: was just: sn3_beta *) +lemma csn_appl_beta: ∀h,g,a,L,W,T1. ⦃h, L⦄ ⊢ ⬊*[g] ⓛ{a}W.T1 → ∀V. ( + ∀T2. ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V.T2 + ) → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.ⓛ{a}W.T1. +#h #g #a #L #W #T1 #HWT1 #V #IHT2 lapply (IHT2 T1 ?) // +#HVT1 lapply (csn_fwd_pair_sn … HVT1) -HVT1 +/3 width=3 by csn_appl_beta_aux/ qed. + +fact csn_appl_theta_aux: ∀h,g,a,L,U. ⦃h, L⦄ ⊢ ⬊*[g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → + ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV1.ⓓ{a}V.T. +#h #g #a #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct +lapply (csn_fwd_pair_sn … HVT) #HV +lapply (csn_fwd_bind_dx … HVT) -HVT #HVT +@csn_intro #X #HL #H +elim (cpx_inv_appl1 … HL) -HL * +[ -HV #V0 #Y #HLV10 #HL #H0 destruct + elim (cpx_inv_abbr1 … HL) -HL * + [ #V3 #T3 #HV3 #HLT3 #H0 destruct + elim (lift_total V0 0 1) #V4 #HV04 + elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3)) + [ -IHVT #H0 destruct + elim (eq_false_inv_tpair_sn … H) -H + [ -HLV10 -HV3 -HLT3 -HVT + >(lift_inj … HV12 … HV04) -V4 + #H elim H // + | * #_ #H elim H // + ] + | -H -HVT #H + lapply (cpx_lift … HLV10 (L. ⓓV) … HV12 … HV04) -HLV10 -HV12 /2 width=1/ #HV24 + @(IHVT … H … HV04) -IHVT // -H -HV04 /4 width=1/ + ] + | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct + lapply (csn_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0 + lapply (csn_inv_lift … L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY + @(csn_cpx_trans … HVY) /2 width=1/ + ] +| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct +| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct + lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23 + @csn_abbr /2 width=3 by csn_cpx_trans/ -HV + @(csn_lpx_conf … (L. ⓓW0)) /2 width=1/ -W1 + @(csn_cpxs_trans … HVT) -HVT /3 width=1/ +] +qed-. + +lemma csn_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 → + ∀L,V,T. ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V.ⓐV2.T → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV1.ⓓ{a}V.T. +/2 width=5 by csn_appl_theta_aux/ qed. + +(* Basic_1: was just: sn3_appl_appl *) +lemma csn_appl_simple_tstc: ∀h,g,L,V. ⦃h, L⦄ ⊢ ⬊*[g] V → ∀T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 → + (∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → (T1 ≃ T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.T2) → + 𝐒⦃T1⦄ → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.T1. +#h #g #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 +@csn_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 + @(csn_cpx_trans … (ⓐV0.T1)) /2 width=1/ -HLT10 + @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0 + #T2 #HLT12 #HT12 + @(csn_cpx_trans … (ⓐV.T2)) /2 width=1/ -HLV0 + @H2T1 -H2T1 // -HLT12 /2 width=1/ +| -IHV -H1T1 -HLV0 * #H #H1T10 destruct + elim (tstc_dec T1 T0) #H2T10 + [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1 + #T2 #HLT02 #HT02 + @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/ + | -IHT1 -H3T1 -H1T10 + @H2T1 -H2T1 /2 width=1/ + ] +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_aaa.ma deleted file mode 100644 index eb94c05ee..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_aaa.ma +++ /dev/null @@ -1,25 +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/lpx_aaa.ma". -include "basic_2/computation/lprs.ma". - -(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) - -(* Properties about atomic arity assignment on terms ************************) - -lemma aaa_lprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ⁝ A. -#L1 #T #A #HT #L2 #HL12 -@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3 by aaa_lpr_conf/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma index 3a7475d0a..508b306d3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma @@ -23,17 +23,17 @@ definition lprsa: relation lenv ≝ lpx_sn … cprs. interpretation "parallel computation (local environment, sn variant) alternative" 'PRedSnStarAlt L1 L2 = (lprsa L1 L2). -(* Main properties on the alternative definition **********************************) +(* Main properties on the alternative definition ****************************) theorem lprsa_lprs: ∀L1,L2. L1 ⊢ ➡➡* L2 → L1 ⊢ ➡* L2. /2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-. -(* Main inversion lemmas on the alternative definition ****************************) +(* Main inversion lemmas on the alternative definition **********************) theorem lprs_inv_lprsa: ∀L1,L2. L1 ⊢ ➡* L2 → L1 ⊢ ➡➡* L2. /3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpr_cprs_trans/ qed-. -(* Alternative eliminators ********************************************************) +(* Alternative eliminators **************************************************) lemma lprs_ind_alt: ∀R:relation lenv. R (⋆) (⋆) → ( diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma index 7ef78d271..7056fae47 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma @@ -27,5 +27,5 @@ lemma lprs_strip: confluent2 … lprs lpr. theorem lprs_conf: confluent2 … lprs lprs. /3 width=3 by TC_confluent2, lpr_conf/ qed-. -theorem lfprs_trans: Transitive … lprs. +theorem lprs_trans: Transitive … lprs. /2 width=3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma new file mode 100644 index 000000000..2f979ae46 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma @@ -0,0 +1,72 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". +include "basic_2/computation/lprs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) + +definition lpxs: ∀h. sd h → relation lenv ≝ λh,g. TC … (lpx h g). + +interpretation "extended parallel computation (local environment, sn variant)" + 'PRedSnStar h g L1 L2 = (lpxs h g L1 L2). + +(* Basic eliminators ********************************************************) + +lemma lpxs_ind: ∀h,g,L1. ∀R:predicate lenv. R L1 → + (∀L,L2. ⦃h, L1⦄ ⊢ ➡*[g] L → ⦃h, L⦄ ⊢ ➡[g] L2 → R L → R L2) → + ∀L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → R L2. +#h #g #L1 #R #HL1 #IHL1 #L2 #HL12 +@(TC_star_ind … HL1 IHL1 … HL12) // +qed-. + +lemma lpxs_ind_dx: ∀h,g,L2. ∀R:predicate lenv. R L2 → + (∀L1,L. ⦃h, L1⦄ ⊢ ➡[g] L → ⦃h, L⦄ ⊢ ➡*[g] L2 → R L → R L1) → + ∀L1. ⦃h, L1⦄ ⊢ ➡*[g] L2 → R L1. +#h #g #L2 #R #HL2 #IHL2 #L1 #HL12 +@(TC_star_ind_dx … HL2 IHL2 … HL12) // +qed-. + +(* Basic properties *********************************************************) + +lemma lprs_lpxs: ∀h,g,L1,L2. L1 ⊢ ➡* L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2. +/3 width=3/ qed. + +lemma lpx_lpxs: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2. +/2 width=1/ qed. + +lemma lpxs_refl: ∀h,g,L. ⦃h, L⦄ ⊢ ➡*[g] L. +/2 width=1/ qed. + +lemma lpxs_strap1: ∀h,g,L1,L,L2. ⦃h, L1⦄ ⊢ ➡*[g] L → ⦃h, L⦄ ⊢ ➡[g] L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2. +/2 width=3/ qed. + +lemma lpxs_strap2: ∀h,g,L1,L,L2. ⦃h, L1⦄ ⊢ ➡[g] L → ⦃h, L⦄ ⊢ ➡*[g] L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2. +/2 width=3/ qed. + +lemma lpxs_pair_refl: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → ∀I,V. ⦃h, L1. ⓑ{I}V⦄ ⊢ ➡*[g] L2. ⓑ{I}V. +/2 width=1 by TC_lpx_sn_pair_refl/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma lpxs_inv_atom1: ∀h,g,L2. ⦃h, ⋆⦄ ⊢ ➡*[g] L2 → L2 = ⋆. +/2 width=2 by TC_lpx_sn_inv_atom1/ qed-. + +lemma lpxs_inv_atom2: ∀h,g,L1. ⦃h, L1⦄ ⊢ ➡*[g] ⋆ → L1 = ⋆. +/2 width=2 by TC_lpx_sn_inv_atom2/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lpxs_fwd_length: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → |L1| = |L2|. +/2 width=2 by TC_lpx_sn_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma new file mode 100644 index 000000000..b05385da5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.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/reduction/lpx_aaa.ma". +include "basic_2/computation/lpxs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) + +(* Properties about atomic arity assignment on terms ************************) + +lemma aaa_lpxs_conf: ∀h,g,L1,T,A. + L1 ⊢ T ⁝ A → ∀L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → L2 ⊢ T ⁝ A. +#h #g #L1 #T #A #HT #L2 #HL12 +@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_lpx_conf/ +qed-. + +lemma aaa_lprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ⁝ A. +#L1 #T #A #HT #L2 #HL12 +@(aaa_lpxs_conf … HT) -A -T /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma new file mode 100644 index 000000000..e93c88d5c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpxs_cpxs.ma". +include "basic_2/computation/lpxs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) + +(* alternative definition *) +definition lpxsa: ∀h. sd h → relation lenv ≝ λh,g. lpx_sn … (cpxs h g). + +interpretation "extended parallel computation (local environment, sn variant) alternative" + 'PRedSnStarAlt h g L1 L2 = (lpxsa h g L1 L2). + +(* Main properties on the alternative definition ****************************) + +theorem lpxsa_lpxs: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡➡*[g] L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2. +/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-. + +(* Main inversion lemmas on the alternative definition **********************) + +theorem lpxs_inv_lpxsa: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → ⦃h, L1⦄ ⊢ ➡➡*[g] L2. +/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpx_cpxs_trans/ qed-. + +(* Alternative eliminators **************************************************) + +lemma lpxs_ind_alt: ∀h,g. ∀R:relation lenv. + R (⋆) (⋆) → ( + ∀I,K1,K2,V1,V2. + ⦃h, K1⦄ ⊢ ➡*[g] K2 → ⦃h, K1⦄ ⊢ V1 ➡*[g] V2 → + R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + ) → + ∀L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → R L1 L2. +/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma new file mode 100644 index 000000000..960d6778b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma @@ -0,0 +1,91 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpxs_cpxs.ma". +include "basic_2/computation/lpxs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) + +(* Advanced properties ******************************************************) + +lemma lpxs_pair: ∀h,g,I,L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → ∀V1,V2. ⦃h, L1⦄ ⊢ V1 ➡*[g] V2 → + ⦃h, L1.ⓑ{I}V1⦄ ⊢ ➡*[g] L2.ⓑ{I}V2. +/2 width=1 by TC_lpx_sn_pair/ qed. + +(* Advanced inversion lemmas ************************************************) + +lemma lpxs_inv_pair1: ∀h,g,I,K1,L2,V1. ⦃h, K1.ⓑ{I}V1⦄ ⊢ ➡*[g] L2 → + ∃∃K2,V2. ⦃h, K1⦄ ⊢ ➡*[g] K2 & ⦃h, K1⦄ ⊢ V1 ➡*[g] V2 & L2 = K2.ⓑ{I}V2. +/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-. + +lemma lpxs_inv_pair2: ∀h,g,I,L1,K2,V2. ⦃h, L1⦄ ⊢ ➡*[g] K2.ⓑ{I}V2 → + ∃∃K1,V1. ⦃h, K1⦄ ⊢ ➡*[g] K2 & ⦃h, K1⦄ ⊢ V1 ➡*[g] V2 & L1 = K1.ⓑ{I}V1. +/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-. + +(* Properties on context-sensitive extended parallel computation for terms **) + +lemma lpxs_cpx_trans: ∀h,g. s_r_trans … (cpx h g) (lpxs h g). +/3 width=5 by s_r_trans_TC2, lpx_cpxs_trans/ qed-. + +lemma lpxs_cpxs_trans: ∀h,g. s_rs_trans … (cpx h g) (lpxs h g). +/3 width=5 by s_r_trans_TC1, lpxs_cpx_trans/ qed-. + +lemma cpxs_bind2: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 → + ∀I,T1,T2. ⦃h, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[g] T2 → + ∀a. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2. +#h #g #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 +lapply (lpxs_cpxs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/ +qed. + +(* Inversion lemmas on context-sensitive ext parallel computation for terms *) + +lemma cpxs_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1.T1 ➡*[g] U2 → + ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 & ⦃h, L.ⓛV1⦄ ⊢ T1 ➡*[g] T2 & + U2 = ⓛ{a}V2.T2. +#h #g #a #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5/ +#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct +elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct +lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?) /2 width=1/ -HT02 #HT02 +lapply (cpxs_strap1 … HV10 … HV02) -V0 +lapply (cpxs_trans … HT10 … HT02) -T0 /2 width=5/ +qed-. + +lemma cpxs_inv_abbr1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[g] U2 → ( + ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 & ⦃h, L.ⓓV1⦄ ⊢ T1 ➡*[g] T2 & + U2 = ⓓ{a}V2.T2 + ) ∨ + ∃∃T2. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡*[g] T2 & ⇧[0, 1] U2 ≡ T2 & a = true. +#h #g #a #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/ +#U0 #U2 #_ #HU02 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpx_inv_abbr1 … HU02) -HU02 * + [ #V2 #T2 #HV02 #HT02 #H destruct + lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) /2 width=1/ -HT02 #HT02 + lapply (cpxs_strap1 … HV10 … HV02) -V0 + lapply (cpxs_trans … HT10 … HT02) -T0 /3 width=5/ + | #T2 #HT02 #HUT2 + lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02 /2 width=1/ -V0 #HT02 + lapply (cpxs_trans … HT10 … HT02) -T0 /3 width=3/ + ] +| #U1 #HTU1 #HU01 + elim (lift_total U2 0 1) #U #HU2 + lapply (cpx_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0 /2 width=1/ /4 width=3/ +] +qed-. + +(* More advanced properties *************************************************) + +lemma lpxs_pair2: ∀h,g,I,L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → + ∀V1,V2. ⦃h, L2⦄ ⊢ V1 ➡*[g] V2 → ⦃h, L1.ⓑ{I}V1⦄ ⊢ ➡*[g] L2.ⓑ{I}V2. +/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma new file mode 100644 index 000000000..95402030f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.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_ldrop.ma". +include "basic_2/computation/lpxs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) + +(* Properies on local environment slicing ***********************************) + +lemma lpxs_ldrop_conf: ∀h,g. dropable_sn (lpxs h g). +/3 width=3 by dropable_sn_TC, lpx_ldrop_conf/ qed-. + +lemma ldrop_lpxs_trans: ∀h,g. dedropable_sn (lpxs h g). +/3 width=3 by dedropable_sn_TC, ldrop_lpx_trans/ qed-. + +lemma lpxs_ldrop_trans_O1: ∀h,g. dropable_dx (lpxs h g). +/3 width=3 by dropable_dx_TC, lpx_ldrop_trans_O1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma new file mode 100644 index 000000000..d9a152db9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lpxs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) + +(* Main properties **********************************************************) + +theorem lpxs_trans: ∀h,g. Transitive … (lpxs h g). +/2 width=3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma index e2e4eea04..f376f63f0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma @@ -58,7 +58,7 @@ lemma ldrop_lsubc_trans: ∀RR,RS,RP. | #K2 #W2 #A #HV2 #HW2 #HK12 #H1 #H2 destruct elim (IHLK1 … HK12) #K #HL1K #HK2 lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA - lapply (s7 … HA … HV2 … HLK1 HV21) -HV2 + lapply (s8 … HA … HV2 … HLK1 HV21) -HV2 elim (lift_total W2 d e) /4 width=9/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 003b33747..8b80babf9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -47,7 +47,7 @@ f: flat l: abstraction n: native type annotation -NAMING CONVENTIONS FOR TRANSFORMATIONS +NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS - first letter @@ -59,8 +59,11 @@ t: context-free for terms -second letter -p: parallel -s: sequential +i: irreducible form +n: normal form +p: parallel transformation +r: reducible form +s: sequential transformation - third letter @@ -73,6 +76,6 @@ x: extended reduction - forth letter (if present) -p: non-reflexive transitive closure -q: reflexive closure -s: reflexive transitive closure +p: non-reflexive transitive closure (plus) +q: reflexive closure (question) +s: reflexive transitive closure (star) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index a0e62745a..2a0b3c119 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -242,18 +242,30 @@ notation "hvbox( T1 ⊢ ➤ * break term 46 T2 )" (* Reduction ****************************************************************) -notation "hvbox( L ⊢ break 𝐑 ⦃ term 46 T ⦄ )" +notation "hvbox( L ⊢ 𝐑 break ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'Reducible $L $T }. -notation "hvbox( L ⊢ break 𝐈 ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ 𝐑 break [ term 46 g ] break ⦃ term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'Reducible $h $g $L $T }. + +notation "hvbox( L ⊢ 𝐈 break ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'NotReducible $L $T }. -notation "hvbox( L ⊢ break 𝐍 ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ 𝐈 break [ term 46 g ] break ⦃ term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'NotReducible $h $g $L $T }. + +notation "hvbox( L ⊢ 𝐍 break ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'Normal $L $T }. +notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ 𝐍 break [ term 46 g ] break ⦃ term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'Normal $h $g $L $T }. + notation "hvbox( L ⊢ break term 46 T1 ➡ break term 46 T2 )" non associative with precedence 45 for @{ 'PRed $L $T1 $T2 }. @@ -272,33 +284,45 @@ notation "hvbox( ⦃ term 46 h, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 g ] (* Computation **************************************************************) +notation "hvbox( ⦃ term 46 L, break term 46 T ⦄ ϵ break [ term 46 R ] break 〚term 46 A 〛 )" + non associative with precedence 45 + for @{ 'InEInt $R $L $T $A }. + +notation "hvbox( T1 ⊑ break [ term 46 R ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'CrSubEq $T1 $R $T2 }. + notation "hvbox( L ⊢ break term 46 T1 ➡ * break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStar $L $T1 $T2 }. +notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 g ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PRedStar $h $g $L $T1 $T2 }. + notation "hvbox( L1 ⊢ ➡* break term 46 L2 )" non associative with precedence 45 for @{ 'PRedSnStar $L1 $L2 }. -notation "hvbox( L1 ⊢ ➡➡* break term 46 L2 )" +notation "hvbox( ⦃ term 46 h, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 g ] break term 46 L2 )" non associative with precedence 45 - for @{ 'PRedSnStarAlt $L1 $L2 }. + for @{ 'PRedSnStar $h $g $L1 $L2 }. -notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )" +notation "hvbox( L1 ⊢ ➡ ➡ * break term 46 L2 )" non associative with precedence 45 - for @{ 'PEval $L $T1 $T2 }. + for @{ 'PRedSnStarAlt $L1 $L2 }. -notation "hvbox( L ⊢ ⬊ * break term 46 T )" +notation "hvbox( ⦃ term 46 h, break term 46 L1 ⦄ ⊢ ➡ ➡ * break [ term 46 g ] break term 46 L2 )" non associative with precedence 45 - for @{ 'SN $L $T }. + for @{ 'PRedSnStarAlt $h $g $L1 $L2 }. -notation "hvbox( L ⊢ ⬊ ⬊ * break term 46 T )" +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 g ] break term 46 T2 )" non associative with precedence 45 - for @{ 'SNAlt $L $T }. + for @{ 'DecomposedPRedStar $h $g $L $T1 $T2 }. -notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 g ] break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )" non associative with precedence 45 - for @{ 'PRedStar $h $g $L $T1 $T2 }. + for @{ 'PEval $L $T1 $T2 }. notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ ⬊ * break [ term 46 g ] break term 46 T )" non associative with precedence 45 @@ -308,22 +332,6 @@ notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ ⬊ ⬊ * break [ term 4 non associative with precedence 45 for @{ 'SNAlt $h $g $L $T }. -notation "hvbox( ⦃ term 46 L, break term 46 T ⦄ ϵ break [ term 46 R ] break 〚term 46 A 〛 )" - non associative with precedence 45 - for @{ 'InEInt $R $L $T $A }. - -notation "hvbox( T1 ⊑ break [ term 46 R ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'CrSubEq $T1 $R $T2 }. - -notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 g ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'DecomposedXPRedStar $h $g $L $T1 $T2 }. - -notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ • * ⬊ * break [ term 46 g ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'DecomposedXSN $h $g $L $T }. - (* Conversion ***************************************************************) notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )" diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cif.ma deleted file mode 100644 index dea2fedab..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cif.ma +++ /dev/null @@ -1,71 +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/crf.ma". - -(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************) - -definition cif: lenv → predicate term ≝ λL,T. L ⊢ 𝐑⦃T⦄ → ⊥. - -interpretation "context-sensitive irreducibility (term)" - 'NotReducible L T = (cif L T). - -(* Basic inversion lemmas ***************************************************) - -lemma cif_inv_delta: ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → L ⊢ 𝐈⦃#i⦄ → ⊥. -/3 width=3/ qed-. - -lemma cif_inv_ri2: ∀I,L,V,T. ri2 I → L ⊢ 𝐈⦃②{I}V.T⦄ → ⊥. -/3 width=1/ qed-. - -lemma cif_inv_ib2: ∀a,I,L,V,T. ib2 a I → L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ → - L ⊢ 𝐈⦃V⦄ ∧ L.ⓑ{I}V ⊢ 𝐈⦃T⦄. -/4 width=1/ qed-. - -lemma cif_inv_bind: ∀a,I,L,V,T. L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ → - ∧∧ L ⊢ 𝐈⦃V⦄ & L.ⓑ{I}V ⊢ 𝐈⦃T⦄ & ib2 a I. -#a * [ elim a -a ] -[ #L #V #T #H elim (H ?) -H /3 width=1/ -|*: #L #V #T #H elim (cif_inv_ib2 … H) -H /2 width=1/ /3 width=1/ -] -qed-. - -lemma cif_inv_appl: ∀L,V,T. L ⊢ 𝐈⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄. -#L #V #T #HVT @and3_intro /3 width=1/ -generalize in match HVT; -HVT elim T -T // -* // #a * #U #T #_ #_ #H elim (H ?) -H /2 width=1/ -qed-. - -lemma cif_inv_flat: ∀I,L,V,T. L ⊢ 𝐈⦃ⓕ{I}V.T⦄ → - ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl. -* #L #V #T #H -[ elim (cif_inv_appl … H) -H /2 width=1/ -| elim (cif_inv_ri2 … H) -H /2 width=1/ -] -qed-. - -(* Basic properties *********************************************************) - -lemma tif_atom: ∀I. ⋆ ⊢ 𝐈⦃⓪{I}⦄. -/2 width=2 by trf_inv_atom/ qed. - -lemma cif_ib2: ∀a,I,L,V,T. ib2 a I → L ⊢ 𝐈⦃V⦄ → L.ⓑ{I}V ⊢ 𝐈⦃T⦄ → L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄. -#a #I #L #V #T #HI #HV #HT #H -elim (crf_inv_ib2 … HI H) -HI -H /2 width=1/ -qed. - -lemma cif_appl: ∀L,V,T. L ⊢ 𝐈⦃V⦄ → L ⊢ 𝐈⦃T⦄ → 𝐒⦃T⦄ → L ⊢ 𝐈⦃ⓐV.T⦄. -#L #V #T #HV #HT #H1 #H2 -elim (crf_inv_appl … H2) -H2 /2 width=1/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cif_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cif_append.ma deleted file mode 100644 index b5a92cbc3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cif_append.ma +++ /dev/null @@ -1,34 +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/crf_append.ma". -include "basic_2/reduction/cif.ma". - -(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************) - -(* Advanved properties ******************************************************) - -lemma cif_labst_last: ∀L,T,W. L ⊢ 𝐈⦃T⦄ → ⋆.ⓛW @@ L ⊢ 𝐈⦃T⦄. -/3 width=2 by crf_inv_labst_last/ qed. - -lemma cif_tif: ∀T,W. ⋆ ⊢ 𝐈⦃T⦄ → ⋆.ⓛW ⊢ 𝐈⦃T⦄. -/3 width=2 by crf_inv_trf/ qed. - -(* Advanced inversion lemmas ************************************************) - -lemma cif_inv_labst_last: ∀L,T,W. ⋆.ⓛW @@ L ⊢ 𝐈⦃T⦄ → L ⊢ 𝐈⦃T⦄. -/3 width=1/ qed-. - -lemma cif_inv_tif: ∀T,W. ⋆.ⓛW ⊢ 𝐈⦃T⦄ → ⋆ ⊢ 𝐈⦃T⦄. -/3 width=1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma new file mode 100644 index 000000000..49ef68156 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma @@ -0,0 +1,77 @@ +(**************************************************************************) +(* ___ *) +(* ||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/crr.ma". + +(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************) + +definition cir: lenv → predicate term ≝ λL,T. L ⊢ 𝐑⦃T⦄ → ⊥. + +interpretation "context-sensitive irreducibility (term)" + 'NotReducible L T = (cir L T). + +(* Basic inversion lemmas ***************************************************) + +lemma cir_inv_delta: ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → L ⊢ 𝐈⦃#i⦄ → ⊥. +/3 width=3/ qed-. + +lemma cir_inv_ri2: ∀I,L,V,T. ri2 I → L ⊢ 𝐈⦃②{I}V.T⦄ → ⊥. +/3 width=1/ qed-. + +lemma cir_inv_ib2: ∀a,I,L,V,T. ib2 a I → L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ → + L ⊢ 𝐈⦃V⦄ ∧ L.ⓑ{I}V ⊢ 𝐈⦃T⦄. +/4 width=1/ qed-. + +lemma cir_inv_bind: ∀a,I,L,V,T. L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ → + ∧∧ L ⊢ 𝐈⦃V⦄ & L.ⓑ{I}V ⊢ 𝐈⦃T⦄ & ib2 a I. +#a * [ elim a -a ] +[ #L #V #T #H elim H -H /3 width=1/ +|*: #L #V #T #H elim (cir_inv_ib2 … H) -H /2 width=1/ /3 width=1/ +] +qed-. + +lemma cir_inv_appl: ∀L,V,T. L ⊢ 𝐈⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄. +#L #V #T #HVT @and3_intro /3 width=1/ +generalize in match HVT; -HVT elim T -T // +* // #a * #U #T #_ #_ #H elim H -H /2 width=1/ +qed-. + +lemma cir_inv_flat: ∀I,L,V,T. L ⊢ 𝐈⦃ⓕ{I}V.T⦄ → + ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl. +* #L #V #T #H +[ elim (cir_inv_appl … H) -H /2 width=1/ +| elim (cir_inv_ri2 … H) -H /2 width=1/ +] +qed-. + +(* Basic properties *********************************************************) + +lemma cir_sort: ∀L,k. L ⊢ 𝐈⦃⋆k⦄. +/2 width=3 by crr_inv_sort/ qed. + +lemma cir_gref: ∀L,p. L ⊢ 𝐈⦃§p⦄. +/2 width=3 by crr_inv_gref/ qed. + +lemma tir_atom: ∀I. ⋆ ⊢ 𝐈⦃⓪{I}⦄. +/2 width=2 by trr_inv_atom/ qed. + +lemma cir_ib2: ∀a,I,L,V,T. ib2 a I → L ⊢ 𝐈⦃V⦄ → L.ⓑ{I}V ⊢ 𝐈⦃T⦄ → L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄. +#a #I #L #V #T #HI #HV #HT #H +elim (crr_inv_ib2 … HI H) -HI -H /2 width=1/ +qed. + +lemma cir_appl: ∀L,V,T. L ⊢ 𝐈⦃V⦄ → L ⊢ 𝐈⦃T⦄ → 𝐒⦃T⦄ → L ⊢ 𝐈⦃ⓐV.T⦄. +#L #V #T #HV #HT #H1 #H2 +elim (crr_inv_appl … H2) -H2 /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma new file mode 100644 index 000000000..fb88321ef --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/crr_append.ma". +include "basic_2/reduction/cir.ma". + +(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************) + +(* Advanved properties ******************************************************) + +lemma cir_labst_last: ∀L,T,W. L ⊢ 𝐈⦃T⦄ → ⋆.ⓛW @@ L ⊢ 𝐈⦃T⦄. +/3 width=2 by crr_inv_labst_last/ qed. + +lemma cir_tif: ∀T,W. ⋆ ⊢ 𝐈⦃T⦄ → ⋆.ⓛW ⊢ 𝐈⦃T⦄. +/3 width=2 by crr_inv_trr/ qed. + +(* Advanced inversion lemmas ************************************************) + +lemma cir_inv_append_sn: ∀L,K,T. K @@ L ⊢ 𝐈⦃T⦄ → L ⊢ 𝐈⦃T⦄. +/3 width=1/ qed-. + +lemma cir_inv_tir: ∀T,W. ⋆.ⓛW ⊢ 𝐈⦃T⦄ → ⋆ ⊢ 𝐈⦃T⦄. +/3 width=1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma new file mode 100644 index 000000000..9539a6c03 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/crr_lift.ma". +include "basic_2/reduction/cir.ma". + +(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************) + +(* Properties on relocation *************************************************) + +lemma cir_lift: ∀K,T. K ⊢ 𝐈⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K → + ∀U. ⇧[d, e] T ≡ U → L ⊢ 𝐈⦃U⦄. +/3 width=7 by crr_inv_lift/ qed. + +lemma cir_inv_lift: ∀L,U. L ⊢ 𝐈⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K → + ∀T. ⇧[d, e] T ≡ U → K ⊢ 𝐈⦃T⦄. +/3 width=7/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma new file mode 100644 index 000000000..fb49b0de7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma @@ -0,0 +1,92 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cir.ma". +include "basic_2/reduction/crx.ma". + +(* CONTEXT-SENSITIVE EXTENDED IRREDUCIBLE TERMS *****************************) + +definition cix: ∀h. sd h → lenv → predicate term ≝ λh,g,L,T. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → ⊥. + +interpretation "context-sensitive extended irreducibility (term)" + 'NotReducible h g L T = (cix h g L T). + +(* Basic inversion lemmas ***************************************************) + +lemma cix_inv_sort: ∀h,g,L,k,l. deg h g k (l+1) → ⦃h, L⦄ ⊢ 𝐈[g]⦃⋆k⦄ → ⊥. +/3 width=2/ qed-. + +lemma cix_inv_delta: ∀h,g,I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃h, L⦄ ⊢ 𝐈[g]⦃#i⦄ → ⊥. +/3 width=4/ qed-. + +lemma cix_inv_ri2: ∀h,g,I,L,V,T. ri2 I → ⦃h, L⦄ ⊢ 𝐈[g]⦃②{I}V.T⦄ → ⊥. +/3 width=1/ qed-. + +lemma cix_inv_ib2: ∀h,g,a,I,L,V,T. ib2 a I → ⦃h, L⦄ ⊢ 𝐈[g]⦃ⓑ{a,I}V.T⦄ → + ⦃h, L⦄ ⊢ 𝐈[g]⦃V⦄ ∧ ⦃h, L.ⓑ{I}V⦄ ⊢ 𝐈[g]⦃T⦄. +/4 width=1/ qed-. + +lemma cix_inv_bind: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃ⓑ{a,I}V.T⦄ → + ∧∧ ⦃h, L⦄ ⊢ 𝐈[g]⦃V⦄ & ⦃h, L.ⓑ{I}V⦄ ⊢ 𝐈[g]⦃T⦄ & ib2 a I. +#h #g #a * [ elim a -a ] +[ #L #V #T #H elim H -H /3 width=1/ +|*: #L #V #T #H elim (cix_inv_ib2 … H) -H /2 width=1/ /3 width=1/ +] +qed-. + +lemma cix_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃ⓐV.T⦄ → + ∧∧ ⦃h, L⦄ ⊢ 𝐈[g]⦃V⦄ & ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄ & 𝐒⦃T⦄. +#h #g #L #V #T #HVT @and3_intro /3 width=1/ +generalize in match HVT; -HVT elim T -T // +* // #a * #U #T #_ #_ #H elim H -H /2 width=1/ +qed-. + +lemma cix_inv_flat: ∀h,g,I,L,V,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃ⓕ{I}V.T⦄ → + ∧∧ ⦃h, L⦄ ⊢ 𝐈[g]⦃V⦄ & ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄ & 𝐒⦃T⦄ & I = Appl. +#h #g * #L #V #T #H +[ elim (cix_inv_appl … H) -H /2 width=1/ +| elim (cix_inv_ri2 … H) -H /2 width=1/ +] +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma cix_inv_cir: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄ → L ⊢ 𝐈⦃T⦄. +/3 width=1/ qed-. + +(* Basic properties *********************************************************) + +lemma cix_sort: ∀h,g,L,k. deg h g k 0 → ⦃h, L⦄ ⊢ 𝐈[g]⦃⋆k⦄. +#h #g #L #k #Hk #H elim (crx_inv_sort … H) -L #l #Hkl +lapply (deg_mono … Hk Hkl) -h -k (cpr_inv_sort1 … H) // -qed. - -(* Basic_1: was: nf2_abst *) -lemma cnf_abst: ∀a,I,L,V,W,T. L ⊢ 𝐍⦃W⦄ → L. ⓑ{I} V ⊢ 𝐍⦃T⦄ → L ⊢ 𝐍⦃ⓛ{a}W.T⦄. -#a #I #L #V #W #T #HW #HT #X #H -elim (cpr_fwd_abst1 … H I V) -H #W0 #T0 #HW0 #HT0 #H destruct ->(HW … HW0) -W0 >(HT … HT0) -T0 // -qed. - -(* Basic_1: was only: nf2_appl_lref *) -lemma cnf_appl_simple: ∀L,V,T. L ⊢ 𝐍⦃V⦄ → L ⊢ 𝐍⦃T⦄ → 𝐒⦃T⦄ → L ⊢ 𝐍⦃ⓐV.T⦄. -#L #V #T #HV #HT #HS #X #H -elim (cpr_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct ->(HV … HV0) -V0 >(HT … HT0) -T0 // -qed. - -(* Basic_1: was: nf2_dec *) -axiom cnf_dec: ∀L,T1. L ⊢ 𝐍⦃T1⦄ ∨ - ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → ⊥). - -(* Basic_1: removed theorems 1: nf2_abst_shift *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_cif.ma deleted file mode 100644 index e87cdb962..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_cif.ma +++ /dev/null @@ -1,28 +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/cpr_cif.ma". -include "basic_2/reduction/cnf_crf.ma". - -(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) - -(* Main properties on context-sensitive irreducible terms *******************) - -theorem cif_cnf: ∀L,T. L ⊢ 𝐈⦃T⦄ → L ⊢ 𝐍⦃T⦄. -/2 width=3 by cpr_fwd_cif/ qed. - -(* Main inversion lemmas on context-sensitive irreducible terms *************) - -theorem cnf_inv_cif: ∀L,T. L ⊢ 𝐍⦃T⦄ → L ⊢ 𝐈⦃T⦄. -/2 width=4 by cnf_inv_crf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_crf.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_crf.ma deleted file mode 100644 index 0afff1ab0..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_crf.ma +++ /dev/null @@ -1,46 +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/crf.ma". -include "basic_2/reduction/cnf.ma". - -(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) - -(* Advanced inversion lemmas on context-sensitive reducible terms ***********) - -(* Note: this property is unusual *) -lemma cnf_inv_crf: ∀L,T. L ⊢ 𝐑⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ⊥. -#L #T #H elim H -L -T -[ #L #K #V #i #HLK #H - elim (cnf_inv_delta … HLK H) -| #L #V #T #_ #IHV #H - elim (cnf_inv_appl … H) -H /2 width=1/ -| #L #V #T #_ #IHT #H - elim (cnf_inv_appl … H) -H /2 width=1/ -| #I #L #V #T * #H1 #H2 destruct - [ elim (cnf_inv_zeta … H2) - | elim (cnf_inv_tau … H2) - ] -|5,6: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct - [1,3: elim (cnf_inv_abbr … H2) -H2 /2 width=1/ - |*: elim (cnf_inv_abst … H2) -H2 /2 width=1/ - ] -| #a #L #V #W #T #H - elim (cnf_inv_appl … H) -H #_ #_ #H - elim (simple_inv_bind … H) -| #a #L #V #W #T #H - elim (cnf_inv_appl … H) -H #_ #_ #H - elim (simple_inv_bind … H) -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_lift.ma deleted file mode 100644 index acbb020ce..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_lift.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/reduction/cpr_lift.ma". -include "basic_2/reduction/cnf.ma". - -(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) - -(* Advanced properties ******************************************************) - -(* Basic_1: was only: nf2_csort_lref *) -lemma cnf_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → L ⊢ 𝐍⦃#i⦄. -#L #i #HL #X #H -elim (cpr_inv_lref1 … H) -H // * -#K #V1 #V2 #HLK #_ #_ -lapply (ldrop_mono … HL … HLK) -L #H destruct -qed. - -(* Basic_1: was: nf2_lref_abst *) -lemma cnf_lref_abst: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → L ⊢ 𝐍⦃#i⦄. -#L #K #V #i #HLK #X #H -elim (cpr_inv_lref1 … H) -H // * -#K0 #V1 #V2 #HLK0 #_ #_ -lapply (ldrop_mono … HLK … HLK0) -L #H destruct -qed. - -(* Relocation properties ****************************************************) - -(* Basic_1: was: nf2_lift *) -lemma cnf_lift: ∀L0,L,T,T0,d,e. - L ⊢ 𝐍⦃T⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍⦃T0⦄. -#L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H -elim (cpr_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1 -<(HLT … HT1) in HT0; -L #HT0 ->(lift_mono … HT10 … HT0) -T1 -X // -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma new file mode 100644 index 000000000..7bd1ad6d1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma @@ -0,0 +1,101 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpr.ma". + +(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) + +definition cnr: lenv → predicate term ≝ λL. NF … (cpr L) (eq …). + +interpretation + "context-sensitive normality (term)" + 'Normal L T = (cnr L T). + +(* Basic inversion lemmas ***************************************************) + +lemma cnr_inv_delta: ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → L ⊢ 𝐍⦃#i⦄ → ⊥. +#L #K #V #i #HLK #H +elim (lift_total V 0 (i+1)) #W #HVW +lapply (H W ?) -H [ /3 width=6/ ] -HLK #H destruct +elim (lift_inv_lref2_be … HVW) -HVW // +qed-. + +lemma cnr_inv_abst: ∀a,L,V,T. L ⊢ 𝐍⦃ⓛ{a}V.T⦄ → L ⊢ 𝐍⦃V⦄ ∧ L.ⓛV ⊢ 𝐍⦃T⦄. +#a #L #V1 #T1 #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct // +] +qed-. + +lemma cnr_inv_abbr: ∀L,V,T. L ⊢ 𝐍⦃-ⓓV.T⦄ → L ⊢ 𝐍⦃V⦄ ∧ L.ⓓV ⊢ 𝐍⦃T⦄. +#L #V1 #T1 #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct // +] +qed-. + +lemma cnr_inv_zeta: ∀L,V,T. L ⊢ 𝐍⦃+ⓓV.T⦄ → ⊥. +#L #V #T #H elim (is_lift_dec T 0 1) +[ * #U #HTU + lapply (H U ?) -H /2 width=3/ #H destruct + elim (lift_inv_pair_xy_y … HTU) +| #HT + elim (cpss_delift (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12 + lapply (H (+ⓓV.T2) ?) -H /4 width=1/ -HT2 #H destruct /3 width=2/ +] +qed-. + +lemma cnr_inv_appl: ∀L,V,T. L ⊢ 𝐍⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐍⦃V⦄ & L ⊢ 𝐍⦃T⦄ & 𝐒⦃T⦄. +#L #V1 #T1 #HVT1 @and3_intro +[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct // +| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H + [ elim (lift_total V1 0 1) #V2 #HV12 + lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct + | lapply (H (ⓓ{a}V1.U1) ?) -H /3 width=1/ #H destruct +] +qed-. + +lemma cnr_inv_tau: ∀L,V,T. L ⊢ 𝐍⦃ⓝV.T⦄ → ⊥. +#L #V #T #H lapply (H T ?) -H /2 width=1/ #H +@discr_tpair_xy_y // +qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was: nf2_sort *) +lemma cnr_sort: ∀L,k. L ⊢ 𝐍⦃⋆k⦄. +#L #k #X #H +>(cpr_inv_sort1 … H) // +qed. + +(* Basic_1: was: nf2_abst *) +lemma cnr_abst: ∀a,I,L,V,W,T. L ⊢ 𝐍⦃W⦄ → L. ⓑ{I} V ⊢ 𝐍⦃T⦄ → L ⊢ 𝐍⦃ⓛ{a}W.T⦄. +#a #I #L #V #W #T #HW #HT #X #H +elim (cpr_fwd_abst1 … H I V) -H #W0 #T0 #HW0 #HT0 #H destruct +>(HW … HW0) -W0 >(HT … HT0) -T0 // +qed. + +(* Basic_1: was only: nf2_appl_lref *) +lemma cnr_appl_simple: ∀L,V,T. L ⊢ 𝐍⦃V⦄ → L ⊢ 𝐍⦃T⦄ → 𝐒⦃T⦄ → L ⊢ 𝐍⦃ⓐV.T⦄. +#L #V #T #HV #HT #HS #X #H +elim (cpr_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct +>(HV … HV0) -V0 >(HT … HT0) -T0 // +qed. + +(* Basic_1: was: nf2_dec *) +axiom cnr_dec: ∀L,T1. L ⊢ 𝐍⦃T1⦄ ∨ + ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → ⊥). + +(* Basic_1: removed theorems 1: nf2_abst_shift *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma new file mode 100644 index 000000000..50f30ab60 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpr_cir.ma". +include "basic_2/reduction/cnr_crr.ma". + +(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) + +(* Main properties on context-sensitive irreducible terms *******************) + +theorem cir_cnr: ∀L,T. L ⊢ 𝐈⦃T⦄ → L ⊢ 𝐍⦃T⦄. +/2 width=3 by cpr_fwd_cir/ qed. + +(* Main inversion lemmas on context-sensitive irreducible terms *************) + +theorem cnr_inv_cir: ∀L,T. L ⊢ 𝐍⦃T⦄ → L ⊢ 𝐈⦃T⦄. +/2 width=4 by cnr_inv_crr/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma new file mode 100644 index 000000000..6d68cf9e0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/crr.ma". +include "basic_2/reduction/cnr.ma". + +(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) + +(* Advanced inversion lemmas on context-sensitive reducible terms ***********) + +(* Note: this property is unusual *) +lemma cnr_inv_crr: ∀L,T. L ⊢ 𝐑⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ⊥. +#L #T #H elim H -L -T +[ #L #K #V #i #HLK #H + elim (cnr_inv_delta … HLK H) +| #L #V #T #_ #IHV #H + elim (cnr_inv_appl … H) -H /2 width=1/ +| #L #V #T #_ #IHT #H + elim (cnr_inv_appl … H) -H /2 width=1/ +| #I #L #V #T * #H1 #H2 destruct + [ elim (cnr_inv_zeta … H2) + | elim (cnr_inv_tau … H2) + ] +|5,6: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct + [1,3: elim (cnr_inv_abbr … H2) -H2 /2 width=1/ + |*: elim (cnr_inv_abst … H2) -H2 /2 width=1/ + ] +| #a #L #V #W #T #H + elim (cnr_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +| #a #L #V #W #T #H + elim (cnr_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma new file mode 100644 index 000000000..5e3c2c419 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpr_lift.ma". +include "basic_2/reduction/cnr.ma". + +(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) + +(* Advanced properties ******************************************************) + +(* Basic_1: was only: nf2_csort_lref *) +lemma cnr_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → L ⊢ 𝐍⦃#i⦄. +#L #i #HL #X #H +elim (cpr_inv_lref1 … H) -H // * +#K #V1 #V2 #HLK #_ #_ +lapply (ldrop_mono … HL … HLK) -L #H destruct +qed. + +(* Basic_1: was: nf2_lref_abst *) +lemma cnr_lref_abst: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → L ⊢ 𝐍⦃#i⦄. +#L #K #V #i #HLK #X #H +elim (cpr_inv_lref1 … H) -H // * +#K0 #V1 #V2 #HLK0 #_ #_ +lapply (ldrop_mono … HLK … HLK0) -L #H destruct +qed. + +(* Relocation properties ****************************************************) + +(* Basic_1: was: nf2_lift *) +lemma cnr_lift: ∀L0,L,T,T0,d,e. + L ⊢ 𝐍⦃T⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍⦃T0⦄. +#L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H +elim (cpr_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1 +<(HLT … HT1) in HT0; -L #HT0 +>(lift_mono … HT10 … HT0) -T1 -X // +qed. + +(* Note: this was missing in basic_1 *) +lemma cnr_inv_lift: ∀L0,L,T,T0,d,e. + L0 ⊢ 𝐍⦃T0⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L ⊢ 𝐍⦃T⦄. +#L0 #L #T #T0 #d #e #HLT0 #HL0 #HT0 #X #H +elim (lift_total X d e) #X0 #HX0 +lapply (cpr_lift … H … HL0 … HT0 … HX0) -L #HTX0 +>(HLT0 … HTX0) in HX0; -L0 -X0 #H +>(lift_inj … H … HT0) -T0 -X -d -e // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma new file mode 100644 index 000000000..ecc67cb4f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma @@ -0,0 +1,121 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/reduction/cnr.ma". +include "basic_2/reduction/cpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************) + +definition cnx: ∀h. sd h → lenv → predicate term ≝ + λh,g,L. NF … (cpx h g L) (eq …). + +interpretation + "context-sensitive extended normality (term)" + 'Normal h g L T = (cnx h g L T). + +(* Basic inversion lemmas ***************************************************) + +lemma cnx_inv_sort: ∀h,g,L,k. ⦃h, L⦄ ⊢ 𝐍[g]⦃⋆k⦄ → deg h g k 0. +#h #g #L #k #H elim (deg_total h g k) +#l @(nat_ind_plus … l) -l // #l #_ #Hkl +lapply (H (⋆(next h k)) ?) -H /2 width=2/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *) +lapply (next_lt h k) >e1 -e1 #H elim (lt_refl_false … H) +qed-. + +lemma cnx_inv_delta: ∀h,g,I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃h, L⦄ ⊢ 𝐍[g]⦃#i⦄ → ⊥. +#h #g #I #L #K #V #i #HLK #H +elim (lift_total V 0 (i+1)) #W #HVW +lapply (H W ?) -H [ /3 width=7/ ] -HLK #H destruct +elim (lift_inv_lref2_be … HVW) -HVW // +qed-. + +lemma cnx_inv_abst: ∀h,g,a,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓛ{a}V.T⦄ → + ⦃h, L⦄ ⊢ 𝐍[g]⦃V⦄ ∧ ⦃h, L.ⓛV⦄ ⊢ 𝐍[g]⦃T⦄. +#h #g #a #L #V1 #T1 #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct // +] +qed-. + +lemma cnx_inv_abbr: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃-ⓓV.T⦄ → + ⦃h, L⦄ ⊢ 𝐍[g]⦃V⦄ ∧ ⦃h, L.ⓓV⦄ ⊢ 𝐍[g]⦃T⦄. +#h #g #L #V1 #T1 #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct // +] +qed-. + +lemma cnx_inv_zeta: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃+ⓓV.T⦄ → ⊥. +#h #g #L #V #T #H elim (is_lift_dec T 0 1) +[ * #U #HTU + lapply (H U ?) -H /2 width=3/ #H destruct + elim (lift_inv_pair_xy_y … HTU) +| #HT + elim (cpss_delift (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12 + lapply (H (+ⓓV.T2) ?) -H /5 width=1/ -HT2 #H destruct /3 width=2/ +] +qed-. + +lemma cnx_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓐV.T⦄ → + ∧∧ ⦃h, L⦄ ⊢ 𝐍[g]⦃V⦄ & ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ & 𝐒⦃T⦄. +#h #g #L #V1 #T1 #HVT1 @and3_intro +[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct // +| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H + [ elim (lift_total V1 0 1) #V2 #HV12 + lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct + | lapply (H (ⓓ{a}V1.U1) ?) -H /3 width=1/ #H destruct +] +qed-. + +lemma cnx_inv_tau: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓝV.T⦄ → ⊥. +#h #g #L #V #T #H lapply (H T ?) -H /2 width=1/ #H +@discr_tpair_xy_y // +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma cnx_fwd_cnr: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → L ⊢ 𝐍⦃T⦄. +#h #g #L #T #H #U #HTU +@H /2 width=1/ (**) (* auto fails because a δ-expansion gets in the way *) +qed-. + +(* Basic properties *********************************************************) + +lemma cnx_sort: ∀h,g,L,k. deg h g k 0 → ⦃h, L⦄ ⊢ 𝐍[g]⦃⋆k⦄. +#h #g #L #k #Hk #X #H elim (cpx_inv_sort1 … H) -H // * #l #Hkl #_ +lapply (deg_mono … Hkl Hk) -h -L (HW … HW0) -W0 >(HT … HT0) -T0 // +qed. + +lemma cnx_appl_simple: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃V⦄ → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → 𝐒⦃T⦄ → + ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓐV.T⦄. +#h #g #L #V #T #HV #HT #HS #X #H +elim (cpx_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct +>(HV … HV0) -V0 >(HT … HT0) -T0 // +qed. + +axiom cnx_dec: ∀h,g,L,T1. ⦃h, L⦄ ⊢ 𝐍[g]⦃T1⦄ ∨ + ∃∃T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 & (T1 = T2 → ⊥). diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma new file mode 100644 index 000000000..05f1acedb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpx_cix.ma". +include "basic_2/reduction/cnx_crx.ma". + +(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************) + +(* Main properties on context-sensitive extended irreducible terms **********) + +theorem cix_cnr: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄ → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄. +/2 width=5 by cpx_fwd_cix/ qed. + +(* Main inversion lemmas on context-sensitive extended irreducible terms ****) + +theorem cnr_inv_cix: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄. +/2 width=6 by cnx_inv_crx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma new file mode 100644 index 000000000..99ca32c13 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||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/crx.ma". +include "basic_2/reduction/cnx.ma". + +(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************) + +(* Advanced inversion lemmas on context-sensitive reducible terms ***********) + +(* Note: this property is unusual *) +lemma cnx_inv_crx: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ⊥. +#h #g #L #T #H elim H -L -T +[ #L #k #l #Hkl #H + lapply (cnx_inv_sort … H) -H #H + lapply (deg_mono … H Hkl) -h -L -k (lift_mono … HT10 … HT0) -T1 -X // +qed. + +lemma cnx_inv_lift: ∀h,g,L0,L,T,T0,d,e. ⦃h, L0⦄ ⊢ 𝐍[g]⦃T0⦄ → ⇩[d, e] L0 ≡ L → + ⇧[d, e] T ≡ T0 → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄. +#h #g #L0 #L #T #T0 #d #e #HLT0 #HL0 #HT0 #X #H +elim (lift_total X d e) #X0 #HX0 +lapply (cpx_lift … H … HL0 … HT0 … HX0) -L #HTX0 +>(HLT0 … HTX0) in HX0; -L0 -X0 #H +>(lift_inj … H … HT0) -T0 -X -d -e // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cif.ma deleted file mode 100644 index 2366a0865..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cif.ma +++ /dev/null @@ -1,52 +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/cif.ma". -include "basic_2/reduction/cpr.ma". - -(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) - -(* Advanced forward lemmas on context-sensitive irreducible terms ***********) - -lemma cpr_fwd_cif: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ 𝐈⦃T1⦄ → T2 = T1. -#L #T1 #T2 #H elim H -L -T1 -T2 -[ // -| #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H - elim (cif_inv_delta … HLK ?) // -| #a * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H - [ elim (cif_inv_bind … H) -H #HV1 #HT1 * #H destruct - lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct - lapply (IHT1 … HT1) -IHT1 #H destruct // - | elim (cif_inv_ib2 … H) -H /2 width=1/ /3 width=2/ - ] -| * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H - [ elim (cif_inv_appl … H) -H #HV1 #HT1 #_ - >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // - | elim (cif_inv_ri2 … H) /2 width=1/ - ] -| #L #V1 #T1 #T #T2 #_ #_ #_ #H - elim (cif_inv_ri2 … H) /2 width=1/ -| #L #V1 #T1 #T2 #_ #_ #H - elim (cif_inv_ri2 … H) /2 width=1/ -| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H - elim (cif_inv_appl … H) -H #_ #_ #H - elim (simple_inv_bind … H) -| #a #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H - elim (cif_inv_appl … H) -H #_ #_ #H - elim (simple_inv_bind … H) -] -qed-. - -lemma cpss_fwd_cif_eq: ∀L,T1,T2. L ⊢ T1 ▶* T2 → L ⊢ 𝐈⦃T1⦄ → T2 = T1. -/3 width=3 by cpr_fwd_cif, cpss_cpr/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma new file mode 100644 index 000000000..0a9b0a6db --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cir.ma". +include "basic_2/reduction/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) + +(* Advanced forward lemmas on context-sensitive irreducible terms ***********) + +lemma cpr_fwd_cir: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ 𝐈⦃T1⦄ → T2 = T1. +#L #T1 #T2 #H elim H -L -T1 -T2 +[ // +| #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H + elim (cir_inv_delta … HLK) // +| #a * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H + [ elim (cir_inv_bind … H) -H #HV1 #HT1 * #H destruct + lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct + lapply (IHT1 … HT1) -IHT1 #H destruct // + | elim (cir_inv_ib2 … H) -H /2 width=1/ /3 width=2/ + ] +| * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H + [ elim (cir_inv_appl … H) -H #HV1 #HT1 #_ + >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // + | elim (cir_inv_ri2 … H) /2 width=1/ + ] +| #L #V1 #T1 #T #T2 #_ #_ #_ #H + elim (cir_inv_ri2 … H) /2 width=1/ +| #L #V1 #T1 #T2 #_ #_ #H + elim (cir_inv_ri2 … H) /2 width=1/ +| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H + elim (cir_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +| #a #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H + elim (cir_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +] +qed-. + +lemma cpss_fwd_cir_eq: ∀L,T1,T2. L ⊢ T1 ▶* T2 → L ⊢ 𝐈⦃T1⦄ → T2 = T1. +/3 width=3 by cpr_fwd_cir, cpss_cpr/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma new file mode 100644 index 000000000..b7a0406cb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cix.ma". +include "basic_2/reduction/cpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +(* Advanced forward lemmas on context-sensitive extended irreducible terms **) + +lemma cpx_fwd_cix: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ⦃h, L⦄ ⊢ 𝐈[g]⦃T1⦄ → T2 = T1. +#h #g #L #T1 #T2 #H elim H -L -T1 -T2 +[ // +| #L #k #l #Hkl #H elim (cix_inv_sort … Hkl H) +| #I #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H + elim (cix_inv_delta … HLK) // +| #a * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H + [ elim (cix_inv_bind … H) -H #HV1 #HT1 * #H destruct + lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct + lapply (IHT1 … HT1) -IHT1 #H destruct // + | elim (cix_inv_ib2 … H) -H /2 width=1/ /3 width=2/ + ] +| * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H + [ elim (cix_inv_appl … H) -H #HV1 #HT1 #_ + >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // + | elim (cix_inv_ri2 … H) /2 width=1/ + ] +| #L #V1 #T1 #T #T2 #_ #_ #_ #H + elim (cix_inv_ri2 … H) /2 width=1/ +| #L #V1 #T1 #T2 #_ #_ #H + elim (cix_inv_ri2 … H) /2 width=1/ +| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H + elim (cix_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +| #a #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H + elim (cix_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +] +qed-. + diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crf.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crf.ma deleted file mode 100644 index af60a2b0d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crf.ma +++ /dev/null @@ -1,116 +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/relocation/ldrop.ma". - -(* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************) - -(* reducible binary items *) -definition ri2: predicate item2 ≝ - λI. I = Bind2 true Abbr ∨ I = Flat2 Cast. - -(* irreducible binary binders *) -definition ib2: relation2 bool bind2 ≝ - λa,I. I = Abst ∨ Bind2 a I = Bind2 false Abbr. - -(* reducible terms *) -inductive crf: lenv → predicate term ≝ -| crf_delta : ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → crf L (#i) -| crf_appl_sn: ∀L,V,T. crf L V → crf L (ⓐV. T) -| crf_appl_dx: ∀L,V,T. crf L T → crf L (ⓐV. T) -| crf_ri2 : ∀I,L,V,T. ri2 I → crf L (②{I}V. T) -| crf_ib2_sn : ∀a,I,L,V,T. ib2 a I → crf L V → crf L (ⓑ{a,I}V. T) -| crf_ib2_dx : ∀a,I,L,V,T. ib2 a I → crf (L.ⓑ{I}V) T → crf L (ⓑ{a,I}V. T) -| crf_beta : ∀a,L,V,W,T. crf L (ⓐV. ⓛ{a}W. T) -| crf_theta : ∀a,L,V,W,T. crf L (ⓐV. ⓓ{a}W. T) -. - -interpretation - "context-sensitive reducibility (term)" - 'Reducible L T = (crf L T). - -(* Basic inversion lemmas ***************************************************) - -fact trf_inv_atom_aux: ∀I,L,T. L ⊢ 𝐑⦃T⦄ → L = ⋆ → T = ⓪{I} → ⊥. -#I #L #T * -L -T -[ #L #K #V #i #HLK #H1 #H2 destruct - elim (ldrop_inv_atom1 … HLK) -HLK #H destruct -| #L #V #T #_ #_ #H destruct -| #L #V #T #_ #_ #H destruct -| #J #L #V #T #_ #_ #H destruct -| #a #J #L #V #T #_ #_ #_ #H destruct -| #a #J #L #V #T #_ #_ #_ #H destruct -| #a #L #V #W #T #_ #H destruct -| #a #L #V #W #T #_ #H destruct -] -qed-. - -lemma trf_inv_atom: ∀I. ⋆ ⊢ 𝐑⦃⓪{I}⦄ → ⊥. -/2 width=6 by trf_inv_atom_aux/ qed-. - -fact crf_inv_lref_aux: ∀L,T. L ⊢ 𝐑⦃T⦄ → ∀i. T = #i → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV. -#L #T * -L -T -[ #L #K #V #j #HLK #i #H destruct /2 width=3/ -| #L #V #T #_ #i #H destruct -| #L #V #T #_ #i #H destruct -| #J #L #V #T #_ #i #H destruct -| #a #J #L #V #T #_ #_ #i #H destruct -| #a #J #L #V #T #_ #_ #i #H destruct -| #a #L #V #W #T #i #H destruct -| #a #L #V #W #T #i #H destruct -] -qed-. - -lemma crf_inv_lref: ∀L,i. L ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV. -/2 width=3 by crf_inv_lref_aux/ qed-. - -fact crf_inv_ib2_aux: ∀a,I,L,W,U,T. ib2 a I → L ⊢ 𝐑⦃T⦄ → T = ⓑ{a,I}W. U → - L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃U⦄. -#a #I #L #W #U #T #HI * -T -[ #L #K #V #i #_ #H destruct -| #L #V #T #_ #H destruct -| #L #V #T #_ #H destruct -| #J #L #V #T #H1 #H2 destruct - elim H1 -H1 #H destruct - elim HI -HI #H destruct -| #b #J #L #V #T #_ #HV #H destruct /2 width=1/ -| #b #J #L #V #T #_ #HT #H destruct /2 width=1/ -| #b #L #V #W #T #H destruct -| #b #L #V #W #T #H destruct -] -qed-. - -lemma crf_inv_ib2: ∀a,I,L,W,T. ib2 a I → L ⊢ 𝐑⦃ⓑ{a,I}W.T⦄ → - L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃T⦄. -/2 width=5 by crf_inv_ib2_aux/ qed-. - -fact crf_inv_appl_aux: ∀L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓐW. U → - ∨∨ L ⊢ 𝐑⦃W⦄ | L ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥). -#L #W #U #T * -T -[ #L #K #V #i #_ #H destruct -| #L #V #T #HV #H destruct /2 width=1/ -| #L #V #T #HT #H destruct /2 width=1/ -| #J #L #V #T #H1 #H2 destruct - elim H1 -H1 #H destruct -| #a #I #L #V #T #_ #_ #H destruct -| #a #I #L #V #T #_ #_ #H destruct -| #a #L #V #W0 #T #H destruct - @or3_intro2 #H elim (simple_inv_bind … H) -| #a #L #V #W0 #T #H destruct - @or3_intro2 #H elim (simple_inv_bind … H) -] -qed-. - -lemma crf_inv_appl: ∀L,V,T. L ⊢ 𝐑⦃ⓐV.T⦄ → ∨∨ L ⊢ 𝐑⦃V⦄ | L ⊢ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥). -/2 width=3 by crf_inv_appl_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crf_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crf_append.ma deleted file mode 100644 index 0a86278d0..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crf_append.ma +++ /dev/null @@ -1,56 +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/relocation/ldrop_append.ma". -include "basic_2/reduction/crf.ma". - -(* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************) - -(* Advanved properties ******************************************************) - -lemma crf_labst_last: ∀L,T,W. L ⊢ 𝐑⦃T⦄ → ⋆.ⓛW @@ L ⊢ 𝐑⦃T⦄. -#L #T #W #H elim H -L -T /2 width=1/ -#L #K #V #i #HLK -lapply (ldrop_fwd_length_lt2 … HLK) #Hi -lapply (ldrop_O1_append_sn_le … HLK … (⋆.ⓛW)) -HLK /2 width=2/ -Hi /2 width=3/ -qed. - -lemma crf_trf: ∀T,W. ⋆ ⊢ 𝐑⦃T⦄ → ⋆.ⓛW ⊢ 𝐑⦃T⦄. -#T #W #H lapply (crf_labst_last … W H) // -qed. - -(* Advanced inversion lemmas ************************************************) - -fact crf_inv_labst_last_aux: ∀L1,T,W. L1 ⊢ 𝐑⦃T⦄ → - ∀L2. L1 = ⋆.ⓛW @@ L2 → L2 ⊢ 𝐑⦃T⦄. -#L1 #T #W #H elim H -L1 -T /2 width=1/ /3 width=1/ -[ #L1 #K1 #V1 #i #HLK1 #L2 #H destruct - lapply (ldrop_fwd_length_lt2 … HLK1) - >append_length >commutative_plus normalize in ⊢ (??% → ?); #H - elim (le_to_or_lt_eq i (|L2|) ?) /2 width=1/ -H #Hi destruct - [ elim (ldrop_O1_lt … Hi) #I2 #K2 #V2 #HLK2 - lapply (ldrop_O1_inv_append1_le … HLK1 … HLK2) -HLK1 /2 width=2/ -Hi - normalize #H destruct /2 width=3/ - | lapply (ldrop_O1_inv_append1_ge … HLK1 ?) -HLK1 // append_length >commutative_plus normalize in ⊢ (??% → ?); #H + elim (le_to_or_lt_eq i (|L2|) ?) /2 width=1/ -H #Hi destruct + [ elim (ldrop_O1_lt … Hi) #I2 #K2 #V2 #HLK2 + lapply (ldrop_O1_inv_append1_le … HLK1 … HLK2) -HLK1 /2 width=2/ -Hi + normalize #H destruct /2 width=3/ + | lapply (ldrop_O1_inv_append1_ge … HLK1 ?) -HLK1 // (lift_inv_sort1 … H) -X /2 width=2/ +| #I #K #K0 #V #i #HK0 #L #d #e #HLK #X #H + elim (lift_inv_lref1 … H) -H * #Hid #H destruct + [ elim (ldrop_trans_lt … HLK … HK0) -K // /2 width=4/ + | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // /2 width=4/ + ] +| #K #V #T #_ #IHV #L #d #e #HLK #X #H + elim (lift_inv_flat1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/ +| #K #V #T #_ #IHT #L #d #e #HLK #X #H + elim (lift_inv_flat1 … H) -H #W #U #_ #HTU #H destruct /3 width=4/ +| #I #K #V #T #HI #L #d #e #_ #X #H + elim (lift_fwd_pair1 … H) -H #W #U #_ #H destruct /2 width=1/ +| #a #I #K #V #T #HI #_ #IHV #L #d #e #HLK #X #H + elim (lift_inv_bind1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/ +| #a #I #K #V #T #HI #_ #IHT #L #d #e #HLK #X #H + elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=4/ +| #a #K #V #V0 #T #L #d #e #_ #X #H + elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct + elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/ +| #a #K #V #V0 #T #L #d #e #_ #X #H + elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct + elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/ +] +qed. + +lemma crx_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊢ 𝐑[g]⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K → + ∀T. ⇧[d, e] T ≡ U → ⦃h, K⦄ ⊢ 𝐑[g]⦃T⦄. +#h #g #L #U #H elim H -L -U +[ #L #k #l #Hkl #K #d #e #_ #X #H + >(lift_inv_sort2 … H) -X /2 width=2/ +| #I #L #L0 #W #i #HK0 #K #d #e #HLK #X #H + elim (lift_inv_lref2 … H) -H * #Hid #H destruct + [ elim (ldrop_conf_lt … HLK … HK0) -L // /2 width=4/ + | lapply (ldrop_conf_ge … HLK … HK0 ?) -L // /2 width=4/ + ] +| #L #W #U #_ #IHW #K #d #e #HLK #X #H + elim (lift_inv_flat2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/ +| #L #W #U #_ #IHU #K #d #e #HLK #X #H + elim (lift_inv_flat2 … H) -H #V #T #_ #HTU #H destruct /3 width=4/ +| #I #L #W #U #HI #K #d #e #_ #X #H + elim (lift_fwd_pair2 … H) -H #V #T #_ #H destruct /2 width=1/ +| #a #I #L #W #U #HI #_ #IHW #K #d #e #HLK #X #H + elim (lift_inv_bind2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/ +| #a #I #L #W #U #HI #_ #IHU #K #d #e #HLK #X #H + elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/ +| #a #L #W #W0 #U #K #d #e #_ #X #H + elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct + elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/ +| #a #L #W #W0 #U #K #d #e #_ #X #H + elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct + elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma index 3863f7bb5..56eebf47c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma @@ -16,7 +16,7 @@ include "basic_2/static/aaa_lift.ma". include "basic_2/static/lsuba_aaa.ma". include "basic_2/reduction/lpx_ldrop.ma". -(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) +(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) (* Properties on atomic arity assignment for terms **************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma index 5a7ac853f..386884296 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma @@ -135,6 +135,8 @@ qed. axiom ldrop_div: ∀e1,L1,L. ⇩[0, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L2 ≡ L → ∃∃L0. ⇩[0, e1] L0 ≡ L2 & ⇩[e1, e2] L0 ≡ L1. +(* Advanced properties ******************************************************) + (* Basic_1: was: drop_conf_lt *) lemma ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 → ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. ⓑ{I} V2 → @@ -146,6 +148,17 @@ elim (ldrop_conf_le … H1 … H2) -L [2: /2 width=2/] #K #HL1K #HK2 elim (ldrop_inv_skip1 … HK2) -HK2 [2: /2 width=1/] #K1 #V1 #HK21 #HV12 #H destruct /2 width=5/ qed. +(* Note: apparently this was missing in basic_1 *) +lemma ldrop_trans_lt: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L → + ∀e2,L2,I,V2. ⇩[0, e2] L ≡ L2.ⓑ{I}V2 → + e2 < d1 → let d ≝ d1 - e2 - 1 in + ∃∃L0,V0. ⇩[0, e2] L1 ≡ L0.ⓑ{I}V0 & + ⇩[d, e1] L0 ≡ L2 & ⇧[d, e1] V2 ≡ V0. +#d1 #e1 #L1 #L #HL1 #e2 #L2 #I #V2 #HL2 #Hd21 +elim (ldrop_trans_le … HL1 … HL2) -L [2: /2 width=1/ ] #L0 #HL10 #HL02 +elim (ldrop_inv_skip2 … HL02) -HL02 [2: /2 width=1/ ] #L #V1 #HL2 #HV21 #H destruct /2 width=5/ +qed-. + lemma ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L. ⇩[d1, e1] L1 ≡ L → ⇩[0, e2] L ≡ L2 → d1 ≤ e2 → ⇩[0, e2 + e1] L1 ≡ L2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma index da4dd9c5a..e72288dff 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma @@ -268,6 +268,22 @@ qed-. (* Basic forward lemmas *****************************************************) +lemma lift_fwd_pair1: ∀I,T2,V1,U1,d,e. ⇧[d,e] ②{I}V1.U1 ≡ T2 → + ∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & T2 = ②{I}V2.U2. +* [ #a ] #I #T2 #V1 #U1 #d #e #H +[ elim (lift_inv_bind1 … H) -H /2 width=4/ +| elim (lift_inv_flat1 … H) -H /2 width=4/ +] +qed-. + +lemma lift_fwd_pair2: ∀I,T1,V2,U2,d,e. ⇧[d,e] T1 ≡ ②{I}V2.U2 → + ∃∃V1,U1. ⇧[d,e] V1 ≡ V2 & T1 = ②{I}V1.U1. +* [ #a ] #I #T1 #V2 #U2 #d #e #H +[ elim (lift_inv_bind2 … H) -H /2 width=4/ +| elim (lift_inv_flat2 … H) -H /2 width=4/ +] +qed-. + lemma lift_fwd_tw: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}. #d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma index 79d9f0740..35500d952 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma @@ -92,6 +92,11 @@ let rec sd_l (h:sh) (k:nat) (l:nat) on l : sd h ≝ (* Basic properties *********************************************************) +lemma deg_iter: ∀h,g,k,l1,l2. deg h g k l1 → deg h g ((next h)^l2 k) (l1-l2). +#h #g #k #l1 #l2 @(nat_ind_plus … l2) -l2 [ iter_SO iter_SO +lapply (nexts_le h k l) #H +@(le_to_lt_to_lt … H) // +qed. + axiom nexts_dec: ∀h,k1,k2. Decidable (∃l. (next h)^l k1 = k2). axiom nexts_inj: ∀h,k,l1,l2. (next h)^l1 k = (next h)^l2 k → l1 = l2. 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 714792343..2754de2a0 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 @@ -83,22 +83,23 @@ table { [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_lpss" + "dxprs_aaa" + "dxprs_dxprs" * ] } ] - [ { "context-sensitive extended computation" * } { - [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?] ? )" "cpxs_lift" * ] - } - ] [ { "weakly normalizing computation" * } { [ "cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpe_cpe" * ] } ] [ { "strongly normalizing computation" * } { [ "csn_vector ( ? ⊢ ⬊* ? )" "csn_tstc_vector" + "csn_aaa" * ] - [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_lpr" * ] + [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_lpx" * ] + } + ] + [ { "context-sensitive extended computation" * } { + [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?] ? )" "lpxs_ldrop" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_aaa" + "cpxs_cpxs" * ] } ] [ { "context-sensitive computation" * } { - [ "lprs ( ? ⊢ ➡* ? )" "lprs_alt ( ? ⊢ ➡➡* ? )" "lprs_ldrop" + "lprs_lpss" + "lprs_aaa" + "lprs_cprs" + "lprs_lprs" * ] - [ "cprs ( ? ⊢ ? ➡* ?)" "cprs_tstc" + "cprs_tstc_vector" + "cprs_lift" + "cprs_lpss" + "cprs_aaa" + "cprs_cprs" * ] + [ "lprs ( ? ⊢ ➡* ? )" "lprs_alt ( ? ⊢ ➡➡* ? )" "lprs_ldrop" + "lprs_lpss" + "lprs_cprs" + "lprs_lprs" * ] + [ "cprs ( ? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_lpss" + "cprs_cprs" * ] } ] [ { "local env. ref. for abstract candidates of reducibility" * } { @@ -113,22 +114,38 @@ table { ] class "water" [ { "reduction" * } { + [ { "context-sensitive extended normal forms" * } { + [ "cnx ( ⦃?,?⦄ ⊢ 𝐍[?]⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ] + } + ] [ { "context-sensitive extended reduction" * } { [ "lpx ( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpx_ldrop" + "lpx_aaa" * ] - [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpx_lift" * ] + [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpx_lift" + "cpx_cix" * ] + } + ] + [ { "context-sensitive extended irreducible forms" * } { + [ "cix ( ⦃?,?⦄ ⊢ 𝐈[?]⦃?⦄ )" "cix_append" + "cix_lift" * ] + } + ] + [ { "context-sensitive extended reducible forms" * } { + [ "crx ( ⦃?,?⦄ ⊢ 𝐑[?]⦃?⦄ )" "crx_append" + "crx_lift" * ] } ] [ { "context-sensitive normal forms" * } { - [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_liftt" + "cnf_crf" + "cnf_cif" * ] + [ "cnr ( ? ⊢ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ] } ] [ { "context-sensitive reduction" * } { [ "lpr ( ? ⊢ ➡ ? )" "lpr_ldrop" + "lpr_lpss" + "lpr_lpr" * ] - [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cif" * ] + [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cir" * ] + } + ] + [ { "context-sensitive irreducible forms" * } { + [ "cir ( ? ⊢ 𝐈⦃?⦄ )" "cir_append" + "cir_lift" * ] } ] [ { "context-sensitive reducible forms" * } { - [ "crf ( ? ⊢ 𝐑⦃?⦄ )" "crf_append" "cif ( ? ⊢ 𝐈⦃?⦄ )" "cif_append" * ] + [ "crr ( ? ⊢ 𝐑⦃?⦄ )" "crr_append" + "crr_lift" * ] } ] } @@ -224,7 +241,7 @@ table { ] class "red" [ { "grammar" * } { - [ { "pointwise extension of a relation" * } { + [ { "pointwise extension of a relation" * } { [ "lpx_sn" "lpx_sn_tc" + "lpx_sn_lpx_sn" * ] } ] diff --git a/matita/matita/contribs/lambdadelta/ground_2/star.ma b/matita/matita/contribs/lambdadelta/ground_2/star.ma index 1358f8da2..671881857 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/star.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/star.ma @@ -117,6 +117,10 @@ qed. definition NF: ∀A. relation A → relation A → predicate A ≝ λA,R,S,a1. ∀a2. R a1 a2 → S a2 a1. +definition NF_dec: ∀A. relation A → relation A → Prop ≝ + λA,R,S. ∀a1. NF A R S a1 ∨ + ∃∃a2. R … a1 a2 & (S a2 a1 → ⊥). + inductive SN (A) (R,S:relation A): predicate A ≝ | SN_intro: ∀a1. (∀a2. R a1 a2 → (S a2 a1 → ⊥) → SN A R S a2) → SN A R S a1 . @@ -127,6 +131,14 @@ lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a. elim HSa12 -HSa12 /2 width=1/ qed. +lemma SN_to_NF: ∀A,R,S. NF_dec A R S → + ∀a1. SN A R S a1 → + ∃∃a2. star … R a1 a2 & NF A R S a2. +#A #R #S #HRS #a1 #H elim H -a1 +#a1 #_ #IHa1 elim (HRS a1) -HRS /2 width=3/ +* #a0 #Ha10 #Ha01 elim (IHa1 … Ha10 Ha01) -IHa1 -Ha01 /3 width=3/ +qed-. + definition NF_sn: ∀A. relation A → relation A → predicate A ≝ λA,R,S,a2. ∀a1. R a1 a2 → S a2 a1.