From 1df995bc8675c8b1118889cf470fc4d1d2ab5a22 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 21 Apr 2011 14:16:26 +0000 Subject: [PATCH] - we added notation for the zetable and thetable items - the first inversion lemma for lift shows a bug in the destruct tactic :( --- matita/matita/lib/lambda-delta/language/item.ma | 8 ++++++-- matita/matita/lib/lambda-delta/notation.ma | 8 ++++++++ matita/matita/lib/lambda-delta/substitution/lift.ma | 10 ++++++++++ 3 files changed, 24 insertions(+), 2 deletions(-) diff --git a/matita/matita/lib/lambda-delta/language/item.ma b/matita/matita/lib/lambda-delta/language/item.ma index 4d7f5c93e..d85127ad7 100644 --- a/matita/matita/lib/lambda-delta/language/item.ma +++ b/matita/matita/lib/lambda-delta/language/item.ma @@ -29,8 +29,12 @@ inductive item2: Type[0] ≝ (* reduction-related categorization *****************************************) +(* binary items entitled for zeta-reduction *) +definition zable2 ≝ λI. I = Abbr ∨ I = Cast. + +interpretation "is entitled for zeta-reduction" 'Zeta I = (zable2 I). + (* binary items entitled for theta reduction *) definition thable2 ≝ λI. I = Abbr. -(* binary items entitled for zeta reduction *) -definition zable2 ≝ λI. I = Abbr ∨ I = Cast. +interpretation "is entitled for theta-reduction" 'Theta I = (thable2 I). diff --git a/matita/matita/lib/lambda-delta/notation.ma b/matita/matita/lib/lambda-delta/notation.ma index 368053f5c..b71dd7780 100644 --- a/matita/matita/lib/lambda-delta/notation.ma +++ b/matita/matita/lib/lambda-delta/notation.ma @@ -13,6 +13,14 @@ (* language *****************************************************************) +notation "hvbox( ζ I )" + non associative with precedence 45 + for @{ 'Zeta $I }. + +notation "hvbox( θ I )" + non associative with precedence 45 + for @{ 'Theta $I }. + notation "hvbox( ⋆ )" non associative with precedence 90 for @{ 'Star }. diff --git a/matita/matita/lib/lambda-delta/substitution/lift.ma b/matita/matita/lib/lambda-delta/substitution/lift.ma index 17ece9a2a..a550123b5 100644 --- a/matita/matita/lib/lambda-delta/substitution/lift.ma +++ b/matita/matita/lib/lambda-delta/substitution/lift.ma @@ -23,3 +23,13 @@ inductive lift: term → nat → nat → term → Prop ≝ . interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2). + +(* The basic inversion lemmas ***********************************************) + +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 (***) (* DESTRUCT FAILS *) + +lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k. +#d #e #T1 #k #H lapply (lift_inv_sort2_aux … H) /2/ +qed. -- 2.39.2