[Agda] Does the order of patterns matter?

[Martin Escardo]

On 28/09/12 12:15, Andreas Abel wrote:
> I agree that equations not holding definitionally is a major source of
> confusion.

Interestingly, I had never come across this problem myself! But I did
get confused when Achim presented his example. And I did suggest to
him in e-writing that this might have to do with the way pattern
matching is compiled into combinators, before he posted his message,
which Nils confirmed to be the case. Except that the compilation into
patterns doesn't seem to happen internally. What you seem to have is a
direct interpretation of the patterns that simulates the same
behaviour as if you would have compiled to eliminator trees.

> I back your proposal, but to realize it in full would be a
> bigger change of the theory of definitional equality.

It is not a proposal really (although I suppose it might be
useful). It is more a theoretical question. Suppose we did add a new
definitional equality for each equation in an Agda proofgram (provided
the patterns are mutually exclusive). Would we get any new
propositional equality. No, I don't think so. Would we get to prove a
new theorem? No, I don't think so. But are my thoughts right? If they
are, then this could be useful: we can get shorter proofs of the same
theorems we could prove before, and no new theorem.

> It would take us from a theory based on eliminators or computational
> rules to a theory with more general rewriting rules.

Yes, this perhaps can be a formulation of my question. This reminds me
of Kleene's thoughts in some of his books and papers. He has a
combinator-based approach to primitive recursive functions and to
general recursive functions, but then he wants to write arbitrary
recursive equations to make his life simpler - and he proved a theorem
to be able to do that. There should be a meta-theorem saying that
accepting agda equations as definitional equalities (under certain
conditions) doesn't give you anything new.

> But at least, there should be a way of telling Agda that one want the
> equations to hold, and that it should be an error if Agda cannot make it
> work (needs more splitting than one specified).

This seems reasonable if the above conjectures hold.

Best,
Martin