-- An encoding of the classic proof by induction that all horses
-- are the same color.

module Horse where

data ∃ {A : Set} (T : A → Set) : Set where
  _,_ : (x : A) (w : T x) → ∃ T

-- Natural numbers, starting at 1 instead of the usual 0
data ℕ : Set where
  one : ℕ
  suc : ℕ → ℕ

-- Induction on the naturals
induction : (P : ℕ → Set) → P one → (∀ n → P n → P (suc n)) → ∀ n → P n
induction P P1 Pn one     = P1
induction P P1 Pn (suc n) = Pn n (induction P P1 Pn n)

-- Finite sets with natural numbers of elements. We'll assume that we
-- always have a finite number of horses.
data Fin : ℕ → Set where
  zero : ∀{n} → Fin n
  suc  : ∀{n} → Fin n → Fin (suc n)

-- An injection from smaller finite sets to larger ones not using the
-- successor operation. 0 -> 0, 1 -> 1, etc.
lift : ∀{n} → Fin n → Fin (suc n)
lift zero     = zero
lift (suc fn) = suc (lift fn)

-- Horse colors
data Color : Set where
  black : Color
  brown : Color
  white : Color

-- Value equality
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

symm : ∀{A} {x y : A} → x ≡ y → y ≡ x
symm refl = refl

trans : ∀{A} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

-- Representations of the colors of finite sets of horses.
Coloring : ℕ → Set
Coloring n = Fin n → Color

-- Given a set of n+1 horses and their colors, gives a set of
-- n horses and their colors by removing the 'last' horse from the set.
init : ∀{n} → Coloring (suc n) → Coloring n
init c n = c (lift n)

-- Like the above, only removing the 'first' horse.
tail : ∀{n} → Coloring (suc n) → Coloring n
tail c n = c (suc n)

-- Fin n → A is an encoding of vectors of As of size n. All represents
-- a proof that a predicate holds for all elements of the vector.
All : ∀{n} {A : Set} → (P : A → Set) → (Fin n → A) → Set
All P v = ∀ i → P (v i)

-- A proof that all horses in a given set are the same color.
Uniform : ∀{n} → Coloring n → Set
Uniform C = ∃ (λ c → All (_≡_ c) C)

-- This module assumes the flawed part of the reasoning for the
-- induction proof. The inductive case of the proof requires that
-- for a set of n+1 horses, if we remove a horse in two different ways,
-- and the resulting sets all have horses of the same color, then
-- the original set has horses of all the same color.
--
-- However, this fact would itself have to be proved by induction, and
-- the base case of that proof does not hold, as two horses are not the
-- same color given that each is the same color as itself.
module Trick (wrong : ∀{n} → (C : Coloring (suc n))
                           → Uniform (init C)
                           → Uniform (tail C)
                           → Uniform C) where

  same : ∀{n} → (C : Coloring n) → Uniform C
  same {n} C = induction P base ind n C
   where
   P : ℕ → Set
   P n = (C : Coloring n) → Uniform C

   ind : ∀ n → P n → P (suc n)
   ind n Pn C = wrong C (Pn (init C)) (Pn (tail C))

   base : P one
   base C = C zero , pf
    where pf : All (_≡_ (C zero)) C
          pf zero = refl