Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2000P3

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Data.List.Permutation
public import Mathlib.Order.ConditionallyCompleteLattice.Basic
public import Mathlib.Tactic

public section


/-!
# USA Mathematical Olympiad 2000, Problem 3

A player starts with A blue cards, B red cards and C white cards. He scores
points as he plays each card. If he plays a blue card, his score is the number
of white cards remaining in his hand. If he plays a red card it is three times
the number of blue cards remaining in his hand. If he plays a white card, it is
twice the number of red cards remaining in his hand. What is the lowest
possible score as a function of A, B and C and how many different ways can it
be achieved?
-/

namespace Usa2000P3

/-- The three colors of cards. -/
inductive Card where
  | blue
  | red
  | white
  deriving BEq, DecidableEq

instance : LawfulBEq Card where
  eq_of_beq := fun {a b} => by
    cases a <;> cases b <;> intro h <;> first | rfl | (exact absurd h (by decide))
  rfl := fun {a} => by cases a <;> rfl

/-- The score accumulated when playing the sequence of cards `l`, listed in the
order they are played. When a blue card is played, the score gained is the
number of white cards remaining; for a red card it is three times the number of
blue cards remaining; for a white card it is twice the number of red cards
remaining. -/
def score : List Card → ℕ
  | [] => 0
  | .blue :: t => t.count .white + score t
  | .red :: t => 3 * t.count .blue + score t
  | .white :: t => 2 * t.count .red + score t

/-- The canonical play: all blue cards, then all red cards, then all white
cards. Every play with the same card counts is a permutation of this one. -/
def canonicalPlay (A B C : ℕ) : List Card :=
  List.replicate A .blue ++ (List.replicate B .red ++ List.replicate C .white)

/-- The finite set of all plays with `A` blue, `B` red and `C` white cards. -/
def plays (A B C : ℕ) : Finset (List Card) :=
  (canonicalPlay A B C).permutations.toFinset

/- determine -/ abbrev lowestScore (A B C : ℕ) : ℕ := sorry

/-- The number of different ways the lowest score can be achieved. -/
/- determine -/ abbrev fewestWays (A B C : ℕ) : ℕ := sorry

theorem usa2000_p3 (A B C : ℕ) :
    IsLeast {s : ℕ | ∃ l ∈ plays A B C, score l = s} (lowestScore A B C) ∧
    ((plays A B C).filter (fun l ↦ score l = lowestScore A B C)).card =
      fewestWays A B C := sorry

end Usa2000P3

File author(s): Kimi K3

This problem has a complete formalized solution.