CODEWITHSUNDEEP
proofidris
Ignat Insarov
Ignat Insarov

Reputation: 4832

Can I extract a proof of bounds from an enumeration expression?

Consider this trivial program:

module Study

g : Nat -> Nat -> Nat
g x y = x - y

f : Nat -> List Nat
f x = map (g x) [1, 2 .. x]

It gives an obvious error:

  |
4 | g x y = x - y
  |           ^
When checking right hand side of g with expected type
        Nat

When checking argument smaller to function Prelude.Nat.-:
        Can't find a value of type 
                LTE y x

— Saying I should offer some proof that this subtraction is safe to perform.

Surely, in the given context, g is always invoked safely. This follows from the way enumerations behave. How can I extract a proof of that fact so that I can give it to the invocation of g?

I know that I can use isLTE to obtain the proof:

g : Nat -> Nat -> Nat
g x y = case y `isLTE` x of
             (Yes prf)   => x - y
             (No contra) => ?s_2

This is actually the only way I know of, and it seems to me that in a situation such as we have here, where x ≥ y by construction, there should be a way to avoid a superfluous case statement. Is there?

Upvotes: 1

Views: 37

Answers (1)

xash
xash

Reputation: 3722

For map (\y = x - y) [1, 2 .. x] there needs to be a proof \y => LTE y x for every element of [1, 2 .. x]. There is Data.List.Quantifiers.All for this: All (\y => LTE y x) [1, 2 .. x].

But constructing and applying this proof is not so straight-forward. You could either build a proof about the range function lteRange : (x : Nat) -> All (\y => LTE y x) (natRange x) or define a function that returns a range and its proof lteRange : (x : Nat) -> (xs : List Nat ** All (\y => LTE y x) xs). For simplicity, I'll show an example with the second type.

import Data.List.Quantifiers

(++) : All p xs -> All p ys -> All p (xs ++ ys)
(++) []        ys = ys
(++) (x :: xs) ys = x :: (xs ++ ys)

lteRange : (x : Nat) -> (xs : List Nat ** All (\y => LTE y x) xs)
lteRange Z = ([] ** [])
lteRange (S k) = let (xs ** ps) = lteRange k in
  (xs ++ [S k] ** weakenRange ps ++ [lteRefl])
  where
    weakenRange : All (\y => LTE y x) xs -> All (\y => LTE y (S x)) xs
    weakenRange []       = []
    weakenRange (y :: z) = lteSuccRight y :: weakenRange z

Also, map only applies one argument, but (-) needs the proof, too. So with a little helper function …

all_map : (xs : List a) -> All p xs -> (f : (x : a) -> p x -> b) -> List b
all_map [] [] f = []
all_map (x :: xs) (p :: ps) f = f x p :: all_map xs ps f

We can roughly do what you wanted without checking for LTE during the run-time:

f : Nat -> List Nat
f x = let (xs ** prfs) = lteRange x in all_map xs prfs (\y, p => x - y)

Upvotes: 1

Related Questions