From 7e6643f9ce7ae87e9241aeac5b6d828e9d47fb63 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 4 Jan 2012 16:32:04 +0000 Subject: [PATCH] the support for reducibility candidates evolves ,,,, --- .../lambda_delta/Basic_2/computation/acp.ma | 25 ++++- .../Basic_2/computation/acp_aaa.ma | 50 +++++++--- .../Basic_2/computation/acp_cr.ma | 95 +++++++++++++----- .../lambda_delta/Basic_2/reducibility/tpr.ma | 1 - .../lambda_delta/Basic_2/substitution/lift.ma | 13 +++ .../Basic_2/substitution/lift_vector.ma | 9 ++ .../lambda_delta/Basic_2/unfold/ldrops.ma | 16 ++- .../lambda_delta/Basic_2/unfold/lifts.ma | 98 ++++++++++++++++++- .../Basic_2/unfold/lifts_vector.ma | 42 ++++++++ .../contribs/lambda_delta/Ground_2/list.ma | 8 ++ .../lambda_delta/Ground_2/notation.ma | 2 +- 11 files changed, 314 insertions(+), 45 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma index 437a51c55..9cd2a3fa6 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/ldrop.ma". +include "Basic_2/unfold/ldrops.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) @@ -25,9 +25,30 @@ definition CP2 ≝ λRR:lenv→relation term. λRS:relation term. definition CP3 ≝ λRR:lenv→relation term. λRP:lenv→predicate term. ∀L,V,k. RP L (𝕔{Appl}⋆k.V) → RP L V. +definition CP4 ≝ λRR:lenv→relation term. λRS:relation term. + ∀L0,L,T,T0,d,e. NF … (RR L) RS T → + ⇓[d,e] L0 ≡ L → ⇑[d, e] T ≡ T0 → NF … (RR L0) RS T0. + +definition CP4s ≝ λRR:lenv→relation term. λRS:relation term. + ∀L0,L,des. ⇓[des] L0 ≡ L → + ∀T,T0. ⇑[des] T ≡ T0 → + NF … (RR L) RS T → NF … (RR L0) RS T0. + (* requirements for abstract computation properties *) record acp (RR:lenv->relation term) (RS:relation term) (RP:lenv→predicate term) : Prop ≝ { cp1: CP1 RR RS; cp2: CP2 RR RS; - cp3: CP3 RR RP + cp3: CP3 RR RP; + cp4: CP4 RR RS }. + +(* Basic properties *********************************************************) + +lemma acp_lifts: ∀RR,RS. CP4 RR RS → CP4s RR RS. +#RR #RS #HRR #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=9/ +] +qed. 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 f3863f38b..a47d224d3 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 @@ -14,33 +14,55 @@ include "Basic_2/static/aaa.ma". include "Basic_2/computation/lsubc.ma". +(* +axiom lsubc_ldrops_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,des. ⇓[des] L2 ≡ K2 → + ∃∃K1. ⇓[des] L1 ≡ K1 & K1 [RP] ⊑ K2. +*) +axiom ldrops_lsubc_trans: ∀RP,L1,K1,des. ⇓[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 → + ∃∃L2. L1 [RP] ⊑ L2 & ⇓[des] L2 ≡ K2. + +axiom lifts_trans: ∀T1,T,des1. ⇑[des1] T1 ≡ T → ∀T2:term. ∀des2. ⇑[des2] T ≡ T2 → + ⇑[des1 @ des2] T1 ≡ T2. + +axiom ldrops_trans: ∀L1,L,des1. ⇓[des1] L1 ≡ L → ∀L2,des2. ⇓[des2] L ≡ L2 → + ⇓[des2 @ des1] L1 ≡ L2. (* ABSTRACT COMPUTATION PROPERTIES ******************************************) (* Main propertis ***********************************************************) -axiom aacr_aaa_csubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → - ∀L1,T,A. L1 ⊢ T ÷ A → - ∀L2. L2 [RP] ⊑ L1 → ⦃L2, T⦄ [RP] ϵ 〚A〛. +axiom aacr_aaa_csubc_lifts: ∀RR,RS,RP. + acp RR RS RP → acr RR RS RP (λL,T. RP L T) → + ∀L1,T,A. L1 ⊢ T ÷ A → ∀L0,des. ⇓[des] L0 ≡ L1 → + ∀T0. ⇑[des] T ≡ T0 → ∀L2. L2 [RP] ⊑ L0 → + ⦃L2, T0⦄ [RP] ϵ 〚A〛. (* #RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A -[ #L #k #L2 #HL2 +[ (*#L #k #L2 #HL2 lapply (aacr_acr … H1RP H2RP 𝕒) #HAtom - @(s2 … HAtom … ◊) // /2 width=2/ -| * #L #K #V #B #i #HLK #_ #IHB #L2 #HL2 + @(s2 … HAtom … ◊) // /2 width=2/ *) +| (* * #L #K #V #B #i #HLK #_ #IHB #L2 #HL2 [ | lapply (aacr_acr … H1RP H2RP B) #HB @(s2 … HB … ◊) // - @(cp2 … H1RP) -| #L #V #T #B #A #_ #_ #IHB #IHA #L2 #HL2 +(* @(cp2 … H1RP) *) + ] *) +| (* #L #V #T #B #A #_ #_ #IHB #IHA #L2 #HL2 lapply (aacr_acr … H1RP H2RP A) #HA lapply (aacr_acr … H1RP H2RP B) #HB lapply (s1 … HB) -HB #HB - @(s5 … HA … ◊ ◊) // /3 width=1/ -| #L #W #T #B #A #_ #_ #IHB #IHA #L2 #HL2 - lapply (aacr_acr … H1RP H2RP B) #HB - lapply (s1 … HB) -HB #HB - @(aacr_abst … H1RP H2RP) /3 width=1/ -HB /4 width=3/ + @(s5 … HA … ◊ ◊) // /3 width=1/ *) +| #L #W #T #B #A #_ #_ #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) + [ lapply (aacr_acr … H1RP H2RP B) #HB + @(s1 … HB) /2 width=5/ + | #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)) + /2 width=3/ /3 width=5/ /4 width=6/ + ] | /3 width=1/ | #L #V #T #A #_ #_ #IH1A #IH2A #L2 #HL2 lapply (aacr_acr … H1RP H2RP A) #HA @@ -52,5 +74,5 @@ lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → ∀L,T,A. L ⊢ T ÷ A → RP L T. #RR #RS #RP #H1RP #H2RP #L #T #A #HT lapply (aacr_acr … H1RP H2RP A) #HA -@(s1 … HA) /2 width=4/ +@(s1 … HA) /2 width=8/ qed. 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 c45bc2591..f954ca15b 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 @@ -13,8 +13,7 @@ (**************************************************************************) include "Basic_2/grammar/aarity.ma". -include "Basic_2/grammar/term_simple.ma". -include "Basic_2/substitution/lift_vector.ma". +include "Basic_2/unfold/lifts_vector.ma". include "Basic_2/computation/acp.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) @@ -42,6 +41,10 @@ definition S6 ≝ λRP,C:lenv→predicate term. definition S7 ≝ λC:lenv→predicate term. ∀L1,L2,T1,T2,d,e. C L1 T1 → ⇓[d, e] L2 ≡ L1 → ⇑[d, e] T1 ≡ T2 → C L2 T2. +definition S7s ≝ λC:lenv→predicate term. + ∀L1,L2,des. ⇓[des] L2 ≡ L1 → + ∀T1,T2. ⇑[des] T1 ≡ T2 → C L1 T1 → C L2 T2. + (* properties of the abstract candidate of reducibility *) record acr (RR:lenv->relation term) (RS:relation term) (RP,C:lenv→predicate term) : Prop ≝ { s1: S1 RP C; @@ -56,7 +59,8 @@ record acr (RR:lenv->relation term) (RS:relation term) (RP,C:lenv→predicate te let rec aacr (RP:lenv→predicate term) (A:aarity) (L:lenv) on A: predicate term ≝ λT. match A with [ AAtom ⇒ RP L T -| APair B A ⇒ ∀V. aacr RP B L V → aacr RP A L (𝕔{Appl} V. T) +| APair B A ⇒ ∀L0,V0,T0,des. aacr RP B L0 V0 → ⇓[des] L0 ≡ L → ⇑[des] T ≡ T0 → + aacr RP A L0 (𝕔{Appl} V0. T0) ]. interpretation @@ -65,37 +69,80 @@ interpretation (* Basic properties *********************************************************) +lemma acr_lifts: ∀C. S7 C → S7s C. +#C #HC #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=9/ +] +qed. + +lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) → + ∀des,L0,L,V,V0. ⇓[des] L0 ≡ L → ⇑[des] V ≡ V0 → + RP L V → RP L0 V0. +#RR #RS #RP #HRP #des #L0 #L #V #V0 #HL0 #HV0 #HV +@acr_lifts /width=6/ +@(s7 … HRP) +qed. + +lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) → + ∀des,L0,L,Vs,V0s. ⇑[des] Vs ≡ V0s → ⇓[des] L0 ≡ L → + all … (RP L) Vs → all … (RP L0) V0s. +#RR #RS #RP #HRP #des #L0 #L #Vs #V0s #H elim H -Vs -V0s normalize // +#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s #HL0 * #HT1 #HT1s +@conj /2 width=1/ /2 width=6 by rp_lifts/ +qed. + 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 - lapply (H (⋆0) ?) -H [ @(s2 … IHB … ◊) // /2 width=2/ ] #H - @(cp3 … H1RP … 0) @(s1 … IHA) // -| #L #Vs #HVs #T #H1T #H2T #V #HB - lapply (s1 … IHB … HB) #HV - @(s2 … IHA … (V :: Vs)) // /2 width=1/ -| #L #Vs #V #T #W #HA #HW #V0 #HB - @(s3 … IHA … (V0 :: Vs)) // /2 width=1/ -| #L #V1s #V2s #HV12s #V #T #HA #HV #V1 #HB - elim (lift_total V1 0 1) #V2 #HV12 - @(s5 … IHA … (V1 :: V1s) (V2 :: V2s)) // /2 width=1/ - @HA @(s7 … IHB … HB … HV12) /2 width=1/ -| #L #Vs #T #W #HA #HW #V0 #HB - @(s6 … IHA … (V0 :: Vs)) // /2 width=1/ -| #L1 #L2 #T1 #T2 #d #e #HA #HL21 #HT12 #V2 #HB - @(s7 … IHA … HL21) [2: @HA [2: + lapply (H ? (⋆0) ? ⟠ ? ? ?) -H + [1,3: // |2,4: skip + | @(s2 … IHB … ◊) // /2 width=2/ + | #H @(cp3 … H1RP … 0) @(s1 … IHA) // + ] +| #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H + elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct + lapply (s1 … IHB … HB) #HV0 + @(s2 … IHA … (V0 :: V0s)) /2 width=4 by lifts_simple_dx/ /3 width=6/ +| #L #Vs #U #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct + elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct + @(s3 … IHA … (V0 :: V0s)) /2 width=6 by rp_lifts/ /4 width=5/ +| #L #V1s #V2s #HV12s #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H + elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct + elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct + elim (lift_total V10 0 1) #V20 #HV120 + elim (liftv_total 0 1 V10s) #V20s #HV120s + @(s5 … IHA … (V10 :: V10s) (V20 :: V20s)) /2 width=1/ /2 width=6 by rp_lifts/ + @(HA … (ss des)) /2 width=1/ + [ @(s7 … IHB … HB … HV120) /2 width=1/ + | @liftsv_applv // + ] +| #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct + @(s6 … IHA … (V0 :: V0s)) /2 width=6 by rp_lifts/ /3 width=4/ +| /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 → - (∀V. ⦃L, V⦄ [RP] ϵ 〚B〛 → ⦃L. 𝕓{Abbr}V, T⦄ [RP] ϵ 〚A〛) → - ⦃L, 𝕓{Abst}W. T⦄ [RP] ϵ 〚𝕔B. A〛. -#RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #V #HB + ∀L,W,T,A,B. RP L W → ( + ∀L0,V0,T0,des. ⇓[des] L0 ≡ L → ⇑[ss des] T ≡ T0 → + ⦃L0, V0⦄ [RP] ϵ 〚B〛→ ⦃L0. 𝕓{Abbr} V0, T0⦄ [RP] ϵ 〚A〛 + ) → + ⦃L, 𝕓{Abst} W. T⦄ [RP] ϵ 〚𝕔 B. A〛. +#RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H lapply (aacr_acr … H1RP H2RP A) #HCA lapply (aacr_acr … H1RP H2RP B) #HCB -lapply (s1 … HCB) -HCB #HCB -@(s3 … HCA … ◊) // @(s5 … HCA … ◊ ◊) // /2 width=1/ +elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct +lapply (s1 … HCB) -HCB #HCB +@(s3 … HCA … ◊) /2 width=6 by rp_lifts/ +@(s5 … HCA … ◊ ◊) // /2 width=1/ /2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma index 4769a39dc..57a619fa5 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term_simple.ma". include "Basic_2/substitution/tps.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma index 9e6b261c8..0e0e6a748 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "Basic_2/grammar/term_weight.ma". +include "Basic_2/grammar/term_simple.ma". (* RELOCATION ***************************************************************) @@ -270,6 +271,18 @@ lemma tw_lift: ∀d,e,T1,T2. ⇑[d, e] T1 ≡ T2 → #[T1] = #[T2]. #d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize // qed-. +lemma lift_simple_dx: ∀d,e,T1,T2. ⇑[d, e] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2]. +#d #e #T1 #T2 #H elim H -d -e -T1 -T2 // +#I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H +elim (simple_inv_bind … H) +qed-. + +lemma lift_simple_sn: ∀d,e,T1,T2. ⇑[d, e] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1]. +#d #e #T1 #T2 #H elim H -d -e -T1 -T2 // +#I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H +elim (simple_inv_bind … H) +qed-. + (* Basic properties *********************************************************) (* Basic_1: was: lift_lref_gt *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma index 91b03c0b9..2f7c9bbc5 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma @@ -26,3 +26,12 @@ inductive liftv (d,e:nat) : relation (list term) ≝ interpretation "relocation (vector)" 'RLift d e T1s T2s = (liftv d e T1s T2s). +(* Basic properties *********************************************************) + +lemma liftv_total: ∀d,e. ∀T1s:list term. ∃T2s. ⇑[d, e] T1s ≡ T2s. +#d #e #T1s elim T1s -T1s +[ /2 width=2/ +| #T1 #T1s * #T2s #HT12s + elim (lift_total T1 d e) /3 width=2/ +] +qed-. 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 c6bb67e79..896415581 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma @@ -20,8 +20,20 @@ include "Basic_2/unfold/lifts.ma". inductive ldrops: list2 nat nat → relation lenv ≝ | ldrops_nil : ∀L. ldrops ⟠ L L | ldrops_cons: ∀L1,L,L2,des,d,e. - ⇓[d,e] L1 ≡ L → ldrops des L L2 → ldrops ({d, e} :: des) L1 L2 + ldrops des L1 L → ⇓[d,e] L ≡ L2 → ldrops ({d, e} :: des) L1 L2 . interpretation "generic local environment slicing" - 'RDrop des T1 T2 = (ldrops des T1 T2). + 'RLDrop des T1 T2 = (ldrops des T1 T2). + +(* Basic properties *********************************************************) + +lemma ldrops_skip: ∀L1,L2,des. ⇓[des] L1 ≡ L2 → ∀V1,V2. ⇑[des] V2 ≡ V1 → + ∀I. ⇓[ss des] L1. 𝕓{I} V1 ≡ L2. 𝕓{I} V2. +#L1 #L2 #des #H elim H -L1 -L2 -des +[ #L #V1 #V2 #HV12 #I + >(lifts_inv_nil … HV12) -HV12 // +| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #V1 #V2 #H #I + elim (lifts_inv_cons … H) -H /3 width=5/ +]. +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma index 9994f44a2..43859f108 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma @@ -12,10 +12,16 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/lift_vector.ma". +include "Basic_2/grammar/term_vector.ma". +include "Basic_2/substitution/lift.ma". (* GENERIC RELOCATION *******************************************************) +let rec ss (des:list2 nat nat) ≝ match des with +[ nil2 ⇒ ⟠ +| cons2 d e des ⇒ {d + 1, e} :: ss des +]. + inductive lifts: list2 nat nat → relation term ≝ | lifts_nil : ∀T. lifts ⟠ T T | lifts_cons: ∀T1,T,T2,des,d,e. @@ -23,3 +29,93 @@ inductive lifts: list2 nat nat → relation term ≝ . interpretation "generic relocation" 'RLift des T1 T2 = (lifts des T1 T2). + +(* Basic inversion lemmas ***************************************************) + +fact lifts_inv_nil_aux: ∀T1,T2,des. ⇑[des] T1 ≡ T2 → des = ⟠ → T1 = T2. +#T1 #T2 #des * -T1 -T2 -des // +#T1 #T #T2 #d #e #des #_ #_ #H destruct +qed. + +lemma lifts_inv_nil: ∀T1,T2. ⇑[⟠] T1 ≡ T2 → T1 = T2. +/2 width=3/ qed-. + +fact lifts_inv_cons_aux: ∀T1,T2,des. ⇑[des] T1 ≡ T2 → + ∀d,e,tl. des = {d, e} :: tl → + ∃∃T. ⇑[d, e] T1 ≡ T & ⇑[tl] T ≡ T2. +#T1 #T2 #des * -T1 -T2 -des +[ #T #d #e #tl #H destruct +| #T1 #T #T2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct + /2 width=3/ +qed. + +lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇑[{d, e} :: des] T1 ≡ T2 → + ∃∃T. ⇑[d, e] T1 ≡ T & ⇑[des] T ≡ T2. +/2 width=3/ qed-. + +lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇑[des] 𝕓{I} V1. U1 ≡ T2 → + ∃∃V2,U2. ⇑[des] V1 ≡ V2 & ⇑[ss des] U1 ≡ U2 & + T2 = 𝕓{I} V2. U2. +#I #T2 #des elim des -des +[ #V1 #U1 #H + <(lifts_inv_nil … H) -H /2 width=5/ +| #d #e #des #IHdes #V1 #U1 #H + elim (lifts_inv_cons … H) -H #X #H #HT2 + elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct + elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct + /3 width=5/ +] +qed-. + +lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇑[des] 𝕗{I} V1. U1 ≡ T2 → + ∃∃V2,U2. ⇑[des] V1 ≡ V2 & ⇑[des] U1 ≡ U2 & + T2 = 𝕗{I} V2. U2. +#I #T2 #des elim des -des +[ #V1 #U1 #H + <(lifts_inv_nil … H) -H /2 width=5/ +| #d #e #des #IHdes #V1 #U1 #H + elim (lifts_inv_cons … H) -H #X #H #HT2 + elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct + elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct + /3 width=5/ +] +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lifts_simple_dx: ∀T1,T2,des. ⇑[des] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2]. +#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/ +qed-. + +lemma lifts_simple_sn: ∀T1,T2,des. ⇑[des] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1]. +#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/ +qed-. + +(* Basic properties *********************************************************) + +lemma lifts_bind: ∀I,T2,V1,V2,des. ⇑[des] V1 ≡ V2 → + ∀T1. ⇑[ss des] T1 ≡ T2 → + ⇑[des] 𝕓{I} V1. T1 ≡ 𝕓{I} V2. T2. +#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des +[ #V #T1 #H >(lifts_inv_nil … H) -H // +| #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H + elim (lifts_inv_cons … H) -H /3 width=3/ +] +qed. + +lemma lifts_flat: ∀I,T2,V1,V2,des. ⇑[des] V1 ≡ V2 → + ∀T1. ⇑[des] T1 ≡ T2 → + ⇑[des] 𝕗{I} V1. T1 ≡ 𝕗{I} V2. T2. +#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des +[ #V #T1 #H >(lifts_inv_nil … H) -H // +| #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H + elim (lifts_inv_cons … H) -H /3 width=3/ +] +qed. + +lemma lifts_total: ∀des,T1. ∃T2. ⇑[des] T1 ≡ T2. +#des elim des -des /2 width=2/ +#d #e #des #IH #T1 +elim (lift_total T1 d e) #T #HT1 +elim (IH T) -IH /3 width=4/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma new file mode 100644 index 000000000..a40736142 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/lift_vector.ma". +include "Basic_2/unfold/lifts.ma". + +(* GENERIC RELOCATION *******************************************************) + +inductive liftsv (des:list2 nat nat) : relation (list term) ≝ +| liftsv_nil : liftsv des ◊ ◊ +| liftsv_cons: ∀T1s,T2s,T1,T2. + ⇑[des] T1 ≡ T2 → liftsv des T1s T2s → + liftsv des (T1 :: T1s) (T2 :: T2s) +. + +interpretation "generic relocation (vector)" + 'RLift des T1s T2s = (liftsv des T1s T2s). + +(* Basic inversion lemmas ***************************************************) + +axiom lifts_inv_applv1: ∀V1s,U1,T2,des. ⇑[des] Ⓐ V1s. U1 ≡ T2 → + ∃∃V2s,U2. ⇑[des] V1s ≡ V2s & ⇑[des] U1 ≡ U2 & + T2 = Ⓐ V2s. U2. + +(* Basic properties *********************************************************) + +lemma liftsv_applv: ∀V1s,V2s,des. ⇑[des] V1s ≡ V2s → + ∀T1,T2. ⇑[des] T1 ≡ T2 → + ⇑[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2. +#V1s #V2s #des #H elim H -V1s -V2s // /3 width=1/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Ground_2/list.ma b/matita/matita/contribs/lambda_delta/Ground_2/list.ma index 78a2305ea..09a52f57d 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/list.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/list.ma @@ -37,3 +37,11 @@ inductive list2 (A1,A2:Type[0]) : Type[0] := interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?). (**) (* 'Nil causes unification error in aacr_abst *) interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl). + +let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with +[ nil2 ⇒ l2 +| cons2 a1 a2 tl ⇒ {a1, a2} :: append2 A1 A2 tl l2 +]. + +interpretation "append (list of pairs)" + 'Append l1 l2 = (append2 ? ? l1 l2). diff --git a/matita/matita/contribs/lambda_delta/Ground_2/notation.ma b/matita/matita/contribs/lambda_delta/Ground_2/notation.ma index 0703963d2..71fbbe0c2 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/notation.ma @@ -33,5 +33,5 @@ notation "hvbox( ⟠ )" for @{'Nil2}. notation "hvbox( { hd1 , break hd2 } :: break tl )" - non associative with precedence 45 + non associative with precedence 47 for @{'Cons $hd1 $hd2 $tl}. -- 2.39.2