[Agda] Does the order of patterns matter?

[Andreas Abel]

Martin,

I agree that equations not holding definitionally is a major source of 
confusion.  I back your proposal, but to realize it in full would be a 
bigger change of the theory of definitional equality.  It would take us 
from a theory based on eliminators or computational rules to a theory 
with more general rewriting rules.

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).  Here is an issue for 
this on the bug tracker:

   http://code.google.com/p/agda/issues/detail?id=408

Cheers,
Andreas

On 27.09.12 12:51 PM, Martin Escardo wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/