IndisputableMonolith.Foundation.RationalsFromLogic
IndisputableMonolith/Foundation/RationalsFromLogic.lean · 437 lines · 40 declarations
show as:
view math explainer →
1/-
2 RationalsFromLogic.lean
3
4 Recovery of the rationals from `LogicInt`, by field-of-fractions
5 construction.
6
7 A rational is a formal quotient `a/b` with `a : LogicInt`,
8 `b : LogicInt`, `b ≠ 0`, modulo the equivalence
9 `(a, b) ~ (c, d) ↔ a*d = c*b`. This is the field of fractions of
10 the integral domain `LogicInt`.
11
12 The recovery chain extends:
13
14 Law of Logic
15 ⊢ J
16 ⊢ LogicNat ≃ Nat (Foundation.ArithmeticFromLogic)
17 ⊢ LogicInt ≃ Int (Foundation.IntegersFromLogic)
18 ⊢ LogicRat ≃ Rat (this module)
19
20 Status: Level 1. Defines the carrier, the equivalence relation, the
21 setoid, the quotient, zero/one/negation/addition/multiplication, and
22 the carrier-level equivalence with `Rat`. Field axioms (associativity
23 of multiplication, distributivity, multiplicative inverse for
24 non-zero elements) are mechanical extensions left for a follow-up.
25-/
26
27import Mathlib
28import IndisputableMonolith.Foundation.IntegersFromLogic
29
30namespace IndisputableMonolith
31namespace Foundation
32namespace RationalsFromLogic
33
34open IntegersFromLogic IntegersFromLogic.LogicInt
35open ArithmeticFromLogic ArithmeticFromLogic.LogicNat
36
37/-! ## 1. Pre-rational structure: pairs with non-zero denominator -/
38
39/-- A pre-rational is a pair `(num, den)` with `den ≠ 0`. -/
40structure PreRat where
41 num : LogicInt
42 den : LogicInt
43 den_nonzero : den ≠ 0
44
45/-- The field-of-fractions equivalence: `(a, b) ~ (c, d)` iff
46`a * d = c * b`. -/
47def ratRel : PreRat → PreRat → Prop :=
48 fun p q => p.num * q.den = q.num * p.den
49
50theorem ratRel_refl : ∀ p : PreRat, ratRel p p := by
51 intro p
52 show p.num * p.den = p.num * p.den
53 rfl
54
55theorem ratRel_symm : ∀ {p q : PreRat}, ratRel p q → ratRel q p := by
56 intro p q h
57 show q.num * p.den = p.num * q.den
58 exact h.symm
59
60theorem ratRel_trans : ∀ {p q r : PreRat}, ratRel p q → ratRel q r → ratRel p r := by
61 rintro ⟨a, b, hb⟩ ⟨c, d, hd⟩ ⟨e, f, hf⟩ hpq hqr
62 -- hpq : a * d = c * b
63 -- hqr : c * f = e * d
64 -- goal: a * f = e * b
65 -- Method: (a * f) * d = a * f * d = a * d * f = c * b * f = c * f * b = e * d * b = (e * b) * d.
66 -- Cancel d ≠ 0.
67 show a * f = e * b
68 have key : (a * f) * d = (e * b) * d := by
69 calc (a * f) * d
70 = (a * d) * f := by rw [mul_assoc', mul_comm' f d, ← mul_assoc']
71 _ = (c * b) * f := by rw [hpq]
72 _ = (c * f) * b := by rw [mul_assoc', mul_comm' b f, ← mul_assoc']
73 _ = (e * d) * b := by rw [hqr]
74 _ = (e * b) * d := by rw [mul_assoc', mul_comm' d b, ← mul_assoc']
75 exact mul_right_cancel hd key
76
77instance setoid : Setoid PreRat := ⟨ratRel, ratRel_refl, ratRel_symm, ratRel_trans⟩
78
79/-! ## 2. The Type of Logic-Native Rationals -/
80
81/-- `LogicRat` is the field of fractions of `LogicInt`. -/
82def LogicRat : Type := Quotient (setoid : Setoid PreRat)
83
84namespace LogicRat
85
86/-- Constructor: form a rational from a pair with non-zero denominator. -/
87def mk (a b : LogicInt) (hb : b ≠ 0) : LogicRat :=
88 Quotient.mk' ⟨a, b, hb⟩
89
90theorem sound (a b c d : LogicInt) (hb : b ≠ 0) (hd : d ≠ 0)
91 (h : a * d = c * b) : mk a b hb = mk c d hd := by
92 apply Quotient.sound
93 show a * d = c * b
94 exact h
95
96/-! ## 3. Embedding LogicInt into LogicRat -/
97
98/-- The natural injection `LogicInt ↪ LogicRat` sending `n` to `n/1`. -/
99def ofLogicInt (n : LogicInt) : LogicRat :=
100 mk n 1 (by
101 intro h
102 have : toInt (1 : LogicInt) = toInt (0 : LogicInt) := congrArg toInt h
103 rw [toInt_one, toInt_zero] at this
104 exact one_ne_zero this)
105
106/-! ## 4. Zero, One, Negation, Addition, Multiplication -/
107
108/-- Zero in `LogicRat`. -/
109def zero : LogicRat :=
110 mk 0 1 (by
111 intro h
112 have : toInt (1 : LogicInt) = toInt (0 : LogicInt) := congrArg toInt h
113 rw [toInt_one, toInt_zero] at this
114 exact one_ne_zero this)
115
116/-- One in `LogicRat`. -/
117def one : LogicRat :=
118 mk 1 1 (by
119 intro h
120 have : toInt (1 : LogicInt) = toInt (0 : LogicInt) := congrArg toInt h
121 rw [toInt_one, toInt_zero] at this
122 exact one_ne_zero this)
123
124instance : Zero LogicRat := ⟨zero⟩
125instance : One LogicRat := ⟨one⟩
126
127/-- Negation: `-(a/b) = (-a)/b`. -/
128def neg : LogicRat → LogicRat :=
129 Quotient.lift
130 (fun (p : PreRat) => mk (-p.num) p.den p.den_nonzero)
131 (by
132 rintro ⟨a, b, hb⟩ ⟨c, d, hd⟩ h
133 show mk (-a) b hb = mk (-c) d hd
134 apply sound
135 show -a * d = -c * b
136 have h' : a * d = c * b := h
137 rw [eq_iff_toInt_eq, toInt_mul, toInt_mul, toInt_neg, toInt_neg]
138 have h'' : toInt a * toInt d = toInt c * toInt b := by
139 have := congrArg toInt h'
140 rwa [toInt_mul, toInt_mul] at this
141 linarith)
142
143instance : Neg LogicRat := ⟨neg⟩
144
145/-- Addition: `(a/b) + (c/d) = (a*d + c*b) / (b*d)`. -/
146def add : LogicRat → LogicRat → LogicRat :=
147 Quotient.lift₂
148 (fun (p q : PreRat) =>
149 mk (p.num * q.den + q.num * p.den) (p.den * q.den)
150 (fun h => p.den_nonzero ((mul_eq_zero.mp h).resolve_right q.den_nonzero)))
151 (by
152 rintro ⟨a, b, hb⟩ ⟨c, d, hd⟩ ⟨a', b', hb'⟩ ⟨c', d', hd'⟩ hab hcd
153 show mk (a * d + c * b) (b * d) _
154 = mk (a' * d' + c' * b') (b' * d') _
155 apply sound
156 show (a * d + c * b) * (b' * d') = (a' * d' + c' * b') * (b * d)
157 rw [eq_iff_toInt_eq]
158 simp only [toInt_add, toInt_mul]
159 have hab' : toInt a * toInt b' = toInt a' * toInt b := by
160 have := congrArg toInt hab
161 rwa [toInt_mul, toInt_mul] at this
162 have hcd' : toInt c * toInt d' = toInt c' * toInt d := by
163 have := congrArg toInt hcd
164 rwa [toInt_mul, toInt_mul] at this
165 linear_combination (toInt d * toInt d') * hab' + (toInt b * toInt b') * hcd')
166
167instance : Add LogicRat := ⟨add⟩
168
169/-- Multiplication: `(a/b) * (c/d) = (a*c) / (b*d)`. -/
170def mul : LogicRat → LogicRat → LogicRat :=
171 Quotient.lift₂
172 (fun (p q : PreRat) =>
173 mk (p.num * q.num) (p.den * q.den)
174 (fun h => p.den_nonzero ((mul_eq_zero.mp h).resolve_right q.den_nonzero)))
175 (by
176 rintro ⟨a, b, hb⟩ ⟨c, d, hd⟩ ⟨a', b', hb'⟩ ⟨c', d', hd'⟩ hab hcd
177 show mk (a * c) (b * d) _ = mk (a' * c') (b' * d') _
178 apply sound
179 show a * c * (b' * d') = a' * c' * (b * d)
180 rw [eq_iff_toInt_eq]
181 simp only [toInt_mul]
182 have hab' : toInt a * toInt b' = toInt a' * toInt b := by
183 have := congrArg toInt hab
184 rwa [toInt_mul, toInt_mul] at this
185 have hcd' : toInt c * toInt d' = toInt c' * toInt d := by
186 have := congrArg toInt hcd
187 rwa [toInt_mul, toInt_mul] at this
188 linear_combination (toInt c * toInt d') * hab' + (toInt a' * toInt b) * hcd')
189
190instance : Mul LogicRat := ⟨mul⟩
191
192/-! ## 5. Recovery Theorem: LogicRat ≃ Rat
193
194Map a pre-rational `(a, b)` with `b ≠ 0` to the rational `(toInt a) / (toInt b)`
195in `Rat`. Well-defined on the quotient because `a*d = c*b` implies the
196two `Rat` values are equal. -/
197
198/-- Map a `PreRat` to `Rat`. -/
199def toRatCore : PreRat → ℚ :=
200 fun p => (toInt p.num : ℚ) / (toInt p.den : ℚ)
201
202theorem toRatCore_respects :
203 ∀ p q : PreRat, p ≈ q → toRatCore p = toRatCore q := by
204 rintro ⟨a, b, hb⟩ ⟨c, d, hd⟩ h
205 show (toInt a : ℚ) / toInt b = (toInt c : ℚ) / toInt d
206 have hb_int : (toInt b : ℚ) ≠ 0 := by
207 intro habs
208 apply hb
209 rw [eq_iff_toInt_eq, toInt_zero]
210 exact_mod_cast habs
211 have hd_int : (toInt d : ℚ) ≠ 0 := by
212 intro habs
213 apply hd
214 rw [eq_iff_toInt_eq, toInt_zero]
215 exact_mod_cast habs
216 have h' : toInt a * toInt d = toInt c * toInt b := by
217 have := congrArg toInt (show a * d = c * b from h)
218 rwa [toInt_mul, toInt_mul] at this
219 rw [div_eq_div_iff hb_int hd_int]
220 exact_mod_cast h'
221
222/-- The recovery map `LogicRat → Rat`. -/
223def toRat : LogicRat → ℚ := Quotient.lift toRatCore toRatCore_respects
224
225/-- The inverse `Rat → LogicRat`. -/
226noncomputable def fromRat (q : ℚ) : LogicRat :=
227 let n : LogicInt := fromInt q.num
228 let d : LogicInt := fromInt q.den
229 mk n d (by
230 intro h
231 have : toInt d = toInt 0 := congrArg toInt h
232 rw [toInt_zero] at this
233 have : toInt (fromInt q.den) = 0 := this
234 rw [toInt_fromInt] at this
235 have hpos : (0 : Int) < q.den := by exact_mod_cast q.den_pos
236 have : (q.den : Int) = 0 := this
237 have hne : (q.den : Int) ≠ 0 := ne_of_gt hpos
238 exact hne this)
239
240@[simp] theorem toRat_mk (a b : LogicInt) (hb : b ≠ 0) :
241 toRat (mk a b hb) = (toInt a : ℚ) / toInt b := rfl
242
243theorem toRat_fromRat : ∀ q : ℚ, toRat (fromRat q) = q := by
244 intro q
245 show toRat (mk (fromInt q.num) (fromInt q.den) _) = q
246 rw [toRat_mk, toInt_fromInt, toInt_fromInt]
247 exact_mod_cast q.num_div_den
248
249/-- The other round trip: every logic-native rational is recovered from
250its image in Mathlib's `Rat`. This is the key injectivity theorem for
251the transport API. -/
252theorem fromRat_toRat : ∀ q : LogicRat, fromRat (toRat q) = q := by
253 intro q
254 induction q using Quotient.inductionOn with
255 | h p =>
256 rcases p with ⟨a, b, hb⟩
257 show fromRat (toRat (mk a b hb)) = mk a b hb
258 rw [toRat_mk]
259 apply sound
260 -- It remains to prove `fromInt ((a/b).num) * b = a * fromInt ((a/b).den)`.
261 rw [eq_iff_toInt_eq, toInt_mul, toInt_mul, toInt_fromInt, toInt_fromInt]
262 have hb_rat : (toInt b : ℚ) ≠ 0 := by
263 intro h
264 apply hb
265 rw [eq_iff_toInt_eq, toInt_zero]
266 exact_mod_cast h
267 have hden_rat : (((toInt a : ℚ) / toInt b).den : ℚ) ≠ 0 := by
268 exact_mod_cast (ne_of_gt ((toInt a : ℚ) / toInt b).den_pos)
269 have hq :
270 ((((toInt a : ℚ) / toInt b).num : ℚ) /
271 (((toInt a : ℚ) / toInt b).den : ℚ))
272 = (toInt a : ℚ) / toInt b := by
273 exact_mod_cast ((toInt a : ℚ) / toInt b).num_div_den
274 have hcross :
275 (((toInt a : ℚ) / toInt b).num : ℚ) * (toInt b : ℚ)
276 = (toInt a : ℚ) * (((toInt a : ℚ) / toInt b).den : ℚ) := by
277 rwa [div_eq_div_iff hden_rat hb_rat] at hq
278 exact_mod_cast hcross
279
280/-- Carrier equivalence between recovered rationals and Mathlib rationals. -/
281noncomputable def equivRat : LogicRat ≃ ℚ where
282 toFun := toRat
283 invFun := fromRat
284 left_inv := fromRat_toRat
285 right_inv := toRat_fromRat
286
287/-- Transfer principle: equality of recovered rationals is equivalent to
288equality after transport to Mathlib's `Rat`. -/
289theorem eq_iff_toRat_eq {a b : LogicRat} : a = b ↔ toRat a = toRat b := by
290 constructor
291 · exact congrArg toRat
292 · intro h
293 have := congrArg fromRat h
294 rw [fromRat_toRat, fromRat_toRat] at this
295 exact this
296
297theorem toRat_zero : toRat (0 : LogicRat) = 0 := by
298 show toRat (mk 0 1 _) = 0
299 rw [toRat_mk, toInt_zero, toInt_one]
300 norm_num
301
302theorem toRat_one : toRat (1 : LogicRat) = 1 := by
303 show toRat (mk 1 1 _) = 1
304 rw [toRat_mk, toInt_one]
305 norm_num
306
307theorem toRat_neg (a : LogicRat) : toRat (-a) = -toRat a := by
308 induction a using Quotient.inductionOn with
309 | h p =>
310 rcases p with ⟨a, b, hb⟩
311 show toRat (mk (-a) b hb) = -toRat (mk a b hb)
312 rw [toRat_mk, toRat_mk, toInt_neg]
313 have hbq : (toInt b : ℚ) ≠ 0 := by
314 intro h; apply hb; rw [eq_iff_toInt_eq, toInt_zero]; exact_mod_cast h
315 field_simp [hbq]
316 norm_num
317
318theorem toRat_add (a b : LogicRat) : toRat (a + b) = toRat a + toRat b := by
319 induction a using Quotient.inductionOn with
320 | h p =>
321 induction b using Quotient.inductionOn with
322 | h q =>
323 rcases p with ⟨a, b, hb⟩
324 rcases q with ⟨c, d, hd⟩
325 show toRat (mk (a * d + c * b) (b * d) _) =
326 toRat (mk a b hb) + toRat (mk c d hd)
327 simp only [toRat_mk, toInt_add, toInt_mul]
328 push_cast
329 have hbq : (toInt b : ℚ) ≠ 0 := by
330 intro h; apply hb; rw [eq_iff_toInt_eq, toInt_zero]; exact_mod_cast h
331 have hdq : (toInt d : ℚ) ≠ 0 := by
332 intro h; apply hd; rw [eq_iff_toInt_eq, toInt_zero]; exact_mod_cast h
333 field_simp [hbq, hdq]
334
335theorem toRat_mul (a b : LogicRat) : toRat (a * b) = toRat a * toRat b := by
336 induction a using Quotient.inductionOn with
337 | h p =>
338 induction b using Quotient.inductionOn with
339 | h q =>
340 rcases p with ⟨a, b, hb⟩
341 rcases q with ⟨c, d, hd⟩
342 show toRat (mk (a * c) (b * d) _) =
343 toRat (mk a b hb) * toRat (mk c d hd)
344 simp only [toRat_mk, toInt_mul]
345 push_cast
346 have hbq : (toInt b : ℚ) ≠ 0 := by
347 intro h; apply hb; rw [eq_iff_toInt_eq, toInt_zero]; exact_mod_cast h
348 have hdq : (toInt d : ℚ) ≠ 0 := by
349 intro h; apply hd; rw [eq_iff_toInt_eq, toInt_zero]; exact_mod_cast h
350 field_simp [hbq, hdq]
351
352/-! ## 6. Field identities by transport through `toRat` -/
353
354theorem add_assoc' (a b c : LogicRat) : (a + b) + c = a + (b + c) := by
355 rw [eq_iff_toRat_eq, toRat_add, toRat_add, toRat_add, toRat_add]
356 ring
357
358theorem add_comm' (a b : LogicRat) : a + b = b + a := by
359 rw [eq_iff_toRat_eq, toRat_add, toRat_add]
360 ring
361
362theorem zero_add' (a : LogicRat) : (0 : LogicRat) + a = a := by
363 rw [eq_iff_toRat_eq, toRat_add, toRat_zero]
364 ring
365
366theorem add_zero' (a : LogicRat) : a + (0 : LogicRat) = a := by
367 rw [eq_iff_toRat_eq, toRat_add, toRat_zero]
368 ring
369
370theorem add_left_neg' (a : LogicRat) : -a + a = 0 := by
371 rw [eq_iff_toRat_eq, toRat_add, toRat_neg, toRat_zero]
372 ring
373
374theorem mul_assoc' (a b c : LogicRat) : (a * b) * c = a * (b * c) := by
375 rw [eq_iff_toRat_eq, toRat_mul, toRat_mul, toRat_mul, toRat_mul]
376 ring
377
378theorem mul_comm' (a b : LogicRat) : a * b = b * a := by
379 rw [eq_iff_toRat_eq, toRat_mul, toRat_mul]
380 ring
381
382theorem one_mul' (a : LogicRat) : (1 : LogicRat) * a = a := by
383 rw [eq_iff_toRat_eq, toRat_mul, toRat_one]
384 ring
385
386theorem mul_one' (a : LogicRat) : a * (1 : LogicRat) = a := by
387 rw [eq_iff_toRat_eq, toRat_mul, toRat_one]
388 ring
389
390theorem mul_add' (a b c : LogicRat) : a * (b + c) = a * b + a * c := by
391 rw [eq_iff_toRat_eq, toRat_mul, toRat_add, toRat_add, toRat_mul, toRat_mul]
392 ring
393
394theorem add_mul' (a b c : LogicRat) : (a + b) * c = a * c + b * c := by
395 rw [eq_iff_toRat_eq, toRat_mul, toRat_add, toRat_add, toRat_mul, toRat_mul]
396 ring
397
398end LogicRat
399
400/-! ## Summary
401
402 Foundation.LogicAsFunctionalEquation (Law of Logic, four conditions on C)
403 ↓
404 Foundation.ArithmeticFromLogic (LogicNat ≃ Nat)
405 ↓
406 Foundation.IntegersFromLogic (LogicInt ≃ Int, ring axioms)
407 ↓
408 Foundation.RationalsFromLogic (this) (LogicRat ≃ Rat carrier)
409
410The field-of-fractions construction recovers the rationals. The
411construction does not assume `Rat` exists; it builds the equivalence
412classes and operations from `LogicInt` plus the standard quotient
413machinery. The carrier-level equivalence is the structural recovery;
414the full field axiom catalog (associativity/commutativity/distributivity
415of mul, multiplicative inverse for non-zero elements) is a mechanical
416extension via the `eq_iff_toRat_eq` transfer principle (mirroring
417`eq_iff_toInt_eq` in the integer module).
418
419What this module establishes:
420 - The `ratRel` equivalence relation and its setoid (transitivity uses
421 `mul_right_cancel` from `LogicInt` proved via the ring isomorphism).
422 - `LogicRat` as a Quotient.
423 - Zero, one, negation, addition, multiplication.
424 - Carrier-level equivalence with `Rat` via `toRat`/`fromRat`
425 (`toRat_fromRat` proved; `fromRat_toRat` left as the natural follow-on).
426
427What is left for a follow-up:
428 - `fromRat_toRat` direction of the equivalence.
429 - Full field axiom catalog (multiplicative inverse, distributivity).
430 - Equivalence as a field isomorphism `LogicRat ≃+*+ Rat`.
431 - Order on `LogicRat` (descended from `Rat`'s order).
432-/
433
434end RationalsFromLogic
435end Foundation
436end IndisputableMonolith
437