Loop Invariants and Induction

Recall the higher-order loop function

43: loop :: Int -> Int -> a -> (Int -> a -> a) -> a
44: loop lo hi base f            = go lo base
45:   where go i acc | i < hi    = go (i+1) (f i acc)
46:                  | otherwise = acc

To verify output satisfies relation at hi we prove that if

base case initial accumulator base satisfies invariant at lo
- (p base lo)
induction step f preserves the invariant at i
- if (p acc i) then (p (f i acc) (i+1))
then "by induction" result satisfies invariant at hi
- (p (loop lo hi base f) hi)

Encoding Induction With Abstract Refinements

We capture induction with an abstract refinement type for loop

67: {-@ loop :: forall a <p :: Int -> a -> Prop>.
68:              lo:Int 
69:           -> hi:{v:Int|lo <= v}
70:           -> base:a<p lo> 
71:           -> f:(i:Int -> a<p i> -> a<p (i+1)>) 
72:           -> a<p hi>
73:   @-}

p is the index dependent invariant!

79: p     :: Int -> a -> Prop>                  -- ind  hyp 
80: base  :: a<p lo>                            -- base case 
81: f     :: (i:Int -> a<p i> -> a <p (i+1)>)   -- ind. step
82: out   :: a<p hi>                            -- output holds at hi

Encoding Induction With Abstract Refinements

Lets revisit

90: add n m = loop 0 m n (\_ z -> z + 1)

The invariant is: p instantiated with \i acc -> acc = i + n

base case: (p 0 n) holds as n = 0 + n

ind. step \_ z -> z + 1 preserves invariant

acc = i + n implies acc + 1 = (i + 1) + n

output hence, loop 0 m n (\_ z -> z + 1) = m + n

Which lets us verify that

106: add :: n:Nat -> m:Nat -> {v:Int| v = m + n}

Structural Induction With Abstract Refinements

Same idea applies for induction over structures

We define a foldr function that resembles loop.

118: {-@ foldr :: forall a b <p :: L a -> b -> Prop>. 
119:                 (xs:L a -> x:a -> b <p xs> -> b <p (Measures.C x xs)>) 
120:               -> b <p Measures.N> 
121:               -> ys: L a
122:               -> b <p ys>
123:   @-}
124: foldr :: (L a -> a -> b -> b) -> b -> L a -> b
125: forall a b <p :: (Measures.L a)-> b-> Bool>.
(xs:(Measures.L a)
 -> x:a
 -> {VV : b<p xs> | true}
 -> forall [ex:{VV : (Measures.L a) | (VV == (Measures.C x xs))}].{VV : b<p ex> | true})
-> forall [ex:{VV : (Measures.L a) | (VV == (Measures.N))}].{VV : b<p ex> | true}
-> ys:(Measures.L a)
-> {VV : b<p ys> | true}foldr xs:(Measures.L a)
-> x:a
-> {VV : b | ((papp2 p VV xs))}
-> forall [ex:{VV : (Measures.L a) | (VV == (Measures.C x xs))}].{VV : b | ((papp2 p VV ex))}f forall [ex:{VV : (Measures.L a) | (VV == (Measures.N))}].{VV : a | ((papp2 p VV ex))}b N        = forall [ex:{VV : (Measures.L a) | (VV == (Measures.N))}].{VV : a | ((papp2 p VV ex))}b
126: foldr f b (C x xs) = xs:(Measures.L a)
-> x:a
-> {VV : b | ((papp2 p VV xs))}
-> forall [ex:{VV : (Measures.L a) | (VV == (Measures.C x xs))}].{VV : b | ((papp2 p VV ex))}f {VV : (Measures.L {VV : a | (x <= VV)}) | (VV == xs)}xs {VV : a | (VV == x)}x (forall <p :: (Measures.L a)-> b-> Bool>.
(xs:(Measures.L {VV : a | (VV >= x)})
 -> x:{VV : a | (VV >= x)}
 -> {VV : b<p xs> | true}
 -> forall [ex:{VV : (Measures.L {VV : a | (VV >= x)}) | (VV == (Measures.C x xs))}].{VV : b<p ex> | true})
-> forall [ex:{VV : (Measures.L {VV : a | (VV >= x)}) | (VV == (Measures.N))}].{VV : b<p ex> | true}
-> ys:(Measures.L {VV : a | (VV >= x)})
-> {VV : b<p ys> | true}foldr xs:(Measures.L a)
-> x:a
-> {VV : b | ((papp2 p VV xs))}
-> forall [ex:{VV : (Measures.L a) | (VV == (Measures.C x xs))}].{VV : b | ((papp2 p VV ex))}f forall [ex:{VV : (Measures.L a) | (VV == (Measures.N))}].{VV : a | ((papp2 p VV ex))}b {VV : (Measures.L {VV : a | (x <= VV)}) | (VV == xs)}xs)

base case b is related to nil N
ind. step f extends relation over cons C
output relation holds over entire list ys

Structural Induction With Abstract Refinements

We can now verify

143: {-@ size :: xs:L a -> {v: Int | v = (llen xs)} @-}
144: size :: L a -> Int
145: forall a.
xs:(Measures.L a) -> {VV : (GHC.Types.Int) | (VV == (llen xs))}size = forall <p :: (Measures.L a)-> (GHC.Types.Int)-> Bool>.
(xs:(Measures.L a)
 -> x:a
 -> {VV : (GHC.Types.Int)<p xs> | (VV >= 0)}
 -> forall [ex:{VV : (Measures.L a) | (VV == (Measures.C x xs))}].{VV : (GHC.Types.Int)<p ex> | (VV >= 0)})
-> forall [ex:{VV : (Measures.L a) | (VV == (Measures.N))}].{VV : (GHC.Types.Int)<p ex> | (VV >= 0)}
-> ys:(Measures.L a)
-> {VV : (GHC.Types.Int)<p ys> | (VV >= 0)}foldr (x1:(Measures.L a)
-> a
-> n:{VV : (GHC.Types.Int) | (VV == (llen x1)) && (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV == (n + 1)) && (VV > 0) && (VV > n) && (VV >= 0)}\_ _ {VV : (GHC.Types.Int) | (VV >= 0)}n -> {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ {VV : (GHC.Types.Int) | (VV == (1  :  int))}1) {VV : (GHC.Types.Int) | (VV == (0  :  int))}0

Here, the relation

(p xs acc)

is automatically instantiated with

acc = (llen xs)

Structural Induction With Abstract Refinements

Similarly we can now verify

164: {-@ ++ :: xs:L a -> ys:L a -> {v:L a | (llen v) = (llen xs) + (llen ys)} @-} 
165: xs ++ ys = foldr (\_ z zs -> C z zs) ys xs

Here, the relation

(p xs acc)

is automatically instantiated with

(llen acc) = (llen xs) + (llen ys)

Inductive Refinements

`loop` Revisited

Loop Invariants and Induction

Inductive Refinements

Inductive Refinements

loop Revisited

Loop Invariants and Induction

Encoding Induction With Abstract Refinements

Encoding Induction With Abstract Refinements

Structural Induction With Abstract Refinements

Structural Induction With Abstract Refinements

Structural Induction With Abstract Refinements

`loop` Revisited