Lumenary.Counting

Formal library

• goatsdefDefinitionNo axioms

  /-- Nomin's seven goats, in the order they come through the gate. -/
  def goats : List String := ["Snowy", "Patch", "Socks", "Star", "Pebble", "Moss", "Biscuit"]

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

• countAlouddefDefinitionNo axioms

  /-- Counting aloud, starting with the number word `n`: the first object is paired with `n`,
  the next object with the next number, and so on. Counting from one is `countAloud l 1`. -/
  def countAloud {α : Type} : List α → Nat → List (Nat × α)
    | [], _ => []
    | x :: xs, n => (n, x) :: countAloud xs (n + 1)

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

• goats_last_wordtheoremProved here from basic factsNo axioms

  /-- Counting Nomin's goats from one, the last pair is "seven — Biscuit". Lean works out the
  whole count itself, so `rfl` is enough. -/
  theorem goats_last_word : (countAloud goats 1).getLast? = some (7, "Biscuit") := rfl

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

• one_word_eachtheoremProved here from basic factspropext

  /-- Every object is touched exactly once, in order: if we forget the number words and keep only
  the objects, we get back exactly the collection we started with — nothing skipped, nothing
  counted twice. Proof by induction on the list. -/
  theorem one_word_each {α : Type} (l : List α) (n : Nat) :
      (countAloud l n).map Prod.snd = l := by
    induction l generalizing n with
    | nil => rfl
    | cons x xs ih => simp [countAloud, ih]

  Axioms used: propextformal/Lumenary/Counting.leanTry it in the Lean web editor

• words_saidtheoremProved here from basic factspropext

  /-- The number words said are `n, n + 1, n + 2, …`, one for each object, in order and without
  gaps or repeats. (`List.range' n k` is the list `[n, n + 1, …, n + k - 1]`.) -/
  theorem words_said {α : Type} (l : List α) (n : Nat) :
      (countAloud l n).map Prod.fst = List.range' n l.length := by
    induction l generalizing n with
    | nil => rfl
    | cons x xs ih => simp [countAloud, ih, List.range'_succ]

  Axioms used: propextformal/Lumenary/Counting.leanTry it in the Lean web editor

• last_wordtheoremProved here from basic factspropext, Quot.sound

  /-- Starting from the word `n`, the last word said for a non-empty collection is
  `n + (number of objects) - 1`. Proof by induction: a one-object collection ends on `n`; for a
  longer one, the last word is the last word of counting the rest, starting from `n + 1`. -/
  theorem last_word {α : Type} (l : List α) (n : Nat) (h : l ≠ []) :
      ((countAloud l n).map Prod.fst).getLast? = some (n + l.length - 1) := by
    induction l generalizing n with
    | nil => exact absurd rfl h
    | cons x xs ih =>
      cases xs with
      | nil => simp [countAloud]
      | cons y ys =>
        -- The rest of the collection, `y :: ys`, is counted starting from `n + 1`.
        have step := ih (n + 1) (List.cons_ne_nil y ys)
        simp only [countAloud, List.map_cons, List.getLast?_cons_cons] at step ⊢
        rw [step]
        simp only [List.length_cons]
        congr 1
        omega

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

• last_word_is_counttheoremProved here from basic factspropext, Quot.sound

  /-- **The last word tells how many.** Counting a non-empty collection from one, the last
  number word said is exactly the number of objects in it (its length). -/
  theorem last_word_is_count {α : Type} (l : List α) (h : l ≠ []) :
      ((countAloud l 1).map Prod.fst).getLast? = some l.length := by
    rw [last_word l 1 h, Nat.add_comm, Nat.add_sub_cancel]

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

• count_any_ordertheoremProved here from basic factspropext

  /-- **Order does not matter.** If `l₂` is the same collection as `l₁` in a different order
  (`l₁.Perm l₂`: a rearrangement), counting either one ends on the same word. The words said
  are `1, 2, …, length` (`words_said`), and rearranging does not change the length
  (core Lean's `List.Perm.length_eq`). -/
  theorem count_any_order {α : Type} {l₁ l₂ : List α} (h : l₁.Perm l₂) :
      ((countAloud l₁ 1).map Prod.fst).getLast? = ((countAloud l₂ 1).map Prod.fst).getLast? := by
    rw [words_said, words_said, h.length_eq]

  Axioms used: propextformal/Lumenary/Counting.leanTry it in the Lean web editor

• count_reversetheoremApplies a library theorempropext

  /-- Counting backwards along the line of goats gives the same number as counting forwards.
  This applies core Lean's `List.length_reverse`. -/
  theorem count_reverse {α : Type} (l : List α) : l.reverse.length = l.length :=
    List.length_reverse

  Axioms used: propextformal/Lumenary/Counting.leanTry it in the Lean web editor

• empty_counttheoremProved here from basic factsNo axioms

  /-- Counting the empty collection: there is nothing to touch, so no number word is said at all.
  The number of members of the empty collection is zero. -/
  theorem empty_count : countAloud ([] : List String) 1 = [] ∧ ([] : List String).length = 0 :=
    ⟨rfl, rfl⟩

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

• PairedstructureDefinitionNo axioms

  /-- `Paired xs ys` says the two collections can be lined up side by side, one member of `xs`
  with one member of `ys`, with none left over: either both are empty, or we pair their first
  members and can pair up the rest. -/
  inductive Paired {α β : Type} : List α → List β → Prop
    | nil : Paired [] []
    | cons {x : α} {y : β} {xs : List α} {ys : List β} : Paired xs ys → Paired (x :: xs) (y :: ys)

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

• Paired.same_counttheoremProved here from basic factspropext

  /-- If two collections pair up with none left over, counting them gives the same number.
  Proof by induction on the pairing: each pair adds one to both counts. -/
  theorem Paired.same_count {α β : Type} {xs : List α} {ys : List β} (h : Paired xs ys) :
      xs.length = ys.length := by
    induction h with
    | nil => rfl
    | cons _ ih => simp [ih]

  Axioms used: propextformal/Lumenary/Counting.leanTry it in the Lean web editor

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

  /-- Conversely, two collections with the same number of members can be paired up with none
  left over: pair the first members, then pair the rest in the same way. -/
  theorem paired_of_same_count {α β : Type} :
      ∀ (xs : List α) (ys : List β), xs.length = ys.length → Paired xs ys
    | [], [], _ => Paired.nil
    | [], _ :: _, h => absurd h (by simp)
    | _ :: _, [], h => absurd h (by simp)
    | _ :: xs, _ :: ys, h => Paired.cons (paired_of_same_count xs ys (by simpa using h))

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

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

  /-- **Pairing and counting agree.** Two collections pair up with none left over exactly when
  they have the same number of members. -/
  theorem paired_iff_same_count {α β : Type} (xs : List α) (ys : List β) :
      Paired xs ys ↔ xs.length = ys.length :=
    ⟨Paired.same_count, paired_of_same_count xs ys⟩

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

• childrendefDefinitionNo axioms

  /-- Tomás's four friends and Tomás himself: he hands out cups to his guests first. -/
  def children : List String := ["Lina", "Kofi", "Mei", "Arjun", "Tomás"]

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

• cupsdefDefinitionNo axioms

  /-- The cups on the shelf. -/
  def cups : List String := ["red", "blue", "green", "yellow"]

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

• not_enough_cupstheoremProved here from basic factspropext

  /-- The children and the cups cannot be paired with none left over: if they could, there would
  be as many children as cups, but there are 5 children and only 4 cups. -/
  theorem not_enough_cups : ¬ Paired children cups := by
    intro h
    have same : children.length = cups.length := h.same_count
    -- `same` says `5 = 4`, which Lean can see is false.
    exact absurd same (by decide)

  Axioms used: propextformal/Lumenary/Counting.leanTry it in the Lean web editor

• always_a_nexttheoremApplies a library theoremNo axioms

  /-- Every counting number has a next one, and the next one is bigger.
  This applies core Lean's `Nat.lt_succ_self`. -/
  theorem always_a_next (n : Nat) : n < n + 1 := Nat.lt_succ_self n

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

• no_largest_numbertheoremProved here from basic factsNo axioms

  /-- **There is no largest counting number.** Suppose some `n` were at least as big as every
  counting number. Then `n + 1 ≤ n`, which is impossible. -/
  theorem no_largest_number : ¬ ∃ n : Nat, ∀ m : Nat, m ≤ n := by
    intro ⟨n, h⟩
    have h' : n + 1 ≤ n := h (n + 1)
    exact Nat.not_succ_le_self n h'

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