From d833e40ce45e301a01ddd9ea66c29fb2b34bb685 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 19 Jan 2012 16:10:12 +0000 Subject: [PATCH] closure property S4 added to abstract candidates of reducibility ... --- .../Basic_2/computation/acp_aaa.ma | 42 +++++++++++---- .../Basic_2/computation/acp_cr.ma | 10 +++- .../lambda_delta/Basic_2/computation/lsubc.ma | 23 +++++++- .../lambda_delta/Basic_2/unfold/gr2_gr2.ma | 21 ++++++++ .../lambda_delta/Basic_2/unfold/ldrops.ma | 52 ++++++++++++++++--- 5 files changed, 125 insertions(+), 23 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma index 002fe0171..38baa9fb9 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "Basic_2/unfold/gr2_gr2.ma". include "Basic_2/unfold/lifts_lifts.ma". include "Basic_2/unfold/ldrops_ldrops.ma". include "Basic_2/static/aaa.ma". @@ -39,17 +40,36 @@ axiom aacr_aaa_csubc_lifts: ∀RR,RS,RP. >(lifts_inv_sort1 … H) -H lapply (aacr_acr … H1RP H2RP 𝕒) #HAtom @(s2 … HAtom … ◊) // /2 width=2/ -| * #L #K #V #B #i #HLK #_ #IHB #L0 #des #HL0 #X #H #L2 #HL20 - elim (lifts_inv_lref1 … H) -H #i0 #Hi0 #H destruct - elim (ldrops_ldrop_trans … HL0 … HLK) -L #L #des1 #i1 #HL0 #HLK #Hi1 #Hdes1 - - elim (lsubc_ldrop_trans … HL20 … HL0) -L0 #L0 #HL20 #HL0 - [ - | lapply (aacr_acr … H1RP H2RP B) #HB - @(s2 … HB … ◊) // - @(cp2 … H1RP) +| #I #L1 #K1 #V1 #B #i #HLK1 #_ #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 (ldrop_fwd_ldrop2 … HLK1) #HK1b + elim (ldrops_ldrop_trans … HL01 … HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hdes1 + >(at_mono … Hi1 … Hi0) -i1 + elim (ldrops_inv_skip2 … Hdes1 … H) -des1 #K0 #V0 #des0 #Hdes0 #HK01 #HV10 #H destruct + elim (lsubc_ldrop_trans … HL20 … HL0) -HL0 #X #HLK2 #H + elim (lift_total V0 0 (i0 +1)) #V #HV0 + elim (lsubc_inv_pair2 … H) -H * + [ #K2 #HK20 #H destruct + generalize in match HLK2; generalize in match I; -HLK2 -I * #HLK2 + [ @(s4 … HB … ◊ … HV0 HLK2) + @(IHB … HL20) [2: /2 width=6/ | skip ] + | skip + ] +(⇧*[des0]V1≡V0) → (⇧[O,i0+1]V0≡V) → (@[i]des≡i0) → (des+1▭i+1≡des0+1) → +⇧*[{O,i+1}::des]V1≡V) + + Theorem lift1_free: (hds:?; i:?; t:?) + (lift1 hds (lift (S i) (0) t)) = + (lift (S (trans hds i)) (0) (lift1 (ptrans hds i) t)). + + + + + | @(s2 … HB … ◊) // /2 width=3/ + ] + | #K2 #V2 #A2 #HV2 #HV0 #HK20 #H1 #H2 destruct ] - | #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 @@ -64,7 +84,7 @@ axiom aacr_aaa_csubc_lifts: ∀RR,RS,RP. | #L3 #V3 #T3 #des3 #HL32 #HT03 #HB elim (lifts_total des3 W0) #W2 #HW02 elim (ldrops_lsubc_trans … HL32 … HL02) -L2 #L2 #HL32 #HL20 - @(IHA (L2. 𝕓{Abst} W2) … (ss des @ ss des3)) + @(IHA (L2. 𝕓{Abst} W2) … (des + 1 @ des3 + 1)) /2 width=3/ /3 width=5/ /4 width=6/ ] | #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma index cad6aba67..9908cfd16 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma @@ -31,6 +31,10 @@ definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→p definition S3 ≝ λRP,C:lenv→predicate term. ∀L,Vs,V,T,W. C L (ⒶVs. 𝕔{Abbr}V. T) → RP L W → C L (ⒶVs. 𝕔{Appl}V. 𝕔{Abst}W. T). +definition S4 ≝ λRP,C:lenv→predicate term. ∀L,K,Vs,V1,V2,i. + C L (ⒶVs. V2) → ⇧[0, i + 1] V1 ≡ V2 → + ⇩[0, i] L ≡ K. 𝕓{Abbr} V1 → C L (Ⓐ Vs. #i). + definition S5 ≝ λRP,C:lenv→predicate term. ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → ∀V,T. C (L. 𝕓{Abbr}V) (ⒶV2s. T) → RP L V → C L (ⒶV1s. 𝕔{Abbr}V. T). @@ -50,6 +54,7 @@ record acr (RR:lenv->relation term) (RS:relation term) (RP,C:lenv→predicate te { s1: S1 RP C; s2: S2 RR RS RP C; s3: S3 RP C; + s4: S4 RP C; s5: S5 RP C; s6: S6 RP C; s7: S7 C @@ -94,8 +99,9 @@ lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) → @conj /2 width=1/ /2 width=6 by rp_lifts/ qed. -lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → +axiom aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP 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 [ #L #T #H @@ -132,7 +138,7 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → | /3 width=7/ ] qed. - +*) lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → ∀L,W,T,A,B. RP L W → ( ∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des + 1] T ≡ T0 → diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma index 60320a22a..b145a55e1 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma @@ -27,10 +27,29 @@ interpretation "local environment refinement (abstract candidates of reducibility)" 'CrSubEq L1 RP L2 = (lsubc RP L1 L2). +(* Basic inversion lemmas ***************************************************) + +fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K2,W. L2 = K2. 𝕓{I} W → + (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. 𝕓{I} W) ∨ + ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & ⦃K2, W⦄ [RP] ϵ 〚A〛 & + K1 [RP] ⊑ K2 & L1 = K1. 𝕓{Abbr} V & + I = Abst. +#RP #L1 #L2 * -L1 -L2 +[ #I #K2 #W #H destruct +| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/ +| #L1 #L2 #V1 #W2 #A #H #HV1 #HW2 #I #K2 #W #H destruct /3 width=7/ +] +qed. + +lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 [RP] ⊑ K2. 𝕓{I} W → + (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. 𝕓{I} W) ∨ + ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & ⦃K2, W⦄ [RP] ϵ 〚A〛 & + K1 [RP] ⊑ K2 & L1 = K1. 𝕓{Abbr} V & + I = Abst. +/2 width=3/ qed-. + (* Basic properties *********************************************************) lemma lsubc_refl: ∀RP,L. L [RP] ⊑ L. #RP #L elim L -L // /2 width=1/ qed. - -(* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma new file mode 100644 index 000000000..dd2d34d07 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma @@ -0,0 +1,21 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/gr2.ma". + +(* GENERIC RELOCATION WITH PAIRS ********************************************) + +(* Main properties **********************************************************) + +axiom at_mono: ∀des,i,i1. @[i] des ≡ i1 → ∀i2. @[i] des ≡ i2 → i1 = i2. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma index 1bf80b5be..254006f1c 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma @@ -26,6 +26,50 @@ inductive ldrops: list2 nat nat → relation lenv ≝ interpretation "generic local environment slicing" 'RDropStar des T1 T2 = (ldrops des T1 T2). +(* Basic inversion lemmas ***************************************************) + +fact ldrops_inv_nil_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → des = ⟠ → L1 = L2. +#L1 #L2 #des * -L1 -L2 -des // +#L1 #L #L2 #d #e #des #_ #_ #H destruct +qed. + +lemma ldrops_inv_nil: ∀L1,L2. ⇩*[⟠] L1 ≡ L2 → L1 = L2. +/2 width=3/ qed-. + +fact ldrops_inv_cons_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → + ∀d,e,tl. des = {d, e} :: tl → + ∃∃L. ⇩*[tl] L1 ≡ L & ⇩[d, e] L ≡ L2. +#L1 #L2 #des * -L1 -L2 -des +[ #L #d #e #tl #H destruct +| #L1 #L #L2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct + /2 width=3/ +qed. + +lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} :: des] L1 ≡ L2 → + ∃∃L. ⇩*[des] L1 ≡ L & ⇩[d, e] L ≡ L2. +/2 width=3/ qed-. + +lemma ldrops_inv_skip2: ∀I,des,i,des2. des ▭ i ≡ des2 → + ∀L1,K2,V2. ⇩*[des2] L1 ≡ K2. 𝕓{I} V2 → + ∃∃K1,V1,des1. des + 1 ▭ i + 1 ≡ des1 + 1 & + ⇩*[des1] K1 ≡ K2 & + ⇧*[des1] V2 ≡ V1 & + L1 = K1. 𝕓{I} V1. +#I #des #i #des2 #H elim H -des -i -des2 +[ #i #L1 #K2 #V2 #H + >(ldrops_inv_nil … H) -L1 /2 width=7/ +| #des #des2 #d #e #i #Hid #_ #IHdes2 #L1 #K2 #V2 #H + elim (ldrops_inv_cons … H) -H #L #HL1 #H + elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ #K #V >minus_plus #HK2 #HV2 #H destruct + elim (IHdes2 … HL1) -IHdes2 -HL1 #K1 #V1 #des1 #Hdes1 #HK1 #HV1 #X destruct + @(ex4_3_intro … K1 V1 … ) // [3,4: /2 width=7/ | skip ] + normalize >plus_minus // @minuss_lt // /2 width=1/ (**) (* explicit constructors, /3 width=1/ is a bit slow *) +| #des #des2 #d #e #i #Hid #_ #IHdes2 #L1 #K2 #V2 #H + elim (IHdes2 … H) -IHdes2 -H #K1 #V1 #des1 #Hdes1 #HK1 #HV1 #X destruct + /4 width=7/ +] +qed-. + (* Basic properties *********************************************************) lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 → @@ -40,11 +84,3 @@ qed. (* Basic_1: removed theorems 1: drop1_getl_trans *) -(* -lemma ldrops_inv_skip2: ∀des2,L1,I,K2,V2. ⇩*[des2] L1 ≡ K2. 𝕓{I} V2 → - ∀des,i. des ▭ i ≡ des2 → - ∃∃K1,V1,des1. des ▭ (i + 1) ≡ des1 & - ⇩*[des1] K1 ≡ K2 & - ⇧*[des1] V2 ≡ V1 & - L1 = K1. 𝕓{I} V1. -*) \ No newline at end of file -- 2.39.2