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
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
|
From Coq Require Import Ring.
Require Import
MathClasses.interfaces.abstract_algebra
MathClasses.theory.rings MathClasses.theory.dec_fields.
Inductive Frac R `{Rap : Equiv R} `{Rzero : Zero R} : Type := frac { num: R; den: R; den_ne_0: den ≠ 0 }.
(* We used to have [den] and [den_nonzero] bundled, which did work relatively nicely with Program, but the
extra messyness in proofs etc turned out not to be worth it. *)
Arguments frac {R Rap Rzero} _ _ _.
Arguments num {R Rap Rzero} _.
Arguments den {R Rap Rzero} _.
Arguments den_ne_0 {R Rap Rzero} _ _.
Section contents.
Context `{IntegralDomain R} `{∀ x y, Decision (x = y)}.
Add Ring R: (stdlib_ring_theory R).
Global Instance Frac_equiv : Equiv (Frac R) | 0 := λ x y, num x * den y = num y * den x.
Instance: Setoid (Frac R).
Proof with auto.
split; red; unfold equiv, Frac_equiv.
reflexivity.
intros x y E. now symmetry.
intros [nx dx] [ny dy] [nz dz] V W. simpl in *.
apply (left_cancellation_ne_0 (.*.) dy)...
rewrite 2!associativity.
rewrite 2!(commutativity dy).
rewrite V, <- W. ring.
Qed.
Global Instance Frac_dec : ∀ x y: Frac R, Decision (x = y)
:= λ x y, decide_rel (=) (num x * den y) (num y * den x).
(* injection from R *)
Global Program Instance Frac_inject: Cast R (Frac R) := λ r, frac r 1 _.
Next Obligation. exact (is_ne_0 1). Qed.
Instance: Proper ((=) ==> (=)) Frac_inject.
Proof. intros x1 x2 E. unfold equiv, Frac_equiv. simpl. now rewrite E. Qed.
(* Relations, operations and constants *)
Global Program Instance Frac_plus: Plus (Frac R) :=
λ x y, frac (num x * den y + num y * den x) (den x * den y) _.
Next Obligation. destruct x, y. simpl. now apply mult_ne_0. Qed.
Global Instance Frac_0: Zero (Frac R) := ('0 : Frac R).
Global Instance Frac_1: One (Frac R) := ('1 : Frac R).
Global Instance Frac_negate: Negate (Frac R) := λ x, frac (- num x) (den x) (den_ne_0 x).
Global Program Instance Frac_mult: Mult (Frac R) := λ x y, frac (num x * num y) (den x * den y) _.
Next Obligation. destruct x, y. simpl. now apply mult_ne_0. Qed.
Ltac unfolds := unfold Frac_negate, Frac_plus, equiv, Frac_equiv in *; simpl in *.
Ltac ring_on_ring := repeat intro; unfolds; try ring.
Lemma Frac_nonzero_num x : x ≠ 0 ↔ num x ≠ 0.
Proof.
split; intros E F; apply E; unfolds.
rewrite F. ring.
rewrite right_identity in F.
rewrite F. apply left_absorb.
Qed.
Instance: Proper ((=) ==> (=) ==> (=)) Frac_plus.
Proof with try ring.
intros x x' E y y' E'. unfolds.
transitivity (num x * den x' * den y * den y' + num y * den y' * den x * den x')...
rewrite E, E'...
Qed.
Instance: Proper ((=) ==> (=)) Frac_negate.
Proof.
intros x y E. unfolds.
rewrite <-negate_mult_distr_l, E. ring.
Qed.
Instance: Proper ((=) ==> (=) ==> (=)) Frac_mult.
Proof with try ring.
intros x y E x0 y0 E'. unfolds.
transitivity (num x * den y * (num x0 * den y0))...
rewrite E, E'...
Qed.
Global Instance: Ring (Frac R).
Proof. repeat (split; try apply _); ring_on_ring. Qed.
Global Instance Frac_dec_recip: DecRecip (Frac R) := λ x,
match decide_rel (=) (num x) 0 with
| left _ => 0
| right P => frac (den x) (num x) P
end.
Instance: Setoid_Morphism Frac_dec_recip.
Proof.
split; try apply _.
intros [xn xd Px] [yn yd Py]. unfolds. unfold Frac_dec_recip. simpl.
case (decide_rel (=) xn 0); case (decide_rel (=) yn 0); intros Ey Ex; simpl.
reflexivity.
rewrite Ex. intros E. destruct Ey.
apply (right_cancellation_ne_0 (.*.) xd); trivial.
rewrite <-E. ring.
rewrite Ey. intros E. destruct Ex.
apply (right_cancellation_ne_0 (.*.) yd); trivial.
rewrite E. ring.
symmetry.
now rewrite (commutativity yd), (commutativity xd).
Qed.
Global Instance: DecField (Frac R).
Proof.
constructor; try apply _.
red. unfolds.
rewrite 2!mult_1_r.
apply (is_ne_0 1).
unfold dec_recip, Frac_dec_recip.
case (decide_rel); simpl; intuition.
intros [xn xs] Ex.
unfold dec_recip, Frac_dec_recip.
simpl. case (decide_rel); simpl.
intros E. destruct Ex. unfolds. rewrite E. ring.
intros. ring_on_ring.
Qed.
Lemma Frac_dec_mult_num_den x :
x = 'num x / 'den x.
Proof.
unfold dec_recip, Frac_dec_recip.
simpl. case (decide_rel); simpl; intros E.
now destruct (den_ne_0 x).
unfolds. ring.
Qed.
(* A final word about inject *)
Global Instance: SemiRing_Morphism Frac_inject.
Proof.
repeat (constructor; try apply _); try reflexivity.
intros x y. change ((x + y) * (1 * 1) = (x * 1 + y * 1) * 1). ring.
intros x y. change ((x * y) * (1 * 1) = x * y * 1). ring.
Qed.
Global Instance: Injective Frac_inject.
Proof.
repeat (constructor; try apply _).
intros x y. unfolds. rewrite 2!mult_1_r. intuition.
Qed.
End contents.
Set Warnings "-unsupported-attributes". (* FIXME: remove when minimal Coq version is enough *)
#[global]
Typeclasses Opaque Frac_equiv.
Set Warnings "+unsupported-attributes".
Section morphisms.
Context `{IntegralDomain R1} `{∀ x y : R1, Decision (x = y)}.
Context `{IntegralDomain R2} `{∀ x y : R2, Decision (x = y)}.
Context `(f : R1 → R2) `{!SemiRing_Morphism f} `{!Injective f}.
Program Definition Frac_lift (x : Frac R1) : Frac R2 := frac (f (num x)) (f (den x)) _.
Next Obligation.
apply injective_ne_0.
now apply (den_ne_0 x).
Qed.
Instance: Proper ((=) ==> (=)) Frac_lift.
Proof.
intros x y E.
unfold equiv, Frac_equiv, Frac_lift in *. simpl.
now rewrite <-2!preserves_mult, E.
Qed.
Global Instance: SemiRing_Morphism Frac_lift.
Proof.
pose proof (_:Ring (Frac R1)).
repeat (split; try apply _); unfold equiv, Frac_equiv, Frac_lift in *; simpl.
intros x y. now rewrite preserves_plus, ?preserves_mult.
now rewrite preserves_0, preserves_1.
intros x y. now rewrite ?preserves_mult.
now rewrite preserves_1.
Qed.
Global Instance: Injective Frac_lift.
Proof.
split; try apply _.
intros x y E.
unfold equiv, Frac_equiv, Frac_lift in *. simpl in *.
apply (injective f). now rewrite 2!preserves_mult.
Qed.
End morphisms.
|
