Puzzle.agda

module Puzzle where

open import Data.Nat using (ℕ; _+_)
open import Data.Nat.Properties using (suc-injective)
open import Data.Fin using (Fin; splitAt; inject+)
open import Relation.Binary.PropositionalEquality
  using (_≡_; subst; sym; refl; trans; cong)
open import Data.Sum using (inj₁; map)
open import Function using (id)

splitAt-inj₁ : ∀{k}(m : Fin k) → splitAt k (inject+ 0 m) ≡ inj₁ m
splitAt-inj₁ Fin.zero = refl
splitAt-inj₁ (Fin.suc m) = cong (map Fin.suc id) (splitAt-inj₁ m)

subst-zero : ∀{k k'}(p : ℕ.suc k ≡ ℕ.suc k')
  → subst Fin p Fin.zero ≡ Fin.zero
subst-zero refl = refl

subst-suc : ∀{k k'}(m : Fin k)(p : k ≡ k')(q : ℕ.suc k ≡ ℕ.suc k') 
  → subst Fin q (Fin.suc m) ≡ Fin.suc (subst Fin p m)
subst-suc m refl refl = refl

subst-inject+ : ∀{k n}(m : Fin k)(p : k ≡ k + n) → subst Fin p m ≡ inject+ n m
subst-inject+ Fin.zero    p = subst-zero p
subst-inject+ (Fin.suc m) p =
  trans (subst-suc m (suc-injective p) p)
        (cong Fin.suc (subst-inject+ m (suc-injective p)))
        
lemma : (k : ℕ)(m : Fin k)(p : k ≡ k + 0) → splitAt k (subst Fin p m) ≡ inj₁ m
lemma k m p = trans (cong (splitAt k) (subst-inject+ m p)) (splitAt-inj₁ m)

Nice!