IMO 2010 C4 (P5)

In the board, $N = 6$ stacks of coins are given with stack $k < N$ containing one coin each. At any time, one of the following operations are done:

• Remove a coin from a stack $k + 1 < N$ and add two coins to stack $k$.
• Remove a coin from a stack $k + 2 < N$ and swap the content of the stacks $k$ and $k + 1$. Is it possible that, after some operations, we are left with stack $0$ containing $A = 2010^{2010^{2010}}$ coins and all other stacks empty?

Iteration of two-power

def IMOSL.IMO2010C4.P (seed : Nat) : Nat → Nat

Iteration of two-power

Equations

• IMOSL.IMO2010C4.P seed 0 = seed
• IMOSL.IMO2010C4.P seed n.succ = IMOSL.IMO2010C4.P (2 ^ seed) n

theorem IMOSL.IMO2010C4.P_zero (seed : Nat) : P seed 0 = seed

theorem IMOSL.IMO2010C4.P_succ (seed n : Nat) : P seed n.succ = P (2 ^ seed) n

theorem IMOSL.IMO2010C4.P_succ' (seed n : Nat) : P seed n.succ = 2 ^ P seed n

theorem IMOSL.IMO2010C4.P_pos_of_seed {seed : Nat} (h : 0 < seed) (n : Nat) : 0 < P seed n

theorem IMOSL.IMO2010C4.P_lt_of_seed {seed₁ seed₂ : Nat} (h : seed₁ < seed₂) (n : Nat) : P seed₁ n < P seed₂ n

theorem IMOSL.IMO2010C4.Nat_lt_two_pow (n : Nat) : n < 2 ^ n

A copy of Nat.lt_two_pow

theorem IMOSL.IMO2010C4.seed_lt_P_one (seed : Nat) : seed < P seed 1

theorem IMOSL.IMO2010C4.P_lt_succ_iter (seed n : Nat) : P seed n < P seed (n + 1)

theorem IMOSL.IMO2010C4.P_le_add_iter (seed n k : Nat) : P seed n ≤ P seed (n + k)

theorem IMOSL.IMO2010C4.P_monotone_iter {n m : Nat} (seed : Nat) (h : n ≤ m) : P seed n ≤ P seed m

theorem IMOSL.IMO2010C4.P_strict_mono_iter {n m : Nat} (seed : Nat) (h : n < m) : P seed n < P seed m

theorem IMOSL.IMO2010C4.le_of_P_le_iter {seed n m : Nat} (h : P seed n ≤ P seed m) : n ≤ m

theorem IMOSL.IMO2010C4.P_iter_le_iff {seed n m : Nat} : P seed n ≤ P seed m ↔ n ≤ m

More lemmas on log2

theorem IMOSL.IMO2010C4.log2_lt_iff₂ {k n : Nat} (hk : 0 < k) : n.log2 < k ↔ n < 2 ^ k

theorem IMOSL.IMO2010C4.log2_monotone {m n : Nat} (h : m ≤ n) : m.log2 ≤ n.log2

theorem IMOSL.IMO2010C4.log2_two_pow (n : Nat) : (2 ^ n).log2 = n

Iteration of log2

def IMOSL.IMO2010C4.log2_iter (seed : Nat) : Nat → Nat

Equations

• IMOSL.IMO2010C4.log2_iter seed 0 = seed
• IMOSL.IMO2010C4.log2_iter seed n.succ = IMOSL.IMO2010C4.log2_iter seed.log2 n

theorem IMOSL.IMO2010C4.log2_iter_zero (seed : Nat) : log2_iter seed 0 = seed

theorem IMOSL.IMO2010C4.log2_iter_succ (seed n : Nat) : log2_iter seed (n + 1) = log2_iter seed.log2 n

theorem IMOSL.IMO2010C4.log2_iter_add (seed n k : Nat) : log2_iter seed (n + k) = log2_iter (log2_iter seed k) n

theorem IMOSL.IMO2010C4.log2_iter_lt_iff {k seed : Nat} (hk : 0 < k) {n : Nat} : log2_iter seed n < k ↔ seed < P k n

theorem IMOSL.IMO2010C4.log2_iter_eq_zero_iff {seed n : Nat} : log2_iter seed n = 0 ↔ seed < P 1 n

theorem IMOSL.IMO2010C4.log2_iter_monotone_seed {seed₁ seed₂ : Nat} (h : seed₁ ≤ seed₂) (n : Nat) : log2_iter seed₁ n ≤ log2_iter seed₂ n

theorem IMOSL.IMO2010C4.log2_iter_le_self (seed n : Nat) : log2_iter seed n ≤ seed

theorem IMOSL.IMO2010C4.log2_antitone_iter {m n : Nat} (seed : Nat) (h : m ≤ n) : log2_iter seed n ≤ log2_iter seed m

inductive IMOSL.IMO2010C4.isReachable : List Nat → List Nat → Prop

• type1_move (k m : Nat) : isReachable [k + 1, m] [k, m + 2]
• type2_move (k m n : Nat) : isReachable [k + 1, m, n] [k, n, m]
• refl (l : List Nat) : isReachable l l
• trans {l₁ l₂ l₃ : List Nat} (h : isReachable l₁ l₂) : isReachable l₂ l₃ → isReachable l₁ l₃
• append_right {l₁ l₂ : List Nat} (h : isReachable l₁ l₂) (l : List Nat) : isReachable (l₁ ++ l) (l₂ ++ l)
• cons_left {l₁ l₂ : List Nat} (h : isReachable l₁ l₂) (k : Nat) : isReachable (k :: l₁) (k :: l₂)

General observation

theorem IMOSL.IMO2010C4.isReachable.append_left {l₁ l₂ : List Nat} (h : isReachable l₁ l₂) (l : List Nat) : isReachable (l ++ l₁) (l ++ l₂)

theorem IMOSL.IMO2010C4.isReachable.append_left_right {l₁ l₂ : List Nat} (h : isReachable l₁ l₂) (l l' : List Nat) : isReachable (l ++ l₁ ++ l') (l ++ l₂ ++ l')

theorem IMOSL.IMO2010C4.isReachable.type1_repeat (k m n : Nat) : isReachable [k + n, m] [k, m + 2 * n]

theorem IMOSL.IMO2010C4.isReachable.type1_repeat_zero (n : Nat) : isReachable [n, 0] [0, 2 * n]

theorem IMOSL.IMO2010C4.isReachable.two_pow₁ (k n m c : Nat) : isReachable [k + c, n + m, n] [k, n + 2 ^ c * m, n]

theorem IMOSL.IMO2010C4.isReachable.two_pow₂ (k n c : Nat) : isReachable [k + (c + 1), n, n] [k, n + 2 ^ (c + 1), n]

theorem IMOSL.IMO2010C4.isReachable.two_pow₃ {c : Nat} (k n : Nat) (hc : 0 < c) : isReachable [k + c, n, n] [k, n + 2 ^ c, n]

theorem IMOSL.IMO2010C4.isReachable.two_pow_iter₁ {m : Nat} (k n : Nat) (hm : 0 < m) (c : Nat) : isReachable [k + c, n + m, n, n] [k, n + P m c, n, n]

theorem IMOSL.IMO2010C4.isReachable.two_pow_iter₂ (k n c : Nat) : isReachable [k + (c + 1), n, n, n] [k, n + P 1 (c + 1), n, n]

theorem IMOSL.IMO2010C4.isReachable.two_pow_iter₃ {c : Nat} (k n : Nat) (hc : 0 < c) : isReachable [k + c, n, n, n] [k, n + P 1 c, n, n]

theorem IMOSL.IMO2010C4.isReachable.two_pow_iter₄ {c : Nat} (n : Nat) (hc : 0 < c) : isReachable [c, n, n, n] [0, n + P 1 c, n, n]

theorem IMOSL.IMO2010C4.isReachable.type2_repeat_drain₀ (k n c : Nat) : isReachable [k + c, n, n] [k, n, n]

theorem IMOSL.IMO2010C4.isReachable.type2_repeat_drain {k m : Nat} (n : Nat) (h : k ≤ m) : isReachable [m, n, n] [k, n, n]

Reachability of specific states

theorem IMOSL.IMO2010C4.isReachable.replicate_ones_to_3₀ (n : Nat) : isReachable (List.replicate (n + 2) 1) (0 :: 3 :: List.replicate n 0)

theorem IMOSL.IMO2010C4.isReachable.replicate_ones_to_3₁ (n : Nat) : isReachable (List.replicate (n + 2) 1) (0 :: 3 :: List.replicate n 1)

theorem IMOSL.IMO2010C4.isReachable.cons_replicate4_to_P₀ {N : Nat} (n : Nat) (hN : 0 < N) : isReachable [N, n, n, n, n] [0, 0, n + P 1 (n + P 1 N), n, n]

theorem IMOSL.IMO2010C4.isReachable.cons_replicate4_to_P {N : Nat} (n : Nat) (hN : 0 < N) : isReachable [N, n, n, n, n] [0, 0, P 1 (P 1 N), n, n]

theorem IMOSL.IMO2010C4.isReachable.type1_double_repeat (a b c N : Nat) : isReachable [a + N, b, c] [a, b, c + 4 * N]

theorem IMOSL.IMO2010C4.isReachable.type1_double_repeat_a_eq_zero (b c N : Nat) : isReachable [N, b, c] [0, b, c + 4 * N]

theorem IMOSL.IMO2010C4.isReachable.Nadd2_zero_zero_to_4Nadd5 (N : Nat) : isReachable [N + 2, 0, 0] [0, 0, 4 * N + 5]

[2, 0, 0] → [1, 2, 0] → [1, 1, 2] → [0, 2, 1] → [0, 0, 5]

theorem IMOSL.IMO2010C4.isReachable.Nadd2_zero_zero_to_4Nadd2 (N : Nat) : isReachable [N + 2, 0, 0] [0, 0, 4 * N + 2]

[2, 0, 0] → [1, 2, 0] → [0, 0, 2]

theorem IMOSL.IMO2010C4.isReachable.Nadd5_zero_zero_to_4Nadd22 (N : Nat) : isReachable [N + 5, 0, 0] [0, 0, 4 * N + 22]

[5, 0, 0] → [1, 16, 0] → [1, 14, 4] → [0, 4, 14] → [0, 0, 22]

theorem IMOSL.IMO2010C4.isReachable.N_one_one_to_4Nadd3 (N : Nat) : isReachable [N, 1, 1] [0, 0, 4 * N + 3]

theorem IMOSL.IMO2010C4.isReachable.three_stack_0mod4 {A : Nat} (N : Nat) (hA : A % 4 = 0) (h : A < 4 * N) : isReachable [N, 0, 0] [0, 0, A]

theorem IMOSL.IMO2010C4.isReachable.three_stack_1mod4 {N A : Nat} (hN : 2 ≤ N) (hA : A % 4 = 1) (hA0 : A ≠ 1) (h : A < 4 * N) : isReachable [N, 0, 0] [0, 0, A]

theorem IMOSL.IMO2010C4.isReachable.three_stack_2mod4 {N A : Nat} (hN : 6 ≤ N) (hA : A % 4 = 2) (h : A < 4 * N) : isReachable [N, 0, 0] [0, 0, A]

theorem IMOSL.IMO2010C4.isReachable.three_stack_3mod4 {A : Nat} (N : Nat) (hA : A % 4 = 3) (h : A < 4 * N) : isReachable [N, 1, 1] [0, 0, A]

theorem IMOSL.IMO2010C4.isReachable.three_stack_of_bdd {N : Nat} {L : List Nat} {A : Nat} (hN : 6 ≤ N) (hL₀ : isReachable L [0, 0, 0, N, 0, 0]) (hL₁ : isReachable L [0, 0, 0, N, 1, 1]) (h : A ≠ 1) (h0 : A < 4 * N) : isReachable L (List.replicate 5 0 ++ [A])

theorem IMOSL.IMO2010C4.isReachable.six_stack_of_bdd {N : Nat} {L : List Nat} {A : Nat} (hN : 2 ≤ N) (hL₀ : isReachable L (0 :: N :: List.replicate 4 0)) (hL₁ : isReachable L (0 :: N :: List.replicate 4 1)) (hA : A < 4 * P 1 (P 1 N)) : isReachable L (List.replicate 5 0 ++ [A])

theorem IMOSL.IMO2010C4.isReachable.six_stack_of_bdd_log {N : Nat} {L : List Nat} {A : Nat} (hN : 2 ≤ N) (hL₀ : isReachable L (0 :: N :: List.replicate 4 0)) (hL₁ : isReachable L (0 :: N :: List.replicate 4 1)) (hA : log2_iter (A / 4) (P 1 N) = 0) : isReachable L (List.replicate 5 0 ++ [A])

theorem IMOSL.IMO2010C4.isReachable.replicate6_ones_to_A {A : Nat} (hA : log2_iter (A / 4) 16 = 0) : isReachable (List.replicate 6 1) (List.replicate 5 0 ++ [A])

Final solution

theorem IMOSL.IMO2010C4.final_solution : isReachable (List.replicate 6 1) (List.replicate 5 0 ++ [2010 ^ 2010 ^ 2010])

Final solution