Idris: Using the properties of simple constructors for equality and inequality

Among the first question I asked anyone about idris was about proofs that end in having to prove that two things aren’t equal. Idris itself stops being particularly helpful in those cases, giving the weird feeling that you’re just on your own. In some cases you can provide positive proof of the opposite of the required proof and save yourself. In some cases, some rewriting gives a contradiction that idris itself is able to turn into a self evident falsehood.

I wrote a function that, for bools, inverts a proof that two things aren’t equal into a proof that the opposite of one is equal to the other, and leveraged that plenty in the idris I’ve written.

Early on I received some advice that I definitely didn’t fully understand, but came in useful as the foundation of other proof code due to being able to somewhat magically help me combine deciadable cases on a constructor with two arguments.

I’ve been working on providing proof of more properties of this object recently and I finally understand this, and can explain it hopefully in plain language that’s helpful.

My nat-like binary numbers (ugly but functional proof of interop with nat)

https://github.com/prozacchiwawa/idris-binnum:

data Bin = O Nat Bin | BNil

First let’s start with what I was given:

— Thanks: https://www.reddit.com/r/Idris/comments/8yv5fn/using_deceq_in_proofs_extracting_and_applying_the/e2e8a6l/?context=3
O_injective : (O a v = O b w) -> (a = b, v = w)
O_injective Refl = (Refl, Refl)
total aNEBMeansNotEqual : (a : Nat) -> (b : Nat) -> (v : Bin) -> Dec (a = b) -> Dec (O a v = O b v)
aNEBMeansNotEqual a b v (Yes prf) = rewrite prf in Yes Refl
aNEBMeansNotEqual a b v (No contra) =
  No $ \prf =>
    let (ojAB, _) = O_injective prf in
    contra ojAB
total vNEWMeansNotEqual : (v : Bin) -> (w : Bin) -> Dec (v = w) -> Dec (O Z v = O Z w)
vNEWMeansNotEqual v w (Yes prf) = rewrite prf in Yes Refl
vNEWMeansNotEqual v w (No contra) = 
  No $ \prf =>
    let (_, ojVW) = O_injective prf in
    contra ojVW

I’d like to dissect what’s going on here and really dig into how this helps with many proof obligations one might run into on Bin (and really any constructor with multiple arguments).

O_injective is relying on idris to take a single proof step, namely that because a pairs with b and v pairs with w in a proof, then it can infer that a=b and v=w. Since the proof is a function, it conveniently returns both so we can destructure them. Without this, we’d need to use contradictions and either ‘with’ rules or induction to prove them.

The following decision rules follow from this, using the indicated destructured part of the proof to refute the clause with the given contradiction (either the shift or the tail), giving us an easy way to turn a decision about inequality in one part of the constructor to a decision about equality in the constructor as a whole.

It didn’t occur to me at the time why the function is called ‘injective’ because my math is very rusty, but upon refreshing, I realized two things:

• Simple constructors are implicitly injective because each unique set of argument values results in a unique outcome in the space of the constructor’s type. Despite having this code for a while, my experiences with more complex proofs suggested that idris would require me to rewrite these myself. I admittedly was weirdly blind to it for a while.
• Not only simply injective, constructors are also bijective: each unique value of the constructor fully populated also represents a unique set of inputs, and idris also allows us to write this:

O_bijective : (a = b) -> (c = d) -> (O a c = O b d)
O_bijective Refl Refl = Refl

With these, we can compose and decompose proofs about constructors without having to go through labor to show the outcome of each case. I wanted to call it out specifically because it’s very useful and might be missed unless one knows this pattern can be used.