How to implement mathematics induction on Haskell

Question

data Nat = Zero | Succ Nat
type Predicate = (Nat -> Bool)

-- forAllNat p = (p n) for every finite defined n :: Nat

implies :: Bool -> Bool -> Bool
implies p q = (not p) || q 

basecase :: Predicate -> Bool
basecase p = p Zero 

jump :: Predicate -> Predicate
jump p n = implies (p n) (p (Succ n)) 

indstep :: Predicate -> Bool
indstep p = forallnat (jump p) 

Question:

Prove that if basecase p and indstep p, then forAllNat p

What I do not understand is that if basecase p and indstep p, so forAllNat p should be True, of course.

I think basecase p says that P(0) is true, and indstep p says that P(Succ n) which is P(n+1) is true And we need to prove P(n) is true. Am I right? Any suggestion about how to do this?

Answer 1

As Benjamin Hodgson indicates, you can't quite prove that in Haskell. However, you can prove a statement with slightly stronger preconditions. I'll also ignore the unnecessary complexity of Bool.

{-# LANGUAGE GADTs, KindSignatures, DataKinds, RankNTypes, ScopedTypeVariables #-}

data Nat = Z | S Nat

data Natty :: Nat -> * where
  Zy :: Natty 'Z
  Sy :: Natty n -> Natty ('S n)

type Base (p :: Nat -> *) = p 'Z
type Step (p :: Nat -> *) = forall (n :: Nat) . p n -> p ('S n)

induction :: forall (p :: Nat -> *) (n :: Nat) .
             Base p -> Step p -> Natty n -> p n
induction b _ Zy = b
induction b s (Sy n) = s (induction b s n)