Deriv.idr

module Deriv

import Control.Isomorphism

--
-- A type constructor df is the derivative of the type constructor f if for all x and e there exists d such
-- such that
--
-- f (x + e) ~ f x + e * (df x) + e^2 * d
--
-- ie. df approximates f up to a second order term at x.
--
-- DWit is a witness to this isomorphism at x and e.
--
data DWit : (f : Type -> Type) -> (df : Type -> Type) -> (x : Type) -> (e : Type) -> Type where
  dWit : (d : Type) -> (Iso (f (Either x e)) (Either (f x) (Either (e, df x) ((e, e), d)))) -> DWit f df x e

--
-- d is a witness to the fact that for any choice of x and e there exists an appropriate d
--
d : (Type -> Type) -> (Type -> Type) -> Type
d f df = (x : Type) -> (e : Type) -> DWit f df x e

--
-- As a first example, let's show that the derivative of a constant function is the constantly bottom function
--
data Const : (a : Type) -> (t : Type) -> Type where
  MkConst : a -> Const a t
  
runConst : { a : Type } -> { t : Type } -> Const a t -> a
runConst (MkConst a) = a

runConstInverseToMkConst : (x : Const a b) -> MkConst { t = b } (runConst x) = x      
runConstInverseToMkConst (MkConst a) = refl

--
-- Lemma: Const a b ~ a
--
constIso : Iso (Const a b) a
constIso = MkIso runConst MkConst (\x => refl) (\x => runConstInverseToMkConst x)

dUnit : d (Const a) (Const _|_)
dUnit = \x => \e => dWit _|_ ?dUnitProof

Deriv.dUnitProof = proof
  intros
  refine isoTrans
  refine constIso
  refine isoSym
  refine isoTrans
  refine eitherCongLeft
  refine constIso
  refine isoTrans
  refine eitherCongRight
  refine eitherCong
  refine isoTrans
  refine pairCongRight
  refine constIso
  refine pairBotRight
  refine pairBotRight
  refine isoTrans
  refine eitherCongRight
  refine eitherBotLeft
  refine eitherBotRight
  
--
-- The derivative of the identity functor is constantly unit
--
data Id : (a : Type) -> Type where
  MkId : a -> Id a
  
runId : { a : Type } -> Id a -> a
runId (MkId a) = a

runIdInverseToMkId : (x : Id a) -> MkId (runId x) = x     
runIdInverseToMkId (MkId a) = refl

--
-- Lemma: Id a ~ a
--
idIso : Iso (Id a) a
idIso = MkIso runId MkId (\x => refl) (\x => runIdInverseToMkId x)

dId : d Id (Const ())
dId = \x => \e => dWit _|_ ?dIdProof

Deriv.dIdProof = proof
  intros
  refine isoTrans
  refine idIso
  refine eitherCong
  exact (isoSym idIso)
  refine isoSym
  refine isoTrans
  refine eitherCong
  refine pairCongRight
  refine constIso 
  refine pairBotRight 
  refine isoTrans
  refine eitherBotRight 
  refine pairUnitRight 
  
--
-- Derivative of a sum is the sum of derivatives
--

data Sum : (f : Type -> Type) -> (g : Type -> Type) -> (a : Type) -> Type where
  MkSum : Either (f a) (g a) -> Sum f g a

runSum : Sum f g x -> Either (f x) (g x)
runSum (MkSum x) = x

runSumInverseToMkSum : (x : Sum f g a) -> MkSum (runSum x) = x     
runSumInverseToMkSum (MkSum x) = refl 

sumIso : Iso (Sum f g x) (Either (f x) (g x))
sumIso = MkIso runSum MkSum (\x => refl) (\x => runSumInverseToMkSum x)

dEither : d f1 df1 -> d f2 df2 -> d (Sum f1 f2) (Sum df1 df2)
dEither d1 d2 = \x => \e => let (dWit dt1 iso1) = d1 x e in
                            let (dWit dt2 iso2) = d2 x e in
                            dWit (Either dt1 dt2) ?dEitherProof

Deriv.dEitherProof = proof
  intros
  refine isoTrans
  refine sumIso
  refine isoTrans
  refine eitherCong
  refine iso1
  refine iso2
  refine isoSym
  refine isoTrans
  refine eitherCongLeft
  refine sumIso 
  refine isoTrans
  refine eitherCongRight
  refine eitherCongLeft
  refine pairCongRight
  refine sumIso 
  refine isoTrans
  refine eitherCongRight
  refine eitherCong
  refine distribRight
  refine distribRight
  refine isoTrans
  refine eitherAssoc
  refine isoTrans
  refine eitherCongRight
  refine eitherCongRight
  refine eitherAssoc
  refine isoSym
  refine isoTrans
  refine eitherAssoc 
  refine isoTrans
  refine eitherCongRight
  refine eitherAssoc 
  refine isoTrans
  refine eitherCongRight
  refine eitherComm
  refine isoTrans
  refine eitherCongRight
  refine eitherCongLeft
  refine eitherComm
  refine isoTrans
  refine eitherCongRight
  refine eitherAssoc 
  refine isoTrans
  refine eitherCongRight
  refine eitherAssoc 
  refine isoTrans
  refine eitherCongRight
  refine eitherCongRight
  refine eitherAssoc 
  refine eitherCongRight
  refine eitherCongRight
  refine isoSym
  refine isoTrans
  refine isoSym
  refine eitherAssoc
  refine isoTrans
  refine eitherCongLeft
  refine eitherComm
  refine isoTrans
  refine eitherAssoc 
  refine eitherCongRight
  refine isoTrans
  refine eitherComm
  refine isoTrans
  refine eitherCongLeft
  refine eitherComm
  refine isoTrans
  refine eitherAssoc 
  refine eitherCongRight 
  refine isoRefl