Theorem Proving

























Back to fib


module TheoremProving where {-@ LIQUID "--reflection" @-} import Language.Haskell.Liquid.Equational {-@ fib :: i:Int -> Int @-} fib :: Int -> Int fib i | i == 0 = 0 | i == 1 = 1 | otherwise = fib (i-1) + fib (i-2)













Reflect fib in the logic


{-@ reflect fib @-}

  • fib is terminating.

  • You can write fib in the refinements.

  • The logic does not know the definition of fib for all inputs (for decidable checking), but ...

  • ... calling fib i in Haskell unfolds the definition of fib on i in the logic.













Unfolding fib


{-@ fibEq :: () -> {v:() | fib 1 == 1 } @-} fibEq :: () -> () fibEq _ = let f1 = fib 1 -- f1:: { fib 1 == 1 } in const () (f1)

Q: Can you prove fib 2 == 1?













Let's make fibEq look like a proof


Using operators from Equational

{-@ fibEqPretty :: () -> { fib 2 == 1 } @-} fibEqPretty :: () -> () fibEqPretty _ = fib 2 ==. fib 1 + fib 0 ==. 1 + 0 *** QED













Using theorems as explanations


Using operators from Equational

{-@ fibThree :: () -> { fib 3 == 2 } @-} fibThree :: () -> () fibThree _ = fib 3 ==. fib 2 + fib 1 ? fibEqPretty () ==. 1 + 1 *** QED













Pen & Paper Proofs: fib is increasing


{-@ fibUp :: i:Nat -> {fib i <= fib (i+1)} @-} fibUp :: Int -> () fibUp i | i == 0 = fib 0 <. fib 1 *** QED | i == 1 = fib 1 <=. fib 1 + fib 0 <=. fib 2 *** QED | otherwise = fib i ==. fib (i-1) + fib (i-2) ? fibUp (i-1) <=. fib i + fib (i-2) ? fibUp (i-2) <=. fib i + fib (i-1) <=. fib (i+1) *** QED


















Ready for more? fib is monotonic

{-@ fMono :: x:Nat -> y:{Nat | x < y } -> {fib x <= fib y} @-} fMono :: Int -> Int -> () fMono x y | y == x + 1 = fib x ? fibUp x <=. fib (x+1) <=. fib y *** QED | x < y - 1 = fib x ? fMono x y <=. fib (y-1) ? fibUp (y-1) <=. fib y *** QED

Q: Can you fix the proof?

Q: Can you generalize for every increasing function?


















Theorem Application



fib is monotonic!

{-@ fibMono :: n:Nat -> m:{Nat | n < m } -> {fib n <= fib m} @-} fibMono :: Int -> Int -> () fibMono = undefined


















Recap


  • Liquid Haskell allows theorem proving within Haskell about Haskell functions!

    • Theorems are refinement types and

    • proofs are just Haskell functions!

  • Application: Verification of MapReduce


















Appendix
infixl 3 <., <=. {-@ (<=.) :: x:a -> y:{a | x <= y} -> {v:a | v == y && x <= v} @-} (<=.) :: a -> a -> a _ <=. x = x {-@ (<.) :: x:a -> y:{a | x < y} -> {v:a | v == y && x < v} @-} (<.) :: a -> a -> a _ <. x = x