Nicomachus's theorem

Nicomachus.agda

module Nicomachus where

open import Function
open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning as EqReasoning

open import Data.Nat
open import Data.Nat.Properties

-- http://en.wikipedia.org/wiki/Nicomachus%27s_theorem
-- http://blogs.mathworks.com/loren/2010/03/04/nichomachuss-theorem/

-- Our basic sigma notation: takes the number of "iterations" and a function to apply to each element of the summation
Σ : ℕ → (ℕ → ℕ) → ℕ
Σ 0 f = 0
Σ (suc n) f = Σ n f + f (suc n)

open EqReasoning (setoid ℕ)
open SemiringSolver

module Sugar where
  -- The powers we care about
  _² : ℕ → ℕ
  x ² = x * x

  _³ : ℕ → ℕ
  x ³ = x ² * x

  -- To make our reified expressions for the semiring solver a tad more palatable
  1+′_ : ∀ {n} → Polynomial n → Polynomial n
  1+′ n = con 1 :+ n

  2*′_ : ∀ {n} → Polynomial n → Polynomial n
  2*′ n = con 2 :* n

  _²′ : ∀ {n} → Polynomial n → Polynomial n
  n ²′ = n :* n

  _³′ : ∀ {n} → Polynomial n → Polynomial n
  n ³′ = n ²′ :* n

open Sugar

-- The usual form of this is (0 + 1 + 2 + ... n) = (n * (n - 1)) / 2, but the division and subtraction are a pain
-- on naturals, so this is a more useful presentation for our purposes
lemma : ∀ n → 2 * Σ n id ≡ (1 + n) * n
lemma zero = refl
lemma (suc n) = 
  begin
    2 * Σ (suc n) id                          ≡⟨ refl ⟩ -- Expand definition of Σ
    Σ n id + (1 + n) + (Σ n id + (1 + n) + 0) ≡⟨ solve 2 (λ x y → x :+ y :+ (x :+ y :+ con 0) := 2*′ x :+ 2*′ y) refl (Σ n id) (1 + n) ⟩ -- Boring algebra
    2 * Σ n id + 2 * (1 + n)                  ≡⟨ cong (λ q → q + 2 * (1 + n)) (lemma n) ⟩ -- Inductive case
    (suc n) * n + 2 * (1 + n)                 ≡⟨ solve 1 (λ x → (1+′ x) :* x :+ 2*′ (1+′ x) := (1+′ (1+′ x)) :* (1+′ x)) refl n ⟩ -- Boring algebra
    (1 + suc n) * suc n
  ∎

-- Nichomacus's theorem!
theorem : ∀ n → Σ n id ² ≡ Σ n _³
theorem zero = refl
theorem (suc n) =
  begin
    Σ (1 + n) id ²                               ≡⟨ refl ⟩ -- Expand definition of Σ
    (Σ n id + (1 + n)) ²                         ≡⟨ solve 2 (λ x y → (x :+ y) ²′ := x ²′ :+ (2*′ x :* y) :+ y ²′) refl (Σ n id) (1 + n) ⟩ -- Square of a binomial
    Σ n id ² + 2 * Σ n id * (1 + n) + (1 + n) ²  ≡⟨ cong (λ q → q + 2 * Σ n id * (1 + n) + (1 + n) ²) (theorem n) ⟩ -- Inductive case
    Σ n _³ + 2 * Σ n id * (1 + n) + (1 + n) ²    ≡⟨ cong (λ q → Σ n _³ + q * (1 + n) + (1 + n) ²) (lemma n) ⟩ -- Use the lemma defined above
    Σ n _³ + ((1 + n) * n) * (1 + n) + (1 + n) ² ≡⟨ solve 2  (λ x y → x :+ (1+′ y) :* y :* (1+′ y) :+ (1+′ y) ²′ := x :+ (1+′ y) ³′) refl (Σ n _³) n ⟩ -- Boring algebra
    Σ n _³ + (1 + n) ³                           ≡⟨ refl ⟩ -- Contract definition of Σ
    Σ (1 + n) _³
  ∎

Thanks :)