- 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 4d7f5c93e669fe21fefe4d970239b703f5d560ac..d85127ad7645537ccf708a501e986cffa0a3a28d 100644 (file)
--- 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 368053f5c7d36ec92472a345cfb4658fd1cf9147..b71dd77805cb79f4a819d15b8e837fd0b0cf6011 100644 (file)
--- 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 17ece9a2a1cc644ff78eb416ee5ff4851b964e67..a550123b51486976e28605fe25ed9b831b17696b 100644 (file)
--- 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.