From: Ferruccio Guidi Date: Sun, 10 Aug 2014 18:41:31 +0000 (+0000) Subject: some renaming and a minor addition X-Git-Tag: make_still_working~857 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fca909e9e53de73771e1b47e94434ae8f747d7fb;p=helm.git some renaming and a minor addition --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma deleted file mode 100644 index 6bcbfe4c7..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma +++ /dev/null @@ -1,54 +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/genv.ma". -include "basic_2/multiple/drops.ma". - -(* ABSTRACT COMPUTATION PROPERTIES ******************************************) - -definition candidate: Type[0] ≝ relation3 genv lenv term. - -definition CP0 ≝ λRR:relation4 genv lenv term term. λRS:relation term. - ∀G,L0,L,T,T0,s,d,e. NF … (RR G L) RS T → - ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR G L0) RS T0. - -definition CP0s ≝ λRR:relation4 genv lenv term term. λRS:relation term. - ∀G,L0,L,s,des. ⇩*[s, des] L0 ≡ L → - ∀T,T0. ⇧*[des] T ≡ T0 → - NF … (RR G L) RS T → NF … (RR G L0) RS T0. - -definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term. - ∀G,L. ∃k. NF … (RR G L) RS (⋆k). - -definition CP2 ≝ λRP:candidate. - ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T. - -(* requirements for abstract computation properties *) -record acp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝ -{ cp0: CP0 RR RS; - cp1: CP1 RR RS; - cp2: CP2 RP -}. - -(* Basic properties *********************************************************) - -(* Basic_1: was: nf2_lift1 *) -lemma acp_lifts: ∀RR,RS. CP0 RR RS → CP0s RR RS. -#RR #RS #HRR #G #L1 #L2 #s #des #H elim H -L1 -L2 -des -[ #L #T1 #T2 #H #HT1 - <(lifts_inv_nil … H) -H // -| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2 - elim (lifts_inv_cons … H) -H /3 width=10 by/ -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma deleted file mode 100644 index be5351c2b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ /dev/null @@ -1,93 +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/multiple/lifts_lifts.ma". -include "basic_2/multiple/drops_drops.ma". -include "basic_2/static/aaa_lifts.ma". -include "basic_2/static/aaa_aaa.ma". -include "basic_2/computation/lsubc_drops.ma". - -(* ABSTRACT COMPUTATION PROPERTIES ******************************************) - -(* Main properties **********************************************************) - -(* Basic_1: was: sc3_arity_csubc *) -theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. - acp RR RS RP → acr RR RS RP RP → - ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[Ⓕ, des] L0 ≡ L1 → - ∀T0. ⇧*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 → - ⦃G, L2, T0⦄ ϵ[RP] 〚A〛. -#RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A -[ #G #L #k #L0 #des #HL0 #X #H #L2 #HL20 - >(lifts_inv_sort1 … H) -H - lapply (aacr_acr … H1RP H2RP (⓪)) #HAtom - @(s4 … HAtom … (◊)) // -| #I #G #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 - lapply (drop_fwd_drop2 … HLK1) #HK1b - elim (drops_drop_trans … HL01 … HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hdes1 - >(at_mono … Hi1 … Hi0) -i1 - elim (drops_inv_skip2 … Hdes1 … H) -des1 #K0 #V0 #des0 #Hdes0 #HK01 #HV10 #H destruct - elim (lsubc_drop_O1_trans … HL20 … HL0) -HL0 #X #HLK2 #H - elim (lsubc_inv_pair2 … H) -H * - [ #K2 #HK20 #H destruct - 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 by drops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *) - | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0 - #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct - lapply (drop_fwd_drop2 … HLK2) #HLK2b - lapply (aaa_lifts … HK01 … HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B - lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B - elim (lift_total V0 0 (i0 +1)) #V3 #HV03 - elim (lift_total V2 0 (i0 +1)) #V #HV2 - @(s5 … HB … (◊) … (ⓝV3.V) … HLK2) [2: /2 width=1 by lift_flat/ ] - @(s7 … HB … (◊)) [ @(s0 … HB … HKV2A) // | @(s0 … HB … H1KV0A) // ] - ] -| #a #G #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 - @(s6 … HA … (◊) (◊)) /3 width=5 by lsubc_pair, drops_skip, liftv_nil/ -| #a #G #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) [ /2 width=5 by/ ] - #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B - elim (drops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20 - lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B - @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA - /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/ -| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 - elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct - /3 width=10 by drops_nil, lifts_nil/ -| #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20 - elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct - lapply (aacr_acr … H1RP H2RP A) #HA - @(s7 … HA … (◊)) /2 width=5 by/ -] -qed. - -(* Basic_1: was: sc3_arity *) -lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP → - ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛. -/2 width=8 by drops_nil, lifts_nil, aacr_aaa_csubc_lifts/ qed. - -lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP → - ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T. -#RR #RS #RP #H1RP #H2RP #G #L #T #A #HT -lapply (aacr_acr … H1RP H2RP A) #HA -@(s1 … HA) /2 width=4 by aacr_aaa/ -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 deleted file mode 100644 index 1537d175c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ /dev/null @@ -1,193 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/ineint_5.ma". -include "basic_2/grammar/aarity.ma". -include "basic_2/multiple/gr2_gr2.ma". -include "basic_2/multiple/lifts_lift_vector.ma". -include "basic_2/multiple/drops_drop.ma". -include "basic_2/computation/acp.ma". - -(* ABSTRACT COMPUTATION PROPERTIES ******************************************) - -definition S0 ≝ λC:candidate. ∀G,L2,L1,T1,d,e. - C G L1 T1 → ∀T2. ⇩[Ⓕ, d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2. - -definition S0s ≝ λC:candidate. - ∀G,L1,L2,des. ⇩*[Ⓕ, des] L2 ≡ L1 → - ∀T1,T2. ⇧*[des] T1 ≡ T2 → C G L1 T1 → C G L2 T2. - -(* Note: this is Girard's CR1 *) -definition S1 ≝ λRP,C:candidate. - ∀G,L,T. C G L T → RP G L T. - -(* Note: this is Tait's iii, or Girard's CR4 *) -definition S2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. λRP,C:candidate. - ∀G,L,Vs. all … (RP G L) Vs → - ∀T. 𝐒⦃T⦄ → NF … (RR G L) RS T → C G L (ⒶVs.T). - -(* Note: this generalizes Tait's ii *) -definition S3 ≝ λC:candidate. - ∀a,G,L,Vs,V,T,W. - C G L (ⒶVs.ⓓ{a}ⓝW.V.T) → C G L (ⒶVs.ⓐV.ⓛ{a}W.T). - -definition S4 ≝ λRP,C:candidate. - ∀G,L,Vs. all … (RP G L) Vs → ∀k. C G L (ⒶVs.⋆k). - -definition S5 ≝ λC:candidate. ∀I,G,L,K,Vs,V1,V2,i. - C G L (ⒶVs.V2) → ⇧[0, i+1] V1 ≡ V2 → - ⇩[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i). - -definition S6 ≝ λRP,C:candidate. - ∀G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → - ∀a,V,T. C G (L.ⓓV) (ⒶV2s.T) → RP G L V → C G L (ⒶV1s.ⓓ{a}V.T). - -definition S7 ≝ λC:candidate. - ∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T). - -(* properties of the abstract candidate of reducibility *) -record acr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate) : Prop ≝ -{ s0: S0 C; - s1: S1 RP C; - s2: S2 RR RS RP C; - s3: S3 C; - s4: S4 RP C; - s5: S5 C; - s6: S6 RP C; - s7: S7 C -}. - -(* the functional construction for candidates *) -definition cfun: candidate → candidate → candidate ≝ - λC1,C2,G,K,T. ∀L,V,U,des. - ⇩*[Ⓕ, des] L ≡ K → ⇧*[des] T ≡ U → C1 G L V → C2 G L (ⓐV.U). - -(* the candidate associated to an atomic arity *) -let rec aacr (RP:candidate) (A:aarity) on A: candidate ≝ -match A with -[ AAtom ⇒ RP -| APair B A ⇒ cfun (aacr RP B) (aacr RP A) -]. - -interpretation - "candidate of reducibility of an atomic arity (abstract)" - 'InEInt RP G L T A = (aacr RP A G L T). - -(* Basic properties *********************************************************) - -(* Basic_1: was: sc3_lift1 *) -lemma acr_lifts: ∀C. S0 C → S0s C. -#C #HC #G #L1 #L2 #des #H elim H -L1 -L2 -des -[ #L #T1 #T2 #H #HT1 <(lifts_inv_nil … H) -H // -| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2 - elim (lifts_inv_cons … H) -H /3 width=10 by/ -] -qed. - -lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP RP → - ∀des,G,L0,L,V,V0. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] V ≡ V0 → - RP G L V → RP G L0 V0. -#RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV -@acr_lifts /width=7 by/ -@(s0 … HRP) -qed. - -(* Basic_1: was only: sns3_lifts1 *) -lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP RP → - ∀des,G,L0,L,Vs,V0s. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] Vs ≡ V0s → - all … (RP G L) Vs → all … (RP G L0) V0s. -#RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #HL0 #H elim H -Vs -V0s normalize // -#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s * /3 width=7 by rp_lifts, conj/ -qed. - -(* Basic_1: was: - sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift -*) -lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP → - ∀A. acr RR RS RP (aacr RP A). -#RR #RS #RP #H1RP #H2RP #A elim A -A normalize // -#B #A #IHB #IHA @mk_acr normalize -[ /3 width=7 by drops_cons, lifts_cons/ -| #G #L #T #H - elim (cp1 … H1RP G L) #k #HK - lapply (H ? (⋆k) ? (⟠) ? ? ?) -H - [3,5: // |2,4: skip - | @(s2 … IHB … (◊)) // - | #H @(cp2 … H1RP … k) @(s1 … IHA) // - ] -| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HL0 #H #HB - elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct - lapply (s1 … IHB … HB) #HV0 - @(s2 … IHA … (V0 @ V0s)) - /3 width=14 by rp_liftsv_all, acp_lifts, cp0, lifts_simple_dx, conj/ -| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HL0 #H #HB - elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct - 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)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/ -| #G #L #Vs #HVs #k #L0 #V0 #X #des #HL0 #H #HB - 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=7 by rp_liftsv_all, conj/ -| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HL0 #H #HB - elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct - elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct - elim (drops_drop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0 - >(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02 - elim (drops_inv_skip2 … Hdes0 … H) -H -des0 #L2 #W1 #des0 #Hdes0 #HLK #HVW1 #H destruct - 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 - @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_applv/ -| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HL0 #H #HB - 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 - @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/ - @(HA … (des + 1)) /2 width=2 by drops_skip/ - [ @lifts_applv // - elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s - >(liftv_mono … HV12s … HV10s) -V1s // - | @(s0 … IHB … HB … HV120) /2 width=2 by drop_drop/ - ] -| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HL0 #H #HB - elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct - elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct - @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_applv/ -] -qed. - -lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP → - ∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → ( - ∀L0,V0,W0,T0,des. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] W ≡ W0 → ⇧*[des + 1] T ≡ T0 → - ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛 - ) → - ⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛. -#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HL0 #H #HB -lapply (aacr_acr … H1RP H2RP A) #HCA -lapply (aacr_acr … H1RP H2RP B) #HCB -elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct -lapply (acr_lifts … HL0 … HW0 HW) -HW [ @(s0 … HCB) ] #HW0 -@(s3 … HCA … (◊)) -@(s6 … HCA … (◊) (◊)) // -[ @(HA … HL0) // -| lapply (s1 … HCB) -HCB #HCB - @(s7 … H2RP … (◊)) /2 width=1 by/ -] -qed. - -(* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *) -(* Basic_1: removed local theorems 1: sc3_sn3_abst *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma deleted file mode 100644 index c3125bedb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma +++ /dev/null @@ -1,107 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/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,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≂ U. -#h #g #G #L #T #HT #U #H ->(cpxs_inv_cnx1 … H HT) -G -L -T // -qed-. - -lemma cpxs_fwd_sort: ∀h,g,G,L,U,k. ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] U → - ⋆k ≂ U ∨ ⦃G, L⦄ ⊢ ⋆(next h k) ➡*[h, g] U. -#h #g #G #L #U #k #H -elim (cpxs_inv_sort1 … H) -H #n #l generalize in match k; -k @(nat_ind_plus … n) -n -[ #k #_ #H -l destruct /2 width=1 by or_introl/ -| #n #IHn #k >plus_plus_comm_23 #Hnl #H destruct - lapply (deg_next_SO … Hnl) -Hnl #Hnl - elim (IHn … Hnl) -IHn - [ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/ - | generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n - /4 width=3 by cpxs_strap2, cpx_st, or_intror/ - | >iter_SO >iter_n_Sm // - ] -] -qed-. - -(* Basic_1: was just: pr3_iso_beta *) -lemma cpxs_fwd_beta: ∀h,g,a,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{a}W.T ➡*[h, g] U → - ⓐV.ⓛ{a}W.T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V.T ➡*[h, g] U. -#h #g #a #G #L #V #W #T #U #H -elim (cpxs_inv_appl1 … H) -H * -[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ -| #b #W0 #T0 #HT0 #HU - elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct - lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 - /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/ -| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_ - elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct -] -qed-. - -(* Note: probably this is an inversion lemma *) -lemma cpxs_fwd_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → - ∀V2. ⇧[0, i + 1] V1 ≡ V2 → - ∀U. ⦃G, L⦄ ⊢ #i ➡*[h, g] U → - #i ≂ U ∨ ⦃G, L⦄ ⊢ V2 ➡*[h, g] U. -#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H -elim (cpxs_inv_lref1 … H) -H /2 width=1 by or_introl/ -* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0 -lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct -/4 width=10 by cpxs_lift, drop_fwd_drop2, or_intror/ -qed-. - -lemma cpxs_fwd_theta: ∀h,g,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[h, g] U → - ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≂ U ∨ - ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[h, g] U. -#h #g #a #G #L #V1 #V #T #U #H #V2 #HV12 -elim (cpxs_inv_appl1 … H) -H * -[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ -| #b #W #T0 #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 by cpxs_flat_dx, cpxs_bind_dx/ ] -T - @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ] - /4 width=7 by cpx_zeta, lift_bind, lift_flat/ - ] -| #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 - /3 width=2 by cpxs_flat, cpxs_bind, drop_drop/ - | #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=2 by drop_drop/ #HV24 - @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T - @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V5 -T5 - @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/ - ] -] -qed-. - -lemma cpxs_fwd_cast: ∀h,g,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ➡*[h, g] U → - ∨∨ ⓝW. T ≂ U | ⦃G, L⦄ ⊢ T ➡*[h, g] U | ⦃G, L⦄ ⊢ W ➡*[h, g] U. -#h #g #G #L #W #T #U #H -elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ * -#W0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or3_intro0/ -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 deleted file mode 100644 index becbd624d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma +++ /dev/null @@ -1,190 +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/substitution/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,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → - ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U → ⒶVs.T ≂ U. -#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *) -#V #Vs #IHVs #U #H -elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair/ -| #a #W0 #T0 #HT0 #HU - lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (tstc_inv_bind_applv_simple … HT0) // -| #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU - lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (tstc_inv_bind_applv_simple … HT0) // -] -qed-. - -lemma cpxs_fwd_sort_vector: ∀h,g,G,L,k,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆k ➡*[h, g] U → - ⒶVs.⋆k ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.⋆(next h k) ➡*[h, g] U. -#h #g #G #L #k #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/ -#V #Vs #IHVs #U #H -elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ -| #a #W1 #T1 #HT1 #HU - elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_applv_simple … HT1) // - | @or_intror (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV.ⓛ{a}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ - ] -| #a #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU - elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_applv_simple … HT1) // - | @or_intror (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV1.ⓓ{a}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ - ] -] -qed-. - - -(* Basic_1: was just: pr3_iso_appls_beta *) -lemma cpxs_fwd_beta_vector: ∀h,g,a,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[h, g] U → - ⒶVs. ⓐV. ⓛ{a}W. T ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{a}ⓝW.V.T ➡*[h, g] U. -#h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/ -#V0 #Vs #IHVs #V #W #T #U #H -elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ -| #b #W1 #T1 #HT1 #HU - elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_applv_simple … HT1) // - | @or_intror (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓛ{b}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ - ] -| #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU - elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_applv_simple … HT1) // - | @or_intror (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ - ] -] -qed-. - -lemma cpxs_fwd_delta_vector: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → - ∀V2. ⇧[0, i + 1] V1 ≡ V2 → - ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.#i ➡*[h, g] U → - ⒶVs.#i ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.V2 ➡*[h, g] U. -#h #g #I #G #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 by tstc_pair, or_introl/ -| #b #W0 #T0 #HT0 #HU - elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_applv_simple … HT0) // - | @or_intror -i (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ - ] -| #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU - elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_applv_simple … HT0) // - | @or_intror -i (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ - ] -] -qed-. - -(* Basic_1: was just: pr3_iso_appls_abbr *) -lemma cpxs_fwd_theta_vector: ∀h,g,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → - ∀a,V,T,U. ⦃G, L⦄ ⊢ ⒶV1s.ⓓ{a}V.T ➡*[h, g] U → - ⒶV1s. ⓓ{a}V. T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}V.ⒶV2s.T ➡*[h, g] U. -#h #g #G #L #V1s #V2s * -V1s -V2s /3 width=1 by or_intror/ -#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 by tstc_pair, or_introl/ -| #b #W0 #T0 #HT0 #HU - elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0 - [ -HV12a -HV12b -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 #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 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2s - @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0)) - /4 width=7 by cpxs_beta_dx, cpx_zeta, lift_bind, lift_flat/ - ] - ] -| #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 by drop_drop/ ] #HV2a - @(cpxs_trans … (ⓓ{a}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/ - | #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 by drop_drop/ ] #HV2a - @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2s - @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V1 -T1 - @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/ - ] - ] -] -qed-. - -(* Basic_1: was just: pr3_iso_appls_cast *) -lemma cpxs_fwd_cast_vector: ∀h,g,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[h, g] U → - ∨∨ ⒶVs. ⓝW. T ≂ U - | ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U - | ⦃G, L⦄ ⊢ ⒶVs.W ➡*[h, g] U. -#h #g #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/ -#V #Vs #IHVs #W #T #U #H -elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or3_intro0/ -| #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_applv_simple … HT0) // - | @or3_intro1 -W (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ - | @or3_intro2 -T (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ - ] -| #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU - elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_applv_simple … HT0) // - | @or3_intro1 -W (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ - | @or3_intro2 -T (**) (* explicit constructor *) - @(cpxs_trans … HU) -U - @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma new file mode 100644 index 000000000..b1d0f1116 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.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/grammar/tsts.ma". +include "basic_2/computation/lpxs_cpxs.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) + +(* Forward lemmas involving same top term structure *************************) + +lemma cpxs_fwd_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≂ U. +#h #g #G #L #T #HT #U #H +>(cpxs_inv_cnx1 … H HT) -G -L -T // +qed-. + +lemma cpxs_fwd_sort: ∀h,g,G,L,U,k. ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] U → + ⋆k ≂ U ∨ ⦃G, L⦄ ⊢ ⋆(next h k) ➡*[h, g] U. +#h #g #G #L #U #k #H +elim (cpxs_inv_sort1 … H) -H #n #l generalize in match k; -k @(nat_ind_plus … n) -n +[ #k #_ #H -l destruct /2 width=1 by or_introl/ +| #n #IHn #k >plus_plus_comm_23 #Hnl #H destruct + lapply (deg_next_SO … Hnl) -Hnl #Hnl + elim (IHn … Hnl) -IHn + [ #H lapply (tsts_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/ + | generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n + /4 width=3 by cpxs_strap2, cpx_st, or_intror/ + | >iter_SO >iter_n_Sm // + ] +] +qed-. + +(* Basic_1: was just: pr3_iso_beta *) +lemma cpxs_fwd_beta: ∀h,g,a,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{a}W.T ➡*[h, g] U → + ⓐV.ⓛ{a}W.T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V.T ➡*[h, g] U. +#h #g #a #G #L #V #W #T #U #H +elim (cpxs_inv_appl1 … H) -H * +[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ +| #b #W0 #T0 #HT0 #HU + elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct + lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 + /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/ +| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_ + elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct +] +qed-. + +(* Note: probably this is an inversion lemma *) +lemma cpxs_fwd_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → + ∀V2. ⇧[0, i + 1] V1 ≡ V2 → + ∀U. ⦃G, L⦄ ⊢ #i ➡*[h, g] U → + #i ≂ U ∨ ⦃G, L⦄ ⊢ V2 ➡*[h, g] U. +#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H +elim (cpxs_inv_lref1 … H) -H /2 width=1 by or_introl/ +* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0 +lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct +/4 width=10 by cpxs_lift, drop_fwd_drop2, or_intror/ +qed-. + +lemma cpxs_fwd_theta: ∀h,g,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[h, g] U → + ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≂ U ∨ + ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[h, g] U. +#h #g #a #G #L #V1 #V #T #U #H #V2 #HV12 +elim (cpxs_inv_appl1 … H) -H * +[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ +| #b #W #T0 #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 by cpxs_flat_dx, cpxs_bind_dx/ ] -T + @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ] + /4 width=7 by cpx_zeta, lift_bind, lift_flat/ + ] +| #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 + /3 width=2 by cpxs_flat, cpxs_bind, drop_drop/ + | #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=2 by drop_drop/ #HV24 + @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T + @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V5 -T5 + @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/ + ] +] +qed-. + +lemma cpxs_fwd_cast: ∀h,g,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ➡*[h, g] U → + ∨∨ ⓝW. T ≂ U | ⦃G, L⦄ ⊢ T ➡*[h, g] U | ⦃G, L⦄ ⊢ W ➡*[h, g] U. +#h #g #G #L #W #T #U #H +elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ * +#W0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts_vector.ma new file mode 100644 index 000000000..bfbad281c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts_vector.ma @@ -0,0 +1,190 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tsts_vector.ma". +include "basic_2/substitution/lift_vector.ma". +include "basic_2/computation/cpxs_tsts.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) + +(* Vector form of forward lemmas involving same top term structure **********) + +(* Basic_1: was just: nf2_iso_appls_lref *) +lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → + ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U → ⒶVs.T ≂ U. +#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *) +#V #Vs #IHVs #U #H +elim (cpxs_inv_appl1 … H) -H * +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair/ +| #a #W0 #T0 #HT0 #HU + lapply (IHVs … HT0) -IHVs -HT0 #HT0 + elim (tsts_inv_bind_applv_simple … HT0) // +| #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU + lapply (IHVs … HT0) -IHVs -HT0 #HT0 + elim (tsts_inv_bind_applv_simple … HT0) // +] +qed-. + +lemma cpxs_fwd_sort_vector: ∀h,g,G,L,k,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆k ➡*[h, g] U → + ⒶVs.⋆k ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.⋆(next h k) ➡*[h, g] U. +#h #g #G #L #k #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/ +#V #Vs #IHVs #U #H +elim (cpxs_inv_appl1 … H) -H * +[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ +| #a #W1 #T1 #HT1 #HU + elim (IHVs … HT1) -IHVs -HT1 #HT1 + [ elim (tsts_inv_bind_applv_simple … HT1) // + | @or_intror (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV.ⓛ{a}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ + ] +| #a #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU + elim (IHVs … HT1) -IHVs -HT1 #HT1 + [ elim (tsts_inv_bind_applv_simple … HT1) // + | @or_intror (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV1.ⓓ{a}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ + ] +] +qed-. + + +(* Basic_1: was just: pr3_iso_appls_beta *) +lemma cpxs_fwd_beta_vector: ∀h,g,a,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[h, g] U → + ⒶVs. ⓐV. ⓛ{a}W. T ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{a}ⓝW.V.T ➡*[h, g] U. +#h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/ +#V0 #Vs #IHVs #V #W #T #U #H +elim (cpxs_inv_appl1 … H) -H * +[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ +| #b #W1 #T1 #HT1 #HU + elim (IHVs … HT1) -IHVs -HT1 #HT1 + [ elim (tsts_inv_bind_applv_simple … HT1) // + | @or_intror (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV0.ⓛ{b}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ + ] +| #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU + elim (IHVs … HT1) -IHVs -HT1 #HT1 + [ elim (tsts_inv_bind_applv_simple … HT1) // + | @or_intror (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ + ] +] +qed-. + +lemma cpxs_fwd_delta_vector: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → + ∀V2. ⇧[0, i + 1] V1 ≡ V2 → + ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.#i ➡*[h, g] U → + ⒶVs.#i ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.V2 ➡*[h, g] U. +#h #g #I #G #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 by tsts_pair, or_introl/ +| #b #W0 #T0 #HT0 #HU + elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (tsts_inv_bind_applv_simple … HT0) // + | @or_intror -i (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ + ] +| #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU + elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (tsts_inv_bind_applv_simple … HT0) // + | @or_intror -i (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ + ] +] +qed-. + +(* Basic_1: was just: pr3_iso_appls_abbr *) +lemma cpxs_fwd_theta_vector: ∀h,g,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀a,V,T,U. ⦃G, L⦄ ⊢ ⒶV1s.ⓓ{a}V.T ➡*[h, g] U → + ⒶV1s. ⓓ{a}V. T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}V.ⒶV2s.T ➡*[h, g] U. +#h #g #G #L #V1s #V2s * -V1s -V2s /3 width=1 by or_intror/ +#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 by tsts_pair, or_introl/ +| #b #W0 #T0 #HT0 #HU + elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0 + [ -HV12a -HV12b -HU + elim (tsts_inv_pair1 … HT0) #V1 #T1 #H destruct + | @or_intror -V1s (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + elim (cpxs_inv_abbr1 … HT0) -HT0 * + [ -HV12a -HV12b #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 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2s + @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0)) + /4 width=7 by cpxs_beta_dx, cpx_zeta, lift_bind, lift_flat/ + ] + ] +| #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU + elim (IHV12s … HV12b … HT0) -HV12b -IHV12s -HT0 #HT0 + [ -HV12a -HV10a -HV0a -HU + elim (tsts_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 by drop_drop/ ] #HV2a + @(cpxs_trans … (ⓓ{a}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/ + | #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 by drop_drop/ ] #HV2a + @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2s + @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V1 -T1 + @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/ + ] + ] +] +qed-. + +(* Basic_1: was just: pr3_iso_appls_cast *) +lemma cpxs_fwd_cast_vector: ∀h,g,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[h, g] U → + ∨∨ ⒶVs. ⓝW. T ≂ U + | ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U + | ⦃G, L⦄ ⊢ ⒶVs.W ➡*[h, g] U. +#h #g #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/ +#V #Vs #IHVs #W #T #U #H +elim (cpxs_inv_appl1 … H) -H * +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/ +| #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (tsts_inv_bind_applv_simple … HT0) // + | @or3_intro1 -W (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ + | @or3_intro2 -T (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ + ] +| #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU + elim (IHVs … HT0) -IHVs -HT0 #HT0 + [ elim (tsts_inv_bind_applv_simple … HT0) // + | @or3_intro1 -W (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ + | @or3_intro2 -T (**) (* explicit constructor *) + @(cpxs_trans … HU) -U + @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma index 0a42fb1f1..6d8aa3ed9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "basic_2/computation/acp_aaa.ma". +include "basic_2/computation/gcp_aaa.ma". include "basic_2/computation/cpxs_aaa.ma". -include "basic_2/computation/csx_tstc_vector.ma". +include "basic_2/computation/csx_tsts_vector.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) @@ -22,7 +22,7 @@ include "basic_2/computation/csx_tstc_vector.ma". theorem aaa_csx: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, g] T. #h #g #G #L #T #A #H -@(acp_aaa … (csx_acp h g) (csx_acr h g) … H) +@(gcr_aaa … (csx_gcp h g) (csx_gcr h g) … H) qed. (* Advanced eliminators *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma index f81114656..ade57bbd9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/reduction/cnx_lift.ma". -include "basic_2/computation/acp.ma". +include "basic_2/computation/gcp.ma". include "basic_2/computation/csx.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) @@ -109,8 +109,8 @@ qed-. (* Main properties **********************************************************) -theorem csx_acp: ∀h,g. acp (cpx h g) (eq …) (csx h g). -#h #g @mk_acp +theorem csx_gcp: ∀h,g. gcp (cpx h g) (eq …) (csx h g). +#h #g @mk_gcp [ /3 width=13 by cnx_lift/ | #G #L elim (deg_total h g 0) /3 width=8 by cnx_sort_iter, ex_intro/ | /2 width=3 by csx_fwd_flat_dx/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma index 0f6cb8370..bd0ebff18 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/grammar/tstc_tstc.ma". +include "basic_2/grammar/tsts_tsts.ma". include "basic_2/computation/cpxs_cpxs.ma". include "basic_2/computation/csx_alt.ma". include "basic_2/computation/csx_lift.ma". @@ -118,7 +118,7 @@ lemma csx_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 → /2 width=5 by csx_appl_theta_aux/ qed. (* Basic_1: was just: sn3_appl_appl *) -lemma csx_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → +lemma csx_appl_simple_tsts: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≂ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) → 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1. #h #g #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 @@ -130,8 +130,8 @@ elim (eq_false_inv_tpair_sn … H) -H @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10 @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ | -IHV -H1T1 -HLV0 * #H #H1T10 destruct - elim (tstc_dec T1 T0) #H2T10 - [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_repl_dx/ + elim (tsts_dec T1 T0) #H2T10 + [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tsts_canc_sn, simple_tsts_repl_dx/ | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma deleted file mode 100644 index 9573d288b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma +++ /dev/null @@ -1,129 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/acp_cr.ma". -include "basic_2/computation/cpxs_tstc_vector.ma". -include "basic_2/computation/csx_lpx.ma". -include "basic_2/computation/csx_vector.ma". - -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) - -(* Advanced properties ******************************************************) - -(* Basic_1: was just: sn3_appls_lref *) -lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → - ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T. -#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *) -#V #Vs #IHV #H -elim (csxv_inv_cons … H) -H #HV #HVs -@csx_appl_simple_tstc /2 width=1 by applv_simple/ -IHV -HV -HVs -#X #H #H0 -lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H -elim (H0) -H0 // -qed. - -lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k. -#h #g #G #L #k elim (deg_total h g k) -#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ] -#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl -#Hkl #Vs elim Vs -Vs /2 width=1 by/ -#V #Vs #IHVs #HVVs -elim (csxv_inv_cons … HVVs) #HV #HVs -@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs -#X #H #H0 -elim (cpxs_fwd_sort_vector … H) -H #H -[ elim H0 -H0 // -| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h k))) /2 width=1 by cpxs_flat_dx/ -] -qed. - -(* Basic_1: was just: sn3_appls_beta *) -lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T → - ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs. ⓐV.ⓛ{a}W.T. -#h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/ -#V0 #Vs #IHV #V #W #T #H1T -lapply (csx_fwd_pair_sn … H1T) #HV0 -lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T -#X #H #H0 -elim (cpxs_fwd_beta_vector … H) -H #H -[ -H1T elim H0 -H0 // -| -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ -] -qed. - -lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → - ∀V2. ⇧[0, i + 1] V1 ≡ V2 → - ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i). -#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs -[ /4 width=12 by csx_inv_lift, csx_lref_bind, drop_fwd_drop2/ -| #V #Vs #IHV #H1T - lapply (csx_fwd_pair_sn … H1T) #HV - lapply (csx_fwd_flat_dx … H1T) #H2T - @csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T - #X #H #H0 - elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H - [ -H1T elim H0 -H0 // - | -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ - ] -] -qed. - -(* Basic_1: was just: sn3_appls_abbr *) -lemma csx_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → - ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T → - ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T. -#h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1 by/ -#V1s #V2s #V1 #V2 #HV12 #H -generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 -elim H -V1s -V2s /2 width=3 by csx_appl_theta/ -#V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H -lapply (csx_appl_theta … HW12 … H) -H -HW12 #H -lapply (csx_fwd_pair_sn … H) #HW1 -lapply (csx_fwd_flat_dx … H) #H1 -@csx_appl_simple_tstc /2 width=3 by simple_flat/ -IHV12s -HW1 -H1 #X #H1 #H2 -elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1 by liftv_cons/ -HV12s -HV12 -[ -H #H elim H2 -H2 // -| -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ -] -qed. - -(* Basic_1: was just: sn3_appls_cast *) -lemma csx_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T → - ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓝW.T. -#h #g #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/ -#V #Vs #IHV #W #T #H1W #H1T -lapply (csx_fwd_pair_sn … H1W) #HV -lapply (csx_fwd_flat_dx … H1W) #H2W -lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T -#X #H #H0 -elim (cpxs_fwd_cast_vector … H) -H #H -[ -H1W -H1T elim H0 -H0 // -| -H1W -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ -| -H1T -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ -] -qed. - -theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (csx h g). -#h #g @mk_acr // -[ /2 width=8 by csx_lift/ -| /3 width=1 by csx_applv_cnx/ -|3,4,7: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/ -| /2 width=7 by csx_applv_delta/ -| #G #L #V1s #V2s #HV12s #a #V #T #H #HV - @(csx_applv_theta … HV12s) -HV12s - @csx_abbr // -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tsts_vector.ma new file mode 100644 index 000000000..33f847019 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tsts_vector.ma @@ -0,0 +1,129 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/gcp_cr.ma". +include "basic_2/computation/cpxs_tsts_vector.ma". +include "basic_2/computation/csx_lpx.ma". +include "basic_2/computation/csx_vector.ma". + +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) + +(* Advanced properties ******************************************************) + +(* Basic_1: was just: sn3_appls_lref *) +lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → + ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T. +#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *) +#V #Vs #IHV #H +elim (csxv_inv_cons … H) -H #HV #HVs +@csx_appl_simple_tsts /2 width=1 by applv_simple/ -IHV -HV -HVs +#X #H #H0 +lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H +elim (H0) -H0 // +qed. + +lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k. +#h #g #G #L #k elim (deg_total h g k) +#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ] +#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl +#Hkl #Vs elim Vs -Vs /2 width=1 by/ +#V #Vs #IHVs #HVVs +elim (csxv_inv_cons … HVVs) #HV #HVs +@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs +#X #H #H0 +elim (cpxs_fwd_sort_vector … H) -H #H +[ elim H0 -H0 // +| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h k))) /2 width=1 by cpxs_flat_dx/ +] +qed. + +(* Basic_1: was just: sn3_appls_beta *) +lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T → + ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs. ⓐV.ⓛ{a}W.T. +#h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/ +#V0 #Vs #IHV #V #W #T #H1T +lapply (csx_fwd_pair_sn … H1T) #HV0 +lapply (csx_fwd_flat_dx … H1T) #H2T +@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T +#X #H #H0 +elim (cpxs_fwd_beta_vector … H) -H #H +[ -H1T elim H0 -H0 // +| -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ +] +qed. + +lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → + ∀V2. ⇧[0, i + 1] V1 ≡ V2 → + ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i). +#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs +[ /4 width=12 by csx_inv_lift, csx_lref_bind, drop_fwd_drop2/ +| #V #Vs #IHV #H1T + lapply (csx_fwd_pair_sn … H1T) #HV + lapply (csx_fwd_flat_dx … H1T) #H2T + @csx_appl_simple_tsts /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T + #X #H #H0 + elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H + [ -H1T elim H0 -H0 // + | -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ + ] +] +qed. + +(* Basic_1: was just: sn3_appls_abbr *) +lemma csx_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T → + ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T. +#h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1 by/ +#V1s #V2s #V1 #V2 #HV12 #H +generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 +elim H -V1s -V2s /2 width=3 by csx_appl_theta/ +#V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H +lapply (csx_appl_theta … HW12 … H) -H -HW12 #H +lapply (csx_fwd_pair_sn … H) #HW1 +lapply (csx_fwd_flat_dx … H) #H1 +@csx_appl_simple_tsts /2 width=3 by simple_flat/ -IHV12s -HW1 -H1 #X #H1 #H2 +elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1 by liftv_cons/ -HV12s -HV12 +[ -H #H elim H2 -H2 // +| -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ +] +qed. + +(* Basic_1: was just: sn3_appls_cast *) +lemma csx_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T → + ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓝW.T. +#h #g #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/ +#V #Vs #IHV #W #T #H1W #H1T +lapply (csx_fwd_pair_sn … H1W) #HV +lapply (csx_fwd_flat_dx … H1W) #H2W +lapply (csx_fwd_flat_dx … H1T) #H2T +@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T +#X #H #H0 +elim (cpxs_fwd_cast_vector … H) -H #H +[ -H1W -H1T elim H0 -H0 // +| -H1W -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ +| -H1T -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ +] +qed. + +theorem csx_gcr: ∀h,g. gcr (cpx h g) (eq …) (csx h g) (csx h g). +#h #g @mk_gcr // +[ /2 width=8 by csx_lift/ +| /3 width=1 by csx_applv_cnx/ +|3,4,7: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/ +| /2 width=7 by csx_applv_delta/ +| #G #L #V1s #V2s #HV12s #a #V #T #H #HV + @(csx_applv_theta … HV12s) -HV12s + @csx_abbr // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp.ma new file mode 100644 index 000000000..67dd3f6d6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||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/genv.ma". +include "basic_2/multiple/drops.ma". + +(* GENERIC COMPUTATION PROPERTIES *******************************************) + +definition candidate: Type[0] ≝ relation3 genv lenv term. + +definition CP0 ≝ λRR:relation4 genv lenv term term. λRS:relation term. + ∀G,L0,L,T,T0,s,d,e. NF … (RR G L) RS T → + ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR G L0) RS T0. + +definition CP0s ≝ λRR:relation4 genv lenv term term. λRS:relation term. + ∀G,L0,L,s,des. ⇩*[s, des] L0 ≡ L → + ∀T,T0. ⇧*[des] T ≡ T0 → + NF … (RR G L) RS T → NF … (RR G L0) RS T0. + +definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term. + ∀G,L. ∃k. NF … (RR G L) RS (⋆k). + +definition CP2 ≝ λRP:candidate. + ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T. + +(* requirements for generic computation properties *) +record gcp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝ +{ cp0: CP0 RR RS; + cp1: CP1 RR RS; + cp2: CP2 RP +}. + +(* Basic properties *********************************************************) + +(* Basic_1: was: nf2_lift1 *) +lemma gcp_lifts: ∀RR,RS. CP0 RR RS → CP0s RR RS. +#RR #RS #HRR #G #L1 #L2 #s #des #H elim H -L1 -L2 -des +[ #L #T1 #T2 #H #HT1 + <(lifts_inv_nil … H) -H // +| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2 + elim (lifts_inv_cons … H) -H /3 width=10 by/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma new file mode 100644 index 000000000..c890be39e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma @@ -0,0 +1,93 @@ +(**************************************************************************) +(* ___ *) +(* ||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/multiple/lifts_lifts.ma". +include "basic_2/multiple/drops_drops.ma". +include "basic_2/static/aaa_lifts.ma". +include "basic_2/static/aaa_aaa.ma". +include "basic_2/computation/lsubc_drops.ma". + +(* GENERIC COMPUTATION PROPERTIES *******************************************) + +(* Main properties **********************************************************) + +(* Basic_1: was: sc3_arity_csubc *) +theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. + gcp RR RS RP → gcr RR RS RP RP → + ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[Ⓕ, des] L0 ≡ L1 → + ∀T0. ⇧*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 → + ⦃G, L2, T0⦄ ϵ[RP] 〚A〛. +#RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A +[ #G #L #k #L0 #des #HL0 #X #H #L2 #HL20 + >(lifts_inv_sort1 … H) -H + lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom + @(s4 … HAtom … (◊)) // +| #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20 + lapply (acr_gcr … H1RP H2RP B) #HB + elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct + lapply (drop_fwd_drop2 … HLK1) #HK1b + elim (drops_drop_trans … HL01 … HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hdes1 + >(at_mono … Hi1 … Hi0) -i1 + elim (drops_inv_skip2 … Hdes1 … H) -des1 #K0 #V0 #des0 #Hdes0 #HK01 #HV10 #H destruct + elim (lsubc_drop_O1_trans … HL20 … HL0) -HL0 #X #HLK2 #H + elim (lsubc_inv_pair2 … H) -H * + [ #K2 #HK20 #H destruct + 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 by drops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *) + | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0 + #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct + lapply (drop_fwd_drop2 … HLK2) #HLK2b + lapply (aaa_lifts … HK01 … HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B + lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B + elim (lift_total V0 0 (i0 +1)) #V3 #HV03 + elim (lift_total V2 0 (i0 +1)) #V #HV2 + @(s5 … HB … (◊) … (ⓝV3.V) … HLK2) [2: /2 width=1 by lift_flat/ ] + @(s7 … HB … (◊)) [ @(s0 … HB … HKV2A) // | @(s0 … HB … H1KV0A) // ] + ] +| #a #G #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 (acr_gcr … H1RP H2RP A) #HA + lapply (acr_gcr … H1RP H2RP B) #HB + lapply (s1 … HB) -HB #HB + @(s6 … HA … (◊) (◊)) /3 width=5 by lsubc_pair, drops_skip, liftv_nil/ +| #a #G #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 + @(acr_abst … H1RP H2RP) [ /2 width=5 by/ ] + #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B + elim (drops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20 + lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B + @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA + /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/ +| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 + elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct + /3 width=10 by drops_nil, lifts_nil/ +| #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20 + elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct + lapply (acr_gcr … H1RP H2RP A) #HA + @(s7 … HA … (◊)) /2 width=5 by/ +] +qed. + +(* Basic_1: was: sc3_arity *) +lemma acr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛. +/2 width=8 by drops_nil, lifts_nil, acr_aaa_csubc_lifts/ qed. + +lemma gcr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T. +#RR #RS #RP #H1RP #H2RP #G #L #T #A #HT +lapply (acr_gcr … H1RP H2RP A) #HA +@(s1 … HA) /2 width=4 by acr_aaa/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma new file mode 100644 index 000000000..537769345 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma @@ -0,0 +1,193 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/ineint_5.ma". +include "basic_2/grammar/aarity.ma". +include "basic_2/multiple/mr2_mr2.ma". +include "basic_2/multiple/lifts_lift_vector.ma". +include "basic_2/multiple/drops_drop.ma". +include "basic_2/computation/gcp.ma". + +(* GENERIC COMPUTATION PROPERTIES *******************************************) + +definition S0 ≝ λC:candidate. ∀G,L2,L1,T1,d,e. + C G L1 T1 → ∀T2. ⇩[Ⓕ, d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2. + +definition S0s ≝ λC:candidate. + ∀G,L1,L2,des. ⇩*[Ⓕ, des] L2 ≡ L1 → + ∀T1,T2. ⇧*[des] T1 ≡ T2 → C G L1 T1 → C G L2 T2. + +(* Note: this is Girard's CR1 *) +definition S1 ≝ λRP,C:candidate. + ∀G,L,T. C G L T → RP G L T. + +(* Note: this is Tait's iii, or Girard's CR4 *) +definition S2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. λRP,C:candidate. + ∀G,L,Vs. all … (RP G L) Vs → + ∀T. 𝐒⦃T⦄ → NF … (RR G L) RS T → C G L (ⒶVs.T). + +(* Note: this generalizes Tait's ii *) +definition S3 ≝ λC:candidate. + ∀a,G,L,Vs,V,T,W. + C G L (ⒶVs.ⓓ{a}ⓝW.V.T) → C G L (ⒶVs.ⓐV.ⓛ{a}W.T). + +definition S4 ≝ λRP,C:candidate. + ∀G,L,Vs. all … (RP G L) Vs → ∀k. C G L (ⒶVs.⋆k). + +definition S5 ≝ λC:candidate. ∀I,G,L,K,Vs,V1,V2,i. + C G L (ⒶVs.V2) → ⇧[0, i+1] V1 ≡ V2 → + ⇩[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i). + +definition S6 ≝ λRP,C:candidate. + ∀G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀a,V,T. C G (L.ⓓV) (ⒶV2s.T) → RP G L V → C G L (ⒶV1s.ⓓ{a}V.T). + +definition S7 ≝ λC:candidate. + ∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T). + +(* requirements for the generic reducibility candidate *) +record gcr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate) : Prop ≝ +{ s0: S0 C; + s1: S1 RP C; + s2: S2 RR RS RP C; + s3: S3 C; + s4: S4 RP C; + s5: S5 C; + s6: S6 RP C; + s7: S7 C +}. + +(* the functional construction for candidates *) +definition cfun: candidate → candidate → candidate ≝ + λC1,C2,G,K,T. ∀L,V,U,des. + ⇩*[Ⓕ, des] L ≡ K → ⇧*[des] T ≡ U → C1 G L V → C2 G L (ⓐV.U). + +(* the reducibility candidate associated to an atomic arity *) +let rec acr (RP:candidate) (A:aarity) on A: candidate ≝ +match A with +[ AAtom ⇒ RP +| APair B A ⇒ cfun (acr RP B) (acr RP A) +]. + +interpretation + "candidate of reducibility of an atomic arity (abstract)" + 'InEInt RP G L T A = (acr RP A G L T). + +(* Basic properties *********************************************************) + +(* Basic_1: was: sc3_lift1 *) +lemma gcr_lifts: ∀C. S0 C → S0s C. +#C #HC #G #L1 #L2 #des #H elim H -L1 -L2 -des +[ #L #T1 #T2 #H #HT1 <(lifts_inv_nil … H) -H // +| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2 + elim (lifts_inv_cons … H) -H /3 width=10 by/ +] +qed. + +lemma rp_lifts: ∀RR,RS,RP. gcr RR RS RP RP → + ∀des,G,L0,L,V,V0. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] V ≡ V0 → + RP G L V → RP G L0 V0. +#RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV +@gcr_lifts /width=7 by/ +@(s0 … HRP) +qed. + +(* Basic_1: was only: sns3_lifts1 *) +lemma rp_liftsv_all: ∀RR,RS,RP. gcr RR RS RP RP → + ∀des,G,L0,L,Vs,V0s. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] Vs ≡ V0s → + all … (RP G L) Vs → all … (RP G L0) V0s. +#RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #HL0 #H elim H -Vs -V0s normalize // +#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s * /3 width=7 by rp_lifts, conj/ +qed. + +(* Basic_1: was: + sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift +*) +lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀A. gcr RR RS RP (acr RP A). +#RR #RS #RP #H1RP #H2RP #A elim A -A normalize // +#B #A #IHB #IHA @mk_gcr normalize +[ /3 width=7 by drops_cons, lifts_cons/ +| #G #L #T #H + elim (cp1 … H1RP G L) #k #HK + lapply (H ? (⋆k) ? (⟠) ? ? ?) -H + [3,5: // |2,4: skip + | @(s2 … IHB … (◊)) // + | #H @(cp2 … H1RP … k) @(s1 … IHA) // + ] +| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HL0 #H #HB + elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct + lapply (s1 … IHB … HB) #HV0 + @(s2 … IHA … (V0 @ V0s)) + /3 width=14 by rp_liftsv_all, gcp_lifts, cp0, lifts_simple_dx, conj/ +| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HL0 #H #HB + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + 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)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/ +| #G #L #Vs #HVs #k #L0 #V0 #X #des #HL0 #H #HB + 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=7 by rp_liftsv_all, conj/ +| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HL0 #H #HB + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct + elim (drops_drop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0 + >(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02 + elim (drops_inv_skip2 … Hdes0 … H) -H -des0 #L2 #W1 #des0 #Hdes0 #HLK #HVW1 #H destruct + 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 + @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_applv/ +| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HL0 #H #HB + 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 + @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/ + @(HA … (des + 1)) /2 width=2 by drops_skip/ + [ @lifts_applv // + elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s + >(liftv_mono … HV12s … HV10s) -V1s // + | @(s0 … IHB … HB … HV120) /2 width=2 by drop_drop/ + ] +| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HL0 #H #HB + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct + @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_applv/ +] +qed. + +lemma acr_abst: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → ( + ∀L0,V0,W0,T0,des. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] W ≡ W0 → ⇧*[des + 1] T ≡ T0 → + ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛 + ) → + ⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛. +#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HL0 #H #HB +lapply (acr_gcr … H1RP H2RP A) #HCA +lapply (acr_gcr … H1RP H2RP B) #HCB +elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct +lapply (gcr_lifts … HL0 … HW0 HW) -HW [ @(s0 … HCB) ] #HW0 +@(s3 … HCA … (◊)) +@(s6 … HCA … (◊) (◊)) // +[ @(HA … HL0) // +| lapply (s1 … HCB) -HCB #HCB + @(s7 … H2RP … (◊)) /2 width=1 by/ +] +qed. + +(* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *) +(* Basic_1: removed local theorems 1: sc3_sn3_abst *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma index 7c0a785ca..adc75dd3b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma @@ -13,10 +13,11 @@ (**************************************************************************) include "basic_2/notation/relations/lrsubeqc_4.ma". +include "basic_2/static/lsubr.ma". include "basic_2/static/aaa.ma". -include "basic_2/computation/acp_cr.ma". +include "basic_2/computation/gcp_cr.ma". -(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) +(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) inductive lsubc (RP) (G): relation lenv ≝ | lsubc_atom: lsubc RP G (⋆) (⋆) @@ -26,7 +27,7 @@ inductive lsubc (RP) (G): relation lenv ≝ . interpretation - "local environment refinement (abstract candidates of reducibility)" + "local environment refinement (generic reducibility)" 'LRSubEqC RP G L1 L2 = (lsubc RP G L1 L2). (* Basic inversion lemmas ***************************************************) @@ -95,6 +96,12 @@ lemma lsubc_inv_pair2: ∀RP,I,G,L1,K2,W. G ⊢ L1 ⫃[RP] K2.ⓑ{I} W → L1 = K1.ⓓⓝW.V & I = Abst. /2 width=3 by lsubc_inv_pair2_aux/ qed-. +(* Basic forward lemmas *****************************************************) + +lemma lsubc_fwd_lsubr: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 ⫃ L2. +#RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/ +qed-. + (* Basic properties *********************************************************) (* Basic_1: was just: csubc_refl *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma index 9b46f01f0..36f35527c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma @@ -15,7 +15,7 @@ include "basic_2/static/aaa_lift.ma". include "basic_2/computation/lsubc.ma". -(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) +(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) (* Properties concerning basic local environment slicing ********************) @@ -42,10 +42,10 @@ qed-. (* Basic_1: was: csubc_drop_conf_rev *) lemma drop_lsubc_trans: ∀RR,RS,RP. - acp RR RS RP → acr RR RS RP RP → + gcp RR RS RP → gcr RR RS RP RP → ∀G,L1,K1,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 → ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⇩[Ⓕ, d, e] L2 ≡ K2. -#RR #RS #RP #Hacp #Hacr #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e +#RR #RS #RP #Hgcp #Hgcr #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e [ #d #e #He #X #H elim (lsubc_inv_atom1 … H) -H >He /2 width=3 by ex2_intro/ | #L1 #I #V1 #X #H @@ -63,7 +63,7 @@ lemma drop_lsubc_trans: ∀RR,RS,RP. | #K2 #V #W2 #A #HV2 #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct elim (lift_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct elim (IHLK1 … HK12) #K #HL1K #HK2 - lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA + lapply (acr_gcr … Hgcp Hgcr A) -Hgcp -Hgcr #HA lapply (s0 … HA … HV2 … HLK1 HV3) -HV2 lapply (s0 … HA … H1W2 … HLK1 HW23) -H1W2 /4 width=11 by lsubc_beta, aaa_lift, drop_skip, ex2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma index 5685fd1ef..e1c30a75a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma @@ -14,19 +14,19 @@ include "basic_2/computation/lsubc_drop.ma". -(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) +(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) (* Properties concerning generic local environment slicing ******************) (* Basic_1: was: csubc_drop1_conf_rev *) lemma drops_lsubc_trans: ∀RR,RS,RP. - acp RR RS RP → acr RR RS RP RP → + gcp RR RS RP → gcr RR RS RP RP → ∀G,L1,K1,des. ⇩*[Ⓕ, des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 → ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⇩*[Ⓕ, des] L2 ≡ K2. -#RR #RS #RP #Hacp #Hacr #G #L1 #K1 #des #H elim H -L1 -K1 -des +#RR #RS #RP #Hgcp #Hgcr #G #L1 #K1 #des #H elim H -L1 -K1 -des [ /2 width=3 by drops_nil, ex2_intro/ | #L1 #L #K1 #des #d #e #_ #HLK1 #IHL #K2 #HK12 - elim (drop_lsubc_trans … Hacp Hacr … HLK1 … HK12) -Hacp -Hacr -K1 #K #HLK #HK2 + elim (drop_lsubc_trans … Hgcp Hgcr … HLK1 … HK12) -Hgcp -Hgcr -K1 #K #HLK #HK2 elim (IHL … HLK) -IHL -HLK /3 width=5 by drops_cons, ex2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma index d8dcf0e8d..3a17f0e5b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma @@ -13,14 +13,14 @@ (**************************************************************************) include "basic_2/static/lsuba.ma". -include "basic_2/computation/acp_aaa.ma". +include "basic_2/computation/gcp_aaa.ma". -(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) +(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) (* properties concerning lenv refinement for atomic arity assignment ********) -lemma lsuba_lsubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP → +lemma lsuba_lsubc: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → G ⊢ L1 ⫃[RP] L2. #RR #RS #RP #H1RP #H2RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubc_pair/ -#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4 by aacr_aaa, lsubc_beta/ +#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4 by acr_aaa, lsubc_beta/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma deleted file mode 100644 index a861d18a6..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma +++ /dev/null @@ -1,108 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/topiso_2.ma". -include "basic_2/grammar/term_simple.ma". - -(* SAME TOP TERM CONSTRUCTOR ************************************************) - -inductive tstc: relation term ≝ - | tstc_atom: ∀I. tstc (⓪{I}) (⓪{I}) - | tstc_pair: ∀I,V1,V2,T1,T2. tstc (②{I}V1.T1) (②{I}V2.T2) -. - -interpretation "same top constructor (term)" 'TopIso T1 T2 = (tstc T1 T2). - -(* Basic inversion lemmas ***************************************************) - -fact tstc_inv_atom1_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T1 = ⓪{I} → T2 = ⓪{I}. -#T1 #T2 * -T1 -T2 // -#J #V1 #V2 #T1 #T2 #I #H destruct -qed-. - -(* Basic_1: was: iso_gen_sort iso_gen_lref *) -lemma tstc_inv_atom1: ∀I,T2. ⓪{I} ≂ T2 → T2 = ⓪{I}. -/2 width=3 by tstc_inv_atom1_aux/ qed-. - -fact tstc_inv_pair1_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W1,U1. T1 = ②{I}W1.U1 → - ∃∃W2,U2. T2 = ②{I}W2. U2. -#T1 #T2 * -T1 -T2 -[ #J #I #W1 #U1 #H destruct -| #J #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/ -] -qed-. - -(* Basic_1: was: iso_gen_head *) -lemma tstc_inv_pair1: ∀I,W1,U1,T2. ②{I}W1.U1 ≂ T2 → - ∃∃W2,U2. T2 = ②{I}W2. U2. -/2 width=5 by tstc_inv_pair1_aux/ qed-. - -fact tstc_inv_atom2_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T2 = ⓪{I} → T1 = ⓪{I}. -#T1 #T2 * -T1 -T2 // -#J #V1 #V2 #T1 #T2 #I #H destruct -qed-. - -lemma tstc_inv_atom2: ∀I,T1. T1 ≂ ⓪{I} → T1 = ⓪{I}. -/2 width=3 by tstc_inv_atom2_aux/ qed-. - -fact tstc_inv_pair2_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 → - ∃∃W1,U1. T1 = ②{I}W1.U1. -#T1 #T2 * -T1 -T2 -[ #J #I #W2 #U2 #H destruct -| #J #V1 #V2 #T1 #T2 #I #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/ -] -qed-. - -lemma tstc_inv_pair2: ∀I,T1,W2,U2. T1 ≂ ②{I}W2.U2 → - ∃∃W1,U1. T1 = ②{I}W1.U1. -/2 width=5 by tstc_inv_pair2_aux/ qed-. - -(* Basic properties *********************************************************) - -(* Basic_1: was: iso_refl *) -lemma tstc_refl: reflexive … tstc. -#T elim T -T // -qed. - -lemma tstc_sym: symmetric … tstc. -#T1 #T2 #H elim H -T1 -T2 // -qed-. - -lemma tstc_dec: ∀T1,T2. Decidable (T1 ≂ T2). -* #I1 [2: #V1 #T1 ] * #I2 [2,4: #V2 #T2 ] -[ elim (eq_item2_dec I1 I2) #HI12 - [ destruct /2 width=1 by tstc_pair, or_introl/ - | @or_intror #H - elim (tstc_inv_pair1 … H) -H #V #T #H destruct /2 width=1 by/ - ] -| @or_intror #H - lapply (tstc_inv_atom1 … H) -H #H destruct -| @or_intror #H - lapply (tstc_inv_atom2 … H) -H #H destruct -| elim (eq_item0_dec I1 I2) #HI12 - [ destruct /2 width=1 by or_introl/ - | @or_intror #H - lapply (tstc_inv_atom2 … H) -H #H destruct /2 width=1 by/ - ] -] -qed. - -lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. -#T1 #T2 * -T1 -T2 // -#I #V1 #V2 #T1 #T2 #H -elim (simple_inv_pair … H) -H #J #H destruct // -qed-. - -lemma simple_tstc_repl_sn: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. -/3 width=3 by simple_tstc_repl_dx, tstc_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_tstc.ma deleted file mode 100644 index 83a17a679..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_tstc.ma +++ /dev/null @@ -1,32 +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". - -(* SAME TOP TERM CONSTRUCTOR ************************************************) - -(* Main properties **********************************************************) - -(* Basic_1: was: iso_trans *) -theorem tstc_trans: Transitive … tstc. -#T1 #T * -T1 -T // -#I #V1 #V #T1 #T #X #H -elim (tstc_inv_pair1 … H) -H #V2 #T2 #H destruct // -qed-. - -theorem tstc_canc_sn: ∀T,T1. T ≂ T1 → ∀T2. T ≂ T2 → T1 ≂ T2. -/3 width=3 by tstc_trans, tstc_sym/ qed-. - -theorem tstc_canc_dx: ∀T1,T. T1 ≂ T → ∀T2. T2 ≂ T → T1 ≂ T2. -/3 width=3 by tstc_trans, tstc_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_vector.ma deleted file mode 100644 index df30d65b8..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_vector.ma +++ /dev/null @@ -1,31 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/grammar/term_vector.ma". -include "basic_2/grammar/tstc.ma". - -(* SAME TOP TERM CONSTRUCTOR ************************************************) - -(* Advanced inversion lemmas ************************************************) - -(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *) -lemma tstc_inv_bind_applv_simple: ∀a,I,Vs,V2,T1,T2. ⒶVs.T1 ≂ ⓑ{a,I} V2. T2 → - 𝐒⦃T1⦄ → ⊥. -#a #I #Vs #V2 #T1 #T2 #H -elim (tstc_inv_pair2 … H) -H #V0 #T0 -elim Vs -Vs normalize -[ #H destruct #H /2 width=5 by simple_inv_bind/ -| #V #Vs #_ #H destruct -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts.ma new file mode 100644 index 000000000..d3bc8ee96 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts.ma @@ -0,0 +1,108 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/topiso_2.ma". +include "basic_2/grammar/term_simple.ma". + +(* SAME TOP TERM STRUCTURE **************************************************) + +inductive tsts: relation term ≝ + | tsts_atom: ∀I. tsts (⓪{I}) (⓪{I}) + | tsts_pair: ∀I,V1,V2,T1,T2. tsts (②{I}V1.T1) (②{I}V2.T2) +. + +interpretation "same top structure (term)" 'TopIso T1 T2 = (tsts T1 T2). + +(* Basic inversion lemmas ***************************************************) + +fact tsts_inv_atom1_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T1 = ⓪{I} → T2 = ⓪{I}. +#T1 #T2 * -T1 -T2 // +#J #V1 #V2 #T1 #T2 #I #H destruct +qed-. + +(* Basic_1: was: iso_gen_sort iso_gen_lref *) +lemma tsts_inv_atom1: ∀I,T2. ⓪{I} ≂ T2 → T2 = ⓪{I}. +/2 width=3 by tsts_inv_atom1_aux/ qed-. + +fact tsts_inv_pair1_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W1,U1. T1 = ②{I}W1.U1 → + ∃∃W2,U2. T2 = ②{I}W2. U2. +#T1 #T2 * -T1 -T2 +[ #J #I #W1 #U1 #H destruct +| #J #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/ +] +qed-. + +(* Basic_1: was: iso_gen_head *) +lemma tsts_inv_pair1: ∀I,W1,U1,T2. ②{I}W1.U1 ≂ T2 → + ∃∃W2,U2. T2 = ②{I}W2. U2. +/2 width=5 by tsts_inv_pair1_aux/ qed-. + +fact tsts_inv_atom2_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T2 = ⓪{I} → T1 = ⓪{I}. +#T1 #T2 * -T1 -T2 // +#J #V1 #V2 #T1 #T2 #I #H destruct +qed-. + +lemma tsts_inv_atom2: ∀I,T1. T1 ≂ ⓪{I} → T1 = ⓪{I}. +/2 width=3 by tsts_inv_atom2_aux/ qed-. + +fact tsts_inv_pair2_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 → + ∃∃W1,U1. T1 = ②{I}W1.U1. +#T1 #T2 * -T1 -T2 +[ #J #I #W2 #U2 #H destruct +| #J #V1 #V2 #T1 #T2 #I #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/ +] +qed-. + +lemma tsts_inv_pair2: ∀I,T1,W2,U2. T1 ≂ ②{I}W2.U2 → + ∃∃W1,U1. T1 = ②{I}W1.U1. +/2 width=5 by tsts_inv_pair2_aux/ qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was: iso_refl *) +lemma tsts_refl: reflexive … tsts. +#T elim T -T // +qed. + +lemma tsts_sym: symmetric … tsts. +#T1 #T2 #H elim H -T1 -T2 // +qed-. + +lemma tsts_dec: ∀T1,T2. Decidable (T1 ≂ T2). +* #I1 [2: #V1 #T1 ] * #I2 [2,4: #V2 #T2 ] +[ elim (eq_item2_dec I1 I2) #HI12 + [ destruct /2 width=1 by tsts_pair, or_introl/ + | @or_intror #H + elim (tsts_inv_pair1 … H) -H #V #T #H destruct /2 width=1 by/ + ] +| @or_intror #H + lapply (tsts_inv_atom1 … H) -H #H destruct +| @or_intror #H + lapply (tsts_inv_atom2 … H) -H #H destruct +| elim (eq_item0_dec I1 I2) #HI12 + [ destruct /2 width=1 by or_introl/ + | @or_intror #H + lapply (tsts_inv_atom2 … H) -H #H destruct /2 width=1 by/ + ] +] +qed. + +lemma simple_tsts_repl_dx: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. +#T1 #T2 * -T1 -T2 // +#I #V1 #V2 #T1 #T2 #H +elim (simple_inv_pair … H) -H #J #H destruct // +qed-. + +lemma simple_tsts_repl_sn: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. +/3 width=3 by simple_tsts_repl_dx, tsts_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_tsts.ma new file mode 100644 index 000000000..d46b497c8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_tsts.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tsts.ma". + +(* SAME TOP TERM STRUCTURE **************************************************) + +(* Main properties **********************************************************) + +(* Basic_1: was: iso_trans *) +theorem tsts_trans: Transitive … tsts. +#T1 #T * -T1 -T // +#I #V1 #V #T1 #T #X #H +elim (tsts_inv_pair1 … H) -H #V2 #T2 #H destruct // +qed-. + +theorem tsts_canc_sn: ∀T,T1. T ≂ T1 → ∀T2. T ≂ T2 → T1 ≂ T2. +/3 width=3 by tsts_trans, tsts_sym/ qed-. + +theorem tsts_canc_dx: ∀T1,T. T1 ≂ T → ∀T2. T2 ≂ T → T1 ≂ T2. +/3 width=3 by tsts_trans, tsts_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_vector.ma new file mode 100644 index 000000000..936804ce9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_vector.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/grammar/term_vector.ma". +include "basic_2/grammar/tsts.ma". + +(* SAME TOP TERM STRUCTURE **************************************************) + +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *) +lemma tsts_inv_bind_applv_simple: ∀a,I,Vs,V2,T1,T2. ⒶVs.T1 ≂ ⓑ{a,I} V2. T2 → + 𝐒⦃T1⦄ → ⊥. +#a #I #Vs #V2 #T1 #T2 #H +elim (tsts_inv_pair2 … H) -H #V0 #T0 +elim Vs -Vs normalize +[ #H destruct #H /2 width=5 by simple_inv_bind/ +| #V #Vs #_ #H destruct +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma index ff9574ab6..1c0c18888 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma @@ -15,7 +15,7 @@ include "basic_2/notation/relations/rdropstar_3.ma". include "basic_2/notation/relations/rdropstar_4.ma". include "basic_2/substitution/drop.ma". -include "basic_2/multiple/gr2_minus.ma". +include "basic_2/multiple/mr2_minus.ma". include "basic_2/multiple/lifts.ma". (* ITERATED LOCAL ENVIRONMENT SLICING ***************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2.ma deleted file mode 100644 index 57bb952b4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2.ma +++ /dev/null @@ -1,74 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/rat_3.ma". -include "basic_2/grammar/term_vector.ma". - -(* GENERIC RELOCATION WITH PAIRS ********************************************) - -inductive at: list2 nat nat → relation nat ≝ -| at_nil: ∀i. at (⟠) i i -| at_lt : ∀des,d,e,i1,i2. i1 < d → - at des i1 i2 → at ({d, e} @ des) i1 i2 -| at_ge : ∀des,d,e,i1,i2. d ≤ i1 → - at des (i1 + e) i2 → at ({d, e} @ des) i1 i2 -. - -interpretation "application (generic relocation with pairs)" - 'RAt i1 des i2 = (at des i1 i2). - -(* Basic inversion lemmas ***************************************************) - -fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ⟠ → i1 = i2. -#des #i1 #i2 * -des -i1 -i2 -[ // -| #des #d #e #i1 #i2 #_ #_ #H destruct -| #des #d #e #i1 #i2 #_ #_ #H destruct -] -qed-. - -lemma at_inv_nil: ∀i1,i2. @⦃i1, ⟠⦄ ≡ i2 → i1 = i2. -/2 width=3 by at_inv_nil_aux/ qed-. - -fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → - ∀d,e,des0. des = {d, e} @ des0 → - i1 < d ∧ @⦃i1, des0⦄ ≡ i2 ∨ - d ≤ i1 ∧ @⦃i1 + e, des0⦄ ≡ i2. -#des #i1 #i2 * -des -i1 -i2 -[ #i #d #e #des #H destruct -| #des1 #d1 #e1 #i1 #i2 #Hid1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1 by or_introl, conj/ -| #des1 #d1 #e1 #i1 #i2 #Hdi1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1 by or_intror, conj/ -] -qed-. - -lemma at_inv_cons: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 → - i1 < d ∧ @⦃i1, des⦄ ≡ i2 ∨ - d ≤ i1 ∧ @⦃i1 + e, des⦄ ≡ i2. -/2 width=3 by at_inv_cons_aux/ qed-. - -lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 → - i1 < d → @⦃i1, des⦄ ≡ i2. -#des #d #e #i1 #e2 #H -elim (at_inv_cons … H) -H * // #Hdi1 #_ #Hi1d -lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd -elim (lt_refl_false … Hd) -qed-. - -lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 → - d ≤ i1 → @⦃i1 + e, des⦄ ≡ i2. -#des #d #e #i1 #e2 #H -elim (at_inv_cons … H) -H * // #Hi1d #_ #Hdi1 -lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd -elim (lt_refl_false … Hd) -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_gr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_gr2.ma deleted file mode 100644 index 0c04d5bc5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_gr2.ma +++ /dev/null @@ -1,29 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/multiple/gr2.ma". - -(* GENERIC RELOCATION WITH PAIRS ********************************************) - -(* Main properties **********************************************************) - -theorem at_mono: ∀des,i,i1. @⦃i, des⦄ ≡ i1 → ∀i2. @⦃i, des⦄ ≡ i2 → i1 = i2. -#des #i #i1 #H elim H -des -i -i1 -[ #i #x #H <(at_inv_nil … H) -x // -| #des #d #e #i #i1 #Hid #_ #IHi1 #x #H - lapply (at_inv_cons_lt … H Hid) -H -Hid /2 width=1 by/ -| #des #d #e #i #i1 #Hdi #_ #IHi1 #x #H - lapply (at_inv_cons_ge … H Hdi) -H -Hdi /2 width=1 by/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_minus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_minus.ma deleted file mode 100644 index 4cc93992b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_minus.ma +++ /dev/null @@ -1,76 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/rminus_3.ma". -include "basic_2/multiple/gr2.ma". - -(* GENERIC RELOCATION WITH PAIRS ********************************************) - -inductive minuss: nat → relation (list2 nat nat) ≝ -| minuss_nil: ∀i. minuss i (⟠) (⟠) -| minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 → - minuss i ({d, e} @ des1) ({d - i, e} @ des2) -| minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 → - minuss i ({d, e} @ des1) des2 -. - -interpretation "minus (generic relocation with pairs)" - 'RMinus des1 i des2 = (minuss i des1 des2). - -(* Basic inversion lemmas ***************************************************) - -fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ⟠ → des2 = ⟠. -#des1 #des2 #i * -des1 -des2 -i -[ // -| #des1 #des2 #d #e #i #_ #_ #H destruct -| #des1 #des2 #d #e #i #_ #_ #H destruct -] -qed-. - -lemma minuss_inv_nil1: ∀des2,i. ⟠ ▭ i ≡ des2 → des2 = ⟠. -/2 width=4 by minuss_inv_nil1_aux/ qed-. - -fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → - ∀d,e,des. des1 = {d, e} @ des → - d ≤ i ∧ des ▭ e + i ≡ des2 ∨ - ∃∃des0. i < d & des ▭ i ≡ des0 & - des2 = {d - i, e} @ des0. -#des1 #des2 #i * -des1 -des2 -i -[ #i #d #e #des #H destruct -| #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3 by ex3_intro, or_intror/ -| #des1 #des #d1 #e1 #i1 #Hdi1 #Hdes #d2 #e2 #des2 #H destruct /3 width=1 by or_introl, conj/ -] -qed-. - -lemma minuss_inv_cons1: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 → - d ≤ i ∧ des1 ▭ e + i ≡ des2 ∨ - ∃∃des. i < d & des1 ▭ i ≡ des & - des2 = {d - i, e} @ des. -/2 width=3 by minuss_inv_cons1_aux/ qed-. - -lemma minuss_inv_cons1_ge: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 → - d ≤ i → des1 ▭ e + i ≡ des2. -#des1 #des2 #d #e #i #H -elim (minuss_inv_cons1 … H) -H * // #des #Hid #_ #_ #Hdi -lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi -elim (lt_refl_false … Hi) -qed-. - -lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 → - i < d → - ∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} @ des. -#des1 #des2 #d #e #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/ -#Hdi #_ #Hid lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi -#Hi elim (lt_refl_false … Hi) -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_plus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_plus.ma deleted file mode 100644 index 4c96bfdfb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/gr2_plus.ma +++ /dev/null @@ -1,40 +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/multiple/gr2.ma". - -(* GENERIC RELOCATION WITH PAIRS ********************************************) - -let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with -[ nil2 ⇒ ⟠ -| cons2 d e des ⇒ {d + i, e} @ pluss des i -]. - -interpretation "plus (generic relocation with pairs)" - 'plus x y = (pluss x y). - -(* Basic inversion lemmas ***************************************************) - -lemma pluss_inv_nil2: ∀i,des. des + i = ⟠ → des = ⟠. -#i * // normalize -#d #e #des #H destruct -qed. - -lemma pluss_inv_cons2: ∀i,d,e,des2,des. des + i = {d, e} @ des2 → - ∃∃des1. des1 + i = des2 & des = {d - i, e} @ des1. -#i #d #e #des2 * normalize -[ #H destruct -| #d1 #e1 #des1 #H destruct /2 width=3/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma index 217878d05..67e93078e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma @@ -14,7 +14,7 @@ include "basic_2/notation/relations/rliftstar_3.ma". include "basic_2/substitution/lift.ma". -include "basic_2/multiple/gr2_plus.ma". +include "basic_2/multiple/mr2_plus.ma". (* GENERIC TERM RELOCATION **************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma index efa5038d2..5761094ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/substitution/lift_lift.ma". -include "basic_2/multiple/gr2_minus.ma". +include "basic_2/multiple/mr2_minus.ma". include "basic_2/multiple/lifts.ma". (* GENERIC TERM RELOCATION **************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma new file mode 100644 index 000000000..bf4331b89 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/rat_3.ma". +include "basic_2/grammar/term_vector.ma". + +(* MULTIPLE RELOCATION WITH PAIRS *******************************************) + +inductive at: list2 nat nat → relation nat ≝ +| at_nil: ∀i. at (⟠) i i +| at_lt : ∀des,d,e,i1,i2. i1 < d → + at des i1 i2 → at ({d, e} @ des) i1 i2 +| at_ge : ∀des,d,e,i1,i2. d ≤ i1 → + at des (i1 + e) i2 → at ({d, e} @ des) i1 i2 +. + +interpretation "application (multiple relocation with pairs)" + 'RAt i1 des i2 = (at des i1 i2). + +(* Basic inversion lemmas ***************************************************) + +fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ⟠ → i1 = i2. +#des #i1 #i2 * -des -i1 -i2 +[ // +| #des #d #e #i1 #i2 #_ #_ #H destruct +| #des #d #e #i1 #i2 #_ #_ #H destruct +] +qed-. + +lemma at_inv_nil: ∀i1,i2. @⦃i1, ⟠⦄ ≡ i2 → i1 = i2. +/2 width=3 by at_inv_nil_aux/ qed-. + +fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → + ∀d,e,des0. des = {d, e} @ des0 → + i1 < d ∧ @⦃i1, des0⦄ ≡ i2 ∨ + d ≤ i1 ∧ @⦃i1 + e, des0⦄ ≡ i2. +#des #i1 #i2 * -des -i1 -i2 +[ #i #d #e #des #H destruct +| #des1 #d1 #e1 #i1 #i2 #Hid1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1 by or_introl, conj/ +| #des1 #d1 #e1 #i1 #i2 #Hdi1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1 by or_intror, conj/ +] +qed-. + +lemma at_inv_cons: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 → + i1 < d ∧ @⦃i1, des⦄ ≡ i2 ∨ + d ≤ i1 ∧ @⦃i1 + e, des⦄ ≡ i2. +/2 width=3 by at_inv_cons_aux/ qed-. + +lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 → + i1 < d → @⦃i1, des⦄ ≡ i2. +#des #d #e #i1 #e2 #H +elim (at_inv_cons … H) -H * // #Hdi1 #_ #Hi1d +lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd +elim (lt_refl_false … Hd) +qed-. + +lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 → + d ≤ i1 → @⦃i1 + e, des⦄ ≡ i2. +#des #d #e #i1 #e2 #H +elim (at_inv_cons … H) -H * // #Hi1d #_ #Hdi1 +lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd +elim (lt_refl_false … Hd) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma new file mode 100644 index 000000000..a60ba3956 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma @@ -0,0 +1,76 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/rminus_3.ma". +include "basic_2/multiple/mr2.ma". + +(* MULTIPLE RELOCATION WITH PAIRS *******************************************) + +inductive minuss: nat → relation (list2 nat nat) ≝ +| minuss_nil: ∀i. minuss i (⟠) (⟠) +| minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 → + minuss i ({d, e} @ des1) ({d - i, e} @ des2) +| minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 → + minuss i ({d, e} @ des1) des2 +. + +interpretation "minus (multiple relocation with pairs)" + 'RMinus des1 i des2 = (minuss i des1 des2). + +(* Basic inversion lemmas ***************************************************) + +fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ⟠ → des2 = ⟠. +#des1 #des2 #i * -des1 -des2 -i +[ // +| #des1 #des2 #d #e #i #_ #_ #H destruct +| #des1 #des2 #d #e #i #_ #_ #H destruct +] +qed-. + +lemma minuss_inv_nil1: ∀des2,i. ⟠ ▭ i ≡ des2 → des2 = ⟠. +/2 width=4 by minuss_inv_nil1_aux/ qed-. + +fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → + ∀d,e,des. des1 = {d, e} @ des → + d ≤ i ∧ des ▭ e + i ≡ des2 ∨ + ∃∃des0. i < d & des ▭ i ≡ des0 & + des2 = {d - i, e} @ des0. +#des1 #des2 #i * -des1 -des2 -i +[ #i #d #e #des #H destruct +| #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3 by ex3_intro, or_intror/ +| #des1 #des #d1 #e1 #i1 #Hdi1 #Hdes #d2 #e2 #des2 #H destruct /3 width=1 by or_introl, conj/ +] +qed-. + +lemma minuss_inv_cons1: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 → + d ≤ i ∧ des1 ▭ e + i ≡ des2 ∨ + ∃∃des. i < d & des1 ▭ i ≡ des & + des2 = {d - i, e} @ des. +/2 width=3 by minuss_inv_cons1_aux/ qed-. + +lemma minuss_inv_cons1_ge: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 → + d ≤ i → des1 ▭ e + i ≡ des2. +#des1 #des2 #d #e #i #H +elim (minuss_inv_cons1 … H) -H * // #des #Hid #_ #_ #Hdi +lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi +elim (lt_refl_false … Hi) +qed-. + +lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 → + i < d → + ∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} @ des. +#des1 #des2 #d #e #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/ +#Hdi #_ #Hid lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi +#Hi elim (lt_refl_false … Hi) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_mr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_mr2.ma new file mode 100644 index 000000000..03c660fe0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_mr2.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/multiple/mr2.ma". + +(* MULTIPLE RELOCATION WITH PAIRS *******************************************) + +(* Main properties **********************************************************) + +theorem at_mono: ∀des,i,i1. @⦃i, des⦄ ≡ i1 → ∀i2. @⦃i, des⦄ ≡ i2 → i1 = i2. +#des #i #i1 #H elim H -des -i -i1 +[ #i #x #H <(at_inv_nil … H) -x // +| #des #d #e #i #i1 #Hid #_ #IHi1 #x #H + lapply (at_inv_cons_lt … H Hid) -H -Hid /2 width=1 by/ +| #des #d #e #i #i1 #Hdi #_ #IHi1 #x #H + lapply (at_inv_cons_ge … H Hdi) -H -Hdi /2 width=1 by/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma new file mode 100644 index 000000000..d589181ee --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/multiple/mr2.ma". + +(* MULTIPLE RELOCATION WITH PAIRS *******************************************) + +let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with +[ nil2 ⇒ ⟠ +| cons2 d e des ⇒ {d + i, e} @ pluss des i +]. + +interpretation "plus (multiple relocation with pairs)" + 'plus x y = (pluss x y). + +(* Basic inversion lemmas ***************************************************) + +lemma pluss_inv_nil2: ∀i,des. des + i = ⟠ → des = ⟠. +#i * // normalize +#d #e #des #H destruct +qed. + +lemma pluss_inv_cons2: ∀i,d,e,des2,des. des + i = {d, e} @ des2 → + ∃∃des1. des1 + i = des2 & des = {d - i, e} @ des1. +#i #d #e #des2 * normalize +[ #H destruct +| #d1 #e1 #des1 #H destruct /2 width=3/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index 7a26896f5..07c82f98a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -27,10 +27,14 @@ pp. 53-78]. + + Stage "B" Context-sensitive subject equivalence for native type assignment. + + Stage "A": "Weakening the Applicability Condition" Preservation of stratified native validity for context-sensitive computation on terms. 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 81cd8e41d..b14263c1d 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 @@ -94,7 +94,7 @@ table { [ { "strongly normalizing extended computation" * } { [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ] [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )" "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ] - [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] + [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tsts_vector" + "csx_aaa" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lleq" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ] } ] @@ -111,7 +111,7 @@ table { ] [ { "context-sensitive extended computation" * } { [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] } ] [ { "context-sensitive computation" * } { @@ -119,12 +119,12 @@ table { [ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ] } ] - [ { "local env. ref. for abstract candidates of reducibility" * } { + [ { "local env. ref. for generic reducibility" * } { [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsuba" * ] } ] - [ { "support for abstract computation properties" * } { - [ "acp" "acp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "acp_aaa" * ] + [ { "support for generic computation properties" * } { + [ "gcp" "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ] } ] } @@ -252,8 +252,8 @@ table { [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ] } ] - [ { "support for generic relocation" * } { - [ "gr2 ( @⦃?,?⦄ ≡ ? )" "gr2_plus ( ? + ? )" "gr2_minus ( ? ▭ ? ≡ ? )" "gr2_gr2" * ] + [ { "support for multiple relocation" * } { + [ "mr2 ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" "mr2_mr2" * ] } ] } @@ -298,8 +298,8 @@ table { [ "leq ( ? ⩬[?,?] ? )" "leq_leq" * ] } ] - [ { "same top term constructor" * } { - [ "tstc ( ? ≂ ? )" "tstc_tstc" + "tstc_vector" * ] + [ { "same top term structure" * } { + [ "tsts ( ? ≂ ? )" "tsts_tsts" + "tsts_vector" * ] } ] [ { "closures" * } {