From 9ed13b93cd1d7d75d65f1f063b6b4bf27d863f72 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 27 Apr 2014 17:34:22 +0000 Subject: [PATCH] reordering abstract computation properties and saturation conditions --- .../lambdadelta/basic_2/computation/acp.ma | 24 ++++++------ .../basic_2/computation/acp_aaa.ma | 2 +- .../lambdadelta/basic_2/computation/acp_cr.ma | 38 +++++++++---------- .../basic_2/computation/csx_lift.ma | 4 +- .../basic_2/computation/csx_tstc_vector.ma | 6 +-- .../basic_2/computation/lsubc_ldrop.ma | 4 +- 6 files changed, 39 insertions(+), 39 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma index 5de150697..7830fa7c0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma @@ -17,36 +17,36 @@ include "basic_2/substitution/ldrops.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) -definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term. - ∀G,L. ∃k. NF … (RR G L) RS (⋆k). - -definition CP2 ≝ λRR:relation4 genv lenv term term. λRS:relation 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 CP2s ≝ λRR:relation4 genv lenv term term. λRS:relation term. +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 CP3 ≝ λRP:relation3 genv lenv term. +definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term. + ∀G,L. ∃k. NF … (RR G L) RS (⋆k). + +definition CP2 ≝ λRP:relation3 genv lenv term. ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T. -definition CP4 ≝ λRP:relation3 genv lenv term. +definition CP3 ≝ λRP:relation3 genv lenv term. ∀G,L,W,T. RP G L W → RP G L T → RP G L (ⓝW.T). (* requirements for abstract computation properties *) record acp (RR:relation4 genv lenv term term) (RS:relation term) (RP:relation3 genv lenv term) : Prop ≝ -{ cp1: CP1 RR RS; - cp2: CP2 RR RS; - cp3: CP3 RP; - cp4: CP4 RP +{ cp0: CP0 RR RS; + cp1: CP1 RR RS; + cp2: CP2 RP; + cp3: CP3 RP }. (* Basic properties *********************************************************) (* Basic_1: was: nf2_lift1 *) -lemma acp_lifts: ∀RR,RS. CP2 RR RS → CP2s RR RS. +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 // diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma index fc54854ce..13fbb93fe 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma @@ -54,7 +54,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. 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 … (◊)) [ @(s8 … HB … HKV2A) // | @(s8 … HB … H1KV0A) // ] + @(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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma index fa9508a28..7c6464f21 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma @@ -21,6 +21,13 @@ include "basic_2/computation/acp.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) +definition S0 ≝ λC:relation3 genv lenv term. ∀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:relation3 genv lenv term. + ∀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:relation3 genv lenv term. ∀G,L,T. C G L T → RP G L T. @@ -49,23 +56,16 @@ definition S6 ≝ λRP,C:relation3 genv lenv term. definition S7 ≝ λC:relation3 genv lenv term. ∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T). -definition S8 ≝ λC:relation3 genv lenv term. ∀G,L2,L1,T1,d,e. - C G L1 T1 → ∀T2. ⇩[Ⓕ, d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2. - -definition S8s ≝ λC:relation3 genv lenv term. - ∀G,L1,L2,des. ⇩*[Ⓕ, des] L2 ≡ L1 → - ∀T1,T2. ⇧*[des] T1 ≡ T2 → C G L1 T1 → C G L2 T2. - (* properties of the abstract candidate of reducibility *) record acr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:relation3 genv lenv term) : Prop ≝ -{ s1: S1 RP C; +{ 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; - s8: S8 C + s7: S7 C }. (* the abstract candidate of reducibility associated to an atomic arity *) @@ -84,7 +84,7 @@ interpretation (* Basic properties *********************************************************) (* Basic_1: was: sc3_lift1 *) -lemma acr_lifts: ∀C. S8 C → S8s C. +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 @@ -97,7 +97,7 @@ lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) → 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/ -@(s8 … HRP) +@(s0 … HRP) qed. (* Basic_1: was only: sns3_lifts1 *) @@ -115,18 +115,19 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) ∀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 -[ #G #L #T #H +[ /3 width=7 by ldrops_cons, lifts_cons/ +| #G #L #T #H elim (cp1 … H1RP G L) #k #HK lapply (H ? (⋆k) ? (⟠) ? ? ?) -H [1,3: // |2,4: skip | @(s2 … IHB … (◊)) // - | #H @(cp3 … H1RP … k) @(s1 … IHA) // + | #H @(cp2 … H1RP … k) @(s1 … IHA) // ] | #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct lapply (s1 … IHB … HB) #HV0 @(s2 … IHA … (V0 @ V0s)) - /3 width=14 by rp_liftsv_all, acp_lifts, cp2, lifts_simple_dx, conj/ + /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 #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct @@ -154,7 +155,7 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) 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 ldrops_skip/ - [ @(s8 … IHB … HB … HV120) /2 width=2 by ldrop_drop/ + [ @(s0 … IHB … HB … HV120) /2 width=2 by ldrop_drop/ | @lifts_applv // elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s >(liftv_mono … HV12s … HV10s) -V1s // @@ -163,7 +164,6 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) 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/ -| /3 width=7 by ldrops_cons, lifts_cons/ ] qed. @@ -177,12 +177,12 @@ lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) 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 [ @(s8 … HCB) ] #HW0 +lapply (acr_lifts … HL0 … HW0 HW) -HW [ @(s0 … HCB) ] #HW0 @(s3 … HCA … (◊)) @(s6 … HCA … (◊) (◊)) // [ @(HA … HL0) // | lapply (s1 … HCB) -HCB #HCB - @(cp4 … H1RP) /2 width=1 by/ + @(cp3 … H1RP) /2 width=1 by/ ] qed. 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 3ae4bfad0..2d74a929e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma @@ -111,8 +111,8 @@ qed-. theorem csx_acp: ∀h,g. acp (cpx h g) (eq …) (csx h g). #h #g @mk_acp -[ #G #L elim (deg_total h g 0) /3 width=8 by cnx_sort_iter, ex_intro/ -| /3 width=13 by cnx_lift/ +[ /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/ | /2 width=1 by csx_cast/ ] 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 index 5e9ea06c7..5ce3e142a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma @@ -118,12 +118,12 @@ qed. theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (λG,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T). #h #g @mk_acr // -[ /3 width=1 by csx_applv_cnx/ -|2,3,6: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/ +[ /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 // -| /2 width=8 by csx_lift/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma index 2b8133bda..8680fe4f1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma @@ -64,8 +64,8 @@ lemma ldrop_lsubc_trans: ∀RR,RS,RP. 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 (s8 … HA … HV2 … HLK1 HV3) -HV2 - lapply (s8 … HA … H1W2 … HLK1 HW23) -H1W2 + lapply (s0 … HA … HV2 … HLK1 HV3) -HV2 + lapply (s0 … HA … H1W2 … HLK1 HW23) -H1W2 /4 width=11 by lsubc_abbr, aaa_lift, ldrop_skip, ex2_intro/ ] ] -- 2.39.2