/-- A point of the coordinate plane: its `x`-coordinate (horizontal position) and its`y`-coordinate (vertical position), measured from the origin `⟨0, 0⟩`. -/structure Point where x : Rat y : Ratderiving DecidableEq
point_eq_ifftheoremProved here from basic factsNo axioms
point_eq_iffLean 4Proved here from basic factsFormally verified
/-- **One point, one ordered pair.** Two points are the same exactly when their`x`-coordinates agree **and** their `y`-coordinates agree. -/theorem point_eq_iff (P Q : Point) : P = Q ↔ P.x = Q.x ∧ P.y = Q.y := by constructor · intro h rw [h] exact ⟨rfl, rfl⟩ · intro ⟨hx, hy⟩ cases P cases Q simp only at hx hy rw [hx, hy]
order_matterstheoremProved here from basic factspropext, Quot.sound
order_mattersLean 4Proved here from basic factsFormally verified
/-- The order of the coordinates matters: `(3, 2)` and `(2, 3)` are different points. -/theorem order_matters : (⟨3, 2⟩ : Point) ≠ ⟨2, 3⟩ := by decide +kernel
/-- The quadrant of a point: 1 (`x > 0, y > 0`), 2 (`x < 0, y > 0`), 3 (`x < 0, y < 0`),4 (`x > 0, y < 0`), and `0` for points on an axis, which lie in no quadrant. -/def quadrant (P : Point) : Nat := if 0 < P.x ∧ 0 < P.y then 1 else if P.x < 0 ∧ 0 < P.y then 2 else if P.x < 0 ∧ P.y < 0 then 3 else if 0 < P.x ∧ P.y < 0 then 4 else 0
example_quadranttheoremProved here from basic factspropext, Classical.choice, Quot.sound
example_quadrantLean 4Proved here from basic factsFormally verified
/-- The point `(-1/2, 3)` lies in the second quadrant, and `(0, -2)` on an axis. -/theorem example_quadrant : quadrant ⟨-1/2, 3⟩ = 2 ∧ quadrant ⟨0, -2⟩ = 0 := by decide +kernel
reflectX_twicetheoremProved here from basic factspropext, Classical.choice, Quot.sound
reflectX_twiceLean 4Proved here from basic factsFormally verified
/-- Reflecting twice in the same axis brings every point back: `-(-b) = b`. -/theorem reflectX_twice (P : Point) : reflectX (reflectX P) = P := by rw [point_eq_iff] exact ⟨rfl, Rat.neg_neg P.y⟩
reflectY_twicetheoremProved here from basic factspropext, Classical.choice, Quot.sound
reflectY_twiceLean 4Proved here from basic factsFormally verified
/-- Reflecting twice in the `y`-axis brings every point back. -/theorem reflectY_twice (P : Point) : reflectY (reflectY P) = P := by rw [point_eq_iff] exact ⟨Rat.neg_neg P.x, rfl⟩
reflectX_reflectYtheoremProved here from basic factsNo axioms
reflectX_reflectYLean 4Proved here from basic factsFormally verified
/-- Reflecting in the `y`-axis and then in the `x`-axis sends `(a, b)` to `(-a, -b)`: a halfturn about the origin. -/theorem reflectX_reflectY (P : Point) : reflectX (reflectY P) = ⟨-P.x, -P.y⟩ := rfl
reflections_commutetheoremProved here from basic factsNo axioms
reflections_commuteLean 4Proved here from basic factsFormally verified
/-- The two reflections can be done in either order: both orders give `(-a, -b)`. -/theorem reflections_commute (P : Point) : reflectX (reflectY P) = reflectY (reflectX P) := rfl
reflectX_fixed_ifftheoremProved here from basic factspropext, Classical.choice, Quot.sound
reflectX_fixed_iffLean 4Proved here from basic factsFormally verified
/-- The points that reflection in the `x`-axis leaves where they are are exactly the points**on** the `x`-axis: `(a, -b) = (a, b)` exactly when `b = 0`. -/theorem reflectX_fixed_iff (P : Point) : reflectX P = P ↔ P.y = 0 := by rw [point_eq_iff] constructor · intro ⟨_, h⟩ -- `h` says `-b = b`, which forces `b = 0`. simp only [reflectX] at h grind · intro h exact ⟨rfl, by simp only [reflectX]; rw [h]; rfl⟩
abs_sub_commtheoremProved here from basic factspropext, Classical.choice, Quot.sound
abs_sub_commLean 4Proved here from basic factsFormally verified
/-- The distance between `a` and `c` on a number line does not depend on the order:`|a - c| = |c - a|`. -/theorem abs_sub_comm (a c : Rat) : absQ (a - c) = absQ (c - a) := by unfold absQ split <;> split <;> grind
horizontal_distance_exampletheoremProved here from basic factspropext, Classical.choice, Quot.sound
horizontal_distance_exampleLean 4Proved here from basic factsFormally verified
/-- From `(-3, 2)` to `(4, 2)` is `|-3 - 4| = 7` units — **not** `4 - 3 = 1`: the pathcrosses the `y`-axis, 3 units on one side and 4 on the other. -/theorem horizontal_distance_example : absQ (-3 - 4) = 7 := by decide +kernel
/-- The distance between two points when you may only travel along grid lines (horizontaland vertical steps, like a taxi in a city of square blocks): `|a - c| + |b - d|`. -/def gridDist (P Q : Point) : Rat := absQ (P.x - Q.x) + absQ (P.y - Q.y)
abs_add_letheoremProved here from basic factspropext, Classical.choice, Quot.sound
abs_add_leLean 4Proved here from basic factsFormally verified
/-- The triangle inequality on the number line: `|a + b| ≤ |a| + |b|`. Proof: check everycombination of signs of `a`, `b` and `a + b`. -/theorem abs_add_le (a b : Rat) : absQ (a + b) ≤ absQ a + absQ b := by unfold absQ split <;> split <;> split <;> grind
gridDist_triangletheoremProved here from basic factspropext, Classical.choice, Quot.sound
gridDist_triangleLean 4Proved here from basic factsFormally verified
/-- **A detour never helps:** going from `P` to `R` along grid lines is never longer than goingfrom `P` to `Q` and then from `Q` to `R`. Apply `abs_add_le` to the horizontal and the verticalparts separately. -/theorem gridDist_triangle (P Q R : Point) : gridDist P R ≤ gridDist P Q + gridDist Q R := by unfold gridDist have h1 := abs_add_le (P.x - Q.x) (Q.x - R.x) have h2 := abs_add_le (P.y - Q.y) (Q.y - R.y) rw [show P.x - Q.x + (Q.x - R.x) = P.x - R.x by grind] at h1 rw [show P.y - Q.y + (Q.y - R.y) = P.y - R.y by grind] at h2 grind
grid_lines_vs_stepstheoremApplies a library theoremNo axioms
grid_lines_vs_stepsLean 4Applies a library theoremFormally verified
/-- **Count the gaps, not the lines.** Walking `n` unit steps from `a` passes the `n + 1` gridlines `a, a + 1, …, a + n`: one more line than the distance. This applies core Lean's`List.length_range'`. -/theorem grid_lines_vs_steps (a n : Nat) : (List.range' a (n + 1)).length = n + 1 := List.length_range'
/-- Reflecting twice in the `y`-axis brings every point back.Hint: `rw [point_eq_iff]` turns the goal into two equations, one per coordinate. The`x`-coordinate is `-(-a) = a` (`Rat.neg_neg`); the `y`-coordinate does not change (`rfl`). -/theorem reflectY_twice (P : Point) : reflectY (reflectY P) = P := by sorry
Show the compiled solution
reflectY_twiceLean 4Proved here from basic factsFormally verified
/-- Reflecting twice in the `y`-axis brings every point back. -/theorem reflectY_twice (P : Point) : reflectY (reflectY P) = P := by rw [point_eq_iff] exact ⟨Rat.neg_neg P.x, rfl⟩
/-- The distance from `(-3, 2)` to `(4, 2)` is `|-3 - 4| = 7`.Hint: for particular numbers Lean can compute both sides: try `decide +kernel`. -/theorem horizontal_distance_example : absQ (-3 - 4) = 7 := by sorry
Show the compiled solution
horizontal_distance_exampleLean 4Proved here from basic factsFormally verified
/-- From `(-3, 2)` to `(4, 2)` is `|-3 - 4| = 7` units — **not** `4 - 3 = 1`: the pathcrosses the `y`-axis, 3 units on one side and 4 on the other. -/theorem horizontal_distance_example : absQ (-3 - 4) = 7 := by decide +kernel