-
Notifications
You must be signed in to change notification settings - Fork 89
/
Basic.lean
276 lines (235 loc) · 11.4 KB
/
Basic.lean
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
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Std.Data.Nat.Gcd
import Std.Data.Int.DivMod
import Std.Tactic.Ext
/-! # Basics for the Rational Numbers -/
/--
Rational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
-/
@[ext] structure Rat where
/-- Constructs a rational number from components.
We rename the constructor to `mk'` to avoid a clash with the smart constructor. -/
mk' ::
/-- The numerator of the rational number is an integer. -/
num : Int
/-- The denominator of the rational number is a natural number. -/
den : Nat := 1
/-- The denominator is nonzero. -/
den_nz : den ≠ 0 := by decide
/-- The numerator and denominator are coprime: it is in "reduced form". -/
reduced : num.natAbs.coprime den := by decide
deriving DecidableEq
instance : Inhabited Rat := ⟨{ num := 0 }⟩
instance : ToString Rat where
toString a := if a.den = 1 then toString a.num else s!"{a.num}/{a.den}"
instance : Repr Rat where
reprPrec a _ := if a.den = 1 then repr a.num else s!"({a.num} : Rat)/{a.den}"
theorem Rat.den_pos (self : Rat) : 0 < self.den := Nat.pos_of_ne_zero self.den_nz
-- Note: `Rat.normalize` uses `Int.div` internally,
-- but we may want to refactor to use `/` (`Int.ediv`)
/--
Auxiliary definition for `Rat.normalize`. Constructs `num / den` as a rational number,
dividing both `num` and `den` by `g` (which is the gcd of the two) if it is not 1.
-/
@[inline] def Rat.maybeNormalize (num : Int) (den g : Nat)
(den_nz : den / g ≠ 0) (reduced : (num.div g).natAbs.coprime (den / g)) : Rat :=
if hg : g = 1 then
{ num, den
den_nz := by simp [hg] at den_nz; exact den_nz
reduced := by simp [hg, Int.natAbs_ofNat] at reduced; exact reduced }
else { num := num.div g, den := den / g, den_nz, reduced }
theorem Rat.normalize.den_nz {num : Int} {den g : Nat} (den_nz : den ≠ 0)
(e : g = num.natAbs.gcd den) : den / g ≠ 0 :=
e ▸ Nat.ne_of_gt (Nat.div_gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero den_nz))
theorem Rat.normalize.reduced {num : Int} {den g : Nat} (den_nz : den ≠ 0)
(e : g = num.natAbs.gcd den) : (num.div g).natAbs.coprime (den / g) :=
have : Int.natAbs (num.div ↑g) = num.natAbs / g := by
match num, num.eq_nat_or_neg with
| _, ⟨_, .inl rfl⟩ => rfl
| _, ⟨_, .inr rfl⟩ => rw [Int.neg_div, Int.natAbs_neg, Int.natAbs_neg]; rfl
this ▸ e ▸ Nat.coprime_div_gcd_div_gcd (Nat.gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero den_nz))
/--
Construct a normalized `Rat` from a numerator and nonzero denominator.
This is a "smart constructor" that divides the numerator and denominator by
the gcd to ensure that the resulting rational number is normalized.
-/
@[inline] def Rat.normalize (num : Int) (den : Nat := 1) (den_nz : den ≠ 0 := by decide) : Rat :=
Rat.maybeNormalize num den (num.natAbs.gcd den)
(normalize.den_nz den_nz rfl) (normalize.reduced den_nz rfl)
/--
Construct a rational number from a numerator and denominator.
This is a "smart constructor" that divides the numerator and denominator by
the gcd to ensure that the resulting rational number is normalized, and returns
zero if `den` is zero.
-/
def mkRat (num : Int) (den : Nat) : Rat :=
if den_nz : den = 0 then { num := 0 } else Rat.normalize num den den_nz
namespace Rat
/-- Embedding of `Int` in the rational numbers. -/
def ofInt (num : Int) : Rat := { num, reduced := Nat.coprime_one_right _ }
instance : IntCast Rat := ⟨ofInt⟩
instance : OfNat Rat n := ⟨n⟩
/-- Is this rational number integral? -/
@[inline] protected def isInt (a : Rat) : Bool := a.den == 1
/-- Form the quotient `n / d` where `n d : Int`. -/
def divInt : Int → Int → Rat
| n, .ofNat d => inline (mkRat n d)
| n, .negSucc d => normalize (-n) d.succ (fun.)
@[inherit_doc] scoped infixl:70 " /. " => Rat.divInt
/-- Implements "scientific notation" `123.4e-5` for rational numbers. (This definition is
`@[irreducible]` because you don't want to unfold it. Use `Rat.ofScientific_def`,
`Rat.ofScientific_true_def`, or `Rat.ofScientific_false_def` instead.) -/
@[irreducible] protected def ofScientific (m : Nat) (s : Bool) (e : Nat) : Rat :=
if s then
Rat.normalize m (10 ^ e) <| Nat.ne_of_gt <| Nat.pos_pow_of_pos _ (by decide)
else
(m * 10 ^ e : Nat)
instance : OfScientific Rat where ofScientific := Rat.ofScientific
/-- Rational number strictly less than relation, as a `Bool`. -/
protected def blt (a b : Rat) : Bool :=
if a.num < 0 && 0 ≤ b.num then
true
else if a.num = 0 then
0 < b.num
else if 0 < a.num && b.num ≤ 0 then
false
else
-- `a` and `b` must have the same sign
a.num * b.den < b.num * a.den
instance : LT Rat := ⟨(·.blt ·)⟩
instance (a b : Rat) : Decidable (a < b) :=
inferInstanceAs (Decidable (_ = true))
instance : LE Rat := ⟨fun a b => b.blt a = false⟩
instance (a b : Rat) : Decidable (a ≤ b) :=
inferInstanceAs (Decidable (_ = false))
/-- Multiplication of rational numbers. (This definition is `@[irreducible]` because you don't
want to unfold it. Use `Rat.mul_def` instead.) -/
@[irreducible] protected def mul (a b : Rat) : Rat :=
let g1 := Nat.gcd a.num.natAbs b.den
let g2 := Nat.gcd b.num.natAbs a.den
{ num := (a.num.div g1) * (b.num.div g2)
den := (a.den / g2) * (b.den / g1)
den_nz := Nat.ne_of_gt <| Nat.mul_pos
(Nat.div_gcd_pos_of_pos_right _ a.den_pos) (Nat.div_gcd_pos_of_pos_right _ b.den_pos)
reduced := by
simp only [Int.natAbs_mul, Int.natAbs_div, Nat.coprime_mul_iff_left]
refine ⟨Nat.coprime_mul_iff_right.2 ⟨?_, ?_⟩, Nat.coprime_mul_iff_right.2 ⟨?_, ?_⟩⟩
· exact a.reduced.coprime_div_left (Nat.gcd_dvd_left ..)
|>.coprime_div_right (Nat.gcd_dvd_right ..)
· exact Nat.coprime_div_gcd_div_gcd (Nat.gcd_pos_of_pos_right _ b.den_pos)
· exact Nat.coprime_div_gcd_div_gcd (Nat.gcd_pos_of_pos_right _ a.den_pos)
· exact b.reduced.coprime_div_left (Nat.gcd_dvd_left ..)
|>.coprime_div_right (Nat.gcd_dvd_right ..) }
instance : Mul Rat := ⟨Rat.mul⟩
/--
The inverse of a rational number. Note: `inv 0 = 0`. (This definition is `@[irreducible]`
because you don't want to unfold it. Use `Rat.inv_def` instead.)
-/
@[irreducible] protected def inv (a : Rat) : Rat :=
if h : a.num < 0 then
{ num := -a.den, den := a.num.natAbs
den_nz := Nat.ne_of_gt (Int.natAbs_pos.2 (Int.ne_of_lt h))
reduced := Int.natAbs_neg a.den ▸ a.reduced.symm }
else if h : a.num > 0 then
{ num := a.den, den := a.num.natAbs
den_nz := Nat.ne_of_gt (Int.natAbs_pos.2 (Int.ne_of_gt h))
reduced := a.reduced.symm }
else
a
/-- Division of rational numbers. Note: `div a 0 = 0`. -/
protected def div : Rat → Rat → Rat := (· * ·.inv)
/-- Division of rational numbers. Note: `div a 0 = 0`. Written with a separate function `Rat.div`
as a wrapper so that the definition is not unfolded at `.instance` transparency. -/
instance : Div Rat := ⟨Rat.div⟩
theorem add.aux (a b : Rat) {g ad bd} (hg : g = a.den.gcd b.den)
(had : ad = a.den / g) (hbd : bd = b.den / g) :
let den := ad * b.den; let num := a.num * bd + b.num * ad
num.natAbs.gcd g = num.natAbs.gcd den := by
intro den num
have ae : ad * g = a.den := had ▸ Nat.div_mul_cancel (hg ▸ Nat.gcd_dvd_left ..)
have be : bd * g = b.den := hbd ▸ Nat.div_mul_cancel (hg ▸ Nat.gcd_dvd_right ..)
have hden : den = ad * bd * g := by rw [Nat.mul_assoc, be]
rw [hden, Nat.coprime.gcd_mul_left_cancel_right]
have cop : ad.coprime bd := had ▸ hbd ▸ hg ▸
Nat.coprime_div_gcd_div_gcd (Nat.gcd_pos_of_pos_left _ a.den_pos)
have H1 (d : Nat) :
d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad := by
have := d.gcd_dvd_right num.natAbs
rw [← Int.ofNat_dvd, Int.dvd_natAbs] at this
have := Int.dvd_iff_dvd_of_dvd_add this
rwa [← Int.dvd_natAbs, Int.ofNat_dvd, Int.natAbs_mul,
← Int.dvd_natAbs, Int.ofNat_dvd, Int.natAbs_mul] at this
apply Nat.coprime.mul
· have := (H1 ad).2 <| Nat.dvd_trans (Nat.gcd_dvd_left ..) (Nat.dvd_mul_left ..)
have := (cop.coprime_dvd_left <| Nat.gcd_dvd_left ..).dvd_of_dvd_mul_right this
exact Nat.eq_one_of_dvd_one <| a.reduced.gcd_eq_one ▸ Nat.dvd_gcd this <|
Nat.dvd_trans (Nat.gcd_dvd_left ..) (ae ▸ Nat.dvd_mul_right ..)
· have := (H1 bd).1 <| Nat.dvd_trans (Nat.gcd_dvd_left ..) (Nat.dvd_mul_left ..)
have := (cop.symm.coprime_dvd_left <| Nat.gcd_dvd_left ..).dvd_of_dvd_mul_right this
exact Nat.eq_one_of_dvd_one <| b.reduced.gcd_eq_one ▸ Nat.dvd_gcd this <|
Nat.dvd_trans (Nat.gcd_dvd_left ..) (be ▸ Nat.dvd_mul_right ..)
/--
Addition of rational numbers. (This definition is `@[irreducible]` because you don't want to
unfold it. Use `Rat.add_def` instead.)
-/
@[irreducible] protected def add (a b : Rat) : Rat :=
let g := a.den.gcd b.den
if hg : g = 1 then
have den_nz := Nat.ne_of_gt <| Nat.mul_pos a.den_pos b.den_pos
have reduced := add.aux a b hg.symm (Nat.div_one _).symm (Nat.div_one _).symm
|>.symm.trans (Nat.gcd_one_right _)
{ num := a.num * b.den + b.num * a.den, den := a.den * b.den, den_nz, reduced }
else
let den := (a.den / g) * b.den
let num := a.num * ↑(b.den / g) + b.num * ↑(a.den / g)
let g1 := num.natAbs.gcd g
have den_nz := Nat.ne_of_gt <| Nat.mul_pos (Nat.div_gcd_pos_of_pos_left _ a.den_pos) b.den_pos
have e : g1 = num.natAbs.gcd den := add.aux a b rfl rfl rfl
Rat.maybeNormalize num den g1 (normalize.den_nz den_nz e) (normalize.reduced den_nz e)
instance : Add Rat := ⟨Rat.add⟩
/-- Negation of rational numbers. -/
protected def neg (a : Rat) : Rat :=
{ a with num := -a.num, reduced := by rw [Int.natAbs_neg]; exact a.reduced }
instance : Neg Rat := ⟨Rat.neg⟩
theorem sub.aux (a b : Rat) {g ad bd} (hg : g = a.den.gcd b.den)
(had : ad = a.den / g) (hbd : bd = b.den / g) :
let den := ad * b.den; let num := a.num * bd - b.num * ad
num.natAbs.gcd g = num.natAbs.gcd den := by
have := add.aux a (-b) hg had hbd
simp only [show (-b).num = -b.num from rfl, Int.neg_mul] at this
exact this
/-- Subtraction of rational numbers. (This definition is `@[irreducible]` because you don't want to
unfold it. Use `Rat.sub_def` instead.)
-/
@[irreducible] protected def sub (a b : Rat) : Rat :=
let g := a.den.gcd b.den
if hg : g = 1 then
have den_nz := Nat.ne_of_gt <| Nat.mul_pos a.den_pos b.den_pos
have reduced := sub.aux a b hg.symm (Nat.div_one _).symm (Nat.div_one _).symm
|>.symm.trans (Nat.gcd_one_right _)
{ num := a.num * b.den - b.num * a.den, den := a.den * b.den, den_nz, reduced }
else
let den := (a.den / g) * b.den
let num := a.num * ↑(b.den / g) - b.num * ↑(a.den / g)
let g1 := num.natAbs.gcd g
have den_nz := Nat.ne_of_gt <| Nat.mul_pos (Nat.div_gcd_pos_of_pos_left _ a.den_pos) b.den_pos
have e : g1 = num.natAbs.gcd den := sub.aux a b rfl rfl rfl
Rat.maybeNormalize num den g1 (normalize.den_nz den_nz e) (normalize.reduced den_nz e)
instance : Sub Rat := ⟨Rat.sub⟩
/-- The floor of a rational number `a` is the largest integer less than or equal to `a`. -/
protected def floor (a : Rat) : Int :=
if a.den = 1 then
a.num
else
a.num / a.den
/-- The ceiling of a rational number `a` is the smallest integer greater than or equal to `a`. -/
protected def ceil (a : Rat) : Int :=
if a.den = 1 then
a.num
else
a.num / a.den + 1