# Indexed-Dependent Refinements

```7: module LiquidArray where
8:
```

# Indexed-Dependent Refinements

We define a Vector of `a`s implemented as a function from `Int` to `a`s

```20: data Vec a = V (Int -> a)
```

# Abstract Over the Domain and Range

We parameterize the definition with two abstract refinements:

```31: {-@ data Vec a <dom :: Int -> Prop, rng :: Int -> a -> Prop>
32:       = V {a :: i:Int<dom> -> a <rng i>}
33:   @-}
```
• `dom`: describes the domain

• `rng`: describes each value with respect to its index

# Describing Vectors

By instantiating these two predicates, we describe Vector's domain and range
```45: {-@ data Vec a <dom :: Int -> Prop, rng :: Int -> a -> Prop>
46:       = V {a :: i:Int<dom> -> a <rng i>}
47:   @-}
```

A vector of `Int` defined on values less than `42` containing values equal to their index:

```57: {-@ type IdVec =
58:       Vec <{\v -> (v < 42)}, {\j v -> (v = j)}> Int
59:   @-}
```

# Describing Vectors

By instantiating these two predicates, we describe Vector's domain and range
```65: {-@ data Vec a <dom :: Int -> Prop, rng :: Int -> a -> Prop>
66:       = V {a :: i:Int<dom> -> a <rng i>}
67:   @-}
```

A vector defined on the range `[0..n)` with its last element equal to `0`:

```76: {-@ type ZeroTerm N =
77:      Vec <{\v -> (0 <= v && v < N)}, {\j v -> (j = N - 1 => v = 0)}> Int
78:   @-}
```

# Describing Vectors

By instantiating these two predicates, we describe Vector's domain and range
```84: {-@ data Vec a <dom :: Int -> Prop, rng :: Int -> a -> Prop>
85:       = V {a :: i:Int<dom> -> a <rng i>}
86:   @-}
```

A vector defined on integers whose value at index `j` is either `0` or the `j`th fibonacci:

```97: {-@ type FibV =
98:      Vec <{\v -> 0=0}, {\j v -> ((v != 0) => (v = (fib j)))}> Int
99:   @-}
```

# Operations on Vectors

Demo

We give appropriate types to vector operations (empty, set, get...)

• This means abstracting over the domain and range

# Empty

`empty` returns a Vector whose domain is always false

```121: {-@ empty :: forall <p :: Int -> a -> Prop>. Vec < {v:Int | 0=1}, p> a @-}
122: empty     :: Vec  a
123: forall a <p :: (GHC.Types.Int)-> a-> Bool>.
(LiquidArray.Vec <false, \_ VV -> p> a)empty     = ({VV : (GHC.Types.Int) | false} -> {VV : a | false})
-> (LiquidArray.Vec <false, \_ VV -> false> {VV : a | false})V (({VV : (GHC.Types.Int) | false} -> {VV : a | false})
-> (LiquidArray.Vec <false, \_ VV -> false> {VV : a | false}))
-> ({VV : (GHC.Types.Int) | false} -> {VV : a | false})
-> (LiquidArray.Vec <false, \_ VV -> false> {VV : a | false})\$ {VV : (GHC.Types.Int) | false} -> {VV : a | false}\_ -> ([(GHC.Types.Char)] -> {VV : a | false}error {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Empty array!")
```

# Typing Get

If `i` satisfies the domain then if we `get` the `i`th element of an array, the result should satisfy the range at `i`

```136: {-@ get :: forall a <r :: Int -> a -> Prop, d :: Int -> Prop>.
137:            i: Int<d>
138:         -> a: Vec<d, r> a
139:         -> a<r i> @-}
140: get :: Int -> Vec a -> a
141: forall a <r :: (GHC.Types.Int)-> a-> Bool, d :: (GHC.Types.Int)-> Bool>.
i:{VV : (GHC.Types.Int)<d> | true}
-> (LiquidArray.Vec <d, \_ VV -> r> a) -> {VV : a<r i> | true}get {VV : (GHC.Types.Int) | ((papp1 d VV))}i (V f) = i:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> {VV : a | ((papp2 r VV i))}f {VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV == i)}i
```

# Typing Set

If `i` satisfies the domain then if we `set` the `i`th element of a Vector to a value that satisfies range at `i`, then Vector's domain will be extended with `i`

```155: {-@ set :: forall a <r :: Int -> a -> Prop, d :: Int -> Prop>.
156:            i: Int<d>
157:         -> x: a<r i>
158:         -> a: Vec < {v:Int<d> | v != i}, r> a
159:         -> Vec <d, r> a @-}
160: set :: Int -> a -> Vec a -> Vec a
161: forall a <r :: (GHC.Types.Int)-> a-> Bool, d :: (GHC.Types.Int)-> Bool>.
i:{VV : (GHC.Types.Int)<d> | true}
-> {VV : a<r i> | true}
-> (LiquidArray.Vec <d & (VV /= i), \_ VV -> r> a)
-> (LiquidArray.Vec <d, \_ VV -> r> a)set {VV : (GHC.Types.Int) | ((papp1 d VV))}i {VV : a | ((papp2 r VV i))}v (V f) = (i:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> {VV : a | ((papp2 r VV i))})
-> (LiquidArray.Vec <((papp1 d VV)), \x1 VV -> ((papp2 r VV x1))> a)V ((x4:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> {VV : a | ((papp2 r VV x4))})
-> (LiquidArray.Vec <((papp1 d VV)), \x2 VV -> ((papp2 r VV x2))> a))
-> (x4:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> {VV : a | ((papp2 r VV x4))})
-> (LiquidArray.Vec <((papp1 d VV)), \x2 VV -> ((papp2 r VV x2))> a)\$ k:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> {VV : a | ((papp2 r VV k))}\{VV : (GHC.Types.Int) | ((papp1 d VV))}k -> if {VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV == k)}k x:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> y:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x == y))}== {VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV == i)}i then {VV : a | ((papp2 r VV i)) && (VV == v)}v else i:{VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV /= i)}
-> {VV : a | ((papp2 r VV i))}f {VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV == k)}k
```

# Using Vectors

Remember the fibonacci memoization Vector:
```168: type FibV =
169:      Vec <{\v -> 0=0}, {\j v -> ((v != 0) => (v = (fib j)))}> Int
```

Where `fib` is an uninterprented function

```175: {-@ measure fib :: Int -> Int @-}
```

We used `fib` to define the `axiom_fib`

```182: {-@ predicate Fib I =
183:   (fib i) = ((i <= 1)?1:((fib (i-1)) + fib (i-2)))
184:   @-}
185:
186: {-@ assume axiom_fib :: i:Int -> {v: Bool | ((Prop v) <=> (Fib i))} @-}
187: axiom_fib :: Int -> Bool
188: i:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> ((fib i) == (if (i <= 1) then 1 else ((fib (i - 1)) + (fib (i - 2))))))}axiom_fib (GHC.Types.Int)i = forall a. aundefined
```

# Fast Fibonacci

Now we can efficiently compute the `i`th fibonacci number

```197: {-@ fastFib :: x:Int -> {v:Int | v = fib(x)} @-}
198: fastFib     :: Int -> Int
199: x:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (fib x))}fastFib (GHC.Types.Int)n   = ((LiquidArray.Vec <false, \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib n))})
-> {VV : (GHC.Types.Int) | (VV == (fib n))}snd (((LiquidArray.Vec <false, \x2 VV -> ((VV /= 0) => (VV == (fib x2)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib n))})
-> {VV : (GHC.Types.Int) | (VV == (fib n))})
-> ((LiquidArray.Vec <false, \x2 VV -> ((VV /= 0) => (VV == (fib x2)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib n))})
-> {VV : (GHC.Types.Int) | (VV == (fib n))}\$ (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int))
-> i:(GHC.Types.Int)
-> ((LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo (forall <rng :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, dom :: (GHC.Types.Int)-> Bool>.
(i:{VV : (GHC.Types.Int)<dom> | true}
-> {VV : (GHC.Types.Int)<rng i> | ((VV /= 0) => (VV == (fib \$\$"Empty array!"))) && ((VV /= 0) => (VV == (fib n))) && (VV == 0)})
-> (LiquidArray.Vec <dom, rng> {VV : (GHC.Types.Int) | ((VV /= 0) => (VV == (fib \$\$"Empty array!"))) && ((VV /= 0) => (VV == (fib n))) && (VV == 0)})V ((GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (0  :  int))}\_ -> {VV : (GHC.Types.Int) | (VV == (0  :  int))}0)) {VV : (GHC.Types.Int) | (VV == n)}n
```

# Fibonacci Memo

```206: {-@ fibMemo :: FibV -> i:Int -> (FibV, {v: Int | v = fib(i)}) @-}
207: fibMemo :: Vec Int -> Int -> (Vec Int, Int)
208: (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int))
-> i:(GHC.Types.Int)
-> ((LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int))t (GHC.Types.Int)i
209:   | {VV : (GHC.Types.Int) | (VV == i)}i x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x <= y))}<= {VV : (GHC.Types.Int) | (VV == (1  :  int))}1
210:   = forall a b <p2 :: a-> b-> Bool>.
x1_(,):a -> {VV : b<p2 x1_(,)> | true} -> (a, b)<p2>({VV : (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)) | (VV == t)}t, b:(GHC.Types.Bool)
-> {VV : (GHC.Types.Int) | (VV == 1) && (VV > 0) && (VV >= i)}
-> {VV : (GHC.Types.Int) | ((Prop b)) && (VV == 1) && (VV > 0) && (VV >= i)}liquidAssume (i:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> ((fib i) == (if (i <= 1) then 1 else ((fib (i - 1)) + (fib (i - 2))))))}axiom_fib {VV : (GHC.Types.Int) | (VV == i)}i) ({VV : (GHC.Types.Int) | (VV == (1  :  int))}1 :: Int))
211:
212:   | otherwise
213:   = case forall <d :: (GHC.Types.Int)-> Bool, r :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
i:{VV : (GHC.Types.Int)<d> | true}
-> (LiquidArray.Vec <d, \_ VV -> r> (GHC.Types.Int))
-> {VV : (GHC.Types.Int)<r i> | true}get {VV : (GHC.Types.Int) | (VV == i)}i {VV : (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)) | (VV == t)}t of
214:       0 -> let ({VV : (LiquidArray.Vec <True, \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t1)}t1, {VV : (GHC.Types.Int) | (VV == n1)}n1) = (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int))
-> i:(GHC.Types.Int)
-> ((LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo {VV : (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)) | (VV == t)}t  ({VV : (GHC.Types.Int) | (VV == i)}ix:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x - y))}-{VV : (GHC.Types.Int) | (VV == (1  :  int))}1)
215:                ({VV : (LiquidArray.Vec <(VV /= i), \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t2)}t2, {VV : (GHC.Types.Int) | (VV == n2)}n2) = (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int))
-> i:(GHC.Types.Int)
-> ((LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo {VV : (LiquidArray.Vec <True, \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t1) && (VV == t1)}t1 ({VV : (GHC.Types.Int) | (VV == i)}ix:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x - y))}-{VV : (GHC.Types.Int) | (VV == (2  :  int))}2)
216:                (GHC.Types.Int)n        = b:(GHC.Types.Bool)
-> (GHC.Types.Int) -> {VV : (GHC.Types.Int) | ((Prop b))}liquidAssume (i:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> ((fib i) == (if (i <= 1) then 1 else ((fib (i - 1)) + (fib (i - 2))))))}axiom_fib {VV : (GHC.Types.Int) | (VV == i)}i) ({VV : (GHC.Types.Int) | (VV == n1) && (VV == n1)}n1 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ {VV : (GHC.Types.Int) | (VV == n2) && (VV == n2)}n2)
217:            in  forall a b <p2 :: a-> b-> Bool>.
x1_(,):a -> {VV : b<p2 x1_(,)> | true} -> (a, b)<p2>(forall <d :: (GHC.Types.Int)-> Bool, r :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
i:{VV : (GHC.Types.Int)<d> | true}
-> {VV : (GHC.Types.Int)<r i> | true}
-> (LiquidArray.Vec <d & (VV /= i), \_ VV -> r> (GHC.Types.Int))
-> (LiquidArray.Vec <d, \_ VV -> r> (GHC.Types.Int))set {VV : (GHC.Types.Int) | (VV == i)}i {VV : (GHC.Types.Int) | (VV == n)}n {VV : (LiquidArray.Vec <(VV /= i), \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t2) && (VV == t2)}t2,  {VV : (GHC.Types.Int) | (VV == n)}n)
218:       n -> ({VV : (LiquidArray.Vec <True, \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t)}, {VV : (GHC.Types.Int) | (VV == (fib i)) && (VV /= 0)})<\_ VV -> (VV == (fib i)) && (VV /= 0)>({VV : (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)) | (VV == t)}t, {VV : (GHC.Types.Int) | ((VV /= 0) => (VV == (fib i)))}n)
```