[Agda] Proofs for enumerated types

[Gregory Crosswhite]

 Hey everyone! I am in the early stages of playing around with agda in
order to get a feel with how to use it.

I have got an enumeration type, Pauli:

data Pauli : Set where
I : Pauli
X : Pauli
Y : Pauli
Z : Pauli

And I have a product on this type:

_⋅_ : Pauli → Pauli → Pauli
_ ⋅ I = I
I ⋅ _ = I
X ⋅ X = I
X ⋅ Y = Z
X ⋅ Z = Y
Y ⋅ X = Z
Y ⋅ Y = I
Y ⋅ Z = X
Z ⋅ X = Y
Z ⋅ Y = X
Z ⋅ Z = I

This product is associative and commutative. In order to prove that it
is commutative, I used brute force:

open import Relation.Binary.PropositionalEquality as PropEq
using (_≡_; _≢_; refl; sym; cong; cong₂)
import Algebra.FunctionProperties as P; open P _≡_

+-comm : Commutative _⋅_
+-comm I I = refl
+-comm I X = refl
+-comm I Y = refl
+-comm I Z = refl
+-comm X I = refl
+-comm X X = refl
+-comm X Y = refl
+-comm X Z = refl
+-comm Y I = refl
+-comm Y X = refl
+-comm Y Y = refl
+-comm Y Z = refl
+-comm Z I = refl
+-comm Z X = refl
+-comm Z Y = refl
+-comm Z Z = refl

However, I feel like there should be a more elegant way of doing this.
Since the type is a set that only contains a finite number of values,
such properties as associativity, commutativity, existence of an inverse
(I), etc. can be proven by performing a brute-force examination of all
the possibilities. There is probably a way to do this somewhere in the
standard libraries, but there is so much there and so many layers of
abstraction that I'm not sure where it is. :-) I saw the Fin type and
something whose type overwhelmed me a bit but which looked like a way
for me to establish that there are only a finite number of values in
Pauli, but I couldn't see how proving that would open up new proof tools
for me within the library.

So do you all have any suggestions? :-) Thanks in advance!

- Greg