From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 19 Jul 2011 14:25:24 +0000 (+0000)
Subject: - nnAuto.ml: width overflows are warnings, not errors
X-Git-Tag: make_still_working~2361
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2912d9bd61bc451c1135ca0a123cc30f203e93c9;p=helm.git

- nnAuto.ml: width overflows are warnings, not errors
- matitaScript.ml: backup source file with ~ reactivated
- lambda-delta: main properies of lift closed!
---

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 359b5b076..0cb666e39 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -1512,7 +1512,7 @@ let rec auto_clusters ?(top=false)
 	(fun gl ->
 	   if List.length gl > flags.maxwidth then begin
 	      debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); 
-	      HLog.error (sprintf "global width (%u) exceeded: %u"
+	      HLog.warn (sprintf "global width (%u) exceeded: %u"
 	         flags.maxwidth (List.length gl));
 	      raise (Gaveup IntSet.empty)
 	   end else ()) classes;
@@ -1599,7 +1599,7 @@ auto_main flags signature cache depth status: unit =
         (* moved inside auto_clusters *)
         if ng > flags.maxwidth then begin 
           debug_print ~depth (lazy "FAIL LOCAL WIDTH");
-	  HLog.error (sprintf "local width (%u) exceeded: %u"
+	  HLog.warn (sprintf "local width (%u) exceeded: %u"
 	     flags.maxwidth ng);
 	  raise (Gaveup IntSet.empty)
         end else if depth = flags.maxdepth then
diff --git a/matita/matita/lib/bacato.ma b/matita/matita/lib/bacato.ma
deleted file mode 100644
index 41211e69d..000000000
--- a/matita/matita/lib/bacato.ma
+++ /dev/null
@@ -1,21 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic
-    ||A||  Library of Mathematics, developed at the Computer Science
-    ||T||  Department of the University of Bologna, Italy.
-    ||I||
-    ||T||
-    ||A||  This file is distributed under the terms of the
-    \   /  GNU General Public License Version 2
-     \ /
-      V_______________________________________________________________ *)
-
-include "basics/pts.ma".
-
-inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝
-   | ex3_2_intro: ∀x0,x1. (P0 x0 x1)→(P1 x0 x1)→(P2 x0 x1)→(ex3_2 ? ? ? ? ?).
-
-lemma bacato: ∀A0,A1:Type[0]. ∀P0,P1,P2:A0→A1→Prop. ∀x0,x1.
-              P0 x0 x1 → P1 x0 x1 → P2 x0 x1 →
-              ex3_2 … (λx0,x1. P0 x0 x1) (λx0,x1. P1 x0 x1) (λx0,x1. P2 x0 x1).
-#A0 #A1 #P0 #P1 #P2 #x0 #x1 #H0 #H1 #H2
-@ex3_2_intro //
diff --git a/matita/matita/lib/lambda-delta/substitution/lift_main.ma b/matita/matita/lib/lambda-delta/substitution/lift_main.ma
index e847db483..a41e49c5b 100644
--- a/matita/matita/lib/lambda-delta/substitution/lift_main.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift_main.ma
@@ -116,6 +116,28 @@ lemma lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
 ]
 qed.
 
-axiom lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
+lemma lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
                      ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d1 + e1 ≤ d2 →
                      ∃∃T0. ↑[d2 - e1, e2] T1 ≡ T0 & ↑[d1, e1] T0 ≡ T2.
+#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
+[ #k #d1 #e1 #d2 #e2 #X #HX #_
+  >(lift_inv_sort1 … HX) -HX /2/
+| #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hded
+  lapply (lt_to_le_to_lt … (d1+e1) Hid1 ?) // #Hid1e
+  lapply (lt_to_le_to_lt … (d2-e1) Hid1 ?) /2/ #Hid2e
+  lapply (lt_to_le_to_lt … Hid1e Hded) -Hid1e Hded #Hid2
+  lapply (lift_inv_lref1_lt … HX ?) -HX // #HX destruct -X /3/
+| #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_
+  elim (lift_inv_lref1 … HX) -HX * #Hied #HX destruct -X;
+  [2: >plus_plus_comm_23] /4/
+| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded
+  elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
+  elim (IHV12 … HV20 ?) -IHV12 HV20 //
+  elim (IHT12 … HT20 ?) -IHT12 HT20 /2/ #T
+  <plus_minus /3 width=5/
+| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded
+  elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
+  elim (IHV12 … HV20 ?) -IHV12 HV20 //
+  elim (IHT12 … HT20 ?) -IHT12 HT20 /3 width=5/
+]
+qed.
diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 931fb049a..6bf9e5e02 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -829,12 +829,12 @@ object (self)
   method private _saveToBackupFile () =
     if buffer#modified then
       begin
-        let f = self#filename in
+        let f = self#filename ^ "~" in
         let oc = open_out f in
         output_string oc (buffer#get_text ~start:buffer#start_iter
                             ~stop:buffer#end_iter ());
         close_out oc;
-        HLog.debug ("backup " ^ f ^ " saved")                    
+        HLog.debug ("backup " ^ f ^ " saved")
       end
   
   method private reset_buffer =