Types as Propositions, Programs as Proofs

A (Terminating) Program is a Proof

Classic Idea Curry-Howard, Propositions As Types

Types As Propositions


The Refined Type ...

\[\reft{v}{b}{P}\]

... corresponds to the Proposition

\[\mathit{P}\]

Types as Propositions: Example


The Refined Type ...

{-@ type OnePlusOneEqualsTwo = {v:() | 1 + 1 = 2} @-}

... corresponds to the Proposition

\[1 + 1 = 2\]

Programs As Proofs: Example


The Program ...

{-@ easyProof :: OnePlusOneEqualsTwo @-} easyProof = ()

... corresponds to a Proof that

\[1 + 1 = 2\]

Types as Propositions


The Refined Type ...

\[\bindx{n}{\Nat} \rightarrow \reft{v}{b}{P(n)}\]

... corresponds to the Proposition

\[\forall n \in \Nat.\ P(n)\]

Types as Propositions: Example


The Refined Type ...

{-@ type PlusCommutes = n:Int -> m:Int -> { n + m = m + n } @-}

... corresponds to the Proposition

\[\forall n, m.\ n + m = m + n\]

Programs As Proofs: Example


The Program ...

{-@ sillyProof :: PlusCommutes @-} sillyProof n m = ()

... corresponds to a Proof that

\[\forall n, m.\ n + m = m + n\]

Types as Propositions, Programs as Proofs


Code Math
Types are Propositions
Programs are Proofs

Those Proofs were Boring


Simple Arithmetic

Automatically proved by SMT Solver

Those Proofs were Boring


Simple Arithmetic

Automatically proved by SMT Solver


How about proofs about user-defined functions?

Beyond automatic SMT, but the user can write proofs

Theorems about Functions


{-@ reflect sum @-} {-@ sum :: n:Nat -> Int @-} sum 0 = 0 sum n = n + sum (n-1)

How can we prove the the theorems

\(\mathit{sum}(1) = 1\),

\(\mathit{sum}(2) = 3\),

\(\mathit{sum}(3) = 6\).

Refinement Reflection


The annotation

                          {-@ reflect sum @-}

Automatically gives sum the type

      sum :: n:Int -> {v:Int | v = if n == 0 then 0 else n + sum (n-1)}

... but sum is uninterpreted in the refinement logic.

Reflect Function into Output Type


The type of sum connects implementation and specification

sum :: n:Int -> {v:Int | v = if n == 0 then 0 else n + sum (n-1)}

... but sum is uninterpreted in the refinement logic.

Reflect Function into Output Type



The type of sum connects implementation and specification

sum :: n:Int -> {v:Int | v = if n == 0 then 0 else n + sum (n-1)}


Key Idea

"Calling" sum n reveals definition of sum n to the type checker.

Reflection at Result Type



{-@ sum3 :: _ -> { sum 3 == 6 } @-} sum3 _ = let s0 = sum 0 -- s0 :: {sum 0 = 0 } s1 = sum 1 -- s1 :: {sum 1 = 1 + sum 0} -- s2 = sum 2 -- s2 :: {sum 2 = 2 + sum 1} s3 = sum 3 -- s3 :: {sum 3 = 3 + sum 2} in () -- SMT connects the dots.

Key Idea

"Calling" sum n reveals definition of sum n to the type checker.

Structuring Proofs as Calculations



Using combinators from ProofCombinators

            (===) :: x:a -> y:{a | y == x} -> {v:a|v == x && v == y}

Require both sides are equal

Ensure result is equal to both

Structuring Proofs as Calculations


Using combinators from ProofCombinators


{-@ sum3' :: _ -> { sum 3 = 6 } @-} sum3' _ = sum 3 === 3 + sum 2 === 3 + 2 + sum 1 === 3 + 2 + 1 + sum 0 === 6

Types as Propositions, Programs as Proofs


Code Math
Types are Theorems
Programs are Proofs

Reusing Proofs: Functions as Lemmas


Proofs are functions

Reusing Proofs: Functions as Lemmas


Proofs are functions

Reuse by calling the function

Reusing Proofs: Functions as Lemmas


Proofs are functions

Reuse by calling the function

{-@ sum4 :: _ -> { sum 4 = 10 } @-} sum4 _ = sum 4 === 4 + sum 3 === 4 + 6 ? sum3 () -- lemma { sum 3 == 6 } === 10

? is a library operator (read ``because'')

Adds the proposition sum3 () to the known facts (context)

Types as Propositions, Programs as Proofs


Code Math
Types are Theorems
Programs are Proofs

Types as Propositions, Programs as Proofs


Code Math
Types are Theorems
Programs are Proofs
Functions are Lemmas

Proof by Logical Evaluation


Long chains of calculations are tedious

Proof by Logical Evaluation


Long chains of calculations are tedious

Make the machine do the hard work!

An algorithm to emulate computation inside SMT logic (POPL18)

Proof by Logical Evaluation


Long chains of calculations are tedious

Make the machine do the hard work!

An algorithm to emulate computation inside SMT logic

{-@ sum3auto :: _ -> { sum 3 = 6 } @-} sum3auto _ = () {-@ sum4auto :: _ -> { sum 4 = 10 } @-} sum4auto _ = ()

Proof by Induction


Lets prove the theorem

\[\forall n.\ \sum_{i = 0}^n i = \frac{n \times (n + 1)}{2}\]

Proof by Induction


Lets prove the theorem

\[\forall n.\ \sum_{i = 0}^n i = \frac{n \times (n + 1)}{2}\]

that is

\[\forall n \in \Nat.\ 2 \times \mathit{sum}(n) = n \times (n + 1)\]

Proof by Induction

\[\forall n \in \Nat.\ 2 \times \mathit{sum}(n) = n \times (n + 1)\]

{-@ thm_sum :: n:Nat -> { 2 * sum n = n * (n+1) } @-} thm_sum :: Int -> () thm_sum 0 = () thm_sum n = thm_sum (n - 1)

Exercise: Lets calculate the proof!

Types as Propositions, Programs as Proofs


Code Math
Types are Theorems
Programs are Proofs
Functions are Lemmas

Types as Propositions, Programs as Proofs


Code Math
Types are Theorems
Programs are Proofs
Functions are Lemmas
Branches are Case-Splits

Types as Propositions, Programs as Proofs


Code Math
Types are Theorems
Programs are Proofs
Functions are Lemmas
Branches are Case-Splits
Recursion is Induction

Theorems about Data

Recall the list append function:

(++) :: [a] -> [a] -> [a] [] ++ ys = ys (x:xs) ++ ys = x : (xs ++ ys)

Lets prove that the operator is associative

{-@ type AppendAssoc a = xs:[a] -> ys:[a] -> zs:[a] -> {(xs ++ ys) ++ zs = xs ++ (ys ++ zs)} @-}

Theorems about Data: Associativity of append


Lets write fill in a calculational proof:

{-@ appendPf :: AppendAssoc a @-} appendPf :: [a] -> [a] -> [a] -> () appendPf [] ys zs = () appendPf (x:xs) ys zs = appendPf xs ys zs

Exercise: Lets fill the above in!

Types as Propositions, Programs as Proofs


Code Math
Types are Theorems
Programs are Proofs
Functions are Lemmas
Branches are Case-Splits
Recursion is Induction