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

diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma
index 710418d72..4f789a230 100644
--- 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".
 
@@ -25,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.
@@ -57,6 +58,14 @@ intros.rewrite < H.reflexivity.
 apply le_S_S_to_le. assumption.
 qed.
 
+theorem eq_minus_S_pred: \forall n,m. n - (S m) = pred(n -m).
+apply nat_elim2
+  [intro.reflexivity
+  |intro.simplify.autobatch
+  |intros.simplify.assumption
+  ]
+qed.
+
 theorem plus_minus:
 \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
 intros 2.
@@ -69,15 +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.
-generalize in match n.
-elim m.
+intros 2 .elim m in n ⊢ %.
 rewrite < minus_n_O.apply plus_n_O.
-elim n2.simplify.
-apply minus_n_n.
-rewrite < plus_n_Sm.
-change with (S n3 = (S n3 + n1)-n1).
-apply H.
+elim n1.simplify. apply minus_n_n.
+autobatch by H.
+(* rewrite < plus_n_Sm.
+change with (S n2 = (S n2 + n)-n).
+apply H. *)
 qed.
 
 theorem plus_minus_m_m: \forall n,m:nat.
@@ -87,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)).
@@ -103,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 
@@ -132,8 +143,8 @@ intros 2.
 apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O)).
 intros.simplify.reflexivity.
 intros.apply False_ind.
-apply not_le_Sn_O.
-goal 13.apply H.
+apply not_le_Sn_O;
+[2: apply H | skip].
 intros.
 simplify.apply H.apply le_S_S_to_le. apply H1.
 qed.
@@ -146,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.
@@ -154,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.
@@ -184,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.
@@ -222,10 +249,69 @@ 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 *)
+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.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)
+    [intros.apply False_ind.apply (not_le_Sn_O ? H3)
+    |intros.simplify.
+     apply H
+      [
+       apply lt_S_S_to_lt.
+       assumption
+      |apply le_S_S_to_le.assumption
+      ]
+    ]
+  ]
+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
+  |(*
+   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 depth=2|assumption]
+    ]
+  ]
+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.
+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).
 intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
@@ -236,6 +322,59 @@ rewrite < plus_n_Sm.
 apply H.apply H1.
 qed.
 
+theorem lt_O_minus_to_lt: \forall a,b:nat.
+O \lt b-a \to a \lt b.
+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.
+   lapply depth=0 le_n; autobatch;
+  |intros 2.rewrite < minus_n_O.
+   intro.assumption
+  |intros.
+   simplify.
+   cut (n1 < m1+p)
+    [autobatch
+    |apply H.
+     apply H1
+    ]
+  ]
+qed.
+
+theorem lt_plus_to_lt_minus:
+\forall n,m,p. m \le n \to n < m + p \to n - m < p.
+intros 2.
+apply (nat_elim2 ? ? ? ? n m)
+  [simplify.intros 3.
+   apply (le_n_O_elim ? H).
+   simplify.intros.assumption
+  |simplify.intros.assumption.
+  |intros.
+   simplify.
+   apply H
+    [apply le_S_S_to_le.assumption
+    |apply le_S_S_to_le.apply H2
+    ]
+  ]
+qed. 
+
+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;
+qed.
+
 theorem distributive_times_minus: distributive nat times minus.
 unfold distributive.
 intros.
@@ -260,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).
@@ -289,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.