Proving an index is within list bounds given (index + 1) is within bounds

Question

Let's say we have a list : List a, and we want to use its first and second elements:

case inBounds 1 list of
     Yes prf => doSmth (index 0 list) (index 1 list)
     No _ => doSmthElse

Unfortunately, this does not typecheck: indeed, prf is a proof that InBounds 1 list holds, but while it's obvious to us humans that InBounds 0 list immediately follows, it still needs to be shown to the typechecker.

Of course, one might write a helper proof

inBoundsDecr : InBounds (S k) xs -> InBounds k xs
inBoundsDecr {k = Z} (InLater y) = InFirst
inBoundsDecr {k = (S k)} (InLater y) = InLater (inBoundsDecr y)

and then use it in the Yes branch like this:

case inBounds 1 list of
     Yes prf => let prf' = inBoundsDecr prf in
                    doSmth (index 0 list) (index 1 list)
     No _ => doSmthElse

but it seems to be quite verbose.

So, what's the most concise and/or idiomatic way to do this in Idris?

xash xash · Accepted Answer · 2018-02-26T20:17:34

If you have a proof of xs that gives you some information about xs, it is better to use with instead of a case. Then the compiler can see that the argument can be determined by the proof. See this chapter in the tutorial: Views and the "with" rule

addHs : List Nat -> Nat
addHs xs with (inBounds 1 xs)
  addHs xs | p = ?hole

Pattern-matching on p gives Yes prf, then Yes (InLater y), then Yes (InLater InFirst), and updating xs to (x :: y :: xs). And so you can easily use x and y:

addHs : List Nat -> Nat
addHs xs with (inBounds 1 xs)
  addHs (x :: y :: xs) | (Yes (InLater InFirst)) = x + y
  addHs xs | (No contra) = 0

The problem with that is – here it doesn't work properly. If you check if addHs is total, the compiler warns you, because it thinks that another Yes (InLater p) could be reached. Not sure why, the totality checker isn't that great. But in theory it should work fine. :-)

Other than your initial attempt (which may be more verbose, but you don't depend that much on the totality checker), you could of course add a dummy Yes (InLater p) case or stop there and do something like

addHs : List Nat -> Nat
addHs xs with (inBounds 1 xs)
  addHs (x :: xs) | (Yes (InLater prf)) = x + (index 0 xs)
  addHs xs | (No contra) = 0

Or being somewhat unsafe and assert that the case is unreachable:

addHs : List Nat -> Nat
addHs xs with (inBounds 1 xs) proof q
  addHs (x :: y :: xs) | Yes (InLater InFirst) = x + y
  addHs (x :: xs) | Yes (InLater p) = assert_unreachable
  addHs xs | No _ = 0

Proving an index is within list bounds given (index + 1) is within bounds

1 Answers