Byte sized idris: How to handle impossible cases.

art yerkes
Nov 13, 2018 · 1 min read

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!

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store