## Encoding Natural Deduction

Let's see how natural deduction is encoded as type derivation!

module NaturalDeduction where {-@ LIQUID "--higherorder" @-} {-@ LIQUID "--exact-data-con" @-} import Language.Haskell.Liquid.ProofCombinators import Prelude hiding ((++), length) {-@ infix ++ @-}

## Natural Deduction as Type Derivation

For example, the or-elimination rule

becomes

## Exists over Forall in Natural Deduction

ϕ ≡ (∃x.∀y.(p x y)) ⇒ (∀y.∃x.(p x y))

Read bottom up, it is a proof!

## Exists over Forall in Natural Deduction

ϕ ≡ (∃x.∀y.(p x y)) ⇒ (∀y.∃x.(p x y))

λe y.case e of {(x, ex ) → (x, ex y)}

Read top down, we get a proof term!

## Exists over Forall in Haskell!

ϕ ≡ (∃x.∀y.(p x y)) ⇒ (∀y.∃x.(p x y))

λe y.case e of {(x, ex ) → (x, ex y)}

{-@ exAll :: p:(a -> a -> Bool) -> (x::a, y:a -> {v:Proof | p x y}) -> y:a -> (x::a, {v:Proof | p x y}) @-} exAll p = \e y -> case e of {(x, ex) -> (x, ex y)}

## Distributing Existentials

ϕ∃ ≡ (∃x.p x ∨ q x) ⇒ ((∃x.p x) ∨ (∃x.q x))

{-@ exDistOr :: p : _ -> q : _ -> (x :: a ,Either {v:b | p x } {v:c | q x }) -> Either (x::a , {v:b | p x }) (x::a , {v:c | q x }) @-} exDistOr _ _ (x, Left px) = Left (x, px) exDistOr _ _ (x, Right qx) = Right (x, qx)

## Distributing Universals

ϕ∀ ≡ (∀x.p x ∧ q x) ⇒ ((∀x.p x) ∧ (∀x.q x))

{-@ allDistAnd :: p:_ -> q:_ -> (x:a -> ({v:Bool | p x }, {v:Bool| q x})) -> ((x:a -> {v:Bool | p x }), (x:a -> {v:Bool| q x })) @-} allDistAnd _ _ andx = ((\x -> case andx x of (px, _ ) -> px) ,(\x -> case andx x of (_ , qx) -> qx))

Let's use SMT to simplify the proof!

## Properties of User Defined Datatypes

ϕ ≡ ∀xs.((∃ys. xs = ys ++ ys) ⇒ (∃n.length xs = n + n))

{-@ evenLen :: xs:_ -> (ys::L a, {v:Proof | xs = ys ++ ys }) -> (n ::Int, {v:Proof | length xs = n + n }) @-} evenLen xs (ys, pf) = (length ys, lenAppend ys ys &&& pf )
where
{-@ lenAppend :: xs:_ -> ys:_ -> { length (xs ++ ys) = length xs + length ys } @-}

## Induction on Natural Numbers

ϕind ≡ (p 0 ∧ (∀n.p (n − 1) ⇒ p n) ⇒ ∀n.p n)

{-@ ind :: p:_ -> ({v:Proof| p 0}, (n:Nat -> {v:Proof | p (n-1)} -> {v:Proof | p n})) -> n:Nat -> {v:Proof | p n} @-} ind p (p0, pn) n | n == 0 = p0 | otherwise = pn n (ind p (p0, pn) (n-1))

## Summary:

• Refinement Reflection and Proof by Logical Evaluation combined ...

• ... allow for complete verification with SMT-automation!

• Case Study: MapReduce Equivalence
• Case Study: Encoding Natural Deduction

The appending function (++) is Haskell's usual append reflected in the logic.