1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
Require Export ZPlus.
Module Type ZTimesSignature.
Declare Module Export ZPlusModule : ZPlusSignature.
Open Local Scope IntScope.
Parameter Inline times : Z -> Z -> Z.
Notation "x * y" := (times x y) : IntScope.
Add Morphism times with signature E ==> E ==> E as times_wd.
Axiom times_0 : forall n, n * 0 == 0.
Axiom times_S : forall n m, n * (S m) == n * m + n.
End ZTimesSignature.
Module ZTimesProperties (Import ZTimesModule : ZTimesSignature).
Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule.
Open Local Scope IntScope.
Theorem times_P : forall n m, n * (P m) == n * m - n.
Proof.
intros n m. rewrite_S_P m at 2. rewrite times_S. rewrite <- plus_minus_distr.
rewrite minus_diag. now rewrite plus_n_0.
Qed.
Theorem times_0_n : forall n, 0 * n == 0.
Proof.
induct n.
now rewrite times_0.
intros n IH. rewrite times_S. rewrite IH; now rewrite plus_0.
intros n IH. rewrite times_P. rewrite IH; now rewrite minus_0.
Qed.
Theorem times_Sn_m : forall n m, (S n) * m == n * m + m.
Proof.
induct m.
do 2 rewrite times_0. now rewrite plus_0.
intros m IH. do 2 rewrite times_S. rewrite IH.
do 2 rewrite <- plus_assoc. apply plus_wd. reflexivity.
do 2 rewrite plus_n_Sm; now rewrite plus_comm.
intros m IH. do 2 rewrite times_P. rewrite IH.
rewrite <- plus_minus_swap. do 2 rewrite <- plus_minus_distr.
apply plus_wd. reflexivity.
rewrite minus_S. now rewrite minus_Pn_m.
Qed.
Theorem times_Pn_m : forall n m, (P n) * m == n * m - m.
Proof.
intros n m. rewrite_S_P n at 2. rewrite times_Sn_m.
rewrite <- plus_minus_distr. rewrite minus_diag; now rewrite plus_n_0.
Qed.
Theorem times_comm : forall n m, n * m == m * n.
Proof.
intros n m; induct n.
rewrite times_0_n; now rewrite times_0.
intros n IH. rewrite times_Sn_m; rewrite times_S; now rewrite IH.
intros n IH. rewrite times_Pn_m; rewrite times_P; now rewrite IH.
Qed.
Theorem times_opp_r : forall n m, n * (- m) == - (n * m).
Proof.
intros n m; induct m.
rewrite uminus_0; rewrite times_0; now rewrite uminus_0.
intros m IH. rewrite uminus_S. rewrite times_P; rewrite times_S. rewrite IH.
rewrite <- plus_opp_minus; now rewrite opp_plus_distr.
intros m IH. rewrite uminus_P. rewrite times_P; rewrite times_S. rewrite IH.
now rewrite opp_minus_distr.
Qed.
Theorem times_opp_l : forall n m, (- n) * m == - (n * m).
Proof.
intros n m; rewrite (times_comm (- n) m); rewrite (times_comm n m);
now rewrite times_opp_r.
Qed.
Theorem times_opp_opp : forall n m, (- n) * (- m) == n * m.
Proof.
intros n m. rewrite times_opp_l. rewrite times_opp_r. now rewrite double_opp.
Qed.
Theorem times_plus_distr_r : forall n m p, n * (m + p) == n * m + n * p.
Proof.
intros n m p; induct m.
rewrite times_0; now do 2 rewrite plus_0.
intros m IH. rewrite plus_S. do 2 rewrite times_S. rewrite IH.
do 2 rewrite <- plus_assoc; apply plus_wd; [reflexivity | apply plus_comm].
intros m IH. rewrite plus_P. do 2 rewrite times_P. rewrite IH.
apply plus_minus_swap.
Qed.
Theorem times_plus_distr_l : forall n m p, (n + m) * p == n * p + m * p.
Proof.
intros n m p; rewrite (times_comm (n + m) p); rewrite times_plus_distr_r;
rewrite (times_comm p n); now rewrite (times_comm p m).
Qed.
Theorem times_minus_distr_r : forall n m p, n * (m - p) == n * m - n * p.
Proof.
intros n m p.
do 2 rewrite <- plus_opp_minus. rewrite times_plus_distr_r. now rewrite times_opp_r.
Qed.
Theorem times_minus_distr_l : forall n m p, (n - m) * p == n * p - m * p.
Proof.
intros n m p.
do 2 rewrite <- plus_opp_minus. rewrite times_plus_distr_l. now rewrite times_opp_l.
Qed.
Theorem times_assoc : forall n m p, n * (m * p) == (n * m) * p.
Proof.
intros n m p; induct p.
now do 3 rewrite times_0.
intros p IH. do 2 rewrite times_S. rewrite times_plus_distr_r. now rewrite IH.
intros p IH. do 2 rewrite times_P. rewrite times_minus_distr_r. now rewrite IH.
Qed.
End ZTimesProperties.
|
