Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2011P4

module

public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Ring.GeomSum
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Data.Nat.Factorial.DoubleFactorial
public import Mathlib.Order.Lattice.Nat
public import Mathlib.SetTheory.Cardinal.Finite
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Linarith.Lemmas

public section


/-!
# International Mathematical Olympiad 2011, Problem 4

Let n > 0 be an integer. We are given a balance and n weights of weight
2^0, 2^1, . . . , 2^(n−1). We are to place each of the n weights on the
balance, one after another, in such a way that the right pan is never
heavier than the left pan. At each step we choose one of the weights that
has not yet been placed on the balance, and place it on either the left
pan or the right pan, until all of the weights have been placed.
Determine the number of ways in which this can be done.
-/

namespace Imo2011P4

open scoped Nat
open scoped List

/-- The imbalance (left pan minus right pan) after a sequence of placements.
A pair `(i, b)` denotes one placement of the weight `2^i`; the boolean is
`true` if the weight is placed on the left pan and `false` if it is placed
on the right pan. -/
def Balance (l : List (ℕ × Bool)) : ℤ :=
  ((l.map fun p ↦ if p.2 then (2 : ℤ) ^ p.1 else -((2 : ℤ) ^ p.1))).sum

/-- A sequence of placements is *valid* if after every step the right pan is
not heavier than the left pan. -/
def ValidSeq (l : List (ℕ × Bool)) : Prop :=
  ∀ pre : List (ℕ × Bool), pre <+: l → 0 ≤ Balance pre

/-- The set of ways to carry out the process with the weights
`2^0, 2^1, ..., 2^(n-1)`: sequences of placements in which every weight is
used exactly once and the right pan is never heavier than the left pan. -/
def Ways (n : ℕ) : Type :=
  { l : List (ℕ × Bool) // l.map Prod.fst ~ List.range n ∧ ValidSeq l }

/- determine -/ abbrev solution_value : ℕ → ℕ := sorry

theorem imo2011_p4 (n : ℕ) (hn : 0 < n) :
    Nat.card (Ways n) = solution_value n := sorry

end Imo2011P4

File author(s): Kimi K3

This problem has a complete formalized solution.