mprover-0.0.0.0: examples/Test.hs

module Test where

--
-- As a simple case, let's prove a theorem about lazy lists: namely, that
-- map (+1) zeros = ones (paraphrasing a bit, since we're technically talking
-- about Nats rather than Ints).
--
{ data List a = Nil | Cons a (List a)
; data Nat = Z | S Nat

; map :: (a -> b) -> List a -> List b
; map = \ f -> \ l -> case l of
                      { Nil         -> Nil
                      ; (Cons x xs) -> Cons (f x) (map f xs)
                      }

; ones = Cons (S Z) ones
; zeros = Cons Z zeros

; mapPlusOne ::: { map S zeros = ones }
; mapPlusOne = trans
                (eval ::: { map S zeros = Cons (S Z) (map S zeros) })
                (trans
                 (Cons (eval ::: { S Z = S Z }) (mapPlusOne ::: { map S zeros = ones }))
                 (eval ::: { Cons (S Z) ones = ones }))
}