[Agda] Feedback requested on automated decision module

[Samuel Gélineau]

[for some reason, only the attachments of my previous message made it
to the list, so here is the non-attachment part again.]


On 2010-09-13 11:36, Gregory Crosswhite 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 started working on such a library when I saw your first message, but
you posted your own library before I even got the chance to mention
anything. For someone who claims his agda-fu is weak, you sure work
fast!

I think my contribution might still be of interest, however, since we
are focussing on different parts of the task: my library automates the
proof that a datatype is finite, and your library takes that proof as
input to prove everything else. Using my library looks as follows.


finitePauli : Finite Pauli
finitePauli = finite xs w refl where
  xs = I ∷ X ∷ Y ∷ Z ∷ []

  w : FiniteWitness xs
  w I = # 0 , refl
  w X = # 1 , refl
  w Y = # 2 , refl
  w Z = # 3 , refl

pauli4 : SameCardinality Pauli (Fin 4)
pauli4 = proj₂ finitePauli

leftPauli : LeftInverse (setoid Pauli) (setoid (Fin 4))
leftPauli = leftInverse pauli4


One thing which worries me, however, is that type-checking your decide
applications takes much longer when my library is used to define
leftPauli than when it is defined by hand. Worse: checking that _⋅_ is
associative should only take 4×4×4=64 checks, yet the type checker
runs out of memory. What is wrong with agda??

Oh, and let me mention it as soon as possible this time: I am working
on a generalization of decide_n which takes n as an argument.

– Samuel