From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 21 Apr 2011 14:16:26 +0000 (+0000)
Subject: - we added notation for the zetable and thetable items
X-Git-Tag: make_still_working~2525
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1df995bc8675c8b1118889cf470fc4d1d2ab5a22;p=helm.git

- we added notation for the zetable and thetable items
- the first inversion lemma for lift shows a bug in the destruct tactic :(
---

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.