# 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!

An old programmer learning new tricks.

An old programmer learning new tricks.

## We’re Not In A Real Estate Bubble

Get the Medium app