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

diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma
index 10d218d44..4f789a230 100644
--- a/helm/software/matita/library/nat/minus.ma
+++ b/helm/software/matita/library/nat/minus.ma
@@ -23,9 +23,12 @@ 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).
 
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con 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.
@@ -75,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.
@@ -92,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)).
@@ -108,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 
@@ -151,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.
@@ -159,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.
@@ -189,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.
@@ -227,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 *)
@@ -235,8 +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.
-   autobatch
+  |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,13 +278,21 @@ 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
-    |apply H[autobatch|assumption]
+    |apply H[autobatch depth=2|assumption]
     ]
   ]
 qed.
@@ -268,10 +300,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).
@@ -286,18 +324,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.
@@ -331,7 +372,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.
@@ -358,10 +399,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).
@@ -387,7 +431,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.