From 2912d9bd61bc451c1135ca0a123cc30f203e93c9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 19 Jul 2011 14:25:24 +0000 Subject: [PATCH] - nnAuto.ml: width overflows are warnings, not errors - matitaScript.ml: backup source file with ~ reactivated - lambda-delta: main properies of lift closed! --- matita/components/ng_tactics/nnAuto.ml | 4 ++-- matita/matita/lib/bacato.ma | 21 ---------------- .../lambda-delta/substitution/lift_main.ma | 24 ++++++++++++++++++- matita/matita/matitaScript.ml | 4 ++-- 4 files changed, 27 insertions(+), 26 deletions(-) delete mode 100644 matita/matita/lib/bacato.ma 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 +