- 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 d6d233dea1d25964e409d5f39b6f2073fe33619c..f6be4dab7d45b2897afe7bfe73a68f1ea1f526fe 100644 (file)
--- 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 b71dd77805cb79f4a819d15b8e837fd0b0cf6011..0f6387e03c42dd100ae6c32aa41e9413cf34f69d 100644 (file)
--- 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 a550123b51486976e28605fe25ed9b831b17696b..340cffccdab53541332f97dbe3ca75612ea83d2d 100644 (file)
--- 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.