Lumenary.DataAndTallies

Formal library

• WaystructureDefinitionNo axioms

  /-- The four categories for the question "How did you come to school today?". Every child's
  answer is exactly one of them. -/
  inductive Way where
    | walk | bus | bike | car
    deriving DecidableEq, Repr

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

• answersdefDefinitionNo axioms

  /-- The answers of the 24 children in Ms Wanjiru's class, in the order they were asked. -/
  def answers : List Way :=
    [.walk, .bus, .walk, .car, .bike, .walk, .bus, .walk, .bike, .bus, .walk, .car,
     .walk, .bus, .bike, .walk, .bus, .walk, .bike, .bus, .car, .walk, .bus, .bike]

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

• tallydefDefinitionNo axioms

  /-- The tally for category `w`: how many answers in the list are `w`. -/
  def tally (w : Way) (l : List Way) : Nat := l.count w

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

• class_talliestheoremProved here from basic factsNo axioms

  /-- The class's tallies: 9 walk, 7 come by bus, 5 by bike and 3 by car — 24 answers in all.
  `decide` makes Lean count every category itself. -/
  theorem class_tallies :
      tally .walk answers = 9 ∧ tally .bus answers = 7 ∧ tally .bike answers = 5 ∧
        tally .car answers = 3 ∧ answers.length = 24 := by
    decide

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

• totals_add_uptheoremProved here from basic factspropext, Quot.sound

  /-- **The totals add up.** For *every* list of answers, the four tallies add up to the number of
  answers. Proof by induction on the list: one more answer adds one mark to the tally of its own
  category and none to the others, so both sides grow by one. -/
  theorem totals_add_up (l : List Way) :
      tally .walk l + tally .bus l + tally .bike l + tally .car l = l.length := by
    induction l with
    | nil => rfl
    | cons w rest ih =>
      unfold tally at ih ⊢
      -- Look at which category the new answer `w` is in; `simp` uses `List.count_cons`.
      cases w <;> simp <;> omega

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

• walk_is_mosttheoremProved here from basic factsNo axioms

  /-- Walking is the most common answer: no category has a bigger tally. We check each of the
  four categories in turn. -/
  theorem walk_is_most : ∀ w : Way, tally w answers ≤ tally .walk answers := by
    intro w
    cases w <;> decide

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

• how_many_moretheoremProved here from basic factsNo axioms

  /-- "How many more children walk than come by bus?" Two more: `9 − 7 = 2`. -/
  theorem how_many_more : tally .walk answers - tally .bus answers = 2 := by decide

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

• gatesdefDefinitionNo axioms

  /-- The number of complete groups of five ("gates") in a tally of `n` marks. -/
  def gates (n : Nat) : Nat := n / 5

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

• loosedefDefinitionNo axioms

  /-- The marks left over after the complete groups of five. -/
  def loose (n : Nat) : Nat := n % 5

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

• tally_in_fivestheoremApplies a library theorempropext

  /-- Counting a tally by fives, then counting on the loose marks, always gives the number of
  marks: `5 × gates + loose = n`. This applies core Lean's `Nat.div_add_mod`. -/
  theorem tally_in_fives (n : Nat) : 5 * gates n + loose n = n := Nat.div_add_mod n 5

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

• nine_in_fivestheoremProved here from basic factsNo axioms

  /-- A tally of 9 is one gate of five and four loose marks. -/
  theorem nine_in_fives : gates 9 = 1 ∧ loose 9 = 4 := ⟨rfl, rfl⟩

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

• FruitstructureDefinitionNo axioms

  /-- Fruits for the question "Which fruits do you like?", where children may choose several. -/
  inductive Fruit where
    | mango | banana | papaya
    deriving DecidableEq, Repr

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

• likesdefDefinitionNo axioms

  /-- Four children's answers. The second and fourth child each chose two fruits. -/
  def likes : List (List Fruit) := [[.mango], [.banana, .mango], [.papaya], [.mango, .papaya]]

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

• likersdefDefinitionNo axioms

  /-- How many children chose fruit `f`. -/
  def likers (f : Fruit) (l : List (List Fruit)) : Nat := l.countP (fun choices => choices.contains f)

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

• likes_overcounttheoremProved here from basic factsNo axioms

  /-- With several answers allowed, the totals no longer add up to the number of children: the
  three totals are 3, 1 and 2, which make 6, but only 4 children were asked. -/
  theorem likes_overcount :
      likers .mango likes + likers .banana likes + likers .papaya likes = 6 ∧ likes.length = 4 := by
    decide

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