(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/minus".
+set "baseuri" "cic:/matita/library_autobatch/nat/minus".
include "auto/nat/le_arith.ma".
include "auto/nat/compare.ma".
| (S q) \Rightarrow minus p q ]].
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural minus" 'minus x y = (cic:/matita/library_auto/nat/minus/minus.con x y).
+interpretation "natural minus" 'minus x y = (cic:/matita/library_autobatch/nat/minus/minus.con x y).
theorem minus_n_O: \forall n:nat.n=n-O.
intros.
elim n;
-auto. (* applico auto su entrambi i goal aperti*)
+autobatch. (* applico autobatch su entrambi i goal aperti*)
(*simplify;reflexivity.*)
qed.
theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
intro.
elim n
-[ auto
+[ autobatch
(*simplify.reflexivity.*)
| elim H.
reflexivity
apply (nat_elim2
(\lambda n,m.m \leq n \to (S n)-m = S (n-m)));intros
[ apply (le_n_O_elim n1 H).
- auto
+ autobatch
(*simplify.
reflexivity.*)
-| auto
+| autobatch
(*simplify.
reflexivity.*)
| rewrite < H
[ reflexivity
- | auto
+ | autobatch
(*apply le_S_S_to_le.
assumption.*)
]
apply (nat_elim2
(\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m));intros
[ apply (le_n_O_elim ? H).
- auto
+ autobatch
(*simplify.
rewrite < minus_n_O.
reflexivity.*)
-| auto
+| autobatch
(*simplify.
reflexivity.*)
| simplify.
- auto
+ autobatch
(*apply H.
apply le_S_S_to_le.
assumption.*)
[ rewrite < minus_n_O.
apply plus_n_O.
| elim n2
- [ auto
+ [ autobatch
(*simplify.
apply minus_n_n.*)
| rewrite < plus_n_Sm.
apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m));intros
[ apply (le_n_O_elim n1 H).
reflexivity
-| auto
+| autobatch
(*simplify.
rewrite < plus_n_O.
reflexivity.*)
simplify.
apply eq_f.
rewrite < sym_plus.
- auto
+ autobatch
(*apply H.
apply le_S_S_to_le.
assumption.*)
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));auto.
+intros.apply (trans_eq ? ? ((n-m)+m));autobatch.
(*[ apply plus_minus_m_m.
apply H.
| elim H1.
rewrite < H.
rewrite < sym_plus.
symmetry.
-auto.
+autobatch.
(*apply plus_minus_m_m.
rewrite > H.
rewrite > sym_plus.
intro.
apply (lt_O_n_elim m H1).
intro.
-auto.
+autobatch.
(*simplify.reflexivity.*)
qed.
n \leq m \to n-m = O.
intros 2.
apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O));intros
-[ auto
+[ autobatch
(*simplify.
reflexivity.*)
| apply False_ind.
- auto
+ autobatch
(*apply not_le_Sn_O.
goal 15.*) (*prima goal 13*)
(* effettuando un'esecuzione passo-passo, quando si arriva a dover
*)
(*apply H.*)
| simplify.
- auto
+ autobatch
(*apply H.
apply le_S_S_to_le.
apply H1.*)
intros.
elim H
[ elim (minus_Sn_n n).apply le_n
-| rewrite > minus_Sn_m;auto
+| rewrite > minus_Sn_m;autobatch
(*apply le_S.assumption.
apply lt_to_le.assumption.*)
]
| rewrite < minus_n_O.
apply le_n.
]
-| auto
+| autobatch
(*simplify.apply le_n_Sn.*)
| simplify.apply H.
]
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.
-auto.
+autobatch.
(*simplify.
intro.
apply (trans_le (m-n) (S (m-(S n))) p).
theorem le_minus_m: \forall n,m:nat. n-m \leq n.
intros.apply (nat_elim2 (\lambda m,n. n-m \leq n));intros
-[ auto
+[ autobatch
(*rewrite < minus_n_O.
apply le_n.*)
-| auto
+| autobatch
(*simplify.
apply le_n.*)
| simplify.
- auto
+ autobatch
(*apply le_S.
assumption.*)
]
apply (lt_O_n_elim m H1).
intro.
simplify.
-auto.
+autobatch.
(*unfold lt.
apply le_S_S.
apply le_minus_m.*)
assumption
| simplify.
intros.
- auto
+ autobatch
(*apply le_S_S.
apply H.
assumption.*)
| rewrite < minus_n_O.
apply le_minus_m.
| elim a
- [ auto
+ [ autobatch
(*simplify.
apply le_n.*)
| simplify.
- auto
+ autobatch
(*apply H.
apply le_S_S_to_le.
assumption.*)
intros 2.
apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p)))
[ intros.
- auto
+ autobatch
(*simplify.
apply le_O_n.*)
| intros 2.
rewrite < plus_n_O.
- auto
+ autobatch
(*intro.
simplify.
assumption.*)
apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m))));intro
[ rewrite < plus_n_O.
rewrite < minus_n_O.
- auto
+ autobatch
(*intro.
assumption.*)
| intro.
cut (n=O)
- [ auto
+ [ autobatch
(*rewrite > Hcut.
apply le_O_n.*)
| apply sym_eq.
apply le_n_O_to_eq.
- auto
+ autobatch
(*apply (trans_le ? (n+(S n1)))
[ rewrite < sym_plus.
apply le_plus_n
[ intro.
rewrite < plus_n_O.
rewrite < minus_n_O.
- auto
+ autobatch
(*intro.
assumption.*)
| simplify.
unfold lt.
apply le_S_S.
rewrite < plus_n_Sm.
- auto
+ autobatch
(*apply H.
apply H1.*)
]
intros.
apply ((leb_elim z y));intro
[ cut (x*(y-z)+x*z = (x*y-x*z)+x*z)
- [ auto
+ [ autobatch
(*apply (inj_plus_l (x*z)).
assumption.*)
| apply (trans_eq nat ? (x*y))
[ rewrite < distr_times_plus.
- auto
+ autobatch
(*rewrite < (plus_minus_m_m ? ? H).
reflexivity.*)
- | rewrite < plus_minus_m_m;auto
+ | rewrite < plus_minus_m_m;autobatch
(*[ reflexivity.
| apply le_times_r.
assumption.
]
| rewrite > eq_minus_n_m_O
[ rewrite > (eq_minus_n_m_O (x*y))
- [ auto
+ [ autobatch
(*rewrite < sym_times.
simplify.
reflexivity.*)
| apply le_times_r.
apply lt_to_le.
- auto
+ autobatch
(*apply not_le_to_lt.
assumption.*)
]
- | auto
+ | autobatch
(*apply lt_to_le.
apply not_le_to_lt.
assumption.*)
apply plus_to_minus.
rewrite > sym_plus in \vdash (? ? ? %).
rewrite > assoc_plus.
-auto.
+autobatch.
(*rewrite < plus_minus_m_m.
reflexivity.
assumption.
rewrite > (sym_plus p).
rewrite < plus_minus_m_m
[ rewrite > sym_plus.
- rewrite < plus_minus_m_m ; auto
+ rewrite < plus_minus_m_m ; autobatch
(*[ reflexivity.
| apply (trans_le ? (m+p))
[ rewrite < sym_plus.
| apply le_plus_to_minus.
apply lt_to_le.
rewrite < sym_plus.
- auto
+ autobatch
(*apply not_le_to_lt.
assumption.*)
]
- | auto
+ | autobatch
(*apply lt_to_le.
apply not_le_to_lt.
assumption.*)
rewrite < assoc_plus.
rewrite < plus_minus_m_m;
[ rewrite < sym_plus.
- auto
+ autobatch
(*rewrite < plus_minus_m_m
[ reflexivity
| assumption