From 0aa60d67f17b528b896e05bbd01038cbc195f69d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 25 Dec 2011 19:47:29 +0000 Subject: [PATCH] - support for candidates of reducibility continues ... - change in the notation of relatiional relocation and local env. slicing, to allow more usual notation for functional relocation (not working yet) --- .../lambda_delta/Basic_2/computation/acp.ma | 33 +++++++ .../Basic_2/computation/acp_aaa.ma | 56 ++++++++++++ .../Basic_2/computation/acp_cr.ma | 86 ++++++++++++++++-- .../lambda_delta/Basic_2/computation/csn.ma | 5 ++ .../computation/{csn_aarity.ma => csn_aaa.ma} | 15 ++-- .../Basic_2/computation/csn_cr.ma | 7 +- .../lambda_delta/Basic_2/computation/lsubc.ma | 16 ++-- .../lambda_delta/Basic_2/functional/lift.ma | 6 +- .../lambda_delta/Basic_2/functional/subst.ma | 9 +- .../Basic_2/grammar/term_vector.ma | 25 ++++++ .../contribs/lambda_delta/Basic_2/notation.ma | 28 +++--- .../Basic_2/reducibility/cpr_lift.ma | 18 ++-- .../Basic_2/reducibility/ltpr_ldrop.ma | 8 +- .../lambda_delta/Basic_2/reducibility/tpr.ma | 22 ++--- .../Basic_2/reducibility/tpr_lift.ma | 6 +- .../Basic_2/reducibility/tpr_tpr.ma | 8 +- .../lambda_delta/Basic_2/static/aaa.ma | 4 +- .../Basic_2/substitution/gdrop.ma | 13 +-- .../Basic_2/substitution/ldrop.ma | 70 +++++++-------- .../Basic_2/substitution/ldrop_ldrop.ma | 36 ++++---- .../lambda_delta/Basic_2/substitution/lift.ma | 90 +++++++++---------- .../Basic_2/substitution/lift_lift.ma | 34 +++---- .../lsubcs.ma => substitution/lift_vector.ma} | 23 +++-- .../Basic_2/substitution/ltps_ldrop.ma | 24 ++--- .../lambda_delta/Basic_2/substitution/tps.ma | 18 ++-- .../Basic_2/substitution/tps_lift.ma | 38 ++++---- .../lambda_delta/Basic_2/unfold/delift.ma | 2 +- .../Basic_2/unfold/delift_lift.ma | 4 +- .../Basic_2/unfold/ltpss_ldrop.ma | 24 ++--- .../lambda_delta/Basic_2/unfold/tpss_lift.ma | 44 ++++----- .../lambda_delta/Basic_2/unfold/tpss_tpss.ma | 4 +- .../contribs/lambda_delta/Ground_2/list.ma | 10 +-- .../lambda_delta/Ground_2/notation.ma | 4 + 33 files changed, 491 insertions(+), 299 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma rename matita/matita/contribs/lambda_delta/Basic_2/computation/{csn_aarity.ma => csn_aaa.ma} (75%) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma rename matita/matita/contribs/lambda_delta/Basic_2/{computation/lsubcs.ma => substitution/lift_vector.ma} (67%) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma new file mode 100644 index 000000000..437a51c55 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ldrop.ma". + +(* ABSTRACT COMPUTATION PROPERTIES ******************************************) + +definition CP1 ≝ λRR:lenv→relation term. λRS:relation term. + ∀L,k. NF … (RR L) RS (⋆k). + +definition CP2 ≝ λRR:lenv→relation term. λRS:relation term. + ∀L,K,W,i. ⇓[0,i] L ≡ K. 𝕓{Abst} W → NF … (RR L) RS (#i). + +definition CP3 ≝ λRR:lenv→relation term. λRP:lenv→predicate term. + ∀L,V,k. RP L (𝕔{Appl}⋆k.V) → RP L V. + +(* requirements for abstract computation properties *) +record acp (RR:lenv->relation term) (RS:relation term) (RP:lenv→predicate term) : Prop ≝ +{ cp1: CP1 RR RS; + cp2: CP2 RR RS; + cp3: CP3 RR RP +}. 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 new file mode 100644 index 000000000..537d5b235 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/aaa.ma". +include "Basic_2/computation/lsubc.ma". + +(* 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〛. +(* +#RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A +[ #L #k #L2 #HL2 + lapply (aacr_acr … H1RP H2RP 𝕒) #HAtom + @(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 + 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/ +| /3 width=1/ +| #L #V #T #A #_ #_ #IH1A #IH2A #L2 #HL2 + lapply (aacr_acr … H1RP H2RP A) #HA + lapply (s1 … HA) #H + @(s6 … HA … ◊) /2 width=1/ /3 width=1/ +] +*) +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/ +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 449dd7b69..699d997dd 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,17 +13,89 @@ (**************************************************************************) include "Basic_2/grammar/aarity.ma". -include "Basic_2/grammar/lenv.ma". +include "Basic_2/grammar/term_simple.ma". +include "Basic_2/substitution/lift_vector.ma". +include "Basic_2/computation/acp.ma". -(* ABSTRACT CANDIDATES OF REDUCIBILITY **************************************) +(* ABSTRACT COMPUTATION PROPERTIES ******************************************) + +(* Note: this is Girard's CR1 *) +definition S1 ≝ λRP,C:lenv→predicate term. + ∀L,T. C L T → RP L T. + +(* Note: this is Tait's iii, or Girard's CR4 *) +definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→predicate term. + ∀L,Vs. all … (RP L) Vs → + ∀T. 𝕊[T] → NF … (RR L) RS T → C L (ⒶVs.T). + +(* Note: this is Tait's ii *) +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 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). + +definition S6 ≝ λRP,C:lenv→predicate term. + ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. 𝕔{Cast}W. T). + +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. + +(* 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; + s2: S2 RR RS RP C; + s3: S3 RP C; + s5: S5 RP C; + s6: S6 RP C; + s7: S7 C +}. (* the abstract candidate of reducibility associated to an atomic arity *) -let rec acr (R:lenv→predicate term) (A:aarity) (L:lenv) on A: predicate term ≝ +let rec aacr (RP:lenv→predicate term) (A:aarity) (L:lenv) on A: predicate term ≝ λT. match A with -[ AAtom ⇒ R L T -| APair B A ⇒ ∀V. acr R B L V → acr R A L (𝕔{Appl} V. T) +[ AAtom ⇒ RP L T +| APair B A ⇒ ∀V. aacr RP B L V → aacr RP A L (𝕔{Appl} V. T) ]. interpretation - "candidate of reducibility (abstract)" - 'InEInt R L T A = (acr R A L T). + "candidate of reducibility of an atomic arity (abstract)" + 'InEInt RP L T A = (aacr RP A L T). + +(* Basic properties *********************************************************) + +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: +] +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 +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/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma index fb94c8eee..b6ebc547f 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "Basic_2/reducibility/cpr.ma". +include "Basic_2/computation/acp.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) @@ -21,3 +22,7 @@ definition csn: lenv → predicate term ≝ λL. SN … (cpr L) (eq …). interpretation "context-sensitive strong normalization (term)" 'SN L T = (csn L T). + +(* Basic properties *********************************************************) + +axiom csn_acp: acp cpr (eq …) (csn …). diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aarity.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aaa.ma similarity index 75% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aarity.ma rename to matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aaa.ma index 7c84f3c08..097b045dc 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aarity.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aaa.ma @@ -12,17 +12,14 @@ (* *) (**************************************************************************) -include "Basic_2/static/aaa.ma". +include "Basic_2/computation/acp_aaa.ma". include "Basic_2/computation/csn_cr.ma". -include "Basic_2/computation/lsubcs.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) -(* Main propertis ***********************************************************) +(* Main properties **********************************************************) -axiom snc_aarity_csubcs: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L2 ⊑ L1 → {L2, T} ϵ 〚A〛. - -lemma snc_aarity: ∀L,T,A. L ⊢ T ÷ A → {L, T} ϵ 〚A〛. -/2 width=3/ qed. - -axiom csn_arity: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⇓ T. +theorem csn_aaa: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⇓ T. +#L #T #A #H +@(acp_aaa … csn_acp csn_acr … H) +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma index 915b17288..5dadd06de 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma @@ -17,9 +17,6 @@ include "Basic_2/computation/csn.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) -(* the candidate of reducibility associated to an atomic arity *) -definition snc: aarity → lenv → predicate term ≝ acr csn. +(* Advanced properties ******************************************************) -interpretation - "candidate of reducibility (contex-sensitive strong normalization)" - 'InEInt L T A = (snc A L T). +axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⇓ T). 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 8cf302dc8..9d38f25d7 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma @@ -16,21 +16,21 @@ include "Basic_2/computation/acp_cr.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) -inductive lsubc (R:lenv→predicate term) : relation lenv ≝ -| lsubc_atom: lsubc R (⋆) (⋆) -| lsubc_pair: ∀I,L1,L2,V. lsubc R L1 L2 → lsubc R (L1. 𝕓{I} V) (L2. 𝕓{I} V) -| lsubc_abbr: ∀L1,L2,V,W,A. R ⊢ {L1, V} ϵ 〚A〛 → R ⊢ {L2, W} ϵ 〚A〛 → - lsubc R L1 L2 → lsubc R (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W) +inductive lsubc (RP:lenv→predicate term): relation lenv ≝ +| lsubc_atom: lsubc RP (⋆) (⋆) +| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. 𝕓{I} V) (L2. 𝕓{I} V) +| lsubc_abbr: ∀L1,L2,V,W,A. {L1, V} [RP] ϵ 〚A〛 → {L2, W} [RP] ϵ 〚A〛 → + lsubc RP L1 L2 → lsubc RP (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W) . interpretation "local environment refinement (abstract candidates of reducibility)" - 'CrSubEq L1 R L2 = (lsubc R L1 L2). + 'CrSubEq L1 RP L2 = (lsubc RP L1 L2). (* Basic properties *********************************************************) -lemma lsubc_refl: ∀R,L. L [R] ⊑ L. -#R #L elim L -L // /2 width=1/ +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/functional/lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma index 4debfaabf..c94f11c8b 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma @@ -33,7 +33,7 @@ interpretation "functional relocation" 'Lift d e T = (flift d e T). (* Main properties **********************************************************) -theorem flift_lift: ∀T,d,e. ↑[d, e] T ≡ ↟[d, e] T. +theorem flift_lift: ∀T,d,e. ⇑[d, e] T ≡ ↑[d, e] T. #T elim T -T [ * #i #d #e // elim (lt_or_eq_or_gt i d) #Hid normalize @@ -47,7 +47,7 @@ qed. (* Main inversion properties ************************************************) -theorem flift_inv_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → ↟[d, e] T1 = T2. +theorem flift_inv_lift: ∀d,e,T1,T2. ⇑[d, e] T1 ≡ T2 → ↑[d, e] T1 = T2. #d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize // [ #i #d #e #Hid >(tri_lt ?????? Hid) // | #i #d #e #Hid @@ -60,7 +60,7 @@ qed-. (* Derived properties *******************************************************) -lemma flift_join: ∀e1,e2,T. ↑[e1, e2] ↟[0, e1] T ≡ ↟[0, e1 + e2] T. +lemma flift_join: ∀e1,e2,T. ⇑[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T. #e1 #e2 #T lapply (flift_lift T 0 (e1+e2)) #H elim (lift_split … H e1 e1 ? ? ?) -H // #U #H diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma index 5c92a1293..05f698ff8 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma @@ -20,7 +20,7 @@ include "Basic_2/functional/lift.ma". let rec fsubst W d U on U ≝ match U with [ TAtom I ⇒ match I with [ Sort _ ⇒ U - | LRef i ⇒ tri … i d (#i) (↟[0, i] W) (#(i-1)) + | LRef i ⇒ tri … i d (#i) (↑[0, i] W) (#(i-1)) | GRef _ ⇒ U ] | TPair I V T ⇒ match I with @@ -34,7 +34,7 @@ interpretation "functional core substitution" 'Subst V d T = (fsubst V d T). (* Main properties **********************************************************) theorem fsubst_delift: ∀K,V,T,L,d. - ↓[0, d] L ≡ K. 𝕓{Abbr} V → L ⊢ T [d, 1] ≡ ↡[d ← V] T. + ⇓[0, d] L ≡ K. 𝕓{Abbr} V → L ⊢ T [d, 1] ≡ ↓[d ← V] T. #K #V #T elim T -T [ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/ elim (lt_or_eq_or_gt i d) #Hid @@ -48,8 +48,8 @@ qed. (* Main inversion properties ************************************************) -theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ↓[0, d] L ≡ K. 𝕓{Abbr} V → - L ⊢ T1 [d, 1] ≡ T2 → ↡[d ← V] T1 = T2. +theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇓[0, d] L ≡ K. 𝕓{Abbr} V → + L ⊢ T1 [d, 1] ≡ T2 → ↓[d ← V] T1 = T2. #K #V #T1 elim T1 -T1 [ * #i #L #T2 #d #HLK #H [ -HLK >(delift_fwd_sort1 … H) -H // @@ -71,4 +71,3 @@ theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ↓[0, d] L ≡ K. 𝕓{Abbr} V → ] ] qed-. - \ No newline at end of file diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma new file mode 100644 index 000000000..6c9ea1ce5 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". + +(* TERMS ********************************************************************) + +let rec applv Vs T on Vs ≝ + match Vs with + [ nil ⇒ T + | cons hd tl ⇒ 𝕔{Appl} hd. (applv tl T) + ]. + +interpretation "application construction (vector)" 'ApplV Vs T = (applv Vs T). diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index 4d71723d0..49f126019 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -56,6 +56,10 @@ notation "hvbox( 𝕗 { I } break term 90 T1 . break term 90 T )" non associative with precedence 90 for @{ 'SFlat $I $T1 $T }. +notation "hvbox( Ⓐ term 90 T1 . break term 90 T )" + non associative with precedence 90 + for @{ 'ApplV $T1 $T }. + notation "hvbox( T . break 𝕓 { I } break term 90 T1 )" non associative with precedence 89 for @{ 'DBind $T $I $T1 }. @@ -82,17 +86,13 @@ notation "hvbox( T1 break [ d , break e ] ≼ break T2 )" (* Substitution *************************************************************) -notation "hvbox( ↑ [ d , break e ] break T1 ≡ break T2 )" +notation "hvbox( ⇑ [ d , break e ] break T1 ≡ break T2 )" non associative with precedence 45 for @{ 'RLift $d $e $T1 $T2 }. -notation "hvbox( ↓ [ e ] break L1 ≡ break L2 )" - non associative with precedence 45 - for @{ 'RDrop $e $L1 $L2 }. - -notation "hvbox( ↓ [ d , break e ] break L1 ≡ break L2 )" +notation "hvbox( ⇓ [ d , break e ] break L1 ≡ break L2 )" non associative with precedence 45 - for @{ 'RDrop $d $e $L1 $L2 }. + for @{ 'RLDrop $d $e $L1 $L2 }. notation "hvbox( T1 break [ d , break e ] ≫ break T2 )" non associative with precedence 45 @@ -104,6 +104,14 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≫ break T2 )" (* Unfold *******************************************************************) +notation "hvbox( ⇑ [ e ] break T1 ≡ break T2 )" + non associative with precedence 45 + for @{ 'RLift $e $T1 $T2 }. + +notation "hvbox( ⇓ [ e ] break L1 ≡ break L2 )" + non associative with precedence 45 + for @{ 'RLDrop $e $L1 $L2 }. + notation "hvbox( T1 break [ d , break e ] ≫* break T2 )" non associative with precedence 45 for @{ 'PSubstStar $T1 $d $e $T2 }. @@ -214,7 +222,7 @@ notation "hvbox( { L, break T } ϵ break 〚 A 〛 )" non associative with precedence 45 for @{ 'InEInt $L $T $A }. -notation "hvbox( R ⊢ break { L, break T } ϵ break 〚 A 〛 )" +notation "hvbox( { L, break T } break [ R ] ϵ break 〚 A 〛 )" non associative with precedence 45 for @{ 'InEInt $R $L $T $A }. @@ -228,11 +236,11 @@ notation "hvbox( T1 break [ R ] ⊑ break T2 )" (* Functional ***************************************************************) -notation "hvbox( ↟ [ d , break e ] break T )" +notation "hvbox( ↑ [ d , break e ] break T )" non associative with precedence 80 for @{ 'Lift $d $e $T }. -notation "hvbox( ↡ [ d ← break V ] break T )" +notation "hvbox( ↓ [ d ← break V ] break T )" non associative with precedence 80 for @{ 'Subst $V $d $T }. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma index f33692b42..380c6816b 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma @@ -21,8 +21,8 @@ include "Basic_2/reducibility/cpr.ma". (* Advanced properties ******************************************************) lemma cpr_cdelta: ∀L,K,V1,W1,W2,i. - ↓[0, i] L ≡ K. 𝕓{Abbr} V1 → K ⊢ V1 [0, |L| - i - 1] ≫* W1 → - ↑[0, i + 1] W1 ≡ W2 → L ⊢ #i ⇒ W2. + ⇓[0, i] L ≡ K. 𝕓{Abbr} V1 → K ⊢ V1 [0, |L| - i - 1] ≫* W1 → + ⇑[0, i + 1] W1 ≡ W2 → L ⊢ #i ⇒ W2. #L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12 lapply (ldrop_fwd_ldrop2_length … HLK) #Hi @ex2_1_intro [2: // | skip | @tpss_subst /width=6/ ] (**) (* /3 width=6/ is too slow *) @@ -33,9 +33,9 @@ qed. (* Basic_1: was: pr2_gen_lref *) lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ⇒ T2 → T2 = #i ∨ - ∃∃K,V1,T1. ↓[0, i] L ≡ K. 𝕓{Abbr} V1 & + ∃∃K,V1,T1. ⇓[0, i] L ≡ K. 𝕓{Abbr} V1 & K ⊢ V1 [0, |L| - i - 1] ≫* T1 & - ↑[0, i + 1] T1 ≡ T2 & + ⇑[0, i + 1] T1 ≡ T2 & i < |L|. #L #T2 #i * #X #H >(tpr_inv_atom1 … H) -H #H @@ -51,8 +51,8 @@ lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → (* Relocation properties ****************************************************) (* Basic_1: was: pr2_lift *) -lemma cpr_lift: ∀L,K,d,e. ↓[d, e] L ≡ K → - ∀T1,U1. ↑[d, e] T1 ≡ U1 → ∀T2,U2. ↑[d, e] T2 ≡ U2 → +lemma cpr_lift: ∀L,K,d,e. ⇓[d, e] L ≡ K → + ∀T1,U1. ⇑[d, e] T1 ≡ U1 → ∀T2,U2. ⇑[d, e] T2 ≡ U2 → K ⊢ T1 ⇒ T2 → L ⊢ U1 ⇒ U2. #L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 * #T #HT1 #HT2 elim (lift_total T d e) #U #HTU @@ -64,9 +64,9 @@ elim (lt_or_ge (|K|) d) #HKd qed. (* Basic_1: was: pr2_gen_lift *) -lemma cpr_inv_lift: ∀L,K,d,e. ↓[d, e] L ≡ K → - ∀T1,U1. ↑[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ⇒ U2 → - ∃∃T2. ↑[d, e] T2 ≡ U2 & K ⊢ T1 ⇒ T2. +lemma cpr_inv_lift: ∀L,K,d,e. ⇓[d, e] L ≡ K → + ∀T1,U1. ⇑[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ⇒ U2 → + ∃∃T2. ⇑[d, e] T2 ≡ U2 & K ⊢ T1 ⇒ T2. #L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2 elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1 elim (lt_or_ge (|L|) d) #HLd diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma index 38e7858dc..08ac62aaf 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma @@ -18,8 +18,8 @@ include "Basic_2/reducibility/ltpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) (* Basic_1: was: wcpr0_ldrop *) -lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 → - ∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2. +lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ⇓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 → + ∃∃K2. ⇓[d, e] L2 ≡ K2 & K1 ⇒ K2. #L1 #K1 #d #e #H elim H -L1 -K1 -d -e [ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/ | #K1 #I #V1 #X #H @@ -35,8 +35,8 @@ lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 qed. (* Basic_1: was: wcpr0_ldrop_back *) -lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 → - ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2. +lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ⇓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 → + ∃∃L2. ⇓[d, e] L2 ≡ K2 & L1 ⇒ L2. #L1 #K1 #d #e #H elim H -L1 -K1 -d -e [ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/ | #K1 #I #V1 #X #H 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 cf0c7cae2..4769a39dc 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma @@ -29,9 +29,9 @@ inductive tpr: relation term ≝ tpr V1 V2 → tpr T1 T2 → ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T → tpr (𝕓{I} V1. T1) (𝕓{I} V2. T) | tpr_theta: ∀V,V1,V2,W1,W2,T1,T2. - tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 → + tpr V1 V2 → ⇑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 → tpr (𝕔{Appl} V1. 𝕔{Abbr} W1. T1) (𝕔{Abbr} W2. 𝕔{Appl} V. T2) -| tpr_zeta : ∀V,T,T1,T2. ↑[0,1] T1 ≡ T → tpr T1 T2 → +| tpr_zeta : ∀V,T,T1,T2. ⇑[0,1] T1 ≡ T → tpr T1 T2 → tpr (𝕔{Abbr} V. T) T2 | tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (𝕔{Cast} V. T1) T2 . @@ -43,7 +43,7 @@ interpretation (* Basic properties *********************************************************) lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 → - 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. + 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. /2 width=3/ qed. (* Basic_1: was by definition: pr0_refl *) @@ -75,7 +75,7 @@ fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T & U2 = 𝕓{I} V2. T ) ∨ - ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. + ∃∃T. ⇑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. #U1 #U2 * -U1 -U2 [ #J #I #V #T #H destruct | #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct @@ -92,7 +92,7 @@ lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 → ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T & U2 = 𝕓{I} V2. T ) ∨ - ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. + ∃∃T. ⇑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. /2 width=3/ qed-. (* Basic_1: was pr0_gen_abbr *) @@ -101,7 +101,7 @@ lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 → ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T & U2 = 𝕓{Abbr} V2. T ) ∨ - ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2. + ∃∃T. ⇑[0,1] T ≡ T1 & T ⇒ U2. #V1 #T1 #U2 #H elim (tpr_inv_bind1 … H) -H * /3 width=7/ qed-. @@ -113,7 +113,7 @@ fact tpr_inv_flat1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0 U0 = 𝕔{Abst} W. T1 & U2 = 𝕔{Abbr} V2. T2 & I = Appl | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & - ↑[0,1] V2 ≡ V & + ⇑[0,1] V2 ≡ V & U0 = 𝕔{Abbr} W1. T1 & U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 & I = Appl @@ -136,7 +136,7 @@ lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 → U0 = 𝕔{Abst} W. T1 & U2 = 𝕔{Abbr} V2. T2 & I = Appl | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & - ↑[0,1] V2 ≡ V & + ⇑[0,1] V2 ≡ V & U0 = 𝕔{Abbr} W1. T1 & U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 & I = Appl @@ -151,7 +151,7 @@ lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 → U0 = 𝕔{Abst} W. T1 & U2 = 𝕔{Abbr} V2. T2 | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & - ↑[0,1] V2 ≡ V & + ⇑[0,1] V2 ≡ V & U0 = 𝕔{Abbr} W1. T1 & U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2. #V1 #U0 #U2 #H @@ -185,7 +185,7 @@ qed-. fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i → ∨∨ T1 = #i - | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & + | ∃∃V,T,T0. ⇑[O,1] T0 ≡ T & T0 ⇒ #i & T1 = 𝕔{Abbr} V. T | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T. #T1 #T2 * -T1 -T2 @@ -201,7 +201,7 @@ qed. lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i → ∨∨ T1 = #i - | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & + | ∃∃V,T,T0. ⇑[O,1] T0 ≡ T & T0 ⇒ #i & T1 = 𝕔{Abbr} V. T | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T. /2 width=3/ qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma index d9d9c549a..32a80aafc 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma @@ -21,7 +21,7 @@ include "Basic_2/reducibility/tpr.ma". (* Basic_1: was: pr0_lift *) lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 → - ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2. + ∀d,e,U1. ⇑[d, e] T1 ≡ U1 → ∀U2. ⇑[d, e] T2 ≡ U2 → U1 ⇒ U2. #T1 #T2 #H elim H -T1 -T2 [ * #i #d #e #U1 #HU1 #U2 #HU2 lapply (lift_mono … HU1 … HU2) -HU1 #H destruct @@ -58,8 +58,8 @@ qed. (* Basic_1: was: pr0_gen_lift *) lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 → - ∀d,e,U1. ↑[d, e] U1 ≡ T1 → - ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2. + ∀d,e,U1. ⇑[d, e] U1 ≡ T1 → + ∃∃U2. ⇑[d, e] U2 ≡ T2 & U1 ⇒ U2. #T1 #T2 #H elim H -T1 -T2 [ * #i #d #e #U1 #HU1 [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct /2 width=3/ diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma index 40feeff2f..e541b5777 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma @@ -59,7 +59,7 @@ fact tpr_conf_flat_theta: ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → ∃∃X. X1 ⇒ X & X2 ⇒ X ) → - V0 ⇒ V1 → V0 ⇒ V2 → ↑[O,1] V2 ≡ V → + V0 ⇒ V1 → V0 ⇒ V2 → ⇑[O,1] V2 ≡ V → W0 ⇒ W2 → U0 ⇒ U2 → 𝕔{Abbr} W0. U0 ⇒ T1 → ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ⇒ X. #V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H @@ -142,7 +142,7 @@ fact tpr_conf_delta_zeta: ∃∃X. X1 ⇒ X & X2 ⇒ X ) → V0 ⇒ V1 → T0 ⇒ T1 → ⋆. 𝕓{Abbr} V1 ⊢ T1 [O,1] ≫ TT1 → - T2 ⇒ X2 → ↑[O, 1] T2 ≡ T0 → + T2 ⇒ X2 → ⇑[O, 1] T2 ≡ T0 → ∃∃X. 𝕓{Abbr} V1. TT1 ⇒ X & X2 ⇒ X. #X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20 elim (tpr_inv_lift … HT01 … HTT20) -HT01 #TT2 #HTT21 #HTT2 @@ -159,7 +159,7 @@ fact tpr_conf_theta_theta: ∃∃X. X1 ⇒ X & X2 ⇒ X ) → V0 ⇒ V1 → V0 ⇒ V2 → W0 ⇒ W1 → W0 ⇒ W2 → T0 ⇒ T1 → T0 ⇒ T2 → - ↑[O, 1] V1 ≡ VV1 → ↑[O, 1] V2 ≡ VV2 → + ⇑[O, 1] V1 ≡ VV1 → ⇑[O, 1] V2 ≡ VV2 → ∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ⇒ X. #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2 elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 @@ -178,7 +178,7 @@ fact tpr_conf_zeta_zeta: ∃∃X. X1 ⇒ X & X2 ⇒ X ) → T0 ⇒ T1 → T2 ⇒ X2 → - ↑[O, 1] T0 ≡ TT0 → ↑[O, 1] T2 ≡ TT0 → + ⇑[O, 1] T0 ≡ TT0 → ⇑[O, 1] T2 ≡ TT0 → ∃∃X. T1 ⇒ X & X2 ⇒ X. #V0 #X2 #TT0 #T0 #T1 #T2 #IH #HT01 #HTX2 #HTT0 #HTT20 lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa.ma index 01af2572f..526688e5c 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa.ma @@ -19,11 +19,11 @@ include "Basic_2/substitution/ldrop.ma". inductive aaa: lenv → term → predicate aarity ≝ | aaa_sort: ∀L,k. aaa L (⋆k) 𝕒 -| aaa_lref: ∀I,L,K,V,B,i. ↓[0, i] L ≡ K. 𝕓{I} V → aaa K V B → aaa L (#i) B +| aaa_lref: ∀I,L,K,V,B,i. ⇓[0, i] L ≡ K. 𝕓{I} V → aaa K V B → aaa L (#i) B | aaa_abbr: ∀L,V,T,B,A. aaa L V B → aaa (L. 𝕓{Abbr} V) T A → aaa L (𝕔{Abbr} V. T) A | aaa_abst: ∀L,V,T,B,A. - aaa L V B → aaa (L. 𝕓{Abst} V) T A → aaa L (𝕔{Abbr} V. T) (𝕔 B. A) + aaa L V B → aaa (L. 𝕓{Abst} V) T A → aaa L (𝕔{Abst} V. T) (𝕔 B. A) | aaa_appl: ∀L,V,T,B,A. aaa L V B → aaa L T (𝕔 B. A) → aaa L (𝕔{Appl} V. T) A | aaa_cast: ∀L,V,T,A. aaa L V A → aaa L T A → aaa L (𝕔{Cast} V. T) A . diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma index 47d75a4ea..5cef64937 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma @@ -17,15 +17,15 @@ include "Basic_2/substitution/ldrop.ma". (* GLOBAL ENVIRONMENT SLICING ***********************************************) inductive gdrop (e:nat) (G1:lenv) : predicate lenv ≝ -| gdrop_lt: ∀G2. e < |G1| → ↓[0, |G1| - (e + 1)] G1 ≡ G2 → gdrop e G1 G2 +| gdrop_lt: ∀G2. e < |G1| → ⇓[0, |G1| - (e + 1)] G1 ≡ G2 → gdrop e G1 G2 | gdrop_ge: |G1| ≤ e → gdrop e G1 (⋆) . -interpretation "global slicing" 'RDrop e G1 G2 = (gdrop e G1 G2). +interpretation "global slicing" 'RGDrop e G1 G2 = (gdrop e G1 G2). (* basic inversion lemmas ***************************************************) - -fact gdrop_inv_atom2_aux: ∀G1,G2,e. ↓[e] G1 ≡ G2 → G2 = ⋆ → |G1| ≤ e. +(* +fact gdrop_inv_atom2_aux: ∀G1,G2,e. ⇓[e] G1 ≡ G2 → G2 = ⋆ → |G1| ≤ e. #G1 #G2 #e * -G2 // #G2 #He #HG12 #H destruct lapply (ldrop_fwd_O1_length … HG12) -HG12 @@ -33,11 +33,12 @@ lapply (ldrop_fwd_O1_length … HG12) -HG12 >(commutative_plus e) normalize #H destruct qed. -lemma gdrop_inv_atom2: ∀G1,e. ↓[e] G1 ≡ ⋆ → |G1| ≤ e. +lemma gdrop_inv_atom2: ∀G1,e. ⇓[e] G1 ≡ ⋆ → |G1| ≤ e. /2 width=3/ qed-. -lemma gdrop_inv_ge: ∀G1,G2,e. ↓[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆. +lemma gdrop_inv_ge: ∀G1,G2,e. ⇓[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆. #G1 #G2 #e * // #G2 #H1 #_ #H2 lapply (lt_to_le_to_lt … H1 H2) -H1 -H2 #He elim (lt_refl_false … He) qed-. +*) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma index b4d3355d6..c3219f4f4 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma @@ -20,19 +20,19 @@ include "Basic_2/substitution/lift.ma". (* Basic_1: includes: ldrop_skip_bind *) inductive ldrop: nat → nat → relation lenv ≝ -| ldrop_atom: ∀d,e. ldrop d e (⋆) (⋆) -| ldrop_pair: ∀L,I,V. ldrop 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V) +| ldrop_atom : ∀d,e. ldrop d e (⋆) (⋆) +| ldrop_pair : ∀L,I,V. ldrop 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V) | ldrop_ldrop: ∀L1,L2,I,V,e. ldrop 0 e L1 L2 → ldrop 0 (e + 1) (L1. 𝕓{I} V) L2 -| ldrop_skip: ∀L1,L2,I,V1,V2,d,e. - ldrop d e L1 L2 → ↑[d,e] V2 ≡ V1 → - ldrop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2) +| ldrop_skip : ∀L1,L2,I,V1,V2,d,e. + ldrop d e L1 L2 → ⇑[d,e] V2 ≡ V1 → + ldrop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2) . -interpretation "local slicing" 'RDrop d e L1 L2 = (ldrop d e L1 L2). +interpretation "local slicing" 'RLDrop d e L1 L2 = (ldrop d e L1 L2). (* Basic inversion lemmas ***************************************************) -fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2. +fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ⇓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2. #d #e #L1 #L2 * -d -e -L1 -L2 [ // | // @@ -42,10 +42,10 @@ fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 qed. (* Basic_1: was: ldrop_gen_refl *) -lemma ldrop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2. +lemma ldrop_inv_refl: ∀L1,L2. ⇓[0, 0] L1 ≡ L2 → L1 = L2. /2 width=5/ qed-. -fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → +fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ⇓[d, e] L1 ≡ L2 → L1 = ⋆ → L2 = ⋆. #d #e #L1 #L2 * -d -e -L1 -L2 [ // @@ -56,13 +56,13 @@ fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → qed. (* Basic_1: was: ldrop_gen_sort *) -lemma ldrop_inv_atom1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆. +lemma ldrop_inv_atom1: ∀d,e,L2. ⇓[d, e] ⋆ ≡ L2 → L2 = ⋆. /2 width=5/ qed-. -fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → +fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ⇓[d, e] L1 ≡ L2 → d = 0 → ∀K,I,V. L1 = K. 𝕓{I} V → (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ - (0 < e ∧ ↓[d, e - 1] K ≡ L2). + (0 < e ∧ ⇓[d, e - 1] K ≡ L2). #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #K #I #V #H destruct | #L #I #V #_ #K #J #W #HX destruct /3 width=1/ @@ -71,23 +71,23 @@ fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → ] qed. -lemma ldrop_inv_O1: ∀e,K,I,V,L2. ↓[0, e] K. 𝕓{I} V ≡ L2 → +lemma ldrop_inv_O1: ∀e,K,I,V,L2. ⇓[0, e] K. 𝕓{I} V ≡ L2 → (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ - (0 < e ∧ ↓[0, e - 1] K ≡ L2). + (0 < e ∧ ⇓[0, e - 1] K ≡ L2). /2 width=3/ qed-. (* Basic_1: was: ldrop_gen_ldrop *) lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2. - ↓[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ↓[0, e - 1] K ≡ L2. + ⇓[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ⇓[0, e - 1] K ≡ L2. #e #K #I #V #L2 #H #He elim (ldrop_inv_O1 … H) -H * // #H destruct elim (lt_refl_false … He) qed-. -fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → +fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇓[d, e] L1 ≡ L2 → 0 < d → ∀I,K1,V1. L1 = K1. 𝕓{I} V1 → - ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & - ↑[d - 1, e] V2 ≡ V1 & + ∃∃K2,V2. ⇓[d - 1, e] K1 ≡ K2 & + ⇑[d - 1, e] V2 ≡ V1 & L2 = K2. 𝕓{I} V2. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K #V #H destruct @@ -98,16 +98,16 @@ fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → qed. (* Basic_1: was: ldrop_gen_skip_l *) -lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ↓[d, e] K1. 𝕓{I} V1 ≡ L2 → 0 < d → - ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & - ↑[d - 1, e] V2 ≡ V1 & +lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ⇓[d, e] K1. 𝕓{I} V1 ≡ L2 → 0 < d → + ∃∃K2,V2. ⇓[d - 1, e] K1 ≡ K2 & + ⇑[d - 1, e] V2 ≡ V1 & L2 = K2. 𝕓{I} V2. /2 width=3/ qed-. -fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → +fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇓[d, e] L1 ≡ L2 → 0 < d → ∀I,K2,V2. L2 = K2. 𝕓{I} V2 → - ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & - ↑[d - 1, e] V2 ≡ V1 & + ∃∃K1,V1. ⇓[d - 1, e] K1 ≡ K2 & + ⇑[d - 1, e] V2 ≡ V1 & L1 = K1. 𝕓{I} V1. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K #V #H destruct @@ -118,28 +118,28 @@ fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → qed. (* Basic_1: was: ldrop_gen_skip_r *) -lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d → - ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 & +lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ⇓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d → + ∃∃K1,V1. ⇓[d - 1, e] K1 ≡ K2 & ⇑[d - 1, e] V2 ≡ V1 & L1 = K1. 𝕓{I} V1. /2 width=3/ qed-. (* Basic properties *********************************************************) (* Basic_1: was by definition: ldrop_refl *) -lemma ldrop_refl: ∀L. ↓[0, 0] L ≡ L. +lemma ldrop_refl: ∀L. ⇓[0, 0] L ≡ L. #L elim L -L // qed. lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e. - ↓[0, e - 1] L1 ≡ L2 → 0 < e → ↓[0, e] L1. 𝕓{I} V ≡ L2. + ⇓[0, e - 1] L1 ≡ L2 → 0 < e → ⇓[0, e] L1. 𝕓{I} V ≡ L2. #L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/ qed. lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → - ∀K1,V,i. ↓[0, i] L1 ≡ K1. 𝕓{Abbr} V → + ∀K1,V,i. ⇓[0, i] L1 ≡ K1. 𝕓{Abbr} V → d ≤ i → i < d + e → ∃∃K2. K1 [0, d + e - i - 1] ≼ K2 & - ↓[0, i] L2 ≡ K2. 𝕓{Abbr} V. + ⇓[0, i] L2 ≡ K2. 𝕓{Abbr} V. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e [ #d #e #K1 #V #i #H lapply (ldrop_inv_atom1 … H) -H #H destruct @@ -167,8 +167,8 @@ qed. (* Basic forvard lemmas *****************************************************) (* Basic_1: was: ldrop_S *) -lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 → - ↓[O, e + 1] L1 ≡ K2. +lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇓[O, e] L1 ≡ K2. 𝕓{I2} V2 → + ⇓[O, e + 1] L1 ≡ K2. #L1 elim L1 -L1 [ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct | #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H @@ -179,7 +179,7 @@ lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 → ] qed-. -lemma ldrop_fwd_lw: ∀L1,L2,d,e. ↓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. +lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize [ /2 width=3/ | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 @@ -188,7 +188,7 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ↓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. qed-. lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e. - ↓[0, e] L1 ≡ K2. 𝕓{I2} V2 → e < |L1|. + ⇓[0, e] L1 ≡ K2. 𝕓{I2} V2 → e < |L1|. #L1 elim L1 -L1 [ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct | #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H @@ -199,7 +199,7 @@ lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e. ] qed-. -lemma ldrop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e. +lemma ldrop_fwd_O1_length: ∀L1,L2,e. ⇓[0, e] L1 ≡ L2 → |L2| = |L1| - e. #L1 elim L1 -L1 [ #L2 #e #H >(ldrop_inv_atom1 … H) -H // | #K1 #I1 #V1 #IHL1 #L2 #e #H diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma index 3aef19c0e..e9b92d9e3 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma @@ -20,8 +20,8 @@ include "Basic_2/substitution/ldrop.ma". (* Main properties **********************************************************) (* Basic_1: was: ldrop_mono *) -theorem ldrop_mono: ∀d,e,L,L1. ↓[d, e] L ≡ L1 → - ∀L2. ↓[d, e] L ≡ L2 → L1 = L2. +theorem ldrop_mono: ∀d,e,L,L1. ⇓[d, e] L ≡ L1 → + ∀L2. ⇓[d, e] L ≡ L2 → L1 = L2. #d #e #L #L1 #H elim H -d -e -L -L1 [ #d #e #L2 #H >(ldrop_inv_atom1 … H) -L2 // @@ -37,9 +37,9 @@ theorem ldrop_mono: ∀d,e,L,L1. ↓[d, e] L ≡ L1 → qed-. (* Basic_1: was: ldrop_conf_ge *) -theorem ldrop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → - ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 + e1 ≤ e2 → - ↓[0, e2 - e1] L1 ≡ L2. +theorem ldrop_conf_ge: ∀d1,e1,L,L1. ⇓[d1, e1] L ≡ L1 → + ∀e2,L2. ⇓[0, e2] L ≡ L2 → d1 + e1 ≤ e2 → + ⇓[0, e2 - e1] L1 ≡ L2. #d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1 [ #d #e #e2 #L2 #H >(ldrop_inv_atom1 … H) -L2 // @@ -56,11 +56,11 @@ theorem ldrop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → qed. (* Basic_1: was: ldrop_conf_lt *) -theorem ldrop_conf_lt: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → - ∀e2,K2,I,V2. ↓[0, e2] L ≡ K2. 𝕓{I} V2 → +theorem ldrop_conf_lt: ∀d1,e1,L,L1. ⇓[d1, e1] L ≡ L1 → + ∀e2,K2,I,V2. ⇓[0, e2] L ≡ K2. 𝕓{I} V2 → e2 < d1 → let d ≝ d1 - e2 - 1 in - ∃∃K1,V1. ↓[0, e2] L1 ≡ K1. 𝕓{I} V1 & - ↓[d, e1] K2 ≡ K1 & ↑[d, e1] V1 ≡ V2. + ∃∃K1,V1. ⇓[0, e2] L1 ≡ K1. 𝕓{I} V1 & + ⇓[d, e1] K2 ≡ K1 & ⇑[d, e1] V1 ≡ V2. #d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1 [ #d #e #e2 #K2 #I #V2 #H lapply (ldrop_inv_atom1 … H) -H #H destruct @@ -78,9 +78,9 @@ theorem ldrop_conf_lt: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → qed. (* Basic_1: was: ldrop_trans_le *) -theorem ldrop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → - ∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 → - ∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2. +theorem ldrop_trans_le: ∀d1,e1,L1,L. ⇓[d1, e1] L1 ≡ L → + ∀e2,L2. ⇓[0, e2] L ≡ L2 → e2 ≤ d1 → + ∃∃L0. ⇓[0, e2] L1 ≡ L0 & ⇓[d1 - e2, e1] L0 ≡ L2. #d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L [ #d #e #e2 #L2 #H >(ldrop_inv_atom1 … H) -L2 /2 width=3/ @@ -100,8 +100,8 @@ theorem ldrop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → qed. (* Basic_1: was: ldrop_trans_ge *) -theorem ldrop_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → - ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2. +theorem ldrop_trans_ge: ∀d1,e1,L1,L. ⇓[d1, e1] L1 ≡ L → + ∀e2,L2. ⇓[0, e2] L ≡ L2 → d1 ≤ e2 → ⇓[0, e1 + e2] L1 ≡ L2. #d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L [ #d #e #e2 #L2 #H >(ldrop_inv_atom1 … H) -H -L2 // @@ -116,11 +116,11 @@ theorem ldrop_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → qed. theorem ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L. - ↓[d1, e1] L1 ≡ L → ↓[0, e2] L ≡ L2 → d1 ≤ e2 → - ↓[0, e2 + e1] L1 ≡ L2. + ⇓[d1, e1] L1 ≡ L → ⇓[0, e2] L ≡ L2 → d1 ≤ e2 → + ⇓[0, e2 + e1] L1 ≡ L2. #e1 #e1 #e2 >commutative_plus /2 width=5/ qed. (* Basic_1: was: ldrop_conf_rev *) -axiom ldrop_div: ∀e1,L1,L. ↓[0, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L2 ≡ L → - ∃∃L0. ↓[0, e1] L0 ≡ L2 & ↓[e1, e2] L0 ≡ L1. +axiom ldrop_div: ∀e1,L1,L. ⇓[0, e1] L1 ≡ L → ∀e2,L2. ⇓[0, e2] L2 ≡ L → + ∃∃L0. ⇓[0, e1] L0 ≡ L2 & ⇓[e1, e2] L0 ≡ L1. 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 e8e23a555..9e6b261c8 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma @@ -36,14 +36,14 @@ interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2). (* Basic inversion lemmas ***************************************************) -fact lift_inv_refl_O2_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2. +fact lift_inv_refl_O2_aux: ∀d,e,T1,T2. ⇑[d, e] T1 ≡ T2 → e = 0 → T1 = T2. #d #e #T1 #T2 #H elim H -d -e -T1 -T2 // /3 width=1/ qed. -lemma lift_inv_refl_O2: ∀d,T1,T2. ↑[d, 0] T1 ≡ T2 → T1 = T2. +lemma lift_inv_refl_O2: ∀d,T1,T2. ⇑[d, 0] T1 ≡ T2 → T1 = T2. /2 width=4/ qed-. -fact lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k. +fact lift_inv_sort1_aux: ∀d,e,T1,T2. ⇑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k. #d #e #T1 #T2 * -d -e -T1 -T2 // [ #i #d #e #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct @@ -51,10 +51,10 @@ fact lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k ] qed. -lemma lift_inv_sort1: ∀d,e,T2,k. ↑[d,e] ⋆k ≡ T2 → T2 = ⋆k. +lemma lift_inv_sort1: ∀d,e,T2,k. ⇑[d,e] ⋆k ≡ T2 → T2 = ⋆k. /2 width=5/ qed-. -fact lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i → +fact lift_inv_lref1_aux: ∀d,e,T1,T2. ⇑[d,e] T1 ≡ T2 → ∀i. T1 = #i → (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)). #d #e #T1 #T2 * -d -e -T1 -T2 [ #k #d #e #i #H destruct @@ -66,23 +66,23 @@ fact lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i → ] qed. -lemma lift_inv_lref1: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → +lemma lift_inv_lref1: ∀d,e,T2,i. ⇑[d,e] #i ≡ T2 → (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)). /2 width=3/ qed-. -lemma lift_inv_lref1_lt: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → i < d → T2 = #i. +lemma lift_inv_lref1_lt: ∀d,e,T2,i. ⇑[d,e] #i ≡ T2 → i < d → T2 = #i. #d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * // #Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd elim (lt_refl_false … Hdd) qed-. -lemma lift_inv_lref1_ge: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → d ≤ i → T2 = #(i + e). +lemma lift_inv_lref1_ge: ∀d,e,T2,i. ⇑[d,e] #i ≡ T2 → d ≤ i → T2 = #(i + e). #d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * // #Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd elim (lt_refl_false … Hdd) qed-. -fact lift_inv_gref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T1 = §p → T2 = §p. +fact lift_inv_gref1_aux: ∀d,e,T1,T2. ⇑[d,e] T1 ≡ T2 → ∀p. T1 = §p → T2 = §p. #d #e #T1 #T2 * -d -e -T1 -T2 // [ #i #d #e #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct @@ -90,12 +90,12 @@ fact lift_inv_gref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T1 = §p → ] qed. -lemma lift_inv_gref1: ∀d,e,T2,p. ↑[d,e] §p ≡ T2 → T2 = §p. +lemma lift_inv_gref1: ∀d,e,T2,p. ⇑[d,e] §p ≡ T2 → T2 = §p. /2 width=5/ qed-. -fact lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → +fact lift_inv_bind1_aux: ∀d,e,T1,T2. ⇑[d,e] T1 ≡ T2 → ∀I,V1,U1. T1 = 𝕓{I} V1.U1 → - ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & + ∃∃V2,U2. ⇑[d,e] V1 ≡ V2 & ⇑[d+1,e] U1 ≡ U2 & T2 = 𝕓{I} V2. U2. #d #e #T1 #T2 * -d -e -T1 -T2 [ #k #d #e #I #V1 #U1 #H destruct @@ -107,14 +107,14 @@ fact lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ] qed. -lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕓{I} V1. U1 ≡ T2 → - ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & +lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ⇑[d,e] 𝕓{I} V1. U1 ≡ T2 → + ∃∃V2,U2. ⇑[d,e] V1 ≡ V2 & ⇑[d+1,e] U1 ≡ U2 & T2 = 𝕓{I} V2. U2. /2 width=3/ qed-. -fact lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → +fact lift_inv_flat1_aux: ∀d,e,T1,T2. ⇑[d,e] T1 ≡ T2 → ∀I,V1,U1. T1 = 𝕗{I} V1.U1 → - ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & + ∃∃V2,U2. ⇑[d,e] V1 ≡ V2 & ⇑[d,e] U1 ≡ U2 & T2 = 𝕗{I} V2. U2. #d #e #T1 #T2 * -d -e -T1 -T2 [ #k #d #e #I #V1 #U1 #H destruct @@ -126,12 +126,12 @@ fact lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ] qed. -lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕗{I} V1. U1 ≡ T2 → - ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & +lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ⇑[d,e] 𝕗{I} V1. U1 ≡ T2 → + ∃∃V2,U2. ⇑[d,e] V1 ≡ V2 & ⇑[d,e] U1 ≡ U2 & T2 = 𝕗{I} V2. U2. /2 width=3/ qed-. -fact lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k. +fact lift_inv_sort2_aux: ∀d,e,T1,T2. ⇑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k. #d #e #T1 #T2 * -d -e -T1 -T2 // [ #i #d #e #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct @@ -140,10 +140,10 @@ fact lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k qed. (* Basic_1: was: lift_gen_sort *) -lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k. +lemma lift_inv_sort2: ∀d,e,T1,k. ⇑[d,e] T1 ≡ ⋆k → T1 = ⋆k. /2 width=5/ qed-. -fact lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i → +fact lift_inv_lref2_aux: ∀d,e,T1,T2. ⇑[d,e] T1 ≡ T2 → ∀i. T2 = #i → (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)). #d #e #T1 #T2 * -d -e -T1 -T2 [ #k #d #e #i #H destruct @@ -156,12 +156,12 @@ fact lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i → qed. (* Basic_1: was: lift_gen_lref *) -lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → +lemma lift_inv_lref2: ∀d,e,T1,i. ⇑[d,e] T1 ≡ #i → (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)). /2 width=3/ qed-. (* Basic_1: was: lift_gen_lref_lt *) -lemma lift_inv_lref2_lt: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → i < d → T1 = #i. +lemma lift_inv_lref2_lt: ∀d,e,T1,i. ⇑[d,e] T1 ≡ #i → i < d → T1 = #i. #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * // #Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd elim (lt_inv_plus_l … Hdd) -Hdd #Hdd @@ -169,7 +169,7 @@ elim (lt_refl_false … Hdd) qed-. (* Basic_1: was: lift_gen_lref_false *) -lemma lift_inv_lref2_be: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → +lemma lift_inv_lref2_be: ∀d,e,T1,i. ⇑[d,e] T1 ≡ #i → d ≤ i → i < d + e → False. #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * [ #H1 #_ #H2 #_ | #H2 #_ #_ #H1 ] @@ -178,14 +178,14 @@ elim (lt_refl_false … H) qed-. (* Basic_1: was: lift_gen_lref_ge *) -lemma lift_inv_lref2_ge: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → d + e ≤ i → T1 = #(i - e). +lemma lift_inv_lref2_ge: ∀d,e,T1,i. ⇑[d,e] T1 ≡ #i → d + e ≤ i → T1 = #(i - e). #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * // #Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd elim (lt_inv_plus_l … Hdd) -Hdd #Hdd elim (lt_refl_false … Hdd) qed-. -fact lift_inv_gref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T2 = §p → T1 = §p. +fact lift_inv_gref2_aux: ∀d,e,T1,T2. ⇑[d,e] T1 ≡ T2 → ∀p. T2 = §p → T1 = §p. #d #e #T1 #T2 * -d -e -T1 -T2 // [ #i #d #e #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct @@ -193,12 +193,12 @@ fact lift_inv_gref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T2 = §p → ] qed. -lemma lift_inv_gref2: ∀d,e,T1,p. ↑[d,e] T1 ≡ §p → T1 = §p. +lemma lift_inv_gref2: ∀d,e,T1,p. ⇑[d,e] T1 ≡ §p → T1 = §p. /2 width=5/ qed-. -fact lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → +fact lift_inv_bind2_aux: ∀d,e,T1,T2. ⇑[d,e] T1 ≡ T2 → ∀I,V2,U2. T2 = 𝕓{I} V2.U2 → - ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & + ∃∃V1,U1. ⇑[d,e] V1 ≡ V2 & ⇑[d+1,e] U1 ≡ U2 & T1 = 𝕓{I} V1. U1. #d #e #T1 #T2 * -d -e -T1 -T2 [ #k #d #e #I #V2 #U2 #H destruct @@ -211,14 +211,14 @@ fact lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → qed. (* Basic_1: was: lift_gen_bind *) -lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ 𝕓{I} V2. U2 → - ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & +lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ⇑[d,e] T1 ≡ 𝕓{I} V2. U2 → + ∃∃V1,U1. ⇑[d,e] V1 ≡ V2 & ⇑[d+1,e] U1 ≡ U2 & T1 = 𝕓{I} V1. U1. /2 width=3/ qed-. -fact lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → +fact lift_inv_flat2_aux: ∀d,e,T1,T2. ⇑[d,e] T1 ≡ T2 → ∀I,V2,U2. T2 = 𝕗{I} V2.U2 → - ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & + ∃∃V1,U1. ⇑[d,e] V1 ≡ V2 & ⇑[d,e] U1 ≡ U2 & T1 = 𝕗{I} V1. U1. #d #e #T1 #T2 * -d -e -T1 -T2 [ #k #d #e #I #V2 #U2 #H destruct @@ -231,12 +231,12 @@ fact lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → qed. (* Basic_1: was: lift_gen_flat *) -lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ 𝕗{I} V2. U2 → - ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & +lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ⇑[d,e] T1 ≡ 𝕗{I} V2. U2 → + ∃∃V1,U1. ⇑[d,e] V1 ≡ V2 & ⇑[d,e] U1 ≡ U2 & T1 = 𝕗{I} V1. U1. /2 width=3/ qed-. -lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ↑[d, e] 𝕔{I} V. T ≡ V → False. +lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇑[d, e] 𝕔{I} V. T ≡ V → False. #d #e #J #V elim V -V [ * #i #T #H [ lapply (lift_inv_sort2 … H) -H #H destruct @@ -250,7 +250,7 @@ lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ↑[d, e] 𝕔{I} V. T ≡ V → False. ] qed-. -lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ↑[d, e] 𝕔{I} V. T ≡ T → False. +lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇑[d, e] 𝕔{I} V. T ≡ T → False. #J #T elim T -T [ * #i #V #d #e #H [ lapply (lift_inv_sort2 … H) -H #H destruct @@ -266,29 +266,29 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #[T1] = #[T2]. +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-. (* Basic properties *********************************************************) (* Basic_1: was: lift_lref_gt *) -lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d, e] #(i - e) ≡ #i. +lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ⇑[d, e] #(i - e) ≡ #i. #d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %); /2 width=2/ /3 width=2/ qed. -lemma lift_lref_ge_minus_eq: ∀d,e,i,j. d + e ≤ i → j = i - e → ↑[d, e] #j ≡ #i. +lemma lift_lref_ge_minus_eq: ∀d,e,i,j. d + e ≤ i → j = i - e → ⇑[d, e] #j ≡ #i. /2 width=1/ qed-. (* Basic_1: was: lift_r *) -lemma lift_refl: ∀T,d. ↑[d, 0] T ≡ T. +lemma lift_refl: ∀T,d. ⇑[d, 0] T ≡ T. #T elim T -T [ * #i // #d elim (lt_or_ge i d) /2 width=1/ | * /2 width=1/ ] qed. -lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2. +lemma lift_total: ∀T1,d,e. ∃T2. ⇑[d,e] T1 ≡ T2. #T1 elim T1 -T1 [ * #i /2 width=2/ #d #e elim (lt_or_ge i d) /3 width=2/ | * #I #V1 #T1 #IHV1 #IHT1 #d #e @@ -300,9 +300,9 @@ lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2. qed. (* Basic_1: was: lift_free (right to left) *) -lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → +lemma lift_split: ∀d1,e2,T1,T2. ⇑[d1, e2] T1 ≡ T2 → ∀d2,e1. d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 → - ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2. + ∃∃T. ⇑[d1, e1] T1 ≡ T & ⇑[d2, e2 - e1] T ≡ T2. #d1 #e2 #T1 #T2 #H elim H -d1 -e2 -T1 -T2 [ /3 width=3/ | #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_ @@ -321,7 +321,7 @@ lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → qed. (* Basic_1: was only: dnf_dec2 dnf_dec *) -lemma is_lift_dec: ∀T2,d,e. Decidable (∃T1. ↑[d,e] T1 ≡ T2). +lemma is_lift_dec: ∀T2,d,e. Decidable (∃T1. ⇑[d,e] T1 ≡ T2). #T1 elim T1 -T1 [ * [1,3: /3 width=2/ ] #i #d #e elim (lt_dec i d) #Hid diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma index 3666799d4..6626b4e57 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma @@ -19,7 +19,7 @@ include "Basic_2/substitution/lift.ma". (* Main properies ***********************************************************) (* Basic_1: was: lift_inj *) -theorem lift_inj: ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U → T1 = T2. +theorem lift_inj: ∀d,e,T1,U. ⇑[d,e] T1 ≡ U → ∀T2. ⇑[d,e] T2 ≡ U → T1 = T2. #d #e #T1 #U #H elim H -d -e -T1 -U [ #k #d #e #X #HX lapply (lift_inv_sort2 … HX) -HX // @@ -37,10 +37,10 @@ theorem lift_inj: ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U qed-. (* Basic_1: was: lift_gen_lift *) -theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → - ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T → +theorem lift_div_le: ∀d1,e1,T1,T. ⇑[d1, e1] T1 ≡ T → + ∀d2,e2,T2. ⇑[d2 + e1, e2] T2 ≡ T → d1 ≤ d2 → - ∃∃T0. ↑[d1, e1] T0 ≡ T2 & ↑[d2, e2] T0 ≡ T1. + ∃∃T0. ⇑[d1, e1] T0 ≡ T2 & ⇑[d2, e2] T0 ≡ T1. #d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T [ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12 lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct /3 width=3/ @@ -70,10 +70,10 @@ theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → qed. (* Note: apparently this was missing in Basic_1 *) -theorem lift_div_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → - ∀e,e2,T2. ↑[d1 + e, e2] T2 ≡ T → +theorem lift_div_be: ∀d1,e1,T1,T. ⇑[d1, e1] T1 ≡ T → + ∀e,e2,T2. ⇑[d1 + e, e2] T2 ≡ T → e ≤ e1 → e1 ≤ e + e2 → - ∃∃T0. ↑[d1, e] T0 ≡ T2 & ↑[d1, e + e2 - e1] T0 ≡ T1. + ∃∃T0. ⇑[d1, e] T0 ≡ T2 & ⇑[d1, e + e2 - e1] T0 ≡ T1. #d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T [ #k #d1 #e1 #e #e2 #T2 #H >(lift_inv_sort2 … H) -H /2 width=3/ | #i #d1 #e1 #Hid1 #e #e2 #T2 #H #He1 #He1e2 @@ -99,7 +99,7 @@ theorem lift_div_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ] qed. -theorem lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2. +theorem lift_mono: ∀d,e,T,U1. ⇑[d,e] T ≡ U1 → ∀U2. ⇑[d,e] T ≡ U2 → U1 = U2. #d #e #T #U1 #H elim H -d -e -T -U1 [ #k #d #e #X #HX lapply (lift_inv_sort1 … HX) -HX // @@ -117,9 +117,9 @@ theorem lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 qed-. (* Basic_1: was: lift_free (left to right) *) -theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → - ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → - d1 ≤ d2 → d2 ≤ d1 + e1 → ↑[d1, e1 + e2] T1 ≡ T2. +theorem lift_trans_be: ∀d1,e1,T1,T. ⇑[d1, e1] T1 ≡ T → + ∀d2,e2,T2. ⇑[d2, e2] T ≡ T2 → + d1 ≤ d2 → d2 ≤ d1 + e1 → ⇑[d1, e1 + e2] T1 ≡ T2. #d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T [ #k #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_ >(lift_inv_sort1 … HT2) -HT2 // @@ -145,9 +145,9 @@ theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → qed. (* Basic_1: was: lift_d (right to left) *) -theorem lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → - ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d2 ≤ d1 → - ∃∃T0. ↑[d2, e2] T1 ≡ T0 & ↑[d1 + e2, e1] T0 ≡ T2. +theorem lift_trans_le: ∀d1,e1,T1,T. ⇑[d1, e1] T1 ≡ T → + ∀d2,e2,T2. ⇑[d2, e2] T ≡ T2 → d2 ≤ d1 → + ∃∃T0. ⇑[d2, e2] T1 ≡ T0 & ⇑[d1 + e2, e1] T0 ≡ T2. #d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T [ #k #d1 #e1 #d2 #e2 #X #HX #_ >(lift_inv_sort1 … HX) -HX /2 width=3/ @@ -172,9 +172,9 @@ theorem lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → qed. (* Basic_1: was: lift_d (left to right) *) -theorem lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → - ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d1 + e1 ≤ d2 → - ∃∃T0. ↑[d2 - e1, e2] T1 ≡ T0 & ↑[d1, e1] T0 ≡ T2. +theorem lift_trans_ge: ∀d1,e1,T1,T. ⇑[d1, e1] T1 ≡ T → + ∀d2,e2,T2. ⇑[d2, e2] T ≡ T2 → d1 + e1 ≤ d2 → + ∃∃T0. ⇑[d2 - e1, e2] T1 ≡ T0 & ⇑[d1, e1] T0 ≡ T2. #d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T [ #k #d1 #e1 #d2 #e2 #X #HX #_ >(lift_inv_sort1 … HX) -HX /2 width=3/ diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubcs.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma similarity index 67% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/lsubcs.ma rename to matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma index 0d799f964..91b03c0b9 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubcs.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma @@ -12,20 +12,17 @@ (* *) (**************************************************************************) -include "Basic_2/computation/lsubc.ma". -include "Basic_2/computation/csn.ma". +include "Basic_2/grammar/term_vector.ma". +include "Basic_2/substitution/lift.ma". -(* LOCAL ENVIRONMENT REFINEMENT FOR STRONG NORMALIZATION ********************) +(* RELOCATION ***************************************************************) -definition lsubcs: relation lenv ≝ lsubc csn. +inductive liftv (d,e:nat) : relation (list term) ≝ +| liftv_nil : liftv d e ◊ ◊ +| liftv_cons: ∀T1s,T2s,T1,T2. + ⇑[d, e] T1 ≡ T2 → liftv d e T1s T2s → + liftv d e (T1 :: T1s) (T2 :: T2s) +. -interpretation - "local environment refinement (strong normalization)" - 'CrSubEq L1 L2 = (lsubcs L1 L2). +interpretation "relocation (vector)" 'RLift d e T1s T2s = (liftv d e T1s T2s). -(* Basic properties *********************************************************) - -lemma lsubcs_refl: ∀L. L ⊑ L. -// qed. - -(* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma index f777d1cd7..11745b425 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma @@ -17,8 +17,8 @@ include "Basic_2/substitution/ltps.ma". (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************) lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → - d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. + ∀L2,e2. ⇓[0, e2] L0 ≡ L2 → + d1 + e1 ≤ e2 → ⇓[0, e2] L1 ≡ L2. #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // | // @@ -34,8 +34,8 @@ lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → qed. lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → - d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. + ∀L2,e2. ⇓[0, e2] L0 ≡ L2 → + d1 + e1 ≤ e2 → ⇓[0, e2] L1 ≡ L2. #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // | // @@ -51,8 +51,8 @@ lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → qed. lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L2 [0, d1 + e1 - e2] ≫ L & ↓[0, e2] L1 ≡ L. + ∀L2,e2. ⇓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → + ∃∃L. L2 [0, d1 + e1 - e2] ≫ L & ⇓[0, e2] L1 ≡ L. #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 @@ -73,8 +73,8 @@ lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → qed. lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L [0, d1 + e1 - e2] ≫ L2 & ↓[0, e2] L1 ≡ L. + ∀L2,e2. ⇓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → + ∃∃L. L [0, d1 + e1 - e2] ≫ L2 & ⇓[0, e2] L1 ≡ L. #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 @@ -95,8 +95,8 @@ lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → qed. lemma ltps_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → - ∃∃L. L2 [d1 - e2, e1] ≫ L & ↓[0, e2] L1 ≡ L. + ∀L2,e2. ⇓[0, e2] L0 ≡ L2 → e2 ≤ d1 → + ∃∃L. L2 [d1 - e2, e1] ≫ L & ⇓[0, e2] L1 ≡ L. #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | /2 width=3/ @@ -113,8 +113,8 @@ lemma ltps_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → qed. lemma ltps_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → - ∃∃L. L [d1 - e2, e1] ≫ L2 & ↓[0, e2] L1 ≡ L. + ∀L2,e2. ⇓[0, e2] L0 ≡ L2 → e2 ≤ d1 → + ∃∃L. L [d1 - e2, e1] ≫ L2 & ⇓[0, e2] L1 ≡ L. #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | /2 width=3/ diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma index d46642d47..df69749cd 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma @@ -20,7 +20,7 @@ include "Basic_2/substitution/ldrop.ma". inductive tps: nat → nat → lenv → relation term ≝ | tps_atom : ∀L,I,d,e. tps d e L (𝕒{I}) (𝕒{I}) | tps_subst: ∀L,K,V,W,i,d,e. d ≤ i → i < d + e → - ↓[0, i] L ≡ K. 𝕓{Abbr} V → ↑[0, i + 1] V ≡ W → tps d e L (#i) W + ⇓[0, i] L ≡ K. 𝕓{Abbr} V → ⇑[0, i + 1] V ≡ W → tps d e L (#i) W | tps_bind : ∀L,I,V1,V2,T1,T2,d,e. tps d e L V1 V2 → tps (d + 1) e (L. 𝕓{I} V2) T1 T2 → tps d e L (𝕓{I} V1. T1) (𝕓{I} V2. T2) @@ -51,8 +51,8 @@ lemma tps_refl: ∀T,L,d,e. L ⊢ T [d, e] ≫ T. qed. (* Basic_1: was: subst1_ex *) -lemma tps_full: ∀K,V,T1,L,d. ↓[0, d] L ≡ (K. 𝕓{Abbr} V) → - ∃∃T2,T. L ⊢ T1 [d, 1] ≫ T2 & ↑[d, 1] T ≡ T2. +lemma tps_full: ∀K,V,T1,L,d. ⇓[0, d] L ≡ (K. 𝕓{Abbr} V) → + ∃∃T2,T. L ⊢ T1 [d, 1] ≫ T2 & ⇑[d, 1] T ≡ T2. #K #V #T1 elim T1 -T1 [ * #i #L #d #HLK /2 width=4/ elim (lt_or_eq_or_gt i d) #Hid /3 width=4/ @@ -127,8 +127,8 @@ qed. fact tps_inv_atom1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀I. T1 = 𝕒{I} → T2 = 𝕒{I} ∨ ∃∃K,V,i. d ≤ i & i < d + e & - ↓[O, i] L ≡ K. 𝕓{Abbr} V & - ↑[O, i + 1] V ≡ T2 & + ⇓[O, i] L ≡ K. 𝕓{Abbr} V & + ⇑[O, i + 1] V ≡ T2 & I = LRef i. #L #T1 #T2 #d #e * -L -T1 -T2 -d -e [ #L #I #d #e #J #H destruct /2 width=1/ @@ -141,8 +141,8 @@ qed. lemma tps_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ≫ T2 → T2 = 𝕒{I} ∨ ∃∃K,V,i. d ≤ i & i < d + e & - ↓[O, i] L ≡ K. 𝕓{Abbr} V & - ↑[O, i + 1] V ≡ T2 & + ⇓[O, i] L ≡ K. 𝕓{Abbr} V & + ⇑[O, i + 1] V ≡ T2 & I = LRef i. /2 width=3/ qed-. @@ -158,8 +158,8 @@ qed-. lemma tps_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫ T2 → T2 = #i ∨ ∃∃K,V. d ≤ i & i < d + e & - ↓[O, i] L ≡ K. 𝕓{Abbr} V & - ↑[O, i + 1] V ≡ T2. + ⇓[O, i] L ≡ K. 𝕓{Abbr} V & + ⇑[O, i + 1] V ≡ T2. #L #T2 #i #d #e #H elim (tps_inv_atom1 … H) -H /2 width=1/ * #K #V #j #Hdj #Hjde #HLK #HVT2 #H destruct /3 width=4/ diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma index aaecbbf3b..3b1453c37 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma @@ -20,7 +20,7 @@ include "Basic_2/substitution/tps.ma". (* Advanced inversion lemmas ************************************************) fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 → - ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2. + ∀K,V. ⇓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2. #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e [ // | #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct @@ -34,15 +34,15 @@ fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 → qed. lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫ T2 → - ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2. + ∀K,V. ⇓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2. /2 width=8/ qed-. (* Relocation properties ****************************************************) (* Basic_1: was: subst1_lift_lt *) lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → - ∀L,U1,U2,d,e. ↓[d, e] L ≡ K → - ↑[d, e] T1 ≡ U1 → ↑[d, e] T2 ≡ U2 → + ∀L,U1,U2,d,e. ⇓[d, e] L ≡ K → + ⇑[d, e] T1 ≡ U1 → ⇑[d, e] T2 ≡ U2 → dt + et ≤ d → L ⊢ U1 [dt, et] ≫ U2. #K #T1 #T2 #dt #et #H elim H -K -T1 -T2 -dt -et @@ -66,8 +66,8 @@ lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → qed. lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → - ∀L,U1,U2,d,e. ↓[d, e] L ≡ K → - ↑[d, e] T1 ≡ U1 → ↑[d, e] T2 ≡ U2 → + ∀L,U1,U2,d,e. ⇓[d, e] L ≡ K → + ⇑[d, e] T1 ≡ U1 → ⇑[d, e] T2 ≡ U2 → dt ≤ d → d ≤ dt + et → L ⊢ U1 [dt, et + e] ≫ U2. #K #T1 #T2 #dt #et #H elim H -K -T1 -T2 -dt -et @@ -99,8 +99,8 @@ qed. (* Basic_1: was: subst1_lift_ge *) lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → - ∀L,U1,U2,d,e. ↓[d, e] L ≡ K → - ↑[d, e] T1 ≡ U1 → ↑[d, e] T2 ≡ U2 → + ∀L,U1,U2,d,e. ⇓[d, e] L ≡ K → + ⇑[d, e] T1 ≡ U1 → ⇑[d, e] T2 ≡ U2 → d ≤ dt → L ⊢ U1 [dt + e, et] ≫ U2. #K #T1 #T2 #dt #et #H elim H -K -T1 -T2 -dt -et @@ -123,9 +123,9 @@ qed. (* Basic_1: was: subst1_gen_lift_lt *) lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → - ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → + ∀K,d,e. ⇓[d, e] L ≡ K → ∀T1. ⇑[d, e] T1 ≡ U1 → dt + et ≤ d → - ∃∃T2. K ⊢ T1 [dt, et] ≫ T2 & ↑[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 [dt, et] ≫ T2 & ⇑[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H elim H -L -U1 -U2 -dt -et [ #L * #i #dt #et #K #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ @@ -150,9 +150,9 @@ lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → qed. lemma tps_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → - ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → + ∀K,d,e. ⇓[d, e] L ≡ K → ∀T1. ⇑[d, e] T1 ≡ U1 → dt ≤ d → d + e ≤ dt + et → - ∃∃T2. K ⊢ T1 [dt, et - e] ≫ T2 & ↑[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 [dt, et - e] ≫ T2 & ⇑[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H elim H -L -U1 -U2 -dt -et [ #L * #i #dt #et #K #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ @@ -188,9 +188,9 @@ qed. (* Basic_1: was: subst1_gen_lift_ge *) lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → - ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → + ∀K,d,e. ⇓[d, e] L ≡ K → ∀T1. ⇑[d, e] T1 ≡ U1 → d + e ≤ dt → - ∃∃T2. K ⊢ T1 [dt - e, et] ≫ T2 & ↑[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 [dt - e, et] ≫ T2 & ⇑[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H elim H -L -U1 -U2 -dt -et [ #L * #i #dt #et #K #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ @@ -221,7 +221,7 @@ qed. (* Basic_1: was: subst1_gen_lift_eq *) lemma tps_inv_lift1_eq: ∀L,U1,U2,d,e. - L ⊢ U1 [d, e] ≫ U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2. + L ⊢ U1 [d, e] ≫ U2 → ∀T1. ⇑[d, e] T1 ≡ U1 → U1 = U2. #L #U1 #U2 #d #e #H elim H -L -U1 -U2 -d -e [ // | #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #T1 #H @@ -254,9 +254,9 @@ qed. (EX u1 | t1 = (lift (minus (plus d h) (S i)) (S i) u1)). *) lemma tps_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → - ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → + ∀K,d,e. ⇓[d, e] L ≡ K → ∀T1. ⇑[d, e] T1 ≡ U1 → d ≤ dt → dt ≤ d + e → d + e ≤ dt + et → - ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ≫ T2 & ↑[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ≫ T2 & ⇑[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet elim (tps_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2 lapply (tps_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1 @@ -265,9 +265,9 @@ elim (tps_inv_lift1_ge … HU2 … HLK … HTU1 ?) -U -L // (lift_mono … HTU1 … H) -H // @@ -90,8 +90,8 @@ qed. lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 → ∀L,U1,d,e. dt ≤ d → d ≤ dt + et → - ↓[d, e] L ≡ K → ↑[d, e] T1 ≡ U1 → - ∀U2. ↑[d, e] T2 ≡ U2 → L ⊢ U1 [dt, et + e] ≫* U2. + ⇓[d, e] L ≡ K → ⇑[d, e] T1 ≡ U1 → + ∀U2. ⇑[d, e] T2 ≡ U2 → L ⊢ U1 [dt, et + e] ≫* U2. #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(tpss_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 @@ -102,8 +102,8 @@ lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 → qed. lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 → - ∀L,U1,d,e. d ≤ dt → ↓[d, e] L ≡ K → - ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → + ∀L,U1,d,e. d ≤ dt → ⇓[d, e] L ≡ K → + ⇑[d, e] T1 ≡ U1 → ∀U2. ⇑[d, e] T2 ≡ U2 → L ⊢ U1 [dt + e, et] ≫* U2. #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(tpss_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // @@ -115,9 +115,9 @@ lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 → qed. lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 → - ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → + ∀K,d,e. ⇓[d, e] L ≡ K → ∀T1. ⇑[d, e] T1 ≡ U1 → dt + et ≤ d → - ∃∃T2. K ⊢ T1 [dt, et] ≫* T2 & ↑[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 [dt, et] ≫* T2 & ⇑[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -U2 [ /2 width=3/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -126,9 +126,9 @@ lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 → qed. lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 → - ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → + ∀K,d,e. ⇓[d, e] L ≡ K → ∀T1. ⇑[d, e] T1 ≡ U1 → dt ≤ d → d + e ≤ dt + et → - ∃∃T2. K ⊢ T1 [dt, et - e] ≫* T2 & ↑[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 [dt, et - e] ≫* T2 & ⇑[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(tpss_ind … H) -U2 [ /2 width=3/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -137,9 +137,9 @@ lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 → qed. lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 → - ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → + ∀K,d,e. ⇓[d, e] L ≡ K → ∀T1. ⇑[d, e] T1 ≡ U1 → d + e ≤ dt → - ∃∃T2. K ⊢ T1 [dt - e, et] ≫* T2 & ↑[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 [dt - e, et] ≫* T2 & ⇑[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -U2 [ /2 width=3/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -148,16 +148,16 @@ lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 → qed. lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e. - L ⊢ U1 [d, e] ≫* U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2. + L ⊢ U1 [d, e] ≫* U2 → ∀T1. ⇑[d, e] T1 ≡ U1 → U1 = U2. #L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -U2 // #U #U2 #_ #HU2 #IHU destruct <(tps_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 // qed. lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 → - ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → + ∀K,d,e. ⇓[d, e] L ≡ K → ∀T1. ⇑[d, e] T1 ≡ U1 → dt ≤ d → dt + et ≤ d + e → - ∃∃T2. K ⊢ T1 [dt, d - dt] ≫* T2 & ↑[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 [dt, d - dt] ≫* T2 & ⇑[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(tpss_ind … H) -U2 [ /2 width=3/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma index cd7e666b2..9b40460f2 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma @@ -59,9 +59,9 @@ lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 → qed. lemma tpss_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 → - ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → + ∀K,d,e. ⇓[d, e] L ≡ K → ∀T1. ⇑[d, e] T1 ≡ U1 → d ≤ dt → dt ≤ d + e → d + e ≤ dt + et → - ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ≫* T2 & ↑[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ≫* T2 & ⇑[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet elim (tpss_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2 lapply (tpss_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1 diff --git a/matita/matita/contribs/lambda_delta/Ground_2/list.ma b/matita/matita/contribs/lambda_delta/Ground_2/list.ma index 9bdc5c126..846d1f804 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/list.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/list.ma @@ -25,10 +25,8 @@ interpretation "nil (list)" 'Nil = (nil ?). interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl). -let rec append A (l1: list A) l2 on l1 ≝ - match l1 with - [ nil ⇒ l2 - | cons hd tl ⇒ hd :: append A tl l2 +let rec all A (R:predicate A) (l:list A) on l ≝ + match l with + [ nil ⇒ True + | cons hd tl ⇒ R hd ∧ all A R tl ]. - -interpretation "append (list)" 'Append l1 l2 = (append ? 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 45109878f..5238b0d13 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/notation.ma @@ -16,6 +16,10 @@ (* Lists ********************************************************************) +notation "hvbox( ◊ )" + non associative with precedence 90 + for @{'Nil}. + notation "hvbox( hd break :: tl )" right associative with precedence 47 for @{'Cons $hd $tl}. -- 2.39.2