Inductive Refinements

```7: module Loop where
8: import Prelude hiding ((!!), foldr, length, (++))
9: import SimpleRefinements
```

`loop` Revisited

Recall the higher-order `loop` function

```19: loop :: Int -> Int -> a -> (Int -> a -> a) -> a
20: 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            = x1:{VV : (GHC.Types.Int) | (VV == lo) && (VV <= hi)}
-> {VV : a | ((papp2 p VV lo)) && ((papp2 p VV x1)) && (VV == base)}
-> {VV : a | ((papp2 p VV hi))}go {VV : (GHC.Types.Int) | (VV == lo)}lo {VV : a | ((papp2 p VV lo)) && (VV == base)}base
21:   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 x:{VV : (GHC.Types.Int) | (VV >= i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (i <= VV) && (lo <= VV) && (lo <= VV)}
-> y:{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)) <=> (x < y))}< {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)}ix:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+{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)
22:                  | otherwise = {VV : a | ((papp2 p VV i)) && (VV == acc)}acc
```

We used `loop` to write

```28: {-@ add :: n:Nat -> m:Nat -> {v:Int| v = m + n} @-}
29: add :: Int -> Int -> Int
30: 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 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ {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
```40: loop :: Int -> Int -> a -> (Int -> a -> a) -> a
41: loop lo hi base f            = go lo base
42:   where go i acc | i < hi    = go (i+1) (f i acc)
43:                  | 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`

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

`p` is the index dependent invariant!
```76: p     :: Int -> a -> Prop>                  -- ind  hyp
77: base  :: a<p lo>                            -- base case
78: f     :: (i:Int -> a<p i> -> a <p (i+1)>)   -- ind. step
79: out   :: a<p hi>                            -- output holds at hi
```

Encoding Induction With Abstract Refinements

Lets revisit
```87: 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

.
```103: 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.

```114: {-@ foldr :: forall a b <p :: L a -> b -> Prop>.
115:                 (xs:L a -> x:a -> b <p xs> -> b <p (C x xs)>)
116:               -> b <p N>
117:               -> ys: L a
118:               -> b <p ys>
119:   @-}
120: foldr :: (L a -> a -> b -> b) -> b -> L a -> b
121: forall a b <p :: (SimpleRefinements.L a)-> b-> Bool>.
(xs:(SimpleRefinements.L a)
-> x:a
-> {VV : b<p xs> | true}
-> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : b<p ex> | true})
-> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : b<p ex> | true}
-> ys:(SimpleRefinements.L a)
-> {VV : b<p ys> | true}foldr xs:(SimpleRefinements.L a)
-> x:a
-> {VV : b | ((papp2 p VV xs))}
-> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : b | ((papp2 p VV ex))}f forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : a | ((papp2 p VV ex))}b N        = forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : a | ((papp2 p VV ex))}b
122: foldr f b (C x xs) = xs:(SimpleRefinements.L a)
-> x:a
-> {VV : b | ((papp2 p VV xs))}
-> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : b | ((papp2 p VV ex))}f {VV : (SimpleRefinements.L a) | (VV == xs)}xs {VV : a | (VV == x)}x (forall <p :: (SimpleRefinements.L a)-> b-> Bool>.
(xs:(SimpleRefinements.L a)
-> x:a
-> {VV : b<p xs> | true}
-> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : b<p ex> | true})
-> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : b<p ex> | true}
-> ys:(SimpleRefinements.L a)
-> {VV : b<p ys> | true}foldr xs:(SimpleRefinements.L a)
-> x:a
-> {VV : b | ((papp2 p VV xs))}
-> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : b | ((papp2 p VV ex))}f forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : a | ((papp2 p VV ex))}b {VV : (SimpleRefinements.L a) | (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

```139: {-@ size :: xs:L a -> {v: Int | v = (llen xs)} @-}
140: size :: L a -> Int
141: forall a.
xs:(SimpleRefinements.L a)
-> {VV : (GHC.Types.Int) | (VV == (llen xs))}size = forall <p :: (SimpleRefinements.L a)-> (GHC.Types.Int)-> Bool>.
(xs:(SimpleRefinements.L a)
-> x:a
-> {VV : (GHC.Types.Int)<p xs> | (VV >= 0)}
-> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : (GHC.Types.Int)<p ex> | (VV >= 0)})
-> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : (GHC.Types.Int)<p ex> | (VV >= 0)}
-> ys:(SimpleRefinements.L a)
-> {VV : (GHC.Types.Int)<p ys> | (VV >= 0)}foldr (x1:(SimpleRefinements.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 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ {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

```160: {-@ ++ :: xs:L a -> ys:L a -> {v:L a | (llen v) = (llen xs) + (llen ys)} @-}
161: (SimpleRefinements.L a)xs forall a.
xs:(SimpleRefinements.L a)
-> ys:(SimpleRefinements.L a)
-> {VV : (SimpleRefinements.L a) | ((llen VV) == ((llen xs) + (llen ys)))}++ (SimpleRefinements.L a)ys = forall <p :: (SimpleRefinements.L a)-> (SimpleRefinements.L a)-> Bool>.
(xs:(SimpleRefinements.L a)
-> x:a
-> {VV : (SimpleRefinements.L a)<p xs> | true}
-> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : (SimpleRefinements.L a)<p ex> | true})
-> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : (SimpleRefinements.L a)<p ex> | true}
-> ys:(SimpleRefinements.L a)
-> {VV : (SimpleRefinements.L a)<p ys> | true}foldr (x1:(SimpleRefinements.L a)
-> a
-> zs:{VV : (SimpleRefinements.L a) | ((llen VV) == ((llen x1) + (llen ys))) && ((llen VV) == ((llen ys) + (llen x1)))}
-> {VV : (SimpleRefinements.L a) | ((llen VV) == (1 + (llen zs)))}\_ az (SimpleRefinements.L a)zs -> a
-> xs:(SimpleRefinements.L a)
-> {VV : (SimpleRefinements.L a) | ((llen VV) == (1 + (llen xs)))}C {VV : a | (VV == z)}z {VV : (SimpleRefinements.L a) | (VV == zs)}zs) {VV : (SimpleRefinements.L a) | (VV == ys)}ys {VV : (SimpleRefinements.L a) | (VV == xs)}xs
```

Here, the relation

• `(p xs acc)`

is automatically instantiated with

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