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
|
(* The standard library's implementation of the integers (BinInt) uses nasty binary positive
crap with various horrible horrible bit fiddling operations on it (especially Pminus).
The following is a much simpler implementation whose correctness can be shown much
more easily. In particular, it lets us use initiality of the natural numbers to prove initiality
of these integers. *)
Require
MathClasses.theory.naturals.
From Coq Require Import Ring.
Require Import
MathClasses.interfaces.abstract_algebra MathClasses.theory.categories
MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.theory.jections.
Require Export
MathClasses.implementations.semiring_pairs.
Section contents.
Context `{Naturals N}.
Add Ring N : (rings.stdlib_semiring_theory N).
Notation Z := (SRpair N).
(* We show that Z is initial, and therefore a model of the integers. *)
Global Instance SRpair_to_ring: IntegersToRing Z :=
λ _ _ _ _ _ _ z, naturals_to_semiring N _ (pos z) + - naturals_to_semiring N _ (neg z).
(* Hint Rewrite preserves_0 preserves_1 preserves_mult preserves_plus: preservation.
doesn't work for some reason, so we use: *)
Ltac preservation :=
repeat (rewrite rings.preserves_plus || rewrite rings.preserves_mult || rewrite rings.preserves_0 || rewrite rings.preserves_1).
Section for_another_ring.
Context `{Ring R}.
Add Ring R : (rings.stdlib_ring_theory R).
Notation n_to_sr := (naturals_to_semiring N R).
Notation z_to_r := (integers_to_ring Z R).
Instance: Proper ((=) ==> (=)) z_to_r.
Proof.
intros [xp xn] [yp yn].
change (xp + yn = yp + xn → n_to_sr xp - n_to_sr xn = n_to_sr yp - n_to_sr yn). intros E.
apply rings.equal_by_zero_sum.
transitivity (n_to_sr xp + n_to_sr yn - (n_to_sr xn + n_to_sr yp)); [ring|].
rewrite <-2!rings.preserves_plus, E, (commutativity xn yp). ring.
Qed.
Ltac derive_preservation := unfold integers_to_ring, SRpair_to_ring; simpl; preservation; ring.
Let preserves_plus x y: z_to_r (x + y) = z_to_r x + z_to_r y.
Proof. derive_preservation. Qed.
Let preserves_mult x y: z_to_r (x * y) = z_to_r x * z_to_r y.
Proof. derive_preservation. Qed.
Let preserves_1: z_to_r 1 = 1.
Proof. derive_preservation. Qed.
Let preserves_0: z_to_r 0 = 0.
Proof. derive_preservation. Qed.
Global Instance: SemiRing_Morphism z_to_r.
Proof.
repeat (split; try apply _).
exact preserves_plus.
exact preserves_0.
exact preserves_mult.
exact preserves_1.
Qed.
Section for_another_morphism.
Context (f : Z → R) `{!SemiRing_Morphism f}.
Definition g : N → R := f ∘ cast N (SRpair N).
Instance: SemiRing_Morphism g.
Proof. unfold g. repeat (split; try apply _). Qed.
Lemma same_morphism: z_to_r = f.
Proof.
intros [p n] z' E. rewrite <- E. clear E z'.
rewrite SRpair_splits.
preservation. rewrite 2!rings.preserves_negate.
now rewrite 2!(naturals.to_semiring_twice _ _ _).
Qed.
End for_another_morphism.
End for_another_ring.
Instance: Initial (rings.object Z).
Proof. apply integer_initial. intros. now apply same_morphism. Qed.
Global Instance: Integers Z := {}.
Context `{!NatDistance N}.
Global Program Instance SRpair_abs: IntAbs Z N := λ x,
match nat_distance_sig (pos x) (neg x) with
| inl (n↾E) => inr n
| inr (n↾E) => inl n
end.
Next Obligation.
rewrite <-(naturals.to_semiring_unique (cast N (SRpair N))).
do 2 red. simpl. now rewrite rings.plus_0_r, commutativity.
Qed.
Next Obligation.
rewrite <-(naturals.to_semiring_unique (cast N (SRpair N))).
do 2 red. simpl. symmetry. now rewrite rings.plus_0_r, commutativity.
Qed.
Notation n_to_z := (naturals_to_semiring N Z).
(* Without this opaque, typeclasses find a proof of Injective zero,
from [id_injective] *)
Typeclasses Opaque zero.
Let zero_product_aux a b :
n_to_z a * n_to_z b = 0 → n_to_z a = 0 ∨ n_to_z b = 0.
Proof.
rewrite <-rings.preserves_mult.
rewrite <-(naturals.to_semiring_unique (SRpair_inject)).
intros E. setoid_inject.
assert (HN : (a = 0) ∨ (b = 0)) by now apply zero_product.
destruct HN as [HN|HN]; [left|right]; rewrite HN; apply preserves_mon_unit.
Qed.
Global Instance: ZeroProduct Z.
Proof.
intros x y E.
destruct (SRpair_abs x) as [[a A]|[a A]], (SRpair_abs y) as [[b B]|[b B]].
rewrite <-A, <-B in E |- *. now apply zero_product_aux.
destruct (zero_product_aux a b) as [C|C].
rewrite A, B. now apply rings.negate_zero_prod_r.
left. now rewrite <-A.
right. apply rings.flip_negate_0. now rewrite <-B.
destruct (zero_product_aux a b) as [C|C].
rewrite A, B. now apply rings.negate_zero_prod_l.
left. apply rings.flip_negate_0. now rewrite <-A.
right. now rewrite <-B.
destruct (zero_product_aux a b) as [C|C].
now rewrite A, B, rings.negate_mult_negate.
left. apply rings.flip_negate_0. now rewrite <-A.
right. apply rings.flip_negate_0. now rewrite <-B.
Qed.
End contents.
|
