Structural Induction

The list data type

A user defined list,

with its anchored size function.

Reflection of ADTs into the logic

The Liquid pragma

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

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!

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!

Proof:

• Case splitting, and
• recursive call!

Functor Laws: Identity

Pretty Verbose Proof: Proof Automation!

Proof Generation:

• Automatic Unfolding, but
• Manual case splitting.

Functor Laws: Distribution

Lets prove the distribution functor law!

Or, mapFusion!

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

Monoid Laws: Left Identity

Lets prove the left identity monoid law!

Hints:

• Rewrite!

Monoid Laws: Left Identity, Solution

emptyLeft x 
  = append empty x ==. append N x ==. x  *** QED 

Monoid Laws: Right Identity

Lets prove the right identity monoid law!

Hints (surprise, surprise!)

• Case splitting, and
• Recursive call!

Monoid Laws: Right Identity, Solution

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!

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.

Onto Monad Laws!

Define monad list operators

Monoid Laws: Left Identity

Lets prove the left identity monad law!

Hint

• emptyRight on f x

Monad Laws: Left Identity, Solution

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!

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

Monoid Laws: Associativity

Lets prove the associativity monad law!

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 ...

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

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!