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.










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!

{-@ 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










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!

{-@ 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
  • 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



  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!