blob: b72847c08974a3f4fa32a005f2609dd18db421e3 (
plain)
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
|
Require Import Ring.
Require Import NTimes.
Require Export ZTimes.
Require Export ZPairsPlus.
Module NatPairsTimes (Import NTimesModule : NTimesSignature) <: ZTimesSignature.
Module Export ZPlusModule := NatPairsPlus NTimesModule.NPlusModule. (* "NTimesModule." is optional *)
Module Import NTimesPropertiesModule := NTimesProperties NTimesModule.
Open Local Scope NatScope.
Definition times (n m : Z) :=
((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
Notation "x * y" := (times x y) : IntScope.
Add Morphism times with signature E ==> E ==> E as times_wd.
Proof.
unfold times, E; intros x1 y1 H1 x2 y2 H2; simpl.
stepl_ring (fst x1 * fst x2 + (snd x1 * snd x2 + fst y1 * snd y2 + snd y1 * fst y2)).
stepr_ring (fst x1 * snd x2 + (fst y1 * fst y2 + snd y1 * snd y2 + snd x1 * fst x2)).
apply plus_times_repl_pair with (n := fst y2) (m := snd y2); [| now idtac].
stepl_ring (snd x1 * snd x2 + (fst x1 * fst y2 + fst y1 * snd y2 + snd y1 * fst y2)).
stepr_ring (snd x1 * fst x2 + (fst x1 * snd y2 + fst y1 * fst y2 + snd y1 * snd y2)).
apply plus_times_repl_pair with (n := snd y2) (m := fst y2);
[| rewrite plus_comm; symmetry; now rewrite plus_comm].
stepl_ring (snd y2 * snd x1 + (fst x1 * fst y2 + fst y1 * snd y2 + snd y1 * fst y2)).
stepr_ring (snd y2 * fst x1 + (snd x1 * fst y2 + fst y1 * fst y2 + snd y1 * snd y2)).
apply plus_times_repl_pair with (n := snd y1) (m := fst y1);
[| rewrite plus_comm; symmetry; now rewrite plus_comm].
stepl_ring (fst y2 * fst x1 + (snd y2 * snd y1 + fst y1 * snd y2 + snd y1 * fst y2)).
stepr_ring (fst y2 * snd x1 + (snd y2 * fst y1 + fst y1 * fst y2 + snd y1 * snd y2)).
apply plus_times_repl_pair with (n := fst y1) (m := snd y1); [| now idtac].
ring.
Qed.
Open Local Scope IntScope.
Theorem times_0 : forall n, n * 0 == 0.
Proof.
intro n; unfold times, E; simpl.
repeat rewrite times_0_r. now rewrite plus_assoc.
Qed.
Theorem times_S : forall n m, n * (S m) == n * m + n.
Proof.
intros n m; unfold times, S, E; simpl.
do 2 rewrite times_S_r. ring.
Qed.
End NatPairsTimes.
Module NatPairsTimesProperties (NTimesModule : NTimesSignature).
Module Export NatPairsTimesModule := NatPairsTimes NTimesModule.
Module Export NatPairsTimesPropertiesModule := ZTimesProperties NatPairsTimesModule.
End NatPairsTimesProperties.
|
