From 35653f628dc3a3e665fee01acc19c660c9d555e3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 20 Dec 2011 14:29:27 +0000 Subject: [PATCH 1/1] - the definition of the framework for strong normalization continues ... - functional version of relocation and core substitution implemented - standard arithmetics library updated --- .../lambda_delta/Basic_2/computation/csn.ma | 23 ++++++ .../Basic_2/computation/csn_aarity.ma | 28 +++++++ .../Basic_2/computation/csn_cr.ma | 25 +++++++ .../lambda_delta/Basic_2/computation/lsubc.ma | 36 +++++++++ .../Basic_2/computation/lsubcs.ma | 31 ++++++++ .../lambda_delta/Basic_2/functional/lift.ma | 68 +++++++++++++++++ .../lambda_delta/Basic_2/functional/subst.ma | 74 +++++++++++++++++++ .../lambda_delta/Basic_2/grammar/aarity.ma | 66 +++++++++++++++++ .../contribs/lambda_delta/Basic_2/notation.ma | 11 +++ .../lambda_delta/Basic_2/static/aaa.ma | 33 +++++++++ .../lambda_delta/Basic_2/substitution/lift.ma | 7 +- .../Basic_2/substitution/lift_lift.ma | 32 +++++++- .../lambda_delta/Basic_2/substitution/tps.ma | 6 ++ .../lambda_delta/Basic_2/unfold/delift.ma | 61 +++++++++++++++ .../Basic_2/unfold/delift_lift.ma | 54 ++++++++++++++ .../lambda_delta/Basic_2/unfold/tpss.ma | 9 +++ .../contribs/lambda_delta/Ground_2/arith.ma | 29 -------- .../contribs/lambda_delta/Ground_2/tri.ma | 44 +++++++++++ matita/matita/lib/arithmetics/nat.ma | 43 ++++++++++- 19 files changed, 647 insertions(+), 33 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aarity.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/lsubcs.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/static/aaa.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/unfold/delift_lift.ma create mode 100644 matita/matita/contribs/lambda_delta/Ground_2/tri.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma new file mode 100644 index 000000000..fb94c8eee --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/cpr.ma". + +(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) + +definition csn: lenv → predicate term ≝ λL. SN … (cpr L) (eq …). + +interpretation + "context-sensitive strong normalization (term)" + 'SN L T = (csn L T). diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aarity.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aarity.ma new file mode 100644 index 000000000..7c84f3c08 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aarity.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/csn_cr.ma". +include "Basic_2/computation/lsubcs.ma". + +(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) + +(* Main propertis ***********************************************************) + +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. 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 new file mode 100644 index 000000000..915b17288 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.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/computation/acp_cr.ma". +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. + +interpretation + "candidate of reducibility (contex-sensitive strong normalization)" + 'InEInt L T A = (snc A 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 new file mode 100644 index 000000000..8cf302dc8 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic_2/computation/acp_cr.ma". + +(* 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) +. + +interpretation + "local environment refinement (abstract candidates of reducibility)" + 'CrSubEq L1 R L2 = (lsubc R L1 L2). + +(* Basic properties *********************************************************) + +lemma lsubc_refl: ∀R,L. L [R] ⊑ L. +#R #L elim L -L // /2 width=1/ +qed. + +(* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubcs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubcs.ma new file mode 100644 index 000000000..0d799f964 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubcs.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic_2/computation/lsubc.ma". +include "Basic_2/computation/csn.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRONG NORMALIZATION ********************) + +definition lsubcs: relation lenv ≝ lsubc csn. + +interpretation + "local environment refinement (strong normalization)" + 'CrSubEq L1 L2 = (lsubcs L1 L2). + +(* Basic properties *********************************************************) + +lemma lsubcs_refl: ∀L. L ⊑ L. +// 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 new file mode 100644 index 000000000..4debfaabf --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Ground_2/tri.ma". +include "Basic_2/substitution/lift.ma". + +(* RELOCATION ***************************************************************) + +let rec flift d e U on U ≝ match U with +[ TAtom I ⇒ match I with + [ Sort _ ⇒ U + | LRef i ⇒ #(tri … i d i (i + e) (i + e)) + | GRef _ ⇒ U + ] +| TPair I V T ⇒ match I with + [ Bind I ⇒ 𝕓{I} (flift d e V). (flift (d+1) e T) + | Flat I ⇒ 𝕗{I} (flift d e V). (flift d e T) + ] +]. + +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. +#T elim T -T +[ * #i #d #e // + elim (lt_or_eq_or_gt i d) #Hid normalize + [ >(tri_lt ?????? Hid) /2 width=1/ + | /2 width=1/ + | >(tri_gt ?????? Hid) /3 width=2/ + ] +| * /2/ +] +qed. + +(* Main inversion properties ************************************************) + +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 + elim (le_to_or_lt_eq … Hid) -Hid #Hid + [ >(tri_gt ?????? Hid) // + | destruct // + ] +] +qed-. + +(* Derived properties *******************************************************) + +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 +>(flift_inv_lift … H) -H // +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma new file mode 100644 index 000000000..5c92a1293 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic_2/unfold/delift_lift.ma". +include "Basic_2/functional/lift.ma". + +(* CORE SUBSTITUTION ********************************************************) + +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)) + | GRef _ ⇒ U + ] +| TPair I V T ⇒ match I with + [ Bind I ⇒ 𝕓{I} (fsubst W d V). (fsubst W (d+1) T) + | Flat I ⇒ 𝕗{I} (fsubst W d V). (fsubst W d T) + ] +]. + +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. +#K #V #T elim T -T +[ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/ + elim (lt_or_eq_or_gt i d) #Hid + [ -HLK >(tri_lt ?????? Hid) /3 width=3/ + | destruct >tri_eq /4 width=4 by tpss_strap, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *) + | -HLK >(tri_gt ?????? Hid) /3 width=3/ + ] +| * /3 width=1/ /4 width=1/ +] +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. +#K #V #T1 elim T1 -T1 +[ * #i #L #T2 #d #HLK #H + [ -HLK >(delift_fwd_sort1 … H) -H // + | elim (lt_or_eq_or_gt i d) #Hid normalize + [ -HLK >(delift_fwd_lref1_lt … H) -H // /2 width=1/ + | destruct + elim (delift_fwd_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0 + lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H >minus_plus (delift_inv_refl_O2 … HV2) -V >(flift_inv_lift … HVT2) -V2 // + | -HLK >(delift_fwd_lref1_ge … H) -H // /2 width=1/ + ] + | -HLK >(delift_fwd_gref1 … H) -H // + ] +| * #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H + [ elim (delift_fwd_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/ + | elim (delift_fwd_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // + ] +] +qed-. + \ No newline at end of file diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma new file mode 100644 index 000000000..42354e700 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma @@ -0,0 +1,66 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Ground_2/list.ma". +include "Basic_2/notation.ma". + +(* ATOMIC ARITY *************************************************************) + +inductive aarity: Type[0] ≝ + | AAtom: aarity (* atomic aarity construction *) + | APair: aarity → aarity → aarity (* binary aarity construction *) +. + +interpretation "aarity construction (atomic)" 'SItem = AAtom. + +interpretation "aarity construction (binary)" 'SItem A1 A2 = (APair A1 A2). + +(* Basic inversion lemmas ***************************************************) + +lemma discr_apair_xy_x: ∀A,B. 𝕔 B. A = B → False. +#A #B elim B -B +[ #H destruct +| #Y #X #IHY #_ #H destruct + -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *) + /2 width=1/ +] +qed-. + +lemma discr_tpair_xy_y: ∀B,A. 𝕔 B. A = A → False. +#B #A elim A -A +[ #H destruct +| #Y #X #_ #IHX #H destruct + -H (**) (* destruct: the destucted equality is not erased *) + /2 width=1/ +] +qed-. + +(* Basic properties *********************************************************) + +lemma aarity_eq_dec: ∀A1,A2:aarity. Decidable (A1 = A2). +#A1 elim A1 -A1 +[ #A2 elim A2 -A2 /2 width=1/ + #B2 #A2 #_ #_ @or_intror #H destruct +| #B1 #A1 #IHB1 #IHA1 #A2 elim A2 -A2 + [ -IHB1 -IHA1 @or_intror #H destruct + | #B2 #A2 #_ #_ elim (IHB1 B2) -IHB1 + [ #H destruct elim (IHA1 A2) -IHA1 + [ #H destruct /2 width=1/ + | #HA12 @or_intror #H destruct /2 width=1/ + ] + | -IHA1 #HB12 @or_intror #H destruct /2 width=1/ + ] + ] +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index 8e1d4362a..4d71723d0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -225,3 +225,14 @@ notation "hvbox( T1 ⊑ break T2 )" notation "hvbox( T1 break [ R ] ⊑ break T2 )" non associative with precedence 45 for @{ 'CrSubEq $T1 $R $T2 }. + +(* Functional ***************************************************************) + +notation "hvbox( ↟ [ d , break e ] break T )" + non associative with precedence 80 + for @{ 'Lift $d $e $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/static/aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa.ma new file mode 100644 index 000000000..01af2572f --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa.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/grammar/aarity.ma". +include "Basic_2/substitution/ldrop.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +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_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_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 +. + +interpretation + "atomic arity assignment (term)" + 'AtomicArity L T A = (aaa L T A). 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 fa1dfae28..e8e23a555 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma @@ -36,11 +36,11 @@ interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2). (* Basic inversion lemmas ***************************************************) -fact lift_inv_refl_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: ∀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. @@ -277,6 +277,9 @@ 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. +/2 width=1/ qed-. + (* Basic_1: was: lift_r *) lemma lift_refl: ∀T,d. ↑[d, 0] T ≡ T. #T elim T -T 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 cfcf976e0..3666799d4 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 @@ -50,7 +50,7 @@ theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12 elim (lift_inv_lref2 … Hi) -Hi * #Hid2 #H destruct [ -Hd12 lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3 width=3/ - | -Hid1 >plus_plus_comm_23 in Hid2; #H lapply (le_inv_plus_plus_r … H) -H #H + | -Hid1 >plus_plus_comm_23 in Hid2; #H lapply (le_plus_to_le_r … H) -H #H elim (le_inv_plus_l … H) -H #Hide2 #He2i lapply (transitive_le … Hd12 Hide2) -Hd12 #Hd12 >le_plus_minus_comm // >(plus_minus_m_m i e2) in ⊢ (? ? ? %); // -He2i @@ -69,6 +69,36 @@ 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 → + e ≤ e1 → e1 ≤ e + e2 → + ∃∃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 + >(lift_inv_lref2_lt … H) -H [ /3 width=3/ | /2 width=3/ ] +| #i #d1 #e1 #Hid1 #e #e2 #T2 #H #He1 #He1e2 + elim (lt_or_ge (i+e1) (d1+e+e2)) #Hie1d1e2 + [ elim (lift_inv_lref2_be … H ? ?) -H // /2 width=1/ + | >(lift_inv_lref2_ge … H ?) -H // + lapply (le_plus_to_minus … Hie1d1e2) #Hd1e21i + elim (le_inv_plus_l … Hie1d1e2) -Hie1d1e2 #Hd1e12 #He2ie1 + @ex2_1_intro [2: /2 width=1/ | skip ] -Hd1e12 + @lift_lref_ge_minus_eq [ >plus_minus_commutative // | /2 width=1/ ] + ] +| #p #d1 #e1 #e #e2 #T2 #H >(lift_inv_gref2 … H) -H /2 width=3/ +| #I #V1 #V #T1 #T #d1 #e1 #_ #_ #IHV1 #IHT1 #e #e2 #X #H #He1 #He1e2 + elim (lift_inv_bind2 … H) -H #V2 #T2 #HV2 #HT2 #H destruct + elim (IHV1 … HV2 ? ?) -V // >plus_plus_comm_23 in HT2; #HT2 + elim (IHT1 … HT2 ? ?) -T // -He1 -He1e2 /3 width=5/ +| #I #V1 #V #T1 #T #d1 #e1 #_ #_ #IHV1 #IHT1 #e #e2 #X #H #He1 #He1e2 + elim (lift_inv_flat2 … H) -H #V2 #T2 #HV2 #HT2 #H destruct + elim (IHV1 … HV2 ? ?) -V // + elim (IHT1 … HT2 ? ?) -T // -He1 -He1e2 /3 width=5/ +] +qed. + 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 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 969e67485..d46642d47 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma @@ -165,6 +165,12 @@ elim (tps_inv_atom1 … H) -H /2 width=1/ * #K #V #j #Hdj #Hjde #HLK #HVT2 #H destruct /3 width=4/ qed-. +lemma tps_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p [d, e] ≫ T2 → T2 = §p. +#L #T2 #p #d #e #H +elim (tps_inv_atom1 … H) -H // +* #K #V #i #_ #_ #_ #_ #H destruct +qed-. + fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift.ma index 5d19b650e..bb437ef13 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift.ma @@ -21,3 +21,64 @@ definition delift: nat → nat → lenv → relation term ≝ interpretation "delift (term)" 'TSubst L T1 d e T2 = (delift d e L T1 T2). + +(* Basic properties *********************************************************) + +lemma delift_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡ T2 → + ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≡ T2. +#L1 #T1 #T2 #d #e * /3 width=3/ +qed. + +lemma delift_bind: ∀I,L,V1,V2,T1,T2,d,e. + L ⊢ V1 [d, e] ≡ V2 → L. 𝕓{I} V2 ⊢ T1 [d+1, e] ≡ T2 → + L ⊢ 𝕓{I} V1. T1 [d, e] ≡ 𝕓{I} V2. T2. +#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2 +lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /2 width=1/ /3 width=5/ +qed. + +lemma delift_flat: ∀I,L,V1,V2,T1,T2,d,e. + L ⊢ V1 [d, e] ≡ V2 → L ⊢ T1 [d, e] ≡ T2 → + L ⊢ 𝕗{I} V1. T1 [d, e] ≡ 𝕗{I} V2. T2. +#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * /3 width=5/ +qed. + +(* Basic forward lemmas *****************************************************) + +lemma delift_fwd_sort1: ∀L,U2,d,e,k. L ⊢ ⋆k [d, e] ≡ U2 → U2 = ⋆k. +#L #U2 #d #e #k * #U #HU +>(tpss_inv_sort1 … HU) -HU #HU2 +>(lift_inv_sort2 … HU2) -HU2 // +qed-. + +lemma delift_fwd_gref1: ∀L,U2,d,e,p. L ⊢ §p [d, e] ≡ U2 → U2 = §p. +#L #U #d #e #p * #U #HU +>(tpss_inv_gref1 … HU) -HU #HU2 +>(lift_inv_gref2 … HU2) -HU2 // +qed-. + +lemma delift_fwd_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ 𝕓{I} V1. T1 [d, e] ≡ U2 → + ∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 & + L. 𝕓{I} V2 ⊢ T1 [d+1, e] ≡ T2 & + U2 = 𝕓{I} V2. T2. +#I #L #V1 #T1 #U2 #d #e * #U #HU #HU2 +elim (tpss_inv_bind1 … HU) -HU #V #T #HV1 #HT1 #X destruct +elim (lift_inv_bind2 … HU2) -HU2 #V2 #T2 #HV2 #HT2 +lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /2 width=1/ /3 width=5/ +qed-. + +lemma delift_fwd_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ 𝕗{I} V1. T1 [d, e] ≡ U2 → + ∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 & + L ⊢ T1 [d, e] ≡ T2 & + U2 = 𝕗{I} V2. T2. +#I #L #V1 #T1 #U2 #d #e * #U #HU #HU2 +elim (tpss_inv_flat1 … HU) -HU #V #T #HV1 #HT1 #X destruct +elim (lift_inv_flat2 … HU2) -HU2 /3 width=5/ +qed-. + +(* Basic Inversion lemmas ***************************************************) + +lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≡ T2 → T1 = T2. +#L #T1 #T2 #d * #T #HT1 +>(tpss_inv_refl_O2 … HT1) -HT1 #HT2 +>(lift_inv_refl_O2 … HT2) -HT2 // +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift_lift.ma new file mode 100644 index 000000000..02d026ceb --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift_lift.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic_2/unfold/tpss_lift.ma". +include "Basic_2/unfold/delift.ma". + +(* DELIFT ON TERMS **********************************************************) + +(* Advanced forward lemmas **************************************************) + +lemma delift_fwd_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → i < d → U2 = #i. +#L #U2 #i #d #e * #U #HU #HU2 #Hid +elim (tpss_inv_lref1 … HU) -HU +[ #H destruct >(lift_inv_lref2_lt … HU2) // +| * #K #V1 #V2 #Hdi + lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi + elim (lt_refl_false … Hi) +] +qed-. + +lemma delift_fwd_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 → + d ≤ i → i < d + e → + ∃∃K,V1,V2. ↓[0, i] L ≡ K. 𝕓{Abbr} V1 & + K ⊢ V1 [0, d + e - i - 1] ≡ V2 & + ↑[0, d] V2 ≡ U2. +#L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide +elim (tpss_inv_lref1 … HU) -HU +[ #H destruct elim (lift_inv_lref2_be … HU2 ? ?) // +| * #K #V1 #V #_ #_ #HLK #HV1 #HVU + elim (lift_div_be … HVU … HU2 ? ?) -U // /2 width=1/ /3 width=6/ +] +qed-. + +lemma delift_fwd_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → + d + e ≤ i → U2 = #(i - e). +#L #U2 #i #d #e * #U #HU #HU2 #Hdei +elim (tpss_inv_lref1 … HU) -HU +[ #H destruct >(lift_inv_lref2_ge … HU2) // +| * #K #V1 #V2 #_ #Hide + lapply (lt_to_le_to_lt … Hide Hdei) -Hide -Hdei #Hi + elim (lt_refl_false … Hi) +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma index 98a8caa50..0f6196e52 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma @@ -107,6 +107,15 @@ lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ≫* T2 → T2 = ⋆k. ] qed-. +(* Note: this can be derived from tpss_inv_atom1 *) +lemma tpss_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p [d, e] ≫* T2 → T2 = §p. +#L #T2 #p #d #e #H @(tpss_ind … H) -T2 +[ // +| #T #T2 #_ #HT2 #IHT destruct + >(tps_inv_gref1 … HT2) -HT2 // +] +qed-. + lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫* U2 → ∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 & L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫* T2 & diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma index 37fac204b..418a176d5 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma @@ -19,22 +19,12 @@ include "Ground_2/star.ma". (* equations ****************************************************************) -lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y. -// qed. - lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p). /2 by plus_minus/ qed. lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n. /2 by plus_minus/ qed. -lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b. -/3 by monotonic_le_minus_l, le_to_le_to_eq/ qed. - -lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b. -#b #c #a #H >(plus_minus_m_m b c) in ⊢ (? ? ?%); // -qed. - lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b. #a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm // qed. @@ -57,25 +47,12 @@ axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2). axiom lt_dec: ∀n1,n2. Decidable (n1 < n2). -lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m. -#m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/ -qed-. - lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m. #m #n elim (lt_or_ge m n) /2 width=1/ #H elim H -m /2 width=1/ #m #Hm * #H /2 width=1/ /3 width=1/ qed-. -lemma le_inv_plus_plus_r: ∀x,y,z. x + z ≤ y + z → x ≤ y. -/2 by le_plus_to_le/ qed-. - -lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z. -/3 width=2/ qed-. - -lemma lt_inv_plus_l: ∀x,y,z. x + y < z → x < z ∧ y < z - x. -/3 width=2/ qed-. - lemma lt_refl_false: ∀n. n < n → False. #n #H elim (lt_to_not_eq … H) -H /2 width=1/ qed-. @@ -89,12 +66,6 @@ lemma false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x. #Hxy elim (H Hxy) qed-. -lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2. -#m1 #m2 #H #n1 #n2 >commutative_plus -#H elim (le_inv_plus_l … H) -H >commutative_plus (plus_minus_m_m b c) in ⊢ (? ? ?%); // +qed. + +(* Stilll more atomic conclusion ********************************************) + +(* le *) + +lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2. +#m1 #m2 #H #n1 #n2 >commutative_plus +#H elim (le_inv_plus_l … H) -H >commutative_plus