From 7345613effa9d152f940b2ac637e9584c59c0d6e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 6 Jun 2011 17:19:30 +0000 Subject: [PATCH] We reintroduce the distinction between binding and non-binding items. Mon-binding items are now forbidden in environments --- .../matita/lib/lambda-delta/language/item.ma | 39 +++-- .../matita/lib/lambda-delta/language/lenv.ma | 6 +- .../matita/lib/lambda-delta/language/term.ma | 12 +- .../lib/lambda-delta/language/weight.ma | 14 +- matita/matita/lib/lambda-delta/notation.ma | 20 ++- .../lib/lambda-delta/substitution/lift.ma | 147 +++++++++++------- .../lib/lambda-delta/substitution/subst.ma | 23 +-- .../lib/lambda-delta/substitution/thin.ma | 15 +- 8 files changed, 172 insertions(+), 104 deletions(-) diff --git a/matita/matita/lib/lambda-delta/language/item.ma b/matita/matita/lib/lambda-delta/language/item.ma index d85127ad7..60a115dc0 100644 --- a/matita/matita/lib/lambda-delta/language/item.ma +++ b/matita/matita/lib/lambda-delta/language/item.ma @@ -19,22 +19,41 @@ include "lambda-delta/ground.ma". (* BINARY ITEMS *************************************************************) +(* binary binding items *) +inductive bind2: Type[0] ≝ +| Abbr: bind2 (* abbreviation *) +| Abst: bind2 (* abstraction *) +. + +(* binary non-binding items *) +inductive flat2: Type[0] ≝ +| Appl: flat2 (* application *) +| Cast: flat2 (* explicit type annotation *) +. + (* binary items *) inductive item2: Type[0] ≝ - | Abbr: item2 (* abbreviation *) - | Abst: item2 (* abstraction *) - | Appl: item2 (* application *) - | Cast: item2 (* explicit type annotation *) +| Bind: bind2 → item2 (* binding item *) +| Flat: flat2 → item2 (* non-binding item *) . +coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2. + +coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2. + (* reduction-related categorization *****************************************) -(* binary items entitled for zeta-reduction *) -definition zable2 ≝ λI. I = Abbr ∨ I = Cast. +(* binding items entitled for zeta-reduction *) +definition zable ≝ λI. I = Abbr. + +interpretation "is entitled for zeta-reduction" 'Zeta I = (zable I). + +(* non-binding items entitled for zeta-reduction *) +definition table ≝ λI. I = Cast. -interpretation "is entitled for zeta-reduction" 'Zeta I = (zable2 I). +interpretation "is entitled for tau-reduction" 'Tau I = (table I). -(* binary items entitled for theta reduction *) -definition thable2 ≝ λI. I = Abbr. +(* binding items entitled for theta-reduction *) +definition thable ≝ λI. I = Abbr. -interpretation "is entitled for theta-reduction" 'Theta I = (thable2 I). +interpretation "is entitled for theta-reduction" 'Theta I = (thable I). diff --git a/matita/matita/lib/lambda-delta/language/lenv.ma b/matita/matita/lib/lambda-delta/language/lenv.ma index 018b3b4ff..3398de4ee 100644 --- a/matita/matita/lib/lambda-delta/language/lenv.ma +++ b/matita/matita/lib/lambda-delta/language/lenv.ma @@ -15,10 +15,10 @@ include "lambda-delta/language/term.ma". (* local environments *) inductive lenv: Type[0] ≝ - | LSort: lenv (* empty *) - | LCon2: lenv → item2 → term → lenv (* binary item construction *) +| LSort: lenv (* empty *) +| LPair: lenv → bind2 → term → lenv (* binary binding construction *) . interpretation "sort (local environment)" 'Star = LSort. -interpretation "environment construction (binary)" 'DCon L I T = (LCon2 L I T). +interpretation "environment binding construction (binary)" 'DBind L I T = (LPair L I T). diff --git a/matita/matita/lib/lambda-delta/language/term.ma b/matita/matita/lib/lambda-delta/language/term.ma index 22dad92a5..ac3b8fa5e 100644 --- a/matita/matita/lib/lambda-delta/language/term.ma +++ b/matita/matita/lib/lambda-delta/language/term.ma @@ -15,13 +15,17 @@ include "lambda-delta/language/item.ma". (* terms *) inductive term: Type[0] ≝ - | TSort: nat → term (* sort: starting at 0 *) - | TLRef: nat → term (* reference by index: starting at 0 *) - | TCon2: item2 → term → term → term (* binary construction *) +| TSort: nat → term (* sort: starting at 0 *) +| TLRef: nat → term (* reference by index: starting at 0 *) +| TPair: item2 → term → term → term (* binary item construction *) . interpretation "sort (term)" 'Star k = (TSort k). interpretation "local reference (term)" 'Weight i = (TLRef i). -interpretation "term construction (binary)" 'SCon I T1 T2 = (TCon2 I T1 T2). +interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2). + +interpretation "term binding construction (binary)" 'SBind I T1 T2 = (TPair (Bind I) T1 T2). + +interpretation "term flat construction (binary)" 'SFlat I T1 T2 = (TPair (Flat I) T1 T2). diff --git a/matita/matita/lib/lambda-delta/language/weight.ma b/matita/matita/lib/lambda-delta/language/weight.ma index f6be4dab7..f0021be9e 100644 --- a/matita/matita/lib/lambda-delta/language/weight.ma +++ b/matita/matita/lib/lambda-delta/language/weight.ma @@ -15,18 +15,18 @@ include "lambda-delta/language/lenv.ma". (* the weight of a term *) let rec tw T ≝ match T with - [ TSort _ ⇒ 1 - | TLRef _ ⇒ 1 - | TCon2 _ V T ⇒ tw V + tw T + 1 - ]. +[ TSort _ ⇒ 1 +| TLRef _ ⇒ 1 +| TPair _ V T ⇒ tw V + tw T + 1 +]. interpretation "weight (term)" 'Weight T = (tw T). (* the weight of a local environment *) let rec lw L ≝ match L with - [ LSort ⇒ 0 - | LCon2 L _ V ⇒ lw L + #V - ]. +[ LSort ⇒ 0 +| LPair L _ V ⇒ lw L + #V +]. interpretation "weight (local environment)" 'Weight L = (lw L). diff --git a/matita/matita/lib/lambda-delta/notation.ma b/matita/matita/lib/lambda-delta/notation.ma index 0f6387e03..7f5fabf28 100644 --- a/matita/matita/lib/lambda-delta/notation.ma +++ b/matita/matita/lib/lambda-delta/notation.ma @@ -17,6 +17,10 @@ notation "hvbox( ζ I )" non associative with precedence 45 for @{ 'Zeta $I }. +notation "hvbox( τ I )" + non associative with precedence 45 + for @{ 'Tau $I }. + notation "hvbox( θ I )" non associative with precedence 45 for @{ 'Theta $I }. @@ -29,13 +33,21 @@ notation "hvbox( ⋆ k )" non associative with precedence 90 for @{ 'Star $k }. -notation "hvbox( ♭ (term 90 I) break (term 90 T1) . break (term 90 T) )" +notation "hvbox( 𝕚 { I } break (term 90 T1) . break (term 90 T) )" + non associative with precedence 90 + for @{ 'SItem $I $T1 $T }. + +notation "hvbox( 𝕓 { I } break (term 90 T1) . break (term 90 T) )" + non associative with precedence 90 + for @{ 'SBind $I $T1 $T }. + +notation "hvbox( 𝕗 { I } break (term 90 T1) . break (term 90 T) )" non associative with precedence 90 - for @{ 'SCon $I $T1 $T }. + for @{ 'SFlat $I $T1 $T }. -notation "hvbox( T . break ♭ (term 90 I) break (term 90 T1) )" +notation "hvbox( T . break 𝕓 { I } break (term 90 T1) )" non associative with precedence 89 - for @{ 'DCon $T $I $T1 }. + for @{ 'DBind $T $I $T1 }. notation "hvbox( # term 90 x )" non associative with precedence 90 diff --git a/matita/matita/lib/lambda-delta/substitution/lift.ma b/matita/matita/lib/lambda-delta/substitution/lift.ma index 906788968..656946171 100644 --- a/matita/matita/lib/lambda-delta/substitution/lift.ma +++ b/matita/matita/lib/lambda-delta/substitution/lift.ma @@ -14,12 +14,15 @@ include "lambda-delta/language/term.ma". (* RELOCATION ***************************************************************) inductive lift: term → nat → nat → term → Prop ≝ - | lift_sort : ∀k,d,e. lift (⋆k) d e (⋆k) - | lift_lref_lt: ∀i,d,e. i < d → lift (#i) d e (#i) - | lift_lref_ge: ∀i,d,e. d ≤ i → lift (#i) d e (#(i + e)) - | lift_con2 : ∀I,V1,V2,T1,T2,d,e. - lift V1 d e V2 → lift T1 (d + 1) e T2 → - lift (♭I V1. T1) d e (♭I V2. T2) +| lift_sort : ∀k,d,e. lift (⋆k) d e (⋆k) +| lift_lref_lt: ∀i,d,e. i < d → lift (#i) d e (#i) +| lift_lref_ge: ∀i,d,e. d ≤ i → lift (#i) d e (#(i + e)) +| lift_bind : ∀I,V1,V2,T1,T2,d,e. + lift V1 d e V2 → lift T1 (d + 1) e T2 → + lift (𝕓{I} V1. T1) d e (𝕓{I} V2. T2) +| lift_flat : ∀I,V1,V2,T1,T2,d,e. + lift V1 d e V2 → lift T1 d e T2 → + lift (𝕗{I} V1. T1) d e (𝕗{I} V2. T2) . interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2). @@ -34,9 +37,10 @@ qed. lemma lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k. #d #e #T1 #T2 #H elim H -H d e T1 T2 // - [ #i #d #e #_ #k #H destruct - | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct - ] +[ #i #d #e #_ #k #H destruct +| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct +| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct +] qed. lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k. @@ -46,11 +50,12 @@ qed. lemma 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 #H elim H -H d e T1 T2 - [ #k #d #e #i #H destruct - | #j #d #e #Hj #i #Hi destruct /3/ - | #j #d #e #Hj #i #Hi destruct le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2/ | -Hd12 /2/ ] - | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %) /3/ - ] - ] - | #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 - lapply (lift_inv_con22 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2; - elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1 - >plus_plus_comm_23 in HU2 #HU2 elim (IHU … HU2 ?) /3 width = 5/ - ] +[ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12 + lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct -T2 /3/ +| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12 + lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2 + [ -Hid2 /4/ + | elim (lt_false d1 ?) + @(le_to_lt_to_lt … Hd12) -Hd12 @(le_to_lt_to_lt … Hid1) -Hid1 /2/ + ] +| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12 + lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2 + [ -Hd12; lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3/ + | -Hid1; lapply (arith1 … Hid2) -Hid2 #Hid2 + @(ex2_1_intro … #(i - e2)) + [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2/ | -Hd12 /2/ ] + | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %) /3/ + ] + ] +| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 + lapply (lift_inv_bind2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2; + elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1 + >plus_plus_comm_23 in HU2 #HU2 elim (IHU … HU2 ?) /3 width = 5/ +| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 + lapply (lift_inv_flat2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2; + elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1 + elim (IHU … HU2 ?) /3 width = 5/ +] qed. theorem lift_free: ∀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. #d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2 - [ /3/ - | #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_ - lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/ - | #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12 - lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21 - <(plus_plus_minus_m_m e1 e2 i) /3/ - | #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 - elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b - elim (IHT (d2+1) … ? ? He12) /3 width = 5/ - ] +[ /3/ +| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_ + lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/ +| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12 + lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21 + <(plus_plus_minus_m_m e1 e2 i) /3/ +| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 + elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b + elim (IHT (d2+1) … ? ? He12) /3 width = 5/ +| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 + elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b + elim (IHT d2 … ? ? He12) /3 width = 5/ +] qed. diff --git a/matita/matita/lib/lambda-delta/substitution/subst.ma b/matita/matita/lib/lambda-delta/substitution/subst.ma index 519aeaa19..5989693c5 100644 --- a/matita/matita/lib/lambda-delta/substitution/subst.ma +++ b/matita/matita/lib/lambda-delta/substitution/subst.ma @@ -15,16 +15,19 @@ include "lambda-delta/substitution/lift.ma". (* TELESCOPIC SUBSTITUTION **************************************************) inductive subst: lenv → term → nat → nat → term → Prop ≝ - | subst_sort : ∀L,k,d,e. subst L (⋆k) d e (⋆k) - | subst_lref_lt: ∀L,i,d,e. i < d → subst L (#i) d e (#i) - | subst_lref_O : ∀L,V,e. 0 < e → subst (L. ♭Abbr V) #0 0 e V - | subst_lref_S : ∀L,I,V,i,T1,T2,d,e. - d ≤ i → i < d + e → subst L #i d e T1 → ↑[d,1] T1 ≡ T2 → - subst (L. ♭I V) #(i + 1) (d + 1) e T2 - | subst_lref_ge: ∀L,i,d,e. d + e ≤ i → subst L (#i) d e (#(i - e)) - | subst_con2 : ∀L,I,V1,V2,T1,T2,d,e. - subst L V1 d e V2 → subst (L. ♭I V1) T1 (d + 1) e T2 → - subst L (♭I V1. T1) d e (♭I V2. T2) +| subst_sort : ∀L,k,d,e. subst L (⋆k) d e (⋆k) +| subst_lref_lt: ∀L,i,d,e. i < d → subst L (#i) d e (#i) +| subst_lref_O : ∀L,V,e. 0 < e → subst (L. 𝕓{Abbr} V) #0 0 e V +| subst_lref_S : ∀L,I,V,i,T1,T2,d,e. + d ≤ i → i < d + e → subst L #i d e T1 → ↑[d,1] T1 ≡ T2 → + subst (L. 𝕓{I} V) #(i + 1) (d + 1) e T2 +| subst_lref_ge: ∀L,i,d,e. d + e ≤ i → subst L (#i) d e (#(i - e)) +| subst_bind : ∀L,I,V1,V2,T1,T2,d,e. + subst L V1 d e V2 → subst (L. 𝕓{I} V1) T1 (d + 1) e T2 → + subst L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2) +| subst_flat : ∀L,I,V1,V2,T1,T2,d,e. + subst L V1 d e V2 → subst L T1 d e T2 → + subst L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2) . interpretation "telescopic substritution" 'RSubst L T1 d e T2 = (subst L T1 d e T2). diff --git a/matita/matita/lib/lambda-delta/substitution/thin.ma b/matita/matita/lib/lambda-delta/substitution/thin.ma index ab1c5f271..96432922d 100644 --- a/matita/matita/lib/lambda-delta/substitution/thin.ma +++ b/matita/matita/lib/lambda-delta/substitution/thin.ma @@ -14,12 +14,11 @@ include "lambda-delta/substitution/subst.ma". (* THINNING *****************************************************************) inductive thin: lenv → nat → nat → lenv → Prop ≝ - | thin_refl: ∀L. thin L 0 0 L - | thin_thin: ∀L1,L2,I,V,e. - thin L1 0 e L2 → thin (L1. ♭I V) 0 (e + 1) L2 - | thin_skip: ∀L1,L2,I,V1,V2,d,e. - thin L1 d e L2 → L1 ⊢ ↓[d,e] V1 ≡ V2 → - thin (L1. ♭I V1) (d + 1) e (L2. ♭I V2) +| thin_refl: ∀L. thin L 0 0 L +| thin_thin: ∀L1,L2,I,V,e. thin L1 0 e L2 → thin (L1. 𝕓{I} V) 0 (e + 1) L2 +| thin_skip: ∀L1,L2,I,V1,V2,d,e. + thin L1 d e L2 → L1 ⊢ ↓[d,e] V1 ≡ V2 → + thin (L1. 𝕓{I} V1) (d + 1) e (L2. 𝕓{I} V2) . interpretation "thinning" 'RSubst L1 d e L2 = (thin L1 d e L2). @@ -30,6 +29,6 @@ axiom thin_conf_ge: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 → ∀e2,L2. ↓[0,e2] L ≡ L2 → d1 + e1 ≤ e2 → ↓[0,e2-e1] L1 ≡ L2. axiom thin_conf_lt: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 → - ∀e2,K2,I,V2. ↓[0,e2] L ≡ K2. ♭I V2 → + ∀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. -- 2.39.2