]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/nat/minus.ma
fix
[helm.git] / helm / matita / library / nat / minus.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15
16 set "baseuri" "cic:/matita/nat/minus".
17
18 include "nat/le_arith.ma".
19 include "nat/compare.ma".
20
21 let rec minus n m \def 
22  match n with 
23  [ O \Rightarrow O
24  | (S p) \Rightarrow 
25         match m with
26         [O \Rightarrow (S p)
27         | (S q) \Rightarrow minus p q ]].
28
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).
31
32 theorem minus_n_O: \forall n:nat.n=n-O.
33 intros.elim n.simplify.reflexivity.
34 simplify.reflexivity.
35 qed.
36
37 theorem minus_n_n: \forall n:nat.O=n-n.
38 intros.elim n.simplify.
39 reflexivity.
40 simplify.apply H.
41 qed.
42
43 theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
44 intro.elim n.
45 simplify.reflexivity.
46 elim H.reflexivity.
47 qed.
48
49 theorem minus_Sn_m: \forall n,m:nat. m \leq n \to (S n)-m = S (n-m).
50 intros 2.
51 apply (nat_elim2
52 (\lambda n,m.m \leq n \to (S n)-m = S (n-m))).
53 intros.apply (le_n_O_elim n1 H).
54 simplify.reflexivity.
55 intros.simplify.reflexivity.
56 intros.rewrite < H.reflexivity.
57 apply le_S_S_to_le. assumption.
58 qed.
59
60 theorem plus_minus:
61 \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
62 intros 2.
63 apply (nat_elim2
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.
69 qed.
70
71 theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
72 intros 2.
73 generalize in match n.
74 elim m.
75 rewrite < minus_n_O.apply plus_n_O.
76 elim n2.simplify.
77 apply minus_n_n.
78 rewrite < plus_n_Sm.
79 change with (S n3 = (S n3 + n1)-n1).
80 apply H.
81 qed.
82
83 theorem plus_minus_m_m: \forall n,m:nat.
84 m \leq n \to n = (n-m)+m.
85 intros 2.
86 apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m)).
87 intros.apply (le_n_O_elim n1 H).
88 reflexivity.
89 intros.simplify.rewrite < plus_n_O.reflexivity.
90 intros.simplify.rewrite < sym_plus.simplify.
91 apply eq_f.rewrite < sym_plus.apply H.
92 apply le_S_S_to_le.assumption.
93 qed.
94
95 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to 
96 n = m+p.
97 intros.apply (trans_eq ? ? ((n-m)+m)).
98 apply plus_minus_m_m.
99 apply H.elim H1.
100 apply sym_plus.
101 qed.
102
103 theorem plus_to_minus :\forall n,m,p:nat.
104 n = m+p \to n-m = p.
105 intros.
106 apply (inj_plus_r m).
107 rewrite < H.
108 rewrite < sym_plus.
109 symmetry.
110 apply plus_minus_m_m.rewrite > H.
111 rewrite > sym_plus.
112 apply le_plus_n.
113 qed.
114
115 theorem minus_S_S : \forall n,m:nat.
116 eq nat (minus (S n) (S m)) (minus n m).
117 intros.
118 reflexivity.
119 qed.
120
121 theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to 
122 eq nat (minus (pred n) (pred m)) (minus n m).
123 intros.
124 apply (lt_O_n_elim n H).intro.
125 apply (lt_O_n_elim m H1).intro.
126 simplify.reflexivity.
127 qed.
128
129 theorem eq_minus_n_m_O: \forall n,m:nat.
130 n \leq m \to n-m = O.
131 intros 2.
132 apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O)).
133 intros.simplify.reflexivity.
134 intros.apply False_ind.
135 apply not_le_Sn_O.
136 goal 13.apply H.
137 intros.
138 simplify.apply H.apply le_S_S_to_le. apply H1.
139 qed.
140
141 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
142 intros.elim H.elim (minus_Sn_n n).apply le_n.
143 rewrite > minus_Sn_m.
144 apply le_S.assumption.
145 apply lt_to_le.assumption.
146 qed.
147
148 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
149 intros.apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
150 intro.elim n1.simplify.apply le_n_Sn.
151 simplify.rewrite < minus_n_O.apply le_n.
152 intros.simplify.apply le_n_Sn.
153 intros.simplify.apply H.
154 qed.
155
156 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p. 
157 intros 3.simplify.intro.
158 apply (trans_le (m-n) (S (m-(S n))) p).
159 apply minus_le_S_minus_S.
160 assumption.
161 qed.
162
163 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
164 intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)).
165 intros.rewrite < minus_n_O.apply le_n.
166 intros.simplify.apply le_n.
167 intros.simplify.apply le_S.assumption.
168 qed.
169
170 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
171 intros.apply (lt_O_n_elim n H).intro.
172 apply (lt_O_n_elim m H1).intro.
173 simplify.unfold lt.apply le_S_S.apply le_minus_m.
174 qed.
175
176 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
177 intros 2.
178 apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)).
179 intros.apply le_O_n.
180 simplify.intros. assumption.
181 simplify.intros.apply le_S_S.apply H.assumption.
182 qed.
183
184 (* galois *)
185 theorem monotonic_le_minus_r: 
186 \forall p,q,n:nat. q \leq p \to n-p \le n-q.
187 simplify.intros 2.apply (nat_elim2 
188 (\lambda p,q.\forall a.q \leq p \to a-p \leq a-q)).
189 intros.apply (le_n_O_elim n H).apply le_n.
190 intros.rewrite < minus_n_O.
191 apply le_minus_m.
192 intros.elim a.simplify.apply le_n.
193 simplify.apply H.apply le_S_S_to_le.assumption.
194 qed.
195
196 theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)).
197 intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m)))).
198 intros.apply le_O_n.
199 simplify.intros.rewrite < plus_n_O.assumption.
200 intros.
201 rewrite < plus_n_Sm.
202 apply le_S_S.apply H.
203 exact H1.
204 qed.
205
206 theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p).
207 intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p))).
208 intros.simplify.apply le_O_n.
209 intros 2.rewrite < plus_n_O.intro.simplify.assumption.
210 intros.simplify.apply H.
211 apply le_S_S_to_le.rewrite > plus_n_Sm.assumption.
212 qed.
213
214 (* the converse of le_plus_to_minus does not hold *)
215 theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)).
216 intros 3.apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m)))).
217 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
218 intro.intro.cut (n=O).rewrite > Hcut.apply le_O_n.
219 apply sym_eq. apply le_n_O_to_eq.
220 apply (trans_le ? (n+(S n1))).
221 rewrite < sym_plus.
222 apply le_plus_n.assumption.
223 intros.simplify.
224 apply H.apply le_S_S_to_le.
225 rewrite > plus_n_Sm.assumption.
226 qed.
227
228 (* minus and lt - to be completed *)
229 theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
230 intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
231 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
232 simplify.intros.apply False_ind.apply (not_le_Sn_O n H).
233 simplify.intros.unfold lt.
234 apply le_S_S.
235 rewrite < plus_n_Sm.
236 apply H.apply H1.
237 qed.
238
239 theorem distributive_times_minus: distributive nat times minus.
240 unfold distributive.
241 intros.
242 apply ((leb_elim z y)).
243   intro.cut (x*(y-z)+x*z = (x*y-x*z)+x*z).
244     apply (inj_plus_l (x*z)).assumption.
245     apply (trans_eq nat ? (x*y)).
246       rewrite < distr_times_plus.rewrite < (plus_minus_m_m ? ? H).reflexivity.
247       rewrite < plus_minus_m_m.
248         reflexivity.
249         apply le_times_r.assumption.
250   intro.rewrite > eq_minus_n_m_O.
251     rewrite > (eq_minus_n_m_O (x*y)).
252       rewrite < sym_times.simplify.reflexivity.
253         apply le_times_r.apply lt_to_le.apply not_le_to_lt.assumption.
254         apply lt_to_le.apply not_le_to_lt.assumption.
255 qed.
256
257 theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
258 \def distributive_times_minus.
259
260 theorem eq_minus_plus_plus_minus: \forall n,m,p:nat. p \le m \to (n+m)-p = n+(m-p).
261 intros.
262 apply plus_to_minus.
263 rewrite > sym_plus in \vdash (? ? ? %).
264 rewrite > assoc_plus.
265 rewrite < plus_minus_m_m.
266 reflexivity.assumption.
267 qed.
268
269 theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
270 intros.
271 cut (m+p \le n \or m+p \nleq n).
272   elim Hcut.
273     symmetry.apply plus_to_minus.
274     rewrite > assoc_plus.rewrite > (sym_plus p).rewrite < plus_minus_m_m.
275       rewrite > sym_plus.rewrite < plus_minus_m_m.
276         reflexivity.
277         apply (trans_le ? (m+p)).
278           rewrite < sym_plus.apply le_plus_n.
279           assumption.
280       apply le_plus_to_minus_r.rewrite > sym_plus.assumption.   
281     rewrite > (eq_minus_n_m_O n (m+p)).
282       rewrite > (eq_minus_n_m_O (n-m) p).
283         reflexivity.
284       apply le_plus_to_minus.apply lt_to_le. rewrite < sym_plus.
285        apply not_le_to_lt. assumption.
286     apply lt_to_le.apply not_le_to_lt.assumption.          
287   apply (decidable_le (m+p) n).
288 qed.
289
290 theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
291 p+(n-m) = n-(m-p).
292 intros.
293 apply sym_eq.
294 apply plus_to_minus.
295 rewrite < assoc_plus.
296 rewrite < plus_minus_m_m.
297 rewrite < sym_plus.
298 rewrite < plus_minus_m_m.reflexivity.
299 assumption.assumption.
300 qed.