Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1996P4

module

public import Mathlib.AlgebraicTopology.SimplexCategory.Basic

public section


/-!
# USA Mathematical Olympiad 1996, Problem 4

An n-term sequence (x₁, x₂, …, xₙ) in which each term is either 0 or 1 is called a
binary sequence of length n. Let aₙ be the number of binary sequences of length n
containing no three consecutive terms equal to 0, 1, 0 in that order. Let bₙ be the
number of binary sequences of length n that contain no four consecutive terms equal
to 0, 0, 1, 1 or 1, 1, 0, 0 in that order. Prove that bₙ₊₁ = 2aₙ for all positive
integers n.
-/

namespace Usa1996P4

/-- The `i`-th term of a binary sequence `x : Fin n → Bool`, or `false` if `i`
is out of range. -/
def sget {n : ℕ} (x : Fin n → Bool) (i : ℕ) : Bool :=
  if h : i < n then x ⟨i, h⟩ else false

/-- A binary sequence of length `n` (encoded as `x : Fin n → Bool`, with `false`
standing for `0` and `true` for `1`) is `A`-good if it contains no three consecutive
terms equal to `0, 1, 0` in that order. -/
abbrev GoodA {n : ℕ} (x : Fin n → Bool) : Prop :=
  ∀ i : Fin n, (i : ℕ) + 2 < n →
    ¬(sget x (i : ℕ) = false ∧ sget x ((i : ℕ) + 1) = true ∧ sget x ((i : ℕ) + 2) = false)

/-- A binary sequence of length `n` is `B`-good if it contains no four consecutive
terms equal to `0, 0, 1, 1` or `1, 1, 0, 0` in that order. -/
abbrev GoodB {n : ℕ} (y : Fin n → Bool) : Prop :=
  ∀ i : Fin n, (i : ℕ) + 3 < n →
    ¬((sget y (i : ℕ) = false ∧ sget y ((i : ℕ) + 1) = false ∧ sget y ((i : ℕ) + 2) = true ∧
        sget y ((i : ℕ) + 3) = true) ∨
      (sget y (i : ℕ) = true ∧ sget y ((i : ℕ) + 1) = true ∧ sget y ((i : ℕ) + 2) = false ∧
        sget y ((i : ℕ) + 3) = false))

theorem usa1996_p4 (n : ℕ) :
    Fintype.card {y : Fin (n + 1) → Bool // GoodB y} =
      2 * Fintype.card {x : Fin n → Bool // GoodA x} := sorry

end Usa1996P4

File author(s): Kimi K3

This problem has a complete formalized solution.