[Agda] Pattern matching on irrelevant types with only one constructor?

[Matthew Daggitt]

Hi Jesper,
 Thanks for the great reply. I had forgotten about passing of absurd
hypotheses, I obviously spend too much time trying to prove things that are
true in Agda...
Cheers,
Matthew

On Wed, May 1, 2019 at 3:48 PM Jesper Cockx <Jesper at sikanda.be> wrote:

> Hi Matthew,
>
> In our paper on definitional proof irrelevance (
> https://hal.inria.fr/hal-01859964) we give a criterion for when it is
> allowed to pattern match on an irrelevant argument. As we argue in the
> paper, the condition that the datatype has a single constructor is neither
> sufficient nor necessary. The criterion we give is not yet implemented in
> Agda, but I hope to add it in the not-too-distant future (it depends on my
> PR https://github.com/agda/agda/pull/3589 being merged first).
> Unfortunately, the Acc datatype does not satisfy this criterion. In fact,
> allowing pattern matching on irrelevant Acc would break strong
> normalization of the theory, as you can always have an absurd hypothesis of
> type Acc but evaluation would not be blocked on this argument because it's
> irrelevant. So the best you can do is get propositional  (instead of
> definitional) irrelevance by proving irrelevance of Acc by hand (or
> postulate it).
>
> A historical note: Agda used to allow matching on single-constructor
> datatypes under the --experimental-irrelevance flag, but this was
> completely broken so I decided to remove it last year (
> https://github.com/agda/agda/commit/b5f8b509bbe362c4bbb14612a6666e720cabf26a
> )
>
> -- Jesper
>
> On Wed, May 1, 2019 at 8:33 AM Matthew Daggitt <matthewdaggitt at gmail.com>
> wrote:
>
>>  In the Agda documentation
>> <https://agda.readthedocs.io/en/v2.6.0/language/irrelevance.html> it is
>> pretty clear that the only time you can pattern match against irrelevant
>> arguments is when the type is empty. My own reasoning for this has always
>> been that this is to stop decisions being made depending on the result of
>> the pattern match. This leads me to wonder if there are any theoretical
>> reasons why it's not possible to also mark a type irrelevant when it only
>> has a single constructor?
>>
>> Consider the motivating example below. Clearly the `Acc` argument is
>> never actually used in the computation of the final value, and no decisions
>> can be based on its value as it only has a single constructor. It seems
>> like it should be possible to mark it irrelevant. If this were possible
>> then we would immediately get rid of a whole bunch of annoying congruence
>> lemmas.
>> ```
>> gcd : (m n : ℕ) → Acc _<_ m → n < m → ℕ
>> gcd m zero     _         _   = m
>> gcd m (suc n) (acc rec) n<m = gcd′ (suc n) (m % suc n) (rec _ n<m) (a%n<n
>> m n)
>> ```
>> Many thanks,
>> Matthew
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190501/fde65917/attachment.html>