Lumenary.AreaAngles

Formal library

• ShapedefDefinitionNo axioms

  /-- A shape on squared paper: a list of unit squares, each named by `(column, row)`.
  We always list each square once. -/
  abbrev Shape := List (Int × Int)

  Axioms used: No axiomsformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• areadefDefinitionNo axioms

  /-- The **area** of a shape is the number of unit squares that cover it. -/
  def area (s : Shape) : Nat := s.length

  Axioms used: No axiomsformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• columndefDefinitionNo axioms

  /-- One column of squares: the `h` squares `(x, 0), (x, 1), …, (x, h - 1)`. -/
  def column (x : Int) (h : Nat) : Shape :=
    (List.range h).map (fun y : Nat => (x, (y : Int)))

  Axioms used: No axiomsformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• rectdefDefinitionNo axioms

  /-- A rectangle `w` squares wide and `h` squares high, built one column at a time. -/
  def rect : Nat → Nat → Shape
    | 0, _ => []
    | w + 1, h => column w h ++ rect w h

  Axioms used: No axiomsformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• area_recttheoremProved here from basic factspropext, Quot.sound

  /-- **The area of a rectangle is width × height.** Each column holds `h` squares, and there
  are `w` columns, so there are `h + h + ⋯ + h = w × h` squares. The proof adds one column at a
  time (induction on the width). -/
  theorem area_rect (w h : Nat) : area (rect w h) = w * h := by
    induction w with
    | zero => simp [rect, area]
    | succ w ih =>
      simp only [area] at ih ⊢
      simp only [rect, List.length_append, column, List.length_map, List.length_range, ih]
      rw [Nat.succ_mul]
      omega

  Axioms used: propext, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• outsidedefDefinitionpropext, Classical.choice, Quot.sound

  /-- `1` if the square `q` is **not** part of the shape `s`, and `0` if it is. -/
  def outside (s : Shape) (q : Int × Int) : Nat :=
    if q ∈ s then 0 else 1

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• perimeterdefDefinitionpropext, Classical.choice, Quot.sound

  /-- The **perimeter** of a shape, in units: for every square, count those of its four sides
  (right, left, top, bottom) whose neighbouring square is outside the shape. -/
  def perimeter (s : Shape) : Nat :=
    (s.map fun p =>
      outside s (p.1 + 1, p.2) + outside s (p.1 - 1, p.2) +
      outside s (p.1, p.2 + 1) + outside s (p.1, p.2 - 1)).sum

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• same_area_different_perimetertheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **Same area, different perimeters.** Rectangles `3 × 4`, `2 × 6` and `1 × 12` all have
  area 12, but their perimeters are 14, 16 and 26. Lean counts the squares and the sides. -/
  theorem same_area_different_perimeter :
      area (rect 3 4) = 12 ∧ area (rect 2 6) = 12 ∧ area (rect 1 12) = 12 ∧
      perimeter (rect 3 4) = 14 ∧ perimeter (rect 2 6) = 16 ∧ perimeter (rect 1 12) = 26 := by
    decide

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• same_perimeter_different_areatheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **Same perimeter, different areas.** Rectangles `3 × 3`, `2 × 4` and `1 × 5` all have
  perimeter 12, but their areas are 9, 8 and 5. -/
  theorem same_perimeter_different_area :
      perimeter (rect 3 3) = 12 ∧ perimeter (rect 2 4) = 12 ∧ perimeter (rect 1 5) = 12 ∧
      area (rect 3 3) = 9 ∧ area (rect 2 4) = 8 ∧ area (rect 1 5) = 5 := by
    decide

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• perimeter_rect_smalltheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- Walking round a rectangle gives `w + h + w + h = 2 × (w + h)`. Here Lean checks that
  counting the outside sides square by square agrees with this rule for **every** rectangle up to
  `6 × 6` — 36 rectangles, checked one by one. -/
  theorem perimeter_rect_small :
      ∀ w < 6, ∀ h < 6, perimeter (rect (w + 1) (h + 1)) = 2 * ((w + 1) + (h + 1)) := by
    decide

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• lShapedefDefinitionNo axioms

  /-- An L-shape made of 5 squares: a column of 4 with one extra square at the bottom right. -/
  def lShape : Shape := [(0, 0), (0, 1), (0, 2), (0, 3), (1, 0)]

  Axioms used: No axiomsformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• l_shape_measurestheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- The L-shape has area 5 and perimeter 12 — the same perimeter as the `3 × 3` square, whose
  area is 9. -/
  theorem l_shape_measures : area lShape = 5 ∧ perimeter lShape = 12 := by
    decide

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• layerdefDefinitionNo axioms

  /-- One layer of a box: an `l × w` rectangle of unit cubes at height `z`. -/
  def layer (l w : Nat) (z : Int) : List (Int × Int × Int) :=
    (rect l w).map (fun p => (p.1, p.2, z))

  Axioms used: No axiomsformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• boxdefDefinitionNo axioms

  /-- A box `l` cubes long, `w` cubes wide and `h` cubes high, built one layer at a time. -/
  def box (l w : Nat) : Nat → List (Int × Int × Int)
    | 0 => []
    | h + 1 => layer l w h ++ box l w h

  Axioms used: No axiomsformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• volume_boxtheoremProved here from basic factspropext, Quot.sound

  /-- **The volume of a box is length × width × height.** Each layer is a rectangle of `l × w`
  cubes (by `area_rect`), and there are `h` layers. -/
  theorem volume_box (l w h : Nat) : (box l w h).length = l * w * h := by
    induction h with
    | zero => rfl
    | succ h ih =>
      have hl : (layer l w h).length = l * w := by
        simp only [layer, List.length_map]
        exact area_rect l w
      simp only [box, List.length_append, hl, ih]
      rw [Nat.mul_succ]
      omega

  Axioms used: propext, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• vertically_oppositetheoremProved here from basic factspropext, Quot.sound

  /-- **Vertically opposite angles are equal.** Where two straight lines cross, angles `a` and `b`
  sit side by side on one line, and `b` and `c` on the other; each pair makes a straight angle of
  180°. So `a = 180° − b = c`. -/
  theorem vertically_opposite (a b c : Nat) (h₁ : a + b = 180) (h₂ : b + c = 180) : a = c := by
    omega

  Axioms used: propext, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• triangle_angle_sumtheoremProved here from basic factspropext, Quot.sound

  /-- **The angles of a triangle add up to 180°.** Draw the line through the top corner parallel to
  the base. At the top corner, three angles `d`, `c`, `e` lie along this line, so
  `d + c + e = 180`. The angles `d` and `e` are alternate angles to the base angles `a` and `b`,
  so `d = a` and `e = b`. The geometry is in the hypotheses; Lean checks the conclusion. -/
  theorem triangle_angle_sum (a b c d e : Nat)
      (straight : d + c + e = 180) (alt₁ : d = a) (alt₂ : e = b) : a + b + c = 180 :=
    calc a + b + c = d + e + c := by rw [alt₁, alt₂]
      _ = d + c + e := by omega
      _ = 180 := straight

  Axioms used: propext, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• no_two_right_anglestheoremProved here from basic factspropext, Quot.sound

  /-- A triangle cannot have two right angles: the third angle would have to be 0°. -/
  theorem no_two_right_angles (a b c : Nat) (sum : a + b + c = 180) (hc : 0 < c) :
      ¬ (a = 90 ∧ b = 90) := by
    omega

  Axioms used: propext, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• at_most_one_obtusetheoremProved here from basic factspropext, Quot.sound

  /-- A triangle has at most one obtuse angle (more than 90°): two of them would already add up
  to more than 180°. -/
  theorem at_most_one_obtuse (a b c : Nat) (sum : a + b + c = 180) : ¬ (90 < a ∧ 90 < b) := by
    omega

  Axioms used: propext, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• equilateral_anglestheoremProved here from basic factspropext, Quot.sound

  /-- In a triangle whose three angles are equal, each angle is 60°. -/
  theorem equilateral_angles (a b c : Nat) (sum : a + b + c = 180) (hab : a = b) (hbc : b = c) :
      a = 60 := by
    omega

  Axioms used: propext, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• quadrilateral_angle_sumtheoremProved here from basic factspropext, Quot.sound

  /-- **The angles of a quadrilateral add up to 360°.** A diagonal cuts it into two triangles with
  angles `a₁, b₁, c₁` and `a₂, b₂, c₂`. Two corners of the quadrilateral are split by the
  diagonal (`q = b₁ + b₂`, `s = c₁ + c₂`); the other two are whole triangle angles. -/
  theorem quadrilateral_angle_sum (a₁ b₁ c₁ a₂ b₂ c₂ p q r s : Nat)
      (t₁ : a₁ + b₁ + c₁ = 180) (t₂ : a₂ + b₂ + c₂ = 180)
      (hp : p = a₁) (hq : q = b₁ + b₂) (hr : r = a₂) (hs : s = c₁ + c₂) :
      p + q + r + s = 360 := by
    omega

  Axioms used: propext, Quot.soundformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• TriangleKindstructureDefinitionNo axioms

  /-- Triangles sorted by their largest angle. -/
  inductive TriangleKind where
    | acute
    | right
    | obtuse
    deriving DecidableEq, Repr

  Axioms used: No axiomsformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• classifydefDefinitionNo axioms

  /-- Sort a triangle with angles `a`, `b`, `c` (in degrees): obtuse if some angle is more than
  90°, right if some angle is exactly 90°, acute otherwise. -/
  def classify (a b c : Nat) : TriangleKind :=
    if 90 < a ∨ 90 < b ∨ 90 < c then .obtuse
    else if a = 90 ∨ b = 90 ∨ c = 90 then .right
    else .acute

  Axioms used: No axiomsformal/Lumenary/AreaAngles.leanTry it in the Lean web editor

• classify_examplestheoremProved here from basic factsNo axioms

  /-- The triangles in the lesson: 60°, 60°, 60° is acute; 90°, 30°, 60° is right;
  25°, 35°, 120° is obtuse. -/
  theorem classify_examples :
      classify 60 60 60 = .acute ∧ classify 90 30 60 = .right ∧ classify 25 35 120 = .obtuse := by
    decide

  Axioms used: No axiomsformal/Lumenary/AreaAngles.leanTry it in the Lean web editor