Counting

Every evening, Nomin helps her grandmother bring their goats home across the wide grassland of Mongolia. There are seven goats: Snowy, Patch, Socks, Star, Pebble, Moss and Biscuit.

As the goats push through the gate, Nomin counts them: one, two, three, four, five, six, seven. All home!

But goats do not stand still. They wander, jump and swap places. How can Nomin be sure that she counted every goat, and none of them twice? And if she counts again in a different order, will she get the same answer?

Good counters follow three rules.

1. Touch each thing exactly once. Don't skip any, and don't touch any twice.
2. Say the number words in the same order every time: one, two, three, four, five, …
3. The last word you say tells how many. If your last word is seven, there are seven goats.

When things stand in a line, rule 1 is easy. When they stand in a ring or in a muddle, it is harder! Two good tricks: move each thing to a new place as you count it, or mark the thing you started with, so you know when to stop.

Tap the boxes to put dots in or take them out. Count the dots. Then try to see how many without counting one by one: a full row is five, and a full frame is ten.

Here are two frames. Thirteen is one full ten and three more. Can you make 17? What about 20?

You met collections and the empty collection in the lesson on collections. Now we can say how many members a collection has.

Why does the last word tell how many? When Nomin counts, every goat gets one number word: Snowy–one, Patch–two, …, Biscuit–seven. So the goats are paired up with the words one to seven, with none left over. The last word, seven, is not the name of Biscuit. It tells us how far along the number words the pairing reached — and that is exactly what "there are seven goats" means.

Why doesn't the order matter? Count again, starting with Moss. You make different pairs this time — Moss–one, and so on. But you still touch each goat exactly once. No goat was added and none was taken away, so you run out of goats at the same word: seven.

Is there a biggest number? Say any number you like: a hundred, a thousand, a million. I can always say one more: a million and one! Every counting number has a next one, so there is no biggest counting number. The counting words go on for ever.

Gideon likes statements that are clearly true or clearly false. Are these true or false?

1. "Nomin counted seven goats, starting with Snowy. If she starts with Moss instead, she will get seven again." — True. The order of counting never changes the number.
2. "Ravi spread his counters out, so now he has more." — False. Pair them up: none are left over.
3. "If every child gets exactly one cup and no cups are left over, there are just as many cups as children." — True. That is what the same number means.
4. "There is a biggest counting number." — False!

/-- 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)

/-- 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

/-- 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]

/-- 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]

/-- **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]

/-- **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]

/-- 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⟩

/-- `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)

/-- **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⟩

/-- 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)

/-- **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'

Margaret noticed something sneaky: if you skip one goat and touch another goat twice, you get the right answer by luck. A right answer does not always mean careful counting!

"""Counting a small herd in every possible order.

Counting pairs each object with exactly one number word: one, two, three, ...
We count a herd of five goats in all 5! = 120 orders and record the last
number word said each time. Then we show what a counting slip (skipping a
goat, or touching one twice) does to the answer, and compare two collections
by pairing them up, without counting at all.

The checks are exact and cover every order of this one herd; they do not
prove anything about other collections. The lesson explains why the last
word is the same for every collection and every order.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from collections import Counter
from itertools import permutations
from math import factorial
import textwrap

#: Number words in counting order.
NUMBER_WORDS = (
    "one", "two", "three", "four", "five", "six", "seven", "eight", "nine",
    "ten", "eleven", "twelve",
)

#: Five of Nomin's goats.
HERD = ("Snowy", "Patch", "Socks", "Star", "Pebble")

#: Tomás's friends (served first) and Tomás, and the cups on the shelf.
CHILDREN = ("Lina", "Kofi", "Mei", "Arjun", "Tomás")
CUPS = ("red", "blue", "green", "yellow")

def count_aloud(items):
    """Pair each item with a number word, in order: [(word, item), ...]."""
    items = list(items)
    if len(items) > len(NUMBER_WORDS):
        raise ValueError(f"can only count up to {len(NUMBER_WORDS)} items")
    return list(zip(NUMBER_WORDS, items))

def last_word(items):
    """The last number word said when counting ``items`` ("zero" if empty)."""
    pairs = count_aloud(items)
    return pairs[-1][0] if pairs else "zero"

def last_words_in_every_order(items):
    """Count ``items`` in every order; return a Counter of the last words."""
    return Counter(last_word(order) for order in permutations(items))

def touches(items, skip=None, twice=None):
    """The objects touched by a counter who may slip.

    ``skip`` is the position of an item that is missed out, and ``twice`` the
    position of an item that is touched a second time straight away.
    """
    touched = []
    for position, item in enumerate(items):
        if position == skip:
            continue
        touched.append(item)
        if position == twice:
            touched.append(item)
    return touched

def pair_up(first, second):
    """Line two collections up side by side.

    Returns (pairs, left over from first, left over from second); at most one
    of the two left-over lists is non-empty.
    """
    first, second = list(first), list(second)
    n = min(len(first), len(second))
    return list(zip(first, second)), first[n:], second[n:]

def main():
    herd = list(HERD)
    said = ", ".join(f"{goat} {word}" for word, goat in count_aloud(herd))
    print("Counting the herd once:")
    print(f"  {said}")
    orders = factorial(len(herd))
    tally = last_words_in_every_order(herd)
    print(f"Counting in all {orders} orders, the last word said was:")
    for word, times in tally.items():
        print(f"  '{word}' in {times} of the {orders} orders")
    print()
    print("Counting slips:")
    slips = [("skip Socks", touches(herd, skip=2)),
             ("touch Star twice", touches(herd, twice=3)),
             ("both slips at once", touches(herd, skip=2, twice=3))]
    for label, touched in slips:
        print(f"  {label:<18} -> last word '{last_word(touched)}'")
    print("  Two slips can cancel out: a right answer from wrong counting!")
    print()
    pairs, kids_left, cups_left = pair_up(CHILDREN, CUPS)
    print("Pairing children with cups, without counting:")
    print("  " + ", ".join(f"{kid}-{cup}" for kid, cup in pairs))
    print(f"  children left without a cup: {', '.join(kids_left) or 'none'}")
    print(f"  cups left over: {', '.join(cups_left) or 'none'}")
    print("  So there are fewer cups than children.")
    print()
    print("How many different orders are there to try?")
    cells = [f"{n} goat{'s' if n > 1 else ''}: {factorial(n):,}"
             for n in (1, 2, 3, 4, 5, 6, 7, 10)]
    print("  " + ", ".join(cells[:4]))
    print("  " + ", ".join(cells[4:]))
    print()
    print(textwrap.fill(
        f"Epistemic status: exact and exhaustive for this herd: all {orders} "
        "orders of these five goats were counted. That is not a proof for "
        "other collections, and the number of orders grows far too fast to "
        "try them all for a big herd. Why every order of every collection "
        "ends on the same word is explained in the lesson.",
        width=78,
    ))

if __name__ == "__main__":
    main()

Take your time. Touch each thing as you count, and ask for a hint whenever you like.

Pairing also works for collections that never end. Can all the even numbers be paired with all the counting numbers? This trail is for older brothers and sisters — and curious grown-ups. It is completely optional.

People everywhere have counted, in many clever ways.

• The Ishango bone, found at Ishango near Lake Edward, in what is now the Democratic Republic of the Congo, is about 20,000 years old and carries groups of notches. Some researchers think the notches record counts, although nobody knows for certain.
• In ancient Mesopotamia (modern Iraq), people kept track of goods and animals with small clay tokens, one token for each thing — counting by pairing. Archaeologists have even found a hollow clay ball from the town of Nuzi that held small stones, with writing on the outside listing a herd of sheep and goats.
• Languages count in different ways. In Yoruba, spoken in Nigeria and Benin, twenty is an important counting unit, and some numbers are made by taking away: the Yoruba word for sixteen means "four less than twenty".
• The Oksapmin people of Papua New Guinea have traditionally counted by touching body parts in order: the thumb and fingers of one hand, then up the arm, across the face and down to the other hand — a counting sequence of 27 body parts.
• The Indian mathematician Brahmagupta, in 628 CE, gave rules for calculating with zero as a number, and the Maya of Central America used a sign for zero in their calendar.
• More than 2,200 years ago, Archimedes of Syracuse wrote The Sand Reckoner, showing how to name numbers bigger than the number of grains of sand it would take to fill the universe as he pictured it. There is always a bigger number.

• Hung-Hsi Wu, Understanding Numbers in Elementary School Mathematics (2011) — a careful account of whole numbers and counting for teachers.
• Rochel Gelman and C. R. Gallistel, The Child's Understanding of Number (1978) — the classic study of how young children learn to count.
• Claudia Zaslavsky, Africa Counts: Number and Pattern in African Cultures (1973) — counting words, gestures and records across Africa.
• Geoffrey B. Saxe, Cultural Development of Mathematical Ideas: Papua New Guinea Studies (2012) — includes the Oksapmin body-part counting system.
• Stanislas Dehaene, The Number Sense (1997) — what psychology and neuroscience tell us about how humans grasp numbers.