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?
lteMagnitudeObvIsImpossible : (b : Nat) -> (v : Bin) -> LTE (magnitude (O b v)) 0 -> Void
lteMagnitudeObvIsImpossible Z v =
lteMagnitudeObvIsImpossible (S b) v =
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
smallerNumberMeansFitsInNBits Z (O b v) lte =
absurd (lteMagnitudeObvIsImpossible b v lte)