Formal mathematics laboratory
Lumenary.Measurement
Measuring length and time
Formal library
longer_transtheoremApplies a library theoremNo axioms
longer_transLean 4Applies a library theoremFormally verified /-- If A is longer than B, and B is longer than C, then A is longer than C. (Lengths `a, b, c` in whole units; "A is longer than B" is `b < a`.) This applies core Lean's `Nat.lt_trans`. -/ theorem longer_trans {a b c : Nat} (hab : b < a) (hbc : c < b) : c < a := Nat.lt_trans hbc habcompare_with_stringtheoremProved here from basic factsNo axioms
compare_with_stringLean 4Proved here from basic factsFormally verified /-- Comparing two things that cannot be put side by side, using a string as a go-between. Cut a string exactly as long as the table (`string = table`). If the door is wider than the string (`string < door`), the door is wider than the table. -/ theorem compare_with_string {door table string : Nat} (h₁ : string = table) (h₂ : string < door) : table < door := by rw [← h₁] exact h₂smaller_unit_bigger_numbertheoremProved here from basic factsNo axioms
smaller_unit_bigger_numberLean 4Proved here from basic factsFormally verified /-- Measuring with a smaller unit gives a bigger number. If something is `k` big units long (`k ≥ 1`) and one big unit is `m` small units (`m ≥ 2`), then it is `k * m` small units long, and `k < k * m`: `k = k · 1 < k · m`. -/ theorem smaller_unit_bigger_number (k m : Nat) (hk : 0 < k) (hm : 1 < m) : k < k * m := calc k = k * 1 := (Nat.mul_one k).symm _ < k * m := Nat.mul_lt_mul_of_pos_left hm hkreachdefDefinitionNo axioms
reachLean 4Formally verified /-- Lay copies of one unit end to end, with a gap after each copy (a gap of `0` means no gap). Each entry of `gaps` is one copy of the unit followed by its gap; the result is how far the row of units reaches. -/ def reach (unit : Nat) : List Nat → Nat | [] => 0 | gap :: gaps => unit + gap + reach unit gapsreach_no_gapstheoremProved here from basic factspropext
reach_no_gapsLean 4Proved here from basic factsFormally verified /-- With no gaps, `n` copies of a unit reach exactly `n` units: measuring is counting units laid end to end. Proof by induction on the number of copies. -/ theorem reach_no_gaps (unit n : Nat) : reach unit (List.replicate n 0) = n * unit := by induction n with | zero => simp [reach] | succ n ih => simp only [List.replicate, reach, ih, Nat.add_zero, Nat.succ_mul, Nat.add_comm]gaps_reach_furthertheoremProved here from basic factspropext, Quot.sound
gaps_reach_furtherLean 4Proved here from basic factsFormally verified /-- Gaps make a row of units reach further than the number of units says: `n` copies with gaps reach at least `n` units. So if the row ends exactly at the end of an object, counting the copies gives a number that is too small (or exactly right, if there were no gaps). -/ theorem gaps_reach_further (unit : Nat) (gaps : List Nat) : gaps.length * unit ≤ reach unit gaps := by induction gaps with | nil => simp [reach] | cons g gs ih => simp only [List.length_cons, Nat.succ_mul, reach] omegarulerLengthdefDefinitionNo axioms
rulerLengthLean 4Formally verified /-- An object lying along a ruler from the mark `start` to the mark `finish` is `finish - start` units long. -/ def rulerLength (start finish : Nat) : Nat := finish - startpencil_from_threetheoremProved here from basic factsNo axioms
pencil_from_threeLean 4Proved here from basic factsFormally verified /-- A pencil from the 3 mark to the 18 mark is 15 units long, not 18. -/ theorem pencil_from_three : rulerLength 3 18 = 15 := rflread_end_iff_start_zerotheoremProved here from basic factspropext, Classical.choice, Quot.sound
read_end_iff_start_zeroLean 4Proved here from basic factsFormally verified /-- Reading the number at the end of the object gives its length **exactly when** the object starts at 0 (for an object of positive length). This is why we line things up with 0. -/ theorem read_end_iff_start_zero (start finish : Nat) (h : start < finish) : rulerLength start finish = finish ↔ start = 0 := by unfold rulerLength omegaAxioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Measurement.leanTry it in the Lean web editormarksdefDefinitionNo axioms
marksLean 4Formally verified /-- The marks on a ruler from `start` to `finish`, including both ends. -/ def marks (start finish : Nat) : List Nat := List.range' start (finish - start + 1)marks_lengththeoremApplies a library theoremNo axioms
marks_lengthLean 4Applies a library theoremFormally verified /-- There is always one more mark than spaces: from `start` to `finish` there are `(finish - start) + 1` marks but only `finish - start` units. Counting marks instead of the spaces between them gives an answer one too big. This applies core Lean's `List.length_range'`. -/ theorem marks_length (start finish : Nat) : (marks start finish).length = rulerLength start finish + 1 := List.length_range'DirstructureDefinitionNo axioms
DirLean 4Formally verified /-- The four directions a piece of string can point on squared paper. -/ inductive Dir where | right | up | left | down deriving DecidableEq, ReprPiecestructureDefinitionNo axioms
PieceLean 4Formally verified /-- A straight piece of a string: which way it points and how long it is. A string is a list of pieces joined end to end. -/ structure Piece where dir : Dir len : Nat deriving DecidableEq, ReprstringLengthdefDefinitionNo axioms
stringLengthLean 4Formally verified /-- The length of a string: add up the lengths of its pieces. -/ def stringLength : List Piece → Nat | [] => 0 | p :: ps => p.len + stringLength psbenddefDefinitionNo axioms
bendLean 4Formally verified /-- Bend a string: point each piece in a new direction `newDir p`, keeping its length. -/ def bend (newDir : Piece → Dir) (s : List Piece) : List Piece := s.map fun p => ⟨newDir p, p.len⟩bend_keeps_lengththeoremProved here from basic factsNo axioms
bend_keeps_lengthLean 4Proved here from basic factsFormally verified /-- **A bent string is exactly as long as before.** However the pieces are pointed, the lengths being added up are the same. Proof by induction on the pieces. -/ theorem bend_keeps_length (newDir : Piece → Dir) (s : List Piece) : stringLength (bend newDir s) = stringLength s := by induction s with | nil => rfl | cons p ps ih => simp only [bend, List.map, stringLength] at ih ⊢; rw [ih]endPointdefDefinitionNo axioms
endPointLean 4Formally verified /-- Where the far end of a string lands if its near end is at `(0, 0)` on squared paper. -/ def endPoint : List Piece → Int × Int | [] => (0, 0) | ⟨d, n⟩ :: ps => let (x, y) := endPoint ps match d with | .right => (x + n, y) | .up => (x, y + n) | .left => (x - n, y) | .down => (x, y - n)bent_string_exampletheoremProved here from basic factsNo axioms
bent_string_exampleLean 4Proved here from basic factsFormally verified /-- A string 6 units long, first straight and then bent into an L: the length is the same, but the far end lands somewhere else — closer to the start. Bending changes where the ends are, not how long the string is. -/ theorem bent_string_example : stringLength [⟨.right, 6⟩] = stringLength [⟨.right, 3⟩, ⟨.up, 3⟩] ∧ endPoint [⟨.right, 6⟩] = (6, 0) ∧ endPoint [⟨.right, 3⟩, ⟨.up, 3⟩] = (3, 3) := by decidelaterdefDefinitionNo axioms
laterLean 4Formally verified /-- Times on a 12-hour clock face, in minutes after 12 o'clock (`0 ≤ t < 720`). `later t m` is the time `m` minutes after `t`; the clock wraps round after 720 minutes. -/ def later (t m : Nat) : Nat := (t + m) % 720hourShowndefDefinitionNo axioms
hourShownLean 4Formally verified /-- The hour the short hand has reached at time `t`, from 1 to 12. -/ def hourShown (t : Nat) : Nat := if (t / 60) % 12 = 0 then 12 else (t / 60) % 12minuteNumberdefDefinitionNo axioms
minuteNumberLean 4Formally verified /-- The number on the clock face that the long hand points at, when the minutes are a multiple of 5: at 30 minutes past the hour it points at 6. -/ def minuteNumber (t : Nat) : Nat := (t % 60) / 5half_hour_twicetheoremProved here from basic factspropext, Quot.sound
half_hour_twiceLean 4Proved here from basic factsFormally verified /-- Two half hours make an hour, at every time on the clock face — even across 12 o'clock. -/ theorem half_hour_twice (t : Nat) : later (later t 30) 30 = later t 60 := by unfold later omegahalf_past_seventheoremProved here from basic factsNo axioms
half_past_sevenLean 4Proved here from basic factsFormally verified /-- At half past seven (450 minutes after 12 o'clock) the short hand has reached 7 (it is halfway to 8) and the long hand points at 6. Half an hour later it is 8 o'clock. -/ theorem half_past_seven : hourShown 450 = 7 ∧ minuteNumber 450 = 6 ∧ later 450 30 = 8 * 60 := by decidehalf_past_eleventheoremProved here from basic factsNo axioms
half_past_elevenLean 4Proved here from basic factsFormally verified /-- Half an hour after half past eleven, the clock shows 12 o'clock, not 13 o'clock. -/ theorem half_past_eleven : hourShown (later (11 * 60 + 30) 30) = 12 := by decide