From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 28 Apr 2011 15:23:38 +0000 (+0000)
Subject: - weight: bugfix + weight-based eliminator axiomatized
X-Git-Tag: make_still_working~2524
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=05959b8deaafaf3aa4ae59296da9c0fbf36c0feb;p=helm.git

- weight: bugfix + weight-based eliminator axiomatized
- notation: bugfix
- lift: first main property axiomatized
---

diff --git a/matita/matita/lib/lambda-delta/language/weight.ma b/matita/matita/lib/lambda-delta/language/weight.ma
index d6d233dea..f6be4dab7 100644
--- a/matita/matita/lib/lambda-delta/language/weight.ma
+++ b/matita/matita/lib/lambda-delta/language/weight.ma
@@ -31,6 +31,10 @@ let rec lw L ≝ match L with
 interpretation "weight (local environment)" 'Weight L = (lw L).
 
 (* the weight of a closure *)
-definition cw ≝ λL,T. #L + #T.
+definition cw: lenv → term → ? ≝ λL,T. #L + #T.
 
 interpretation "weight (closure)" 'Weight L T = (cw L T).
+
+axiom cw_wf_ind: ∀P:lenv→term→Prop.
+                 (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) →
+                 ∀L,T. P L T.
diff --git a/matita/matita/lib/lambda-delta/notation.ma b/matita/matita/lib/lambda-delta/notation.ma
index b71dd7780..0f6387e03 100644
--- a/matita/matita/lib/lambda-delta/notation.ma
+++ b/matita/matita/lib/lambda-delta/notation.ma
@@ -29,7 +29,7 @@ notation "hvbox( ⋆ k )"
  non associative with precedence 90
  for @{ 'Star $k }.
 
-notation "hvbox( ♭ (term 90 I) break (term 90 T1) . break T )"
+notation "hvbox( ♭ (term 90 I) break (term 90 T1) . break (term 90 T) )"
  non associative with precedence 90
  for @{ 'SCon $I $T1 $T }.
 
diff --git a/matita/matita/lib/lambda-delta/substitution/lift.ma b/matita/matita/lib/lambda-delta/substitution/lift.ma
index a550123b5..340cffccd 100644
--- a/matita/matita/lib/lambda-delta/substitution/lift.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift.ma
@@ -24,12 +24,60 @@ inductive lift: term → nat → nat → term → Prop ≝
 
 interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2).
 
+(* The basic properties *****************************************************)
+
+lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d,e] #(i - e) ≡ #i.
+#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %) /3/
+qed.
+
 (* 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 *)
+   [ #i #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.
 #d #e #T1 #k #H lapply (lift_inv_sort2_aux … H) /2/
-qed.  
+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 <minus_plus_m_m /4/
+   | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
+   ]
+qed.
+
+lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i →
+                      (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
+#d #e #T1 #i #H lapply (lift_inv_lref2_aux … H) /2/
+qed.
+
+lemma lift_inv_con22_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+                          ∀I,V2,U2. T2 = ♭I V2.U2 →
+                          ∃V1,U1. ↑[d,e] V1 ≡ V2 ∧ ↑[d+1,e] U1 ≡ U2 ∧
+                                  T1 = ♭I V1.U1.
+#d #e #T1 #T2 #H elim H -H d e T1 T2
+   [ #k #d #e #I #V2 #U2 #H destruct
+   | #i #d #e #_ #I #V2 #U2 #H destruct
+   | #i #d #e #_ #I #V2 #U2 #H destruct
+   | #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct /5/
+qed.
+
+lemma lift_inv_con22: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡  ♭I V2. U2 →
+                      ∃V1,U1. ↑[d,e] V1 ≡ V2 ∧ ↑[d+1,e] U1 ≡ U2 ∧
+                              T1 = ♭I V1. U1.
+#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_con22_aux … H) /2/
+qed.
+
+(* the main properies *******************************************************)
+
+axiom lift_trans_rev: ∀d1,e1,T1,T. ↑[d1,e1] T1 ≡ T →
+                      ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T →
+                      d1 ≤ d2 →
+                      ∃T0. ↑[d1, e1] T0 ≡ T2 ∧ ↑[d2, e2] T0 ≡ T1.