(**************************************************************************)
-set "baseuri" "cic:/matita/nat/minus".
-
include "nat/le_arith.ma".
include "nat/compare.ma".
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.
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.
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)).
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
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.
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.
(* 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.
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 *)
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)
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.
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).
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.
intros.
apply sym_eq.
apply plus_to_minus.
-autobatch.
+autobatch;
qed.
theorem distributive_times_minus: distributive nat times minus.
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).
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.
projects / helm.git / blobdiff