Programs are Proofs

From previous lecture:

fibMono :: n:Nat -> m:{Nat | n < m }  -> {fib n <= fib m}
fibMono     = fMono fib fibUp

Can we prove any (higher order) logical property?

Logical Properties


Like programming languages, logic has

  • syntax (e,∧,∨,¬,⇒,∀,∃),
  • meaning (If φ and ψ hold, then φ∧ψ holds), and
  • "evaluation" (decision procedures).

Natural Deduction ...


... is a decision procedure for logic.


Curry Howard Correspondence

Propositions <~> Refinement Types

Natural Deduction <~> Lambda Calculus (here Haskell)

Motivation

Propositions <~> Refinement Types

Logic as Types: Native Terms

e <~> {v:() | e}

{-@ fact1 :: {v:() | 2 == 1 + 1 } @-} fact1 = ()
{-@ fact2 :: {v:() | 2 /= 3 } @-} fact2 = ()

Propositions <~> Refinement Types

Logic as Types: Conjunction as Pairs

ϕ1 ∧ ϕ2 <~> (ϕ1,ϕ2)

{-@ conj :: ϕ1:{Bool | ϕ1 } -> ϕ2:{Bool | ϕ2 } -> {v:(Bool, Bool) | ϕ1 && ϕ2} @-} conj ϕ1 ϕ2 = (ϕ1,ϕ2)

If you know ϕ1 and ϕ2 hold...

then (ϕ1,ϕ2) is a λ-term that shows ϕ1 ∧ ϕ2 holds.

Typing Pairs



Q: How do we type right?

Typing Pairs

Conjunction <~> Pairs

Natural Deduction for Conjunction

Conjunction Example: Natural Deduction

Conjunction Example: Isomorphism


Conjunction Example in Practise

Let's prove: ϕconj ≡ ϕ1, φ2 ∧ ϕ3 |- φ1 ∧ ϕ3


{-@ ex1 :: φ1:Bool -> φ2:Bool -> φ3:Bool -> {v:() | φ1} -> ({v:() | φ2}, {v:() | φ3}) -> ({v:() | φ1}, {v:() | φ3}) @-} ex1 _ _ _ x1 x23 = (x1, case x23 of (x2,x3) -> x3)

Propositions <~> Refinement Types

Logic as Types: Disjunction as Either

ϕ1 ∨ ϕ2 <~> Either ϕ1 ϕ2

where data Either a b = Left a | Right b.

{-@ disj :: φ1:Bool -> φ2:Bool -> {v:() | φ1 || φ2 } -> {v:Either () () | φ1 || φ2} @-} disj φ1 φ2 p | φ1 = Left p | φ2 = Right p

If you know ϕ1 or ϕ2 holds...

then Left ϕ1 and Right ϕ2 are λ-terms that shows ϕ1 ∨ ϕ2 holds.

Rules for Disjunction


Propositions <~> Refinement Types

Logic as Types: Implication as Function


Modus Ponens ...


... is another name for the Implication Elimination Rule.

Propositions <~> Refinement Types

Logic as Types: Negation as Impication

Negetion is just implication to False!

Propositions <~> Refinement Types

Logic as Types: Forall as Function

Propositions <~> Refinement Types

Logic as Types: Exists as Pair

Propositions <~> Refinement Types

Q: Can you encode the follοwing? ϕ ≡ (∃x.∀y.(p x y)) ⇒ (∀y.∃x.(p x y))

Example existsAll Encoded

{-@ exAll :: p:(a -> a -> Bool) -> (x::a, y:a -> {v:() | p x y}) -> y:a -> (x::a, {v:() | p x y}) @-} exAll p = undefined

Q: Can you define exAll?

Example existsAll in Natural Deduction


Example II: Distributing Qualifiers

Let's prove: ϕ∃ ≡ (∃x.p x ∨ q x) ⇒ ((∃x.p x) ∨ (∃x.q x))

{- exDistOr :: p : _ -> q : _ @-} exDistOr = undefined

Example III: Distributing Qualifiers

Let's prove: ϕ∀ ≡ (∀x.p x ∧ q x) ⇒ ((∀x.p x) ∧ (∀x.q x))

{- allDistAnd :: p : _ -> q : _ @-} allDistAnd = undefined

Example IV: Lists

Let's prove: ∀xs.((∃ys. xs = ys ++ ys) ⇒ (∃n.length xs = n + n))

{- evenLen :: xs:_ @-} evenLen = undefined
Hint: You can use
{-@ lenAppend :: xs : L a -> ys : L a -> { length ( xs ++ ys ) = length xs + length ys } @-}

Example V: Natural Induction

Let's prove: ϕind ≡ (p 0 ∧ (∀n.p (n − 1) ⇒ p n) ⇒ ∀n.p n)

ind = undefined

Summing up

Natural Deduction Proofs <~> Lambda Calculus (here Haskell)

Propositions <~> Refinement Types

Further Reading:

Propositions as Types, by Wadler & Refinement Reflection, by me et al.

List Helpers

{-@ LIQUID "--higherorder" @-} {-@ LIQUID "--exact-data-con" @-} {-@ LIQUID "--automatic-instances=liquidinstances" @-} {-@ lenAppend :: xs : L a -> ys : L a -> { length ( xs ++ ys ) = length xs + length ys } @-} lenAppend :: L a -> L a -> () lenAppend N _ = () lenAppend (C x xs) ys = lenAppend xs ys data L a = N | C a (L a) {-@ data L [length] a = N | C {hd :: a, tl :: L a} @-} length :: L a -> Int {-@ length :: x:L a -> {v:Nat | v == length x} @-} {-@ measure length @-} length N = 0 length (C _ xs) = 1 + length xs {-@ reflect ++ @-} N ++ ys = ys (C x xs) ++ ys = C x (xs ++ ys)

Appendix

fact1 :: () fact2 :: () conj :: Bool -> Bool -> (Bool,Bool) disj :: Bool -> Bool -> () -> Either () () ex1 :: Bool -> Bool -> Bool -> () -> ((),()) -> ((),()) exAll :: (a -> a -> Bool) -> (a, a -> ()) -> a -> (a, ()) exDistOr :: (a -> Bool) -> (a -> Bool) -> (a, Either c d) -> Either (a, c) (a,d) allDistAnd :: (a -> Bool) -> (a -> Bool) -> (a -> (b,c)) -> (a -> b, a -> c) ind :: (Int -> Bool) -> ((), Int -> () -> ()) -> Int -> () evenLen :: L a -> (L a, Proof) -> (Int, Proof)