Peano.hs

{-@ LIQUID "--higherorder"     @-}
{-@ LIQUID "--exact-data-cons" @-}
{-@ LIQUID "--higherorderqs" @-}

module Peano where

import Prelude hiding (plus)


import Language.Haskell.Liquid.ProofCombinators

-- Why do we need these?
zeroR     :: Peano -> Proof
zeroL     :: Peano -> Proof
plusAssoc :: Peano -> Peano -> Peano -> Proof
plusComm  :: Peano -> Peano -> Proof
plusSuccR :: Peano -> Peano -> Proof



data Peano = Z | S Peano

{-@ data Peano [toInt] = Z | S {prev :: Peano} @-}

{-@ measure toInt @-}
toInt :: Peano -> Int

{-@ toInt :: Peano -> Nat @-}
toInt Z     = 0
toInt (S n) = 1 + toInt n

{-@ axiomatize plus @-}
plus :: Peano -> Peano -> Peano
plus Z m     = m
plus (S n) m = S (plus n m)

{-@ zeroL :: n:Peano -> { plus Z n == n }  @-}
zeroL n
  =   plus Z n
  === n
  *** QED

{-@ zeroR :: n:Peano -> { plus n Z == n }  @-}
zeroR Z
  = plus Z Z
  === Z
  *** QED

zeroR (S n)
  =   plus (S n) Z
  === S (plus n Z)
    ? zeroR n
  === S n
  *** QED

{-@ plusSuccR :: n:Peano -> m:Peano -> { plus n (S m) = S (plus n m) } @-}
plusSuccR Z m
  =   plus Z (S m)
  === S m
  === S (plus Z m)
  *** QED

plusSuccR (S n) m
  =   plus (S n) (S m)
  === S (plus n (S m))
      ? plusSuccR n m
  === S (S (plus n m)) 
  === S (plus (S n) m)
  *** QED

{-@ plusComm :: a:_ -> b:_  -> {plus a b == plus b a} @-}
plusComm Z b
  =   plus Z b
      ? zeroR b
  === plus b Z 
  *** QED

plusComm (S a) b
  =   plus (S a) b
  === S (plus a b)
    ? plusComm a b
  === S (plus b a) 
    ? plusSuccR b a
  === plus b (S a)      
  *** QED

{-@ plusAssoc :: a:_ -> b:_ -> c:_ -> {plus (plus a b) c == plus a (plus b c) } @-}
plusAssoc Z b c
  =   plus (plus Z b) c
  === plus b c
  === plus Z (plus b c)
  *** QED

plusAssoc (S a) b c
  =   plus (plus (S a) b) c
  === plus (S (plus a b)) c
  === S (plus (plus a b) c)
    ? plusAssoc a b c
  === S (plus a (plus b c)) 
  === plus (S a) (plus b c)
  *** QED