Byte sized idris: How to handle impossible cases.

I had something on my mind earlier and admittedly i wasted precisely 37 minutes just now advancing a proof target I’m working on.

I’d had trouble with proofs like “a < b implies f a b = []” for some a and b. The problem comes when you case split and have to contend with (S a) and Z (for example) as values. You know this is impossible, but how to dismiss these proof targets?

Consider this:

lteMagnitudeObvIsImpossible : (b : Nat) -> (v : Bin) -> LTE (magnitude (O b v)) 0 -> Void 
lteMagnitudeObvIsImpossible Z v = 
 succNotLTEzero 
lteMagnitudeObvIsImpossible (S b) v = 
 succNotLTEzero

It’s a pretty straightforward proof that for any b and v, magnitude (O b v) less than or equal to zero is impossible (thanks to the standard prelude for providing succNotLTEzero).

There are a few things in idris that have seemingly similar meanings: impossible, absurd, Not.

In this case, absurd is the right tool since, given a Void, it yields uninhabited.

smallerNumberMeansFitsInNBits : (n : Nat) -> (a : Bin) -> LTE (magnitude a) n -> binToList (magnitude a) a = binToList n a 
smallerNumberMeansFitsInNBits n BNil lte = 
 rewrite binToListZeroIsEmpty n in 
 Refl 
smallerNumberMeansFitsInNBits Z (O b v) lte = 
 absurd (lteMagnitudeObvIsImpossible b v lte)

Satisfying!