]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/nat/times.ma
unreleased version of the bindings, with more gtkmathview method bounds and dependenc...
[helm.git] / helm / matita / library / nat / times.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 set "baseuri" "cic:/matita/nat/times".
16
17 include "logic/equality.ma".
18 include "nat/nat.ma".
19 include "nat/plus.ma".
20
21 let rec times n m \def 
22  match n with 
23  [ O \Rightarrow O
24  | (S p) \Rightarrow (m+(times p m)) ].
25
26 (*CSC: the URI must disappear: there is a bug now *)
27 interpretation "natural times" 'times x y = (cic:/matita/nat/times/times.con x y).
28
29 theorem times_n_O: \forall n:nat. O = n*O.
30 intros.elim n.
31 simplify.reflexivity.
32 simplify.assumption.
33 qed.
34
35 theorem times_n_Sm : 
36 \forall n,m:nat.n+n*m = n*(S m).
37 intros.elim n.
38 simplify.reflexivity.
39 simplify.apply eq_f.rewrite < H.
40 transitivity ((n1+m)+n1*m).symmetry.apply assoc_plus.
41 transitivity ((m+n1)+n1*m).
42 apply eq_f2.
43 apply sym_plus.
44 reflexivity.
45 apply assoc_plus.
46 qed.
47
48 (* same problem with symmetric: see plus 
49 theorem symmetric_times : symmetric nat times. *)
50
51 theorem sym_times : 
52 \forall n,m:nat.n*m = m*n.
53 intros.elim n.
54 simplify.apply times_n_O.
55 simplify.rewrite > H.apply times_n_Sm.
56 qed.
57
58 theorem distributive_times_plus : distributive nat times plus.
59 simplify.
60 intros.elim x.
61 simplify.reflexivity.
62 simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
63 apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? z.
64 rewrite > assoc_plus.reflexivity.
65 qed.
66
67 variant times_plus_distr: \forall n,m,p:nat. n*(m+p)=n*m+n*p
68 \def distributive_times_plus.
69