# Inductive Refinements

```7: module Loop where
8: import Prelude hiding ((!!), foldr, length, (++))
9: import Measures
11: {-@ LIQUID "--no-termination" @-}
```

# `loop` Revisited

Recall the higher-order `loop` function

```21: loop :: Int -> Int -> a -> (Int -> a -> a) -> a
22: forall a <p :: (GHC.Types.Int)-> a-> Bool>.
lo:(GHC.Types.Int)
-> hi:{VV : (GHC.Types.Int) | (lo <= VV)}
-> {VV : a<p lo> | true}
-> (i:(GHC.Types.Int)
-> {VV : a<p i> | true}
-> forall [ex:{VV : (GHC.Types.Int) | (VV == (i + 1))}].{VV : a<p ex> | true})
-> {VV : a<p hi> | true}loop (GHC.Types.Int)lo {VV : (GHC.Types.Int) | (lo <= VV)}hi {VV : a | ((papp2 p VV lo))}base i:(GHC.Types.Int)
-> {VV : a | ((papp2 p VV i))}
-> forall [ex:{VV : (GHC.Types.Int) | (VV == (i + 1))}].{VV : a | ((papp2 p VV ex))}f            = i:{VV : (GHC.Types.Int) | (VV >= lo) && (VV <= hi) && (lo <= VV)}
-> {VV : a | ((papp2 p VV i))} -> {VV : a | ((papp2 p VV hi))}go {VV : (GHC.Types.Int) | (VV == lo)}lo {VV : a | ((papp2 p VV lo)) && (VV == base)}base
23:   where forall a.
lo:{VV : (GHC.Types.Int) | (VV == lo) && (VV <= hi)}
-> hi:{VV : (GHC.Types.Int) | (VV == hi) && (VV >= lo) && (VV >= lo) && (lo <= VV) && (lo <= VV)}
-> {VV : a | ((papp2 p VV lo)) && ((papp2 p VV lo)) && (VV == base)}
-> (x1:{VV : (GHC.Types.Int) | (VV >= lo) && (VV >= lo) && (VV < hi) && (VV < hi) && (lo <= VV) && (lo <= VV)}
-> {VV : a | ((papp2 p VV x1))}
-> {VV : a | ((papp2 p VV (x1 + 1)))})
-> i:{VV : (GHC.Types.Int) | (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (lo <= VV) && (lo <= VV)}
-> {VV : a | ((papp2 p VV i))}
-> {VV : a | ((papp2 p VV hi)) && ((papp2 p VV hi))}go {VV : (GHC.Types.Int) | (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (lo <= VV) && (lo <= VV)}i {VV : a | ((papp2 p VV i))}acc | {VV : (GHC.Types.Int) | (VV == i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (lo <= VV) && (lo <= VV)}i x1:{VV : (GHC.Types.Int) | (VV >= i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (i <= VV) && (lo <= VV) && (lo <= VV)}
-> x2:{VV : (GHC.Types.Int) | (VV >= i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (i <= VV) && (lo <= VV) && (lo <= VV)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 < x2))}< {VV : (GHC.Types.Int) | (VV == hi) && (VV == hi) && (VV >= lo) && (VV >= lo) && (lo <= VV) && (lo <= VV)}hi    = forall a.
lo:{VV : (GHC.Types.Int) | (VV == lo) && (VV <= hi)}
-> hi:{VV : (GHC.Types.Int) | (VV == hi) && (VV >= lo) && (VV >= lo) && (lo <= VV) && (lo <= VV)}
-> {VV : a | ((papp2 p VV lo)) && ((papp2 p VV lo)) && (VV == base)}
-> (x1:{VV : (GHC.Types.Int) | (VV >= lo) && (VV >= lo) && (VV < hi) && (VV < hi) && (lo <= VV) && (lo <= VV)}
-> {VV : a | ((papp2 p VV x1))}
-> {VV : a | ((papp2 p VV (x1 + 1)))})
-> i:{VV : (GHC.Types.Int) | (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (lo <= VV) && (lo <= VV)}
-> {VV : a | ((papp2 p VV i))}
-> {VV : a | ((papp2 p VV hi)) && ((papp2 p VV hi))}go ({VV : (GHC.Types.Int) | (VV == i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (lo <= VV) && (lo <= VV)}ix1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+{VV : (GHC.Types.Int) | (VV == (1  :  int))}1) (x1:{VV : (GHC.Types.Int) | (VV >= lo) && (VV >= lo) && (VV < hi) && (VV < hi) && (lo <= VV) && (lo <= VV)}
-> {VV : a | ((papp2 p VV x1))}
-> {VV : a | ((papp2 p VV (x1 + 1)))}f {VV : (GHC.Types.Int) | (VV == i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (lo <= VV) && (lo <= VV)}i {VV : a | ((papp2 p VV i)) && (VV == acc)}acc)
24:                  | otherwise = {VV : a | ((papp2 p VV i)) && (VV == acc)}acc
```

We used `loop` to write

```30:
31: {-@ add :: n:Nat -> m:{v:Int| v >= 0} -> {v:Int| v = m + n} @-}
32: add :: Int -> Int -> Int
33: n:{VV : (GHC.Types.Int) | (VV >= 0)}
-> m:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV == (m + n))}add {VV : (GHC.Types.Int) | (VV >= 0)}n {VV : (GHC.Types.Int) | (VV >= 0)}m = forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
lo:(GHC.Types.Int)
-> hi:{VV : (GHC.Types.Int) | (lo <= VV)}
-> {VV : (GHC.Types.Int)<p lo> | (VV >= 0) && (VV >= n) && (n <= VV)}
-> (i:(GHC.Types.Int)
-> {VV : (GHC.Types.Int)<p i> | (VV >= 0) && (VV >= n) && (n <= VV)}
-> forall [ex:{VV : (GHC.Types.Int) | (VV == (i + 1))}].{VV : (GHC.Types.Int)<p ex> | (VV >= 0) && (VV >= n) && (n <= VV)})
-> {VV : (GHC.Types.Int)<p hi> | (VV >= 0) && (VV >= n) && (n <= VV)}loop {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV == m) && (VV >= 0)}m {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n (x1:(GHC.Types.Int)
-> i:{VV : (GHC.Types.Int) | (VV == (x1 + n)) && (VV == (n + x1)) && (VV >= 0) && (VV >= x1) && (VV >= n) && (x1 <= VV) && (n <= VV)}
-> {VV : (GHC.Types.Int) | (VV == (i + 1)) && (VV > 0) && (VV > x1) && (VV > i) && (VV > n) && (VV >= 0) && (x1 <= VV) && (n <= VV)}\_ {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n) && (n <= VV)}i -> {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= n) && (n <= VV)}i x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ {VV : (GHC.Types.Int) | (VV == (1  :  int))}1)
```

Problem: Verification requires an index dependent loop invariant `p`

• Which relates index `i` with accumulator `acc`: formally `(p acc i)`

# 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)`