[Agda] Proofs for enumerated types

[Gregory Crosswhite]

 Yay, I knew that there had to be a way to do this!  :-)  Is anyone
working on a library that could automate much of this?  I'm thinking
along the lines of a module parametrized by something like (LeftInverse
s (P.setoid (Fin n))) that would automatically provide _≟_, as well as
functions that could take properties on functions in the s setoid and
decide them by transferring the function and property to Fin n,
performing the decision there, and then lifting this result back to a
result in s.  If not, I am thinking of playing around with writing such
a module myself, though my agda-fu is weak. :-)

Cheers,
Greg

On 09/11/10 12:02, Nils Anders Danielsson wrote:
> 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
>