[Agda] Proofs for enumerated types

[Daniel Brown]

Though it isn't automated, I have something similar that uses
S-expressions instead of natural numbers:
http://acandystore.org/agda/Retract.html —start with the example at
the bottom. I'd be interested to hear if you find it helpful!

 Dan

On Mon, Sep 13, 2010 at 14:36, Gregory Crosswhite
<gcross at phys.washington.edu> wrote:
>  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
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>