[anonymous-sums](http://hackage.haskell.org/package/anonymous-sums) in Idris

anonsum.idr

module anonsum
import Syntax.PreorderReasoning
import Data.HVect

%default total

data Sum : Vect n Type -> Type where
  Inj : (k : Fin n) -> index k ts -> Sum ts

cons : a -> List a -> List a
cons = (::)

mapIndexCommute : (f : a -> b) -> (m : Fin n) -> (xs : Vect n a) -> f (index m xs) = index m (map f xs)
mapIndexCommute f m [] = FinZElim m
mapIndexCommute f fZ (x :: xs) = refl
mapIndexCommute f (fS k) (x :: xs) = mapIndexCommute f k xs

replaceAtMapCommute : (f : a -> b) -> (n : Fin m) -> (ts : Vect m a) -> replaceAt n (f (index n ts)) (map f ts) = map f ts
replaceAtMapCommute f n [] = FinZElim n
replaceAtMapCommute f fZ (x :: xs) = refl
replaceAtMapCommute f (fS y) (x :: xs) = cong $ replaceAtMapCommute f y xs

partitionSum : {ts : Vect n Type} -> List (Sum ts) -> HVect (map List ts)
partitionSum {ts = []} _ = []
partitionSum {ts = t :: ts} [] = [] :: partitionSum []
partitionSum {ts = ts} (Inj n a :: as) = 
  replace (replaceAtMapCommute List n ts) $
  updateAt n (replace {P = \a => a -> List (index n ts)} (mapIndexCommute List n ts) $ cons a)
  (partitionSum as)

lemma_caseSum : (z : Type) -> (m : Fin n) -> (ts : Vect n Type) -> index m (map (\a => a -> z) ts) = (index m ts -> z)
lemma_caseSum z m [] = FinZElim m
lemma_caseSum z fZ (x :: xs) = refl
lemma_caseSum z (fS y) (x :: xs) = lemma_caseSum z y xs

lemma_mapSum : (ts, ts' : Vect n Type) -> (m : Fin n) ->
               index m (zipWith (\a, b => a -> b) ts ts') = (index m ts -> index m ts')
lemma_mapSum [] [] m = FinZElim m
lemma_mapSum (x :: xs) (y :: ys) fZ = refl
lemma_mapSum (x :: xs) (y :: ys) (fS z) = lemma_mapSum xs ys z

caseSum : {ts : Vect n Type} -> HVect (map (\a => a -> z) ts) -> Sum ts -> z
caseSum {z = z} {ts = ts} fs (Inj k a) = 
  replace { P = id } (lemma_caseSum z k ts) (index k fs) a

mapSum : {ts, ts' : Vect n Type} -> HVect (zipWith (\a, b => a -> b) ts ts') -> Sum ts -> Sum ts'
mapSum {ts = ts} {ts' = ts'} fs (Inj k a) = 
  Inj k (replace {P = id} (lemma_mapSum ts ts' k) (index k fs) a)