How to prove equality commutes in Idris?

Question

Trying to prove the following assertion:

equalityCommutesNat : (n : Nat) -> (m : Nat) -> n = m -> m = n

I found plusCommutes in the libraries but nothing for equality.

Answer 1

The only inhabitant of = is Refl : (a = a), so if you pattern match, you'll get evidence that n is m.

Which means you can then use Refl, since Idris's pattern matching now knows they're the same:

equalityCommutesNat : (n : Nat) -> (m : Nat) -> n = m -> m = n
equalityCommutesNat _ _ Refl = Refl

And you can play around with this in the REPL:

> equalityCommutesNat 1 1 Refl
Refl : 1 = 1