Structural Induction



How we express and prove properties on data types?

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


Question: 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))
       }

Prove fancy lists properties


  • 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


  • Monad Laws
    • 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



Termination: Well-founded Metrics
Reflection: Allow Haskell functions in Logic
tructural Induction: Proving Theorems on Lists



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

Appendix: 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)}

Proving Map-Identity


Optimization property: to map identity do not transverse the list!

{-@ 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 by case splitting and recursive call.

Automation: Proving Map-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.

Proving Map-Fusion


Optimization property: transverse the list only once!

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

Exercise: Can you prove map-fusion?

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

Monoid Laws: Right Identity


Lets prove the right identity monoid law!

{-@ automatic-instances emptyRight @-} {-@ emptyRight :: x:L a -> { append x empty == x } @-} emptyRight N = trivial emptyRight (C x xs) = emptyRight xs

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 N _ _ = trivial appendAssoc (C x xs) ys zs = appendAssoc xs ys zs

Onto Monad Laws!


Define monad list operators

{-@ 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 = emptyRight (f x)

Monoid Laws: Right Identity


Lets prove the right identity monad law!

{-@ automatic-instances rightIdentity @-} {-@ rightIdentity :: x:L a -> { bind x return == x } @-} rightIdentity N = trivial rightIdentity (C x xs) = rightIdentity xs &&& emptyLeft xs

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 N f g = trivial associativity (C x xs) f g = bindAppend (f x) (bind xs f) g &&& associativity xs f g