Structural Induction

How we express and prove properties on ADTs?

The list data type

A user defined list,

data L a = N | C a (L a) {-@ data L [length] a = N | C { hd :: a, tl :: L a} @-}

with its anchored size function.

{-@ measure length @-} {-@ length :: L a -> Nat @-} length N = 0 length (C _ xs) = 1 + length xs

Reflection of ADTs into the logic

The Liquid pragma

{-@ LIQUID "--exact-data-cons" @-}

Automatically creates checker and selector measures:

isN :: L a -> Bool
isC :: L a -> Bool

select_C_1 :: L a -> a
select_C_2 :: L a -> L a

Q: Do these function types look familiar?

Reflection of Structural Inductive Functions

With the above measures, map reflects into logic!
{-@ reflect map @-} map :: (a -> b) -> L a -> L b map f N = N map f (C x xs) = f x C map f xs

The body of map reflects in its result type
map :: f:(a->b) -> xs:L a
-> {v:L a | v == map f xs
&& v == if isN xs then N else
C (f (select_C_1 xs)
(map f (select_C_2 xs))
}

Reflection of Non Recursive Functions

Non-recursive functions reflect too!

{-@ reflect id @-} id :: a -> a id x = x {-@ reflect compose @-} compose :: (b -> c) -> (a -> b) -> a -> c compose f g x = f (g x)

Get automatically the "singleton" Liquid Types:

id :: x:a -> {v:a | v == id x && v == x}

compose :: f:(b -> c) -> g:(a -> b) -> x:a
-> {v:c | v == compose f g x && v == f (g x)}

Functor Laws: Identity

Lets prove the identity functor law!

{-@ mapId :: xs:L a -> { map id xs == id xs } @-} mapId N = map id N ==. N ==. id N *** QED mapId (C x xs) = map id (C x xs) ==. id x C map id xs ==. x C map id xs ==. x C id xs ? mapId xs ==. x C xs ==. id (x C xs) *** QED

Proof:

• Case splitting, and
• recursive call!

Functor Laws: Distribution

Lets prove the distribution functor law!

Or, mapFusion!

{-@ mapFusion :: f:(b -> c) -> g:(a -> b) -> xs:L a -> { map (compose f g) xs == (compose (map f) (map g)) (xs) } @-} mapFusion f g xs = trivial

Hints (surprise!)

• Case splitting, and
• recursive call!

Functor Laws: Distribution, Solution

Here is the proof:

mapFusion f g N
=   map (compose f g) N
==. N
==. map f N
==. map f (map g N)
==. (compose (map f) (map g)) N
*** QED
mapFusion f g (C x xs)
=   map (compose f g) (C x xs)
==. (compose f g) x C map (compose f g) xs
==. compose f g x   C map (compose f g) xs
==. f (g x) C (compose (map f) (map g)) xs
? mapFusion f g xs
==. f (g x) C compose (map f) (map g) xs
==. f (g x) C (map f) ((map g) xs)
==. f (g x) C map f (map g xs)
==. map f (g x C map g xs)
==. map f (map g (C x xs))
==. compose (map f) (map g) (C x xs)
*** QED

Onto Monoid Laws

Reflect the monoid list operators

{-@ reflect append @-} append :: L a -> L a -> L a append N ys = ys append (C x xs) ys = x C append xs ys {-@ reflect empty @-} empty :: L a empty = N

Monoid Laws: Left Identity

Lets prove the left identity monoid law!

{-@ emptyLeft :: x:L a -> { append empty x == x } @-} emptyLeft x = trivial

Hints:

• Rewrite!

Monoid Laws: Left Identity, Solution

Here is the proof:
emptyLeft x
= append empty x ==. append N x ==. x  *** QED

Monoid Laws: Right Identity

Lets prove the right identity monoid law!

{-@ emptyRight :: x:L a -> { append x empty == x } @-} emptyRight x = trivial

Hints (surprise, surprise!)

• Case splitting, and
• Recursive call!

Monoid Laws: Right Identity, Solution

Here is the proof:
emptyRight N
=   append N empty
==. append N N
==. N
*** QED

emptyRight (C x xs)
=   append (C x xs) empty
==. x C append  xs empty
==. x C xs                ? emptyRight xs
*** QED

Monoid Laws: Associativity

Lets prove the associativity monoid law!

{-@ appendAssoc :: xs:L a -> ys:L a -> zs:L a -> {append xs (append ys zs) == append (append xs ys) zs } @-} appendAssoc N ys zs = append N (append ys zs) ==. append ys zs ==. append (append N ys) zs *** QED appendAssoc (C x xs) ys zs = append (C x xs) (append ys zs) ==. x C append xs (append ys zs) ==. x C append (append xs ys) zs ? appendAssoc xs ys zs ==. append (x C append xs ys) zs ==. append (append (C x xs) ys) zs *** QED

Proof (surprise!)

• Case splitting, and
• recursive call.

{-@ reflect return @-} return :: a -> L a return x = C x N {-@ reflect bind @-} bind :: L a -> (a -> L b) -> L b bind N _ = N bind (C x xs) f = append (f x) (bind xs f)

Monoid Laws: Left Identity

Lets prove the left identity monad law!

{-@ leftIdentity :: x:a -> f:(a -> L b) -> { bind (return x) f == f x } @-} leftIdentity x f = bind (return x) f ==. bind (C x N) f ==. append (f x) (bind N f) ==. append (f x) N ==. append (f x) empty ==. f x *** QED

Hint

• emptyRight on f x

Here is the proof:
leftIdentity x f
=   bind (return x) f
==. bind (C x N) f
==. append (f x) (bind N f)
==. append (f x) N
==. append (f x) empty
==. f x                    ? emptyRight (f x)
*** QED

Monoid Laws: Right Identity

Lets prove the right identity monad law!

{-@ rightIdentity :: x:L a -> { bind x return == x } @-} rightIdentity N = bind N return ==. N *** QED rightIdentity (C x xs) = bind (C x xs) return ==. return x append bind xs return ==. (C x N) append bind xs return ==. (C x N) append xs ? rightIdentity xs ==. C x (append N xs) ? emptyLeft xs ==. C x xs *** QED

Proof

• Case splitting,
• Recursive call, and
• emptyLeft on xs.

Monoid Laws: Associativity

To prove associativity, lets assume two helper lemmata!

• Beta Equivalence on bind
βequivalence :: f:(a -> L b) -> g:(b -> L c) -> x:a ->
{bind (f x) g == (\y:a -> bind (f y) g) (x)}

• Bind distribution
bindAppend :: xs:L a -> ys:L a -> f:(a -> L b)
-> { bind (append xs ys) f == append (bind xs f) (bind ys f) }

Monoid Laws: Associativity

Lets prove the associativity monad law!

{-@ associativity :: m:L a -> f: (a -> L b) -> g:(b -> L c) -> {bind (bind m f) g == bind m (\x:a -> (bind (f x) g)) } @-} associativity N f g = bind (bind N f) g ==. bind N g ==. N ==. bind N (\x -> (bind (f x) g)) *** QED associativity (C x xs) f g = bind (bind (C x xs) f) g ==. bind (append (f x) (bind xs f)) g ==. append (bind (f x) g) (bind (bind xs f) g) ? bindAppend (f x) (bind xs f) g ==. append (bind (f x) g) (bind xs (\x -> (bind (f x) g))) ? associativity xs f g ==. append ((\x -> bind (f x) g) x) (bind xs (\x -> (bind (f x) g))) ? βequivalence f g x ==. bind (C x xs) (\x -> (bind (f x) g)) *** QED

Hint

• Case splitting,
• recursive call, and
• use of two lemmata.

Proving the Beta Equivalence Lemma

- Proof requires assumptions for β-equivalence ...
{-@ βequivalence :: f:(a -> L b) -> g:(b -> L c) -> x:a -> {bind (f x) g == (\y:a -> bind (f y) g) (x)} @-} βequivalence f g x = trivial

... so, we teach SMT β-equivalence via Liquid pragma.

{-@ LIQUID "--betaequivalence" @-}

Proving the bind function Lemma

A final boring inductive proof...

bindAppend :: L a -> L a -> (a -> L b) -> Proof {-@ bindAppend :: xs:L a -> ys:L a -> f:(a -> L b) -> { bind (append xs ys) f == append (bind xs f) (bind ys f) } @-} bindAppend N ys f = bind (append N ys) f ==. bind ys f ==. append N (bind ys f) ==. append (bind N f) (bind ys f) *** QED bindAppend (C x xs) ys f = bind (append (C x xs) ys) f ==. bind (C x (append xs ys)) f ==. append (f x) (bind (append xs ys) f) ==. append (f x) (append (bind xs f) (bind ys f)) ∵ bindAppend xs ys f ==. append (append (f x) (bind xs f)) (bind ys f) ∵ appendAssoc (f x) (bind xs f) (bind ys f) ==. append (bind (C x xs) f) (bind ys f) *** QED

Summing up the proved laws

• Functor Laws
• Identity: map id == id
• Distribution: map (compose f g) == compose (map f) (map g)
• Monoid Laws
• Left Identity: append empty x == x
• Right Identity: append x empty == x
• Associativity: append xs (append ys zs) == append (append xs ys) zs
• Left Identity: bind (return x) f == f x
• Right Identity: bind x return == x
• Associativity: bind (bind m f) g == bind m (\x:a -> (bind (f x) g))

Recap

1. Refinements: Types + Predicates
2. Subtyping: SMT Implication
3. Measures: Specify Properties of Data
4. Termination: Use Logic to Prove Termination
5. Reflection: Allow Haskell functions in Logic.
6. Structural Induction: Proving Theorems on Lists!

Next: Case Study: MapReduce: Program Properties that matter!