[Agda] Does the order of patterns matter?

[Altenkirch Thorsten]

Hi Andreas,

did you produce the parallel substitution function by splitting or by hand?

It seems to me that the issue only arises with hand crafted patterns but
not patterns that are produced by splitting. Is this correct?

Cheers,
Thorsten

On 28/09/2012 12:15, "Andreas Abel" <andreas.abel at ifi.lmu.de> wrote:

>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/
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.