X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fminus.ma;h=4f789a230ee546caefab79ba748e6045314fdaa5;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=a8e987fc4a699cff453d0161f7c5ac71c7a61985;hpb=dcef667a444aa0f189225855c1433d26b65fb8b7;p=helm.git

diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma
index a8e987fc4..4f789a230 100644
--- a/helm/software/matita/library/nat/minus.ma
+++ b/helm/software/matita/library/nat/minus.ma
@@ -23,9 +23,13 @@ let rec minus n m \def
 	match m with
 	[O \Rightarrow (S p)
         | (S q) \Rightarrow minus p q ]].
-
+        
 interpretation "natural minus" 'minus x y = (minus x y).
 
+theorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
+intros;reflexivity.
+qed.
+
 theorem minus_n_O: \forall n:nat.n=n-O.
 intros.elim n.simplify.reflexivity.
 simplify.reflexivity.
@@ -74,14 +78,13 @@ intros.simplify.apply H.apply le_S_S_to_le.assumption.
 qed.
 
 theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
-intros 2.
-elim m in n ⊢ %.
+intros 2 .elim m in n ⊢ %.
 rewrite < minus_n_O.apply plus_n_O.
-elim n1.simplify.
-apply minus_n_n.
-rewrite < plus_n_Sm.
+elim n1.simplify. apply minus_n_n.
+autobatch by H.
+(* rewrite < plus_n_Sm.
 change with (S n2 = (S n2 + n)-n).
-apply H.
+apply H. *)
 qed.
 
 theorem plus_minus_m_m: \forall n,m:nat.
@@ -91,11 +94,19 @@ apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m)).
 intros.apply (le_n_O_elim n1 H).
 reflexivity.
 intros.simplify.rewrite < plus_n_O.reflexivity.
-intros.simplify.rewrite < sym_plus.simplify.
-apply eq_f.rewrite < sym_plus.apply H.
+intros. 
+rewrite < sym_plus.simplify. apply eq_f.
+rewrite < sym_plus.apply H.
 apply le_S_S_to_le.assumption.
 qed.
 
+theorem le_plus_minus_m_m: \forall n,m:nat. n \le (n-m)+m.
+intro.elim n;
+  [apply le_O_n
+  |cases m; simplify[autobatch|autobatch by H, le_S_S]
+  ]
+qed.
+
 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to 
 n = m+p.
 intros.apply (trans_eq ? ? ((n-m)+m)).
@@ -107,19 +118,15 @@ qed.
 theorem plus_to_minus :\forall n,m,p:nat.
 n = m+p \to n-m = p.
 intros.
-apply (inj_plus_r m).
+(* autobatch by transitive_eq, eq_f2, H. *)
+autobatch depth=4 by inj_plus_r, symmetric_eq, minus_to_plus, le_plus_n_r.
+(* 
 rewrite < H.
 rewrite < sym_plus.
 symmetry.
 apply plus_minus_m_m.rewrite > H.
 rewrite > sym_plus.
-apply le_plus_n.
-qed.
-
-theorem minus_S_S : \forall n,m:nat.
-eq nat (minus (S n) (S m)) (minus n m).
-intros.
-reflexivity.
+apply le_plus_n.*)
 qed.
 
 theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to 
@@ -150,7 +157,8 @@ apply lt_to_le.assumption.
 qed.
 
 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
-intros.apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
+intros.
+apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
 intro.elim n1.simplify.apply le_n_Sn.
 simplify.rewrite < minus_n_O.apply le_n.
 intros.simplify.apply le_n_Sn.
@@ -158,7 +166,9 @@ intros.simplify.apply H.
 qed.
 
 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p. 
-intros 3.simplify.intro.
+intros 3.intro.
+(* autobatch *)
+(* end auto($Revision$) proof: TIME=1.33 SIZE=100 DEPTH=100 *)
 apply (trans_le (m-n) (S (m-(S n))) p).
 apply minus_le_S_minus_S.
 assumption.
@@ -188,36 +198,49 @@ qed.
 (* galois *)
 theorem monotonic_le_minus_r: 
 \forall p,q,n:nat. q \leq p \to n-p \le n-q.
-simplify.intros 2.apply (nat_elim2 
-(\lambda p,q.\forall a.q \leq p \to a-p \leq a-q)).
-intros.apply (le_n_O_elim n H).apply le_n.
-intros.rewrite < minus_n_O.
-apply le_minus_m.
-intros.elim a.simplify.apply le_n.
-simplify.apply H.apply le_S_S_to_le.assumption.
+intros 2.apply (nat_elim2 ???? p q); intros;
+  [apply (le_n_O_elim n H).apply le_n.
+  |applyS le_minus_m.
+  |elim n1;intros;[apply le_n|simplify.apply H.apply le_S_S_to_le.assumption]
+  ]
+qed.
+
+theorem monotonic_le_minus_l: 
+∀p,q,n:nat. q \leq p \to q-n \le p-n.
+intros 2.apply (nat_elim2 ???? p q); intros;
+  [apply (le_n_O_elim n H).apply le_n.
+  |apply le_O_n.
+  |cases n1;[apply H1|simplify. apply H.apply le_S_S_to_le.assumption]
+  ]
 qed.
 
 theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)).
-intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m)))).
-intros.apply le_O_n.
-simplify.intros.rewrite < plus_n_O.assumption.
 intros.
-rewrite < plus_n_Sm.
-apply le_S_S.apply H.
-exact H1.
+(* autobatch by transitive_le, le_plus_minus_m_m, le_plus_l, H.*)
+apply transitive_le
+  [2:apply le_plus_minus_m_m.
+  |3:apply le_plus_l.apply H.
+  ]
+  skip.
 qed.
 
 theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p).
+intros.
+autobatch by (monotonic_le_minus_l (p+m) n m), H.
+(*
 intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p))).
 intros.simplify.apply le_O_n.
 intros 2.rewrite < plus_n_O.intro.simplify.assumption.
 intros.simplify.apply H.
-apply le_S_S_to_le.rewrite > plus_n_Sm.assumption.
+apply le_S_S_to_le.rewrite > plus_n_Sm.assumption. *)
 qed.
 
 (* the converse of le_plus_to_minus does not hold *)
 theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)).
-intros 3.apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m)))).
+intros.
+autobatch by trans_le, le_plus_to_le, H, le_plus_minus_m_m.
+(*
+apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m)))).
 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
 intro.intro.cut (n=O).rewrite > Hcut.apply le_O_n.
 apply sym_eq. apply le_n_O_to_eq.
@@ -226,7 +249,7 @@ rewrite < sym_plus.
 apply le_plus_n.assumption.
 intros.simplify.
 apply H.apply le_S_S_to_le.
-rewrite > plus_n_Sm.assumption.
+rewrite > plus_n_Sm.assumption. *)
 qed.
 
 (* minus and lt - to be completed *)
@@ -234,9 +257,10 @@ theorem lt_minus_l: \forall m,l,n:nat.
   l < m \to m \le n \to n - m < n - l.
 apply nat_elim2
   [intros.apply False_ind.apply (not_le_Sn_O ? H)
-  |intros.rewrite < minus_n_O.
-   change in H1 with (n<n1);
-   apply lt_minus_m; autobatch depth=2;
+  |intros.autobatch.
+   (* rewrite < minus_n_O.
+    change in H1 with (n<n1);
+    apply lt_minus_m; autobatch depth=2; *)
   |intros.
    generalize in match H2.
    apply (nat_case n1)
@@ -254,9 +278,17 @@ qed.
 
 theorem lt_minus_r: \forall n,m,l:nat. 
   n \le l \to l < m \to l -n < m -n.
+  unfold lt.
 intro.elim n
   [applyS H1
-  |rewrite > eq_minus_S_pred.
+  |(*
+   letin x ≝ (lt_pred (l-n1) (m-n1)).
+   clearbody x.
+   unfold lt in x.
+   autobatch depth=4 width=5 size=10 by 
+    x, H, H1, H2, trans_le, le_n_Sn, le_n.
+  ]*)
+  rewrite > eq_minus_S_pred.
    rewrite > eq_minus_S_pred.
    apply lt_pred
     [unfold lt.apply le_plus_to_minus_r.applyS H1