CODEWITHSUNDEEP
idris
Peteris
Peteris

Reputation: 3756

How to prove equality commutes in Idris?

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.

Upvotes: 2

Views: 113

Answers (1)

Brian McKenna
Brian McKenna

Reputation: 46218

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

Upvotes: 2

Related Questions