Puzzle.agda

module Puzzle where

open import Data.Nat using (ℕ; _+_; zero)
open import Data.Fin hiding (_+_)
open import Data.Fin.Properties
open import Function.Base using (id)
open import Relation.Binary.PropositionalEquality
open import Data.Sum using (map; inj₁)

splitAt-inj₁ : (k h : ℕ) (m : Fin k) → splitAt k (inject+ h m) ≡ inj₁ m
splitAt-inj₁ _ h zero = refl
splitAt-inj₁ _ h (suc m) = cong (map suc id) (splitAt-inj₁ _ h m)

inject+-subst : (k : ℕ)(m : Fin k)(p : k ≡ k + 0)
              → inject+ 0 m ≡ subst Fin p m
inject+-subst k m p = toℕ-injective
  (trans (sym (toℕ-inject+ 0 m)) (toℕ-subst (k + 0) p))
  where
    toℕ-subst : (k' : ℕ)(p : k ≡ k') → toℕ m ≡ toℕ (subst Fin p m)
    toℕ-subst .k refl = refl

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) (sym (inject+-subst k m p)))
  (splitAt-inj₁ k 0 m)

Nice. I've used all these ideas before, and yet it didn't occur to me to string them together in quite this way!