[Agda] Proofs for enumerated types

[Nils Anders Danielsson]

On 2010-09-10 23:01, Gregory Crosswhite wrote:
> 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 [...]

Indeed there is:

   module Pauli where

   import Algebra.FunctionProperties
   open import Data.Fin
   open import Data.Fin.Props using (eq?)
   open import Data.Fin.Dec using (all?)
   open import Function
   open import Function.LeftInverse
   open import Relation.Binary.PropositionalEquality as P
   open import Relation.Nullary

   data Pauli : Set where
     I X Y Z : Pauli

   infixl 7 _⋅_

   _⋅_ : 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

   -- Injection into Fin 4.

   to : Pauli → Fin 4
   to I = # 0
   to X = # 1
   to Y = # 2
   to Z = # 3

   from : Fin 4 → Pauli
   from zero = I
   from (suc zero) = X
   from (suc (suc zero)) = Y
   from (suc (suc (suc zero))) = Z
   from (suc (suc (suc (suc ()))))

   finite : LeftInverse (P.setoid Pauli) (P.setoid (Fin 4))
   finite = record
     { to              = P.→-to-⟶ to
     ; from            = P.→-to-⟶ from
     ; left-inverse-of = from∘to
     }
     where
     from∘to : ∀ x → from (to x) ≡ x
     from∘to I = refl
     from∘to X = refl
     from∘to Y = refl
     from∘to Z = refl

   -- Deciding equality is easy for finite sets.

   infix 4 _≟_

   _≟_ : (p₁ p₂ : Pauli) → Dec (p₁ ≡ p₂)
   _≟_ = eq? (LeftInverse.injection finite)

   -- Proving that a commutative operation actually is commutative is
   -- also easy. We can start by deciding whether the operator, lifted to
   -- Fin 4, is commutative.

   private

     _○_ = _⋅_ on from

     ○-comm? : Dec (∀ x y → (x ○ y) ≡ (y ○ x))
     ○-comm? = all? λ x → all? λ y → (x ○ y) ≟ (y ○ x)

   -- If we evaluate ○-comm? we see that the answer is yes <something>.
   -- Let's extract this <something> and polish it a bit.

   fromYes : ∀ {P : Set} (x : Dec P) {p} → x ≡ yes p → P
   fromYes .(yes p) {p} refl = p

   open Algebra.FunctionProperties {A = Pauli} _≡_

   ⋅-comm : Commutative _⋅_
   ⋅-comm x y =
     P.subst (λ y → x ⋅ y ≡ y ⋅ x)
             (LeftInverse.left-inverse-of finite y) $
       P.subst (λ x → x ⋅ from (to y) ≡ from (to y) ⋅ x)
               (LeftInverse.left-inverse-of finite x) $
               fromYes ○-comm? refl (to x) (to y)

--
/NAD