Formulating the chocolate bar theorem

Stream: new members

[Thomas Chaumeny]

The chocolate bar theorem states that breaking a chocolate bar of size N (= a*b with a,b strictly positive integers) into N individual pieces always takes N-1 cuts.

Informally, this is proved very easily by induction on N as it is clear (chocolate(N) being the number of cuts) that chocolate(1) = 0 and if we break a bar of size N+1 in two pieces of sizes N1 and N2 we find that chocolate(N+1) = 1 + chocolate(N1) + chocolate(N2) = 1 + N1 - 1 + N2 - 1 = N.

I would like to prove it in Lean but actually I don't even know how to formulate it.
The documentation on induction doesn't help me much as I don't have such a direct induction as in the examples. Also, I might need to consider a sequence of cuts to formulate the problem properly.

How would you formulate this problem in a smart (and possibly concise) way?

[Andrew Yang]

Is something like this good enough?

def iterate {α : Sort u} (op : α → α) : Nat → α → α
  | 0, a => a
  | Nat.succ k, a => iterate op k (op a)

def cut (n : Nat) := n + 1

theorem chocolate (k N : Nat) : (iterate cut k) 1 = N → k = N - 1 := by
  suffices ∀ m, iterate cut k m = m + k by intro e; rw [← e, this, Nat.add_comm]; rfl
  induction k with
  | zero => exact fun _ => rfl
  | succ k IH => exact fun N => (IH (cut N)).trans (Nat.succ_add N k)

[Yaël Dillies]

I don't think it accurately reflects the two-dimensionality of the problem.

[Yaël Dillies]

This formalisation is more accurate, I hope:

import Mathlib.Data.Nat.Basic

inductive ChocolateBar : ℕ → ℕ → Type where
  | square : ChocolateBar 1 1
  | hCut ⦃a₁ a₂ b : ℕ⦄ : ChocolateBar a₁ b → ChocolateBar a₂ b → ChocolateBar (a₁ + a₂) b
  | vCut ⦃a b₁ b₂ : ℕ⦄ : ChocolateBar a b₁ → ChocolateBar a b₂ → ChocolateBar a (b₁ + b₂)

def ChocolateBar.cuts : ChocolateBar a b → ℕ
  | square => 0
  | hCut choc₁ choc₂ => choc₁.cuts + choc₂.cuts + 1
  | vCut choc₁ choc₂ => choc₁.cuts + choc₂.cuts + 1

theorem ChocolateBar.size_le_cuts_add_one : ∀ choc : ChocolateBar a b, a * b ≤ choc.cuts + 1
  | square => le_rfl
  | hCut choc₁ choc₂ => by
    rw [cuts, add_assoc, Nat.add_add_add_comm, add_mul]
    exact Nat.add_le_add choc₁.size_le_cuts_add_one choc₂.size_le_cuts_add_one
  | vCut choc₁ choc₂ => by
    rw [cuts, add_assoc, Nat.add_add_add_comm, mul_add]
    exact Nat.add_le_add choc₁.size_le_cuts_add_one choc₂.size_le_cuts_add_one

[Yaël Dillies]

In fact, you can just as easily show that this is exactly the number of cuts needed:

theorem ChocolateBar.size_eq_cuts_add_one : ∀ choc : ChocolateBar a b, a * b = choc.cuts + 1
  | square => rfl
  | hCut choc₁ choc₂ => by
    rw [cuts, add_mul, add_assoc, Nat.add_add_add_comm, ← size_eq_cuts_add_one,
      ← size_eq_cuts_add_one]
  | vCut choc₁ choc₂ => by
    rw [cuts, mul_add, add_assoc, Nat.add_add_add_comm, ← size_eq_cuts_add_one,
      ← size_eq_cuts_add_one]

[Thomas Chaumeny]

That looks quite clean!
In your implementation, is this correct to call ChocolateBar a dependent inductive type?

[Yaël Dillies]

Yes, I think so!