# 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: Identity

Pretty Verbose Proof: Proof Automation!

{-@ LIQUID "--automatic-instances=liquidinstanceslocal" @-}
{-@ automatic-instances mapIdAuto @-} {-@ mapIdAuto :: xs:L a -> { map id xs == id xs } @-} mapIdAuto N = trivial mapIdAuto (C x xs) = mapIdAuto xs

Proof Generation:

• Automatic Unfolding, but
• Manual case splitting.

## Functor Laws: Distribution

Lets prove the distribution functor law!

Or, mapFusion!

{- automatic-instances 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!

{- automatic-instances emptyLeft @-} {-@ 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!

{- automatic-instances emptyRight @-} {-@ 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!

{- automatic-instances appendAssoc @-} {-@ appendAssoc :: xs:L a -> ys:L a -> zs:L a -> {append xs (append ys zs) == append (append xs ys) zs } @-} appendAssoc xs ys zs = trivial

## Monoid Laws: Associativity, Solution

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!

{- automatic-instances leftIdentity @-} {-@ leftIdentity :: x:a -> f:(a -> L b) -> { bind (return x) f == f x } @-} leftIdentity x f = trivial

Hint

• emptyRight on f x

## Monad Laws: Left Identity, Solution

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!

{- automatic-instances rightIdentity @-} {-@ rightIdentity :: x:L a -> { bind x return == x } @-} rightIdentity xs = trivial

Proof

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

## Monoid Laws: Right Identity, Solution

Lets prove the right identity monad law!

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


## Monoid Laws: Associativity

To prove associativity, lets assume a helper lemma!

• Bind distribution
{-@ automatic-instances bindAppend @-} {-@ 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 _ _ = trivial bindAppend (C x xs) ys f = appendAssoc (f x) (bind xs f) (bind ys f) &&& bindAppend xs ys f

## Monoid Laws: Associativity

Lets prove the associativity monad law!

{- automatic-instances associativity @-} {-@ 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 xs f g = trivial

## Monoid Laws: Associativity, Solution

Lets prove the associativity monad law!

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

• Explicit 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" @-}

## 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!