1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
16 set "baseuri" "cic:/matita/nat/minus".
18 include "nat/le_arith.ma".
19 include "nat/compare.ma".
21 let rec minus n m \def
27 | (S q) \Rightarrow minus p q ]].
29 (*CSC: the URI must disappear: there is a bug now *)
30 interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y).
32 theorem minus_n_O: \forall n:nat.n=n-O.
33 intros.elim n.simplify.reflexivity.
37 theorem minus_n_n: \forall n:nat.O=n-n.
38 intros.elim n.simplify.
43 theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
49 theorem minus_Sn_m: \forall n,m:nat. m \leq n \to (S n)-m = S (n-m).
52 (\lambda n,m.m \leq n \to (S n)-m = S (n-m)).
53 intros.apply le_n_O_elim n1 H.
55 intros.simplify.reflexivity.
56 intros.rewrite < H.reflexivity.
57 apply le_S_S_to_le. assumption.
61 \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
64 (\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m).
65 intros.apply le_n_O_elim ? H.
66 simplify.rewrite < minus_n_O.reflexivity.
67 intros.simplify.reflexivity.
68 intros.simplify.apply H.apply le_S_S_to_le.assumption.
71 theorem plus_minus_m_m: \forall n,m:nat.
72 m \leq n \to n = (n-m)+m.
74 apply nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m).
75 intros.apply le_n_O_elim n1 H.
77 intros.simplify.rewrite < plus_n_O.reflexivity.
78 intros.simplify.rewrite < sym_plus.simplify.
79 apply eq_f.rewrite < sym_plus.apply H.
80 apply le_S_S_to_le.assumption.
83 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to
85 intros.apply trans_eq ? ? ((n-m)+m) ?.
91 theorem plus_to_minus :\forall n,m,p:nat.m \leq n \to
98 apply plus_minus_m_m.assumption.
101 theorem minus_S_S : \forall n,m:nat.
102 eq nat (minus (S n) (S m)) (minus n m).
107 theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to
108 eq nat (minus (pred n) (pred m)) (minus n m).
110 apply lt_O_n_elim n H.intro.
111 apply lt_O_n_elim m H1.intro.
112 simplify.reflexivity.
115 theorem eq_minus_n_m_O: \forall n,m:nat.
116 n \leq m \to n-m = O.
118 apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O).
119 intros.simplify.reflexivity.
120 intros.apply False_ind.
121 (* ancora problemi con il not *)
122 apply not_le_Sn_O n1 H.
124 simplify.apply H.apply le_S_S_to_le. apply H1.
127 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
128 intros.elim H.elim minus_Sn_n n.apply le_n.
129 rewrite > minus_Sn_m.
130 apply le_S.assumption.
131 apply lt_to_le.assumption.
135 theorem le_plus_minus: \forall n,m,p. n+m \leq p \to n \leq p-m.
137 elim p.simplify.apply trans_le ? (n+m) ?.
139 apply plus_le.assumption.
140 apply le_n_Sm_elim ? ? H1.
144 theorem distributive_times_minus: distributive nat times minus.
147 apply (leb_elim z y).intro.
148 cut x*(y-z)+x*z = (x*y-x*z)+x*z.
149 apply inj_plus_l (x*z).
151 apply trans_eq nat ? (x*y).
152 rewrite < times_plus_distr.
153 rewrite < plus_minus_m_m ? ? H.reflexivity.
154 rewrite < plus_minus_m_m ? ? ?.reflexivity.
158 rewrite > eq_minus_n_m_O.
159 rewrite > eq_minus_n_m_O (x*y).
160 rewrite < sym_times.simplify.reflexivity.
162 apply not_le_to_lt.assumption.
163 apply le_times_r.apply lt_to_le.
164 apply not_le_to_lt.assumption.
167 theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
168 \def distributive_times_minus.
170 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
171 intro.elim n.simplify.apply le_n.
172 elim m.simplify.apply le_n.
173 simplify.apply le_S.apply H.