[Agda] Does the order of patterns matter?

[Dan Doel]

Yes, see Eliminating Dependent Pattern Matching:

  http://www.cs.st-andrews.ac.uk/~james/RESEARCH/pattern-elimination-final.pdf

The --without-K part is more dicey; I don't think anyone's proved that
bit (i.e. that it doesn't require/imply K).

On Thu, Sep 27, 2012 at 11:48 AM, Martin Escardo
<m.escardo at cs.bham.ac.uk> wrote:
> Another question, related to the questions below.
>
> Is there any guarantee (hoped or proved) that any recursive definition that
> the termination checker accepts, by pattern matching, can be compiled to
> Martin-Loef combinators (including K if you don't disable K), for a suitable
> fragment of Agda?
>
> Martin
>
>
> On 27/09/12 11:51, 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda