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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
|
Require Export NPlus.
Module Type NTimesSignature.
Declare Module Export NPlusModule : NPlusSignature.
Open Local Scope NatScope.
Parameter Inline times : N -> N -> N.
Notation "x * y" := (times x y) : NatScope.
Add Morphism times with signature E ==> E ==> E as times_wd.
Axiom times_0_n : forall n, 0 * n == 0.
Axiom times_Sn_m : forall n m, (S n) * m == m + n * m.
End NTimesSignature.
Module NTimesProperties (Import NTimesModule : NTimesSignature).
Module Export NPlusPropertiesModule := NPlusProperties NPlusModule.
Open Local Scope NatScope.
Theorem mult_0_r : forall n, n * 0 == 0.
Proof.
induct n.
now rewrite times_0_n.
intros x IH.
rewrite times_Sn_m; now rewrite plus_0_n.
Qed.
Theorem mult_0_l : forall n, 0 * n == 0.
Proof.
intro n; now rewrite times_0_n.
Qed.
Theorem mult_plus_distr_r : forall n m p, (n + m) * p == n * p + m * p.
Proof.
intros n m p; induct n.
rewrite mult_0_l.
now do 2 rewrite plus_0_l.
intros x IH.
rewrite plus_Sn_m.
do 2 rewrite times_Sn_m.
rewrite IH.
apply plus_assoc.
Qed.
Theorem mult_plus_distr_l : forall n m p, n * (m + p) == n * m + n * p.
Proof.
intros n m p; induct n.
do 3 rewrite mult_0_l; now rewrite plus_0_l.
intros x IH.
do 3 rewrite times_Sn_m.
rewrite IH.
(* Now we have to rearrange the sum of 4 terms *)
rewrite <- (plus_assoc m p (x * m + x * p)).
rewrite (plus_assoc p (x * m) (x * p)).
rewrite (plus_comm p (x * m)).
rewrite <- (plus_assoc (x * m) p (x * p)).
apply (plus_assoc m (x * m) (p + x * p)).
Qed.
Theorem mult_assoc : forall n m p, n * (m * p) == (n * m) * p.
Proof.
intros n m p; induct n.
now do 3 rewrite mult_0_l.
intros x IH.
do 2 rewrite times_Sn_m.
rewrite mult_plus_distr_r.
now rewrite IH.
Qed.
Theorem mult_1_l : forall n, 1 * n == n.
Proof.
intro n.
rewrite times_Sn_m; rewrite times_0_n. now rewrite plus_0_r.
Qed.
Theorem mult_1_r : forall n, n * 1 == n.
Proof.
induct n.
now rewrite times_0_n.
intros x IH.
rewrite times_Sn_m; rewrite IH; rewrite plus_Sn_m; now rewrite plus_0_n.
Qed.
Theorem mult_comm : forall n m, n * m == m * n.
Proof.
intros n m.
induct n.
rewrite mult_0_l; now rewrite mult_0_r.
intros x IH.
rewrite times_Sn_m.
assert (H : S x == S 0 + x).
rewrite plus_Sn_m; rewrite plus_0_n; reflexivity.
rewrite H.
rewrite mult_plus_distr_l.
rewrite mult_1_r; rewrite IH; reflexivity.
Qed.
Theorem times_eq_0 : forall n m, n * m == 0 -> n == 0 \/ m == 0.
Proof.
induct n; induct m.
intros; now left.
intros; now left.
intros; now right.
intros m IH H1.
rewrite times_Sn_m in H1; rewrite plus_Sn_m in H1; now apply S_0 in H1.
Qed.
Definition times_eq_0_dec (n m : N) : bool :=
recursion true (fun _ _ => recursion false (fun _ _ => false) m) n.
Lemma times_eq_0_dec_wd_step :
forall y y', y == y' ->
eq_bool (recursion false (fun _ _ => false) y)
(recursion false (fun _ _ => false) y').
Proof.
intros y y' Eyy'.
apply recursion_wd with (EA := eq_bool).
now unfold eq_bool.
unfold eq_fun2. intros. now unfold eq_bool.
assumption.
Qed.
Add Morphism times_eq_0_dec with signature E ==> E ==> eq_bool
as times_eq_0_dec_wd.
unfold fun2_wd, times_eq_0_dec.
intros x x' Exx' y y' Eyy'.
apply recursion_wd with (EA := eq_bool).
now unfold eq_bool.
unfold eq_fun2; intros. now apply times_eq_0_dec_wd_step.
assumption.
Qed.
Theorem times_eq_0_dec_correct :
forall n m, n * m == 0 ->
(times_eq_0_dec n m = true -> n == 0) /\
(times_eq_0_dec n m = false -> m == 0).
Proof.
nondep_induct n; nondep_induct m; unfold times_eq_0_dec.
rewrite recursion_0; split; now intros.
intro n; rewrite recursion_0; split; now intros.
intro; rewrite recursion_0; rewrite (recursion_S eq_bool);
[split; now intros | now unfold eq_bool | unfold fun2_wd; unfold eq_bool; now intros].
intro m; rewrite (recursion_S eq_bool).
rewrite times_Sn_m. rewrite plus_Sn_m. intro H; now apply S_0 in H.
now unfold eq_bool.
unfold fun2_wd; intros; now unfold eq_bool.
Qed.
Theorem times_eq_1 : forall n m, n * m == 1 -> n == 1 /\ m == 1.
Proof.
nondep_induct n; nondep_induct m.
intro H; rewrite times_0_n in H; symmetry in H; now apply S_0 in H.
intros n H; rewrite times_0_n in H; symmetry in H; now apply S_0 in H.
intro H; rewrite mult_0_r in H; symmetry in H; now apply S_0 in H.
intros m H; rewrite times_Sn_m in H; rewrite plus_Sn_m in H;
apply S_inj in H; rewrite mult_comm in H; rewrite times_Sn_m in H;
apply plus_eq_0 in H; destruct H as [H1 H2];
apply plus_eq_0 in H2; destruct H2 as [H3 _]; rewrite H1; rewrite H3; now split.
Qed.
End NTimesProperties.
|
