huge commit in automation:

[helm.git] / helm / software / matita / library / nat / minus.ma

diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma
index 339e2262c72de402a1d29187e8a41907658038b7..a8e987fc4a699cff453d0161f7c5ac71c7a61985 100644 (file)
--- a/helm/software/matita/library/nat/minus.ma
+++ b/helm/software/matita/library/nat/minus.ma
@@ -13,8 +13,6 @@
 (**************************************************************************)
 
 
-set "baseuri" "cic:/matita/nat/minus".
-
 include "nat/le_arith.ma".
 include "nat/compare.ma".
 
@@ -26,8 +24,7 @@ let rec minus n m \def
        [O \Rightarrow (S p)
         | (S q) \Rightarrow minus p q ]].
 
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y).
+interpretation "natural minus" 'minus x y = (minus x y).
 
 theorem minus_n_O: \forall n:nat.n=n-O.
 intros.elim n.simplify.reflexivity.
@@ -78,13 +75,12 @@ qed.
 
 theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
 intros 2.
-generalize in match n.
-elim m.
+elim m in n ⊢ %.
 rewrite < minus_n_O.apply plus_n_O.
-elim n2.simplify.
+elim n1.simplify.
 apply minus_n_n.
 rewrite < plus_n_Sm.
-change with (S n3 = (S n3 + n1)-n1).
+change with (S n2 = (S n2 + n)-n).
 apply H.
 qed.
 
@@ -239,7 +235,8 @@ theorem lt_minus_l: \forall m,l,n:nat.
 apply nat_elim2
   [intros.apply False_ind.apply (not_le_Sn_O ? H)
   |intros.rewrite < minus_n_O.
-   autobatch
+   change in H1 with (n<n1);
+   apply lt_minus_m; autobatch depth=2;
   |intros.
    generalize in match H2.
    apply (nat_case n1)
@@ -263,7 +260,7 @@ intro.elim n
    rewrite > eq_minus_S_pred.
    apply lt_pred
     [unfold lt.apply le_plus_to_minus_r.applyS H1
-    |apply H[autobatch|assumption]
+    |apply H[autobatch depth=2|assumption]
     ]
   ]
 qed.
@@ -271,10 +268,16 @@ qed.
 lemma lt_to_lt_O_minus : \forall m,n.
   n < m \to O < m - n.
 intros.  
-unfold. apply le_plus_to_minus_r. unfold in H. rewrite > sym_plus. 
+unfold. apply le_plus_to_minus_r. unfold in H.
+cut ((S n ≤ m) = (1 + n ≤ m)) as applyS;
+  [ rewrite < applyS; assumption;
+  | demodulate; reflexivity. ]
+(*
+rewrite > sym_plus. 
 rewrite < plus_n_Sm. 
 rewrite < plus_n_O. 
 assumption.
+*)
 qed.  
 
 theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
@@ -289,18 +292,21 @@ qed.
 
 theorem lt_O_minus_to_lt: \forall a,b:nat.
 O \lt b-a \to a \lt b.
-intros.
+intros. applyS (lt_minus_to_plus O  a b). assumption;
+(*
 rewrite > (plus_n_O a).
 rewrite > (sym_plus a O).
 apply (lt_minus_to_plus O  a b).
 assumption.
+*)
 qed.
 
 theorem lt_minus_to_lt_plus:
 \forall n,m,p. n - m < p \to n < m + p.
 intros 2.
 apply (nat_elim2 ? ? ? ? n m)
-  [simplify.intros.autobatch.
+  [simplify.intros.
+   lapply depth=0 le_n; autobatch;
   |intros 2.rewrite < minus_n_O.
    intro.assumption
   |intros.
@@ -334,7 +340,7 @@ theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
 intros.
 apply sym_eq.
 apply plus_to_minus.
-autobatch.
+autobatch;
 qed.
 
 theorem distributive_times_minus: distributive nat times minus.
@@ -361,10 +367,13 @@ theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 theorem eq_minus_plus_plus_minus: \forall n,m,p:nat. p \le m \to (n+m)-p = n+(m-p).
 intros.
 apply plus_to_minus.
+lapply (plus_minus_m_m ?? H); demodulate. reflexivity.
+(*
 rewrite > sym_plus in \vdash (? ? ? %).
 rewrite > assoc_plus.
 rewrite < plus_minus_m_m.
 reflexivity.assumption.
+*)
 qed.
 
 theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
@@ -390,7 +399,7 @@ qed.
 
 theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
 p+(n-m) = n-(m-p).
-intros.
+intros. 
 apply sym_eq.
 apply plus_to_minus.
 rewrite < assoc_plus.