[Agda] Does the order of patterns matter?

[Martin Escardo]

Nils' message tells us where to find a full explanation of what is going on.

On 27/09/12 11:27, Altenkirch Thorsten wrote:
> The bug is rather that we use the = sign here -
> Epigram avoided this by using |-> and it also kept track of the splittings.

But "|->" would also be wrong, because e.g. in Achim's example, there is 
a situation f lhs = rhs where there is no reduction f lhs |-> rhs. But 
this is just a notational discussion


Here are some questions/conjectures.

(1) It would be possible to implement Agda so that each equation in a 
pattern holds definitionally, if we wished, I believe. Of course, you 
would get new definitional equalities not present in Martin-Loef type 
theory. But does that matter? Conjecture: no new propositional 
equalities arise.

(2) Every equation in a definition by pattern matching should hold 
propositionally (we know that this is not the case definitionally).
This should be a meta-theorem.

(3) Is there a nice characterization of pattern-matching definitions 
such that every "definining equation" does hold definitionally? The 
Berry-function in Nils' response indicates that this may be hard. Such 
pattern-system should be invariant under permuting equations, in 
suitable sense.

(4) What is there against forcing defining equations to hold 
definitionally, other than being able to compile them to 
eliminator-trees? Already in definitions by pattern matching on natural 
numbers there is a departure from Martin-Lof type theory, because in 
MLTT you need an inductive definition to even compute the predecessor 
function. So why not go a bit further, provide (1) and (2) make sense?

It is very disturbing that a proof ceases to type check if we reorder 
mutually exclusive, complete patterns.

Such an extension should be conservative in the sense of allowing more 
proofs, but no new theorems. (Which the eta-rule doesn't satisfy, but 
nevertheless we seem to be happy to add.)

Best,
Martin