From 7b976a01aa6cedbfbef57ace183ce3fc0e2f22a9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 19 Apr 2011 20:59:15 +0000 Subject: [PATCH 1/1] - some bug fixes - we defined the thinning relation --- .../language/{item2.ma => item.ma} | 0 .../matita/lib/lambda-delta/language/term.ma | 2 +- matita/matita/lib/lambda-delta/notation.ma | 16 +++++++++--- .../lib/lambda-delta/substitution/subst.ma | 7 +++--- .../lib/lambda-delta/substitution/thin.ma | 25 +++++++++++++++++++ 5 files changed, 42 insertions(+), 8 deletions(-) rename matita/matita/lib/lambda-delta/language/{item2.ma => item.ma} (100%) create mode 100644 matita/matita/lib/lambda-delta/substitution/thin.ma diff --git a/matita/matita/lib/lambda-delta/language/item2.ma b/matita/matita/lib/lambda-delta/language/item.ma similarity index 100% rename from matita/matita/lib/lambda-delta/language/item2.ma rename to matita/matita/lib/lambda-delta/language/item.ma diff --git a/matita/matita/lib/lambda-delta/language/term.ma b/matita/matita/lib/lambda-delta/language/term.ma index 6a8a9eaf5..22dad92a5 100644 --- a/matita/matita/lib/lambda-delta/language/term.ma +++ b/matita/matita/lib/lambda-delta/language/term.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/language/item2.ma". +include "lambda-delta/language/item.ma". (* TERMS ********************************************************************) diff --git a/matita/matita/lib/lambda-delta/notation.ma b/matita/matita/lib/lambda-delta/notation.ma index 9d74ff3ba..9afd9ac79 100644 --- a/matita/matita/lib/lambda-delta/notation.ma +++ b/matita/matita/lib/lambda-delta/notation.ma @@ -21,12 +21,12 @@ notation "hvbox( ⋆ k )" non associative with precedence 90 for @{ 'Star $k }. -notation "hvbox( ♭ (term 90 I) break T1 . break T )" +notation "hvbox( ♭ (term 90 I) break (term 90 T1) . break T )" non associative with precedence 90 for @{ 'SCon $I $T1 $T }. -notation "hvbox( T . break ♭ (term 90 I) break T1 )" - non associative with precedence 90 +notation "hvbox( T . break ♭ (term 90 I) break (term 90 T1) )" + non associative with precedence 89 for @{ 'DCon $T $I $T1 }. notation "hvbox( # term 90 x )" @@ -46,3 +46,13 @@ notation "hvbox( [ d , break e ] ↑ break T1 ≡ break T2 )" notation "hvbox( [ d , break e ] ← break (term 90 L) / break T1 ≡ break T2 )" non associative with precedence 45 for @{ 'RSubst $L $T1 $d $e $T2 }. + +notation "hvbox( [ d , break e ] ↓ break L1 ≡ break L2 )" + non associative with precedence 45 + for @{ 'RThin $L1 $d $e $L2 }. + +(* reduction ****************************************************************) + +notation "hvbox( L ⊢ break T1 ⇒ break T2 )" + non associative with precedence 45 + for @{ 'PR $L $T1 $T2 }. diff --git a/matita/matita/lib/lambda-delta/substitution/subst.ma b/matita/matita/lib/lambda-delta/substitution/subst.ma index 2ba14fbc1..e09b37f35 100644 --- a/matita/matita/lib/lambda-delta/substitution/subst.ma +++ b/matita/matita/lib/lambda-delta/substitution/subst.ma @@ -12,14 +12,14 @@ include "lambda-delta/language/lenv.ma". include "lambda-delta/substitution/lift.ma". -(* SUBSTITUTION *************************************************************) +(* 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 → [1,d]↑ T1 ≡ T2 → + 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. @@ -31,6 +31,5 @@ interpretation "telescopic substritution" 'RSubst L T1 d e T2 = (subst L T1 d e lemma subst_lift_inv: ∀d,e,T1,T2. [d,e]↑ T1 ≡ T2 → ∀L. [d,e]← L / T2 ≡ T1. #d #e #T1 #T2 #H elim H -H d e T1 T2 /2/ -#i #d #e #Hdi #L >(minus_plus_m_m i e) in ⊢ (? ? ? ? ? %) /3/ +#i #d #e #Hdi #L >(minus_plus_m_m i e) in ⊢ (? ? ? ? ? %) /3/ (**) (* use \ldots *) qed. - diff --git a/matita/matita/lib/lambda-delta/substitution/thin.ma b/matita/matita/lib/lambda-delta/substitution/thin.ma new file mode 100644 index 000000000..03cc81b06 --- /dev/null +++ b/matita/matita/lib/lambda-delta/substitution/thin.ma @@ -0,0 +1,25 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +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 → [d,e]← L1 / V1 ≡ V2 → + thin (L1. ♭I V1) (d + 1) e (L2. ♭I V2) +. + +interpretation "thinning" 'RThin L1 d e L2 = (thin L1 d e L2). -- 2.39.2