/-- A fraction `num / den` of whole numbers. The denominator must not be `0`: it says howmany equal parts the whole is cut into. -/structure Frac where /-- The numerator: how many parts we take. -/ num : Nat /-- The denominator: how many equal parts make one whole. -/ den : Nat /-- A whole cannot be cut into `0` parts. -/ den_pos : 0 < den
/-- `frac a b` is the fraction `a / b`. When `b` is a numeral, Lean checks `0 < b` by itself. -/def frac (a b : Nat) (h : 0 < b := by decide) : Frac := ⟨a, b, h⟩
/-- `a / b` and `c / d` are **equivalent** (they are the same number) when `a × d = c × b`:written over the common denominator `b × d`, they have the same numerator. -/def Frac.Equiv (x y : Frac) : Prop := x.num * y.den = y.num * x.den
/-- Equivalence of two particular fractions can be decided by multiplying, so `decide` cancheck statements such as `frac 2 4 ≈ frac 1 2`. -/instance instDecidableEquiv (x y : Frac) : Decidable (x ≈ y) := inferInstanceAs (Decidable (x.num * y.den = y.num * x.den))
scale_equivtheoremProved here from basic factspropext
scale_equivLean 4Proved here from basic factsFormally verified
/-- Multiplying the numerator and the denominator by the same `n > 0` gives an equivalentfraction: `(n × a) / (n × b) = a / b`. Cutting every part into `n` smaller parts makes `n`times as many parts, each `n` times smaller. -/theorem scale_equiv (a b n : Nat) (hb : 0 < b) (hn : 0 < n) : frac (n * a) (n * b) (Nat.mul_pos hn hb) ≈ frac a b hb := by -- Unfolded, the claim is `(n × a) × b = a × (n × b)`: reorder the product. change n * a * b = a * (n * b) rw [Nat.mul_comm n a, Nat.mul_assoc]
equiv_transtheoremProved here from basic factspropext, Quot.sound
equiv_transLean 4Proved here from basic factsFormally verified
/-- If `a/b ≈ c/d` and `c/d ≈ e/f`, then `a/b ≈ e/f`. We multiply out, use both facts, andcancel the factor `d`, which is allowed because `d > 0` (`Nat.eq_of_mul_eq_mul_right`).`ac_rfl` reorders a product; multiplication is commutative and associative. -/theorem equiv_trans {x y z : Frac} (h1 : x ≈ y) (h2 : y ≈ z) : x ≈ z := by obtain ⟨a, b, _⟩ := x obtain ⟨c, d, hd⟩ := y obtain ⟨e, f, _⟩ := z change a * d = c * b at h1 change c * f = e * d at h2 change a * f = e * b apply Nat.eq_of_mul_eq_mul_right hd calc a * f * d = (a * d) * f := by ac_rfl _ = (c * b) * f := by rw [h1] _ = (c * f) * b := by ac_rfl _ = (e * d) * b := by rw [h2] _ = e * b * d := by ac_rfl
/-- `a / b < c / d` when `a × d < c × b`: over the common denominator `b × d`, the firstnumerator is smaller. -/def Frac.Lt (x y : Frac) : Prop := x.num * y.den < y.num * x.den
/-- Comparing two particular fractions is a calculation, so `decide` can do it. -/instance instDecidableLt (x y : Frac) : Decidable (x < y) := inferInstanceAs (Decidable (x.num * y.den < y.num * x.den))
same_den_lttheoremProved here from basic factspropext, Classical.choice, Quot.sound
same_den_ltLean 4Proved here from basic factsFormally verified
/-- With the same denominator, the fraction with the bigger numerator is bigger:`a / b < c / b` exactly when `a < c` (same-sized pieces, so compare how many). -/theorem same_den_lt (a c b : Nat) (hb : 0 < b) : frac a b hb < frac c b hb ↔ a < c := by change a * b < c * b ↔ a < c exact Nat.mul_lt_mul_right hb
bigger_den_smaller_piecetheoremProved here from basic factsNo axioms
bigger_den_smaller_pieceLean 4Proved here from basic factsFormally verified
/-- A bigger denominator means a *smaller* piece: if `b < d` then `1/d < 1/b`.Cutting the whole into more parts makes each part smaller. -/theorem bigger_den_smaller_piece (b d : Nat) (hb : 0 < b) (hd : 0 < d) (h : b < d) : frac 1 d hd < frac 1 b hb := by change 1 * b < 1 * d rw [Nat.one_mul, Nat.one_mul] exact h
three_quarters_gt_two_thirdstheoremProved here from basic factsNo axioms
three_quarters_gt_two_thirdsLean 4Proved here from basic factsFormally verified
/-- `2/3 < 3/4`, because over the common denominator `12` they are `8/12` and `9/12`. -/theorem three_quarters_gt_two_thirds : frac 2 3 < frac 3 4 := by decide
half_plus_third_not_two_fifthstheoremProved here from basic factsNo axioms
half_plus_third_not_two_fifthsLean 4Proved here from basic factsFormally verified
/-- Adding tops and bottoms is wrong: `1/2 + 1/3` is **not** `2/5`. In fact `2/5` is smallerthan `1/2`, and a sum of two positive fractions must be bigger than each of them. -/theorem half_plus_third_not_two_fifths : ¬ ((frac 1 2).add (frac 1 3) ≈ frac 2 5) ∧ frac 2 5 < frac 1 2 := by decide
add_respects_equivtheoremProved here from basic factspropext, Quot.sound
add_respects_equivLean 4Proved here from basic factsFormally verified
/-- The answer to an addition does not depend on which equivalent fractions we use:if `x ≈ x'` and `y ≈ y'` then `x + y ≈ x' + y'`. So adding `2/4 + 1/3` gives the same numberas `1/2 + 1/3`. The proof multiplies out and uses the two cross-multiplication facts. -/theorem add_respects_equiv {x x' y y' : Frac} (hx : x ≈ x') (hy : y ≈ y') : x.add y ≈ x'.add y' := by obtain ⟨a, b, _⟩ := x obtain ⟨a', b', _⟩ := x' obtain ⟨c, d, _⟩ := y obtain ⟨c', d', _⟩ := y' change a * b' = a' * b at hx change c * d' = c' * d at hy change (a * d + c * b) * (b' * d') = (a' * d' + c' * b') * (b * d) calc (a * d + c * b) * (b' * d') = (a * b') * (d * d') + (c * d') * (b * b') := by rw [Nat.add_mul]; ac_rfl _ = (a' * b) * (d * d') + (c' * d) * (b * b') := by rw [hx, hy] _ = (a' * d' + c' * b') * (b * d) := by rw [Nat.add_mul]; ac_rfl
/-- A whole number times a fraction: `n × (a / b) = (n × a) / b`, that is, `n` groups of`a` pieces of size `1/b`. -/def Frac.natMul (n : Nat) (x : Frac) : Frac := ⟨n * x.num, x.den, x.den_pos⟩
four_times_two_thirdstheoremProved here from basic factsNo axioms
four_times_two_thirdsLean 4Proved here from basic factsFormally verified
/-- `4 × 2/3 = 8/3`, which is `2 2/3`: eight thirds, or two wholes and two thirds. -/theorem four_times_two_thirds : (frac 2 3).natMul 4 ≈ frac 8 3 := by decide
ten_pow_mod_threetheoremProved here from basic factspropext
ten_pow_mod_threeLean 4Proved here from basic factsFormally verified
/-- Every power of ten leaves remainder `1` when divided by `3`: `10 = 9 + 1`,`100 = 99 + 1`, `1000 = 999 + 1`, … Proved by induction, using that the remainder of aproduct depends only on the remainders of the factors (`Nat.mul_mod`). -/theorem ten_pow_mod_three (k : Nat) : 10 ^ k % 3 = 1 := by induction k with | zero => rfl | succ n ih => rw [Nat.pow_succ, Nat.mul_mod, ih]
third_not_terminatingtheoremProved here from basic factspropext
third_not_terminatingLean 4Proved here from basic factsFormally verified
/-- `1/3` has no finite decimal: there are no `m` and `k` with `1/3 = m / 10^k`.By cross-multiplication that would mean `10^k = 3 × m`, a multiple of `3`, but every powerof ten leaves remainder `1` when divided by `3`. -/theorem third_not_terminating (m k : Nat) : ¬ (frac 1 3 ≈ frac m (10 ^ k) (Nat.pow_pos (by decide))) := by intro h change 1 * 10 ^ k = m * 3 at h have hrem : 10 ^ k % 3 = m * 3 % 3 := by rw [← h, Nat.one_mul] rw [ten_pow_mod_three, Nat.mul_mod_left] at hrem -- `hrem : 1 = 0`, which is false. exact absurd hrem (by decide)
rat_cross_multheoremApplies a library theorempropext, Classical.choice, Quot.sound
rat_cross_mulLean 4Applies a library theoremFormally verified
/-- In Lean's own type of fractions `Rat`, `a/b = c/d` exactly when `a × d = c × b`(for nonzero `b`, `d`). This applies core Lean's theorem `Rat.divInt_eq_divInt_iff`. -/theorem rat_cross_mul {a b c d : Int} (hb : b ≠ 0) (hd : d ≠ 0) : (a : Rat) / b = c / d ↔ a * d = c * b := by rw [← Rat.divInt_eq_div, ← Rat.divInt_eq_div] exact Rat.divInt_eq_divInt_iff hb hd
/-- Show that a bigger denominator gives a smaller unit fraction: if `b < d` then `1/d < 1/b`.Hint: `change 1 * b < 1 * d` unfolds the comparison; then `Nat.one_mul` simplifies. -/theorem bigger_den_smaller_piece (b d : Nat) (hb : 0 < b) (hd : 0 < d) (h : b < d) : frac 1 d hd < frac 1 b hb := by sorry
Show the compiled solution
bigger_den_smaller_pieceLean 4Proved here from basic factsFormally verified
/-- A bigger denominator means a *smaller* piece: if `b < d` then `1/d < 1/b`.Cutting the whole into more parts makes each part smaller. -/theorem bigger_den_smaller_piece (b d : Nat) (hb : 0 < b) (hd : 0 < d) (h : b < d) : frac 1 d hd < frac 1 b hb := by change 1 * b < 1 * d rw [Nat.one_mul, Nat.one_mul] exact h
/-- Show that every power of ten leaves remainder `1` when divided by `3`.Hint: induction on `k`; in the step use `Nat.pow_succ` and `Nat.mul_mod`. -/theorem ten_pow_mod_three (k : Nat) : 10 ^ k % 3 = 1 := by sorry
Show the compiled solution
ten_pow_mod_threeLean 4Proved here from basic factsFormally verified
/-- Every power of ten leaves remainder `1` when divided by `3`: `10 = 9 + 1`,`100 = 99 + 1`, `1000 = 999 + 1`, … Proved by induction, using that the remainder of aproduct depends only on the remainders of the factors (`Nat.mul_mod`). -/theorem ten_pow_mod_three (k : Nat) : 10 ^ k % 3 = 1 := by induction k with | zero => rfl | succ n ih => rw [Nat.pow_succ, Nat.mul_mod, ih]