[Agda] slightly wrong sized datatype definition leads to proof of False

[vlad]

Thank you for the reply. Hmm, there are some things I don't understand.

On 19/10/2020 17:05, Andrea Vezzosi wrote:
> The issue here is only incidentally about sized types. but rather an
> issue with the check for when an absurd pattern (i.e. "()") is
> allowed:
>
> https://github.com/agda/agda/issues/4995
Unlike that issue I do not use a postulate but I am using sized types, 
so how can my issue only incidentally be about sized types?
> Btw, the type you defined is more like co-natural numbers, i.e. with
> an extra point at infinity, so it's quite natural to have a fix-point
> for `suc`.

Ok, perhaps the notation is confusing. If I syntactically rewrite the 
definition

data  ℕ {s : Size} :  Set where
   zero :  ℕ
   suc : ({s' : Size< s} → ℕ {s'}) → ℕ {s}

as follows, with Acc instead of ℕ, acc instead of suc, with explicit 
instead of implicit sizes, and forgetting the zero constructor, which 
was there just to make the above look like a definition of natural 
numbers anyway:

data Acc (s : Size) : Set where

     acc : ((s' : Size< s)  → Acc s') → Acc s

then Acc reads as the accessibility predicate for the relation _<_  on 
Size such that i < j iff i : Size< j. The issue I raised can of course 
be rephrased by proving that the accessible part of the relation _<_ 
coincides with the whole relation, in particular, Acc ∞, and since _<_ 
is not well-founded (∞<∞) one gets a proof of False. Or one can use ℕ 
instead of Acc for that purpose, they're interchangeable here.

Now, Acc is an inductive definition, and so is ℕ. I don't see how the 
latter can denote co-natural numbers, which AFAIK require a coinductive 
definition?

Mind, I'm not saying that ℕ above is the appropriate way of defining 
sized natural numbers. But Agda accepts it - and it shouldn't, because 
after a few steps one gets a proof of False in safe mode...


> On Mon, Oct 19, 2020 at 1:44 PM vlad <Vlad.Rusu at inria.fr> wrote:
>> Thanks for finding this. I guess this is in a longer tradition of
>> problems with the sized types implementation, see e.g.
>> https://github.com/agda/agda/issues/2820,
>> https://github.com/agda/agda/issues/3026,
>> https://github.com/agda/agda/issues/1428.
>>
>> I don't understand whether it has overlap with existing issues. You
>> don't use the infinity size, nor equality. So maybe it's a new kind of
>> issue, coming from interaction of sizes with inductive types?
>>
>> It is an elaboration on the bug about well-founded induction and sized types (https://github.com/agda/agda/issues/3026). The main difference with the latter is that, instead of importing the well-founded module of Agda's library, I am using an apparently innocent definition of a sized inductive type :
>>
>> data ℕ  {s : Size} :  Set where
>>    zero :  ℕ
>>    suc : ({s' : Size< s} → ℕ {s'}) → ℕ {s}
>>
>> as an accessibility predicate for the relation between sized induced by the construction Size<. By using the "size-elimproved" construction (also an elaboration of code found here: https://github.com/agda/agda/issues/2820#issuecomment-339969286) I can then define a "natural number" for each size, including infinity (note that sizes are implicit arguments, so infinity does not show up in the code, but it's there all right). For size = infinity, the "natural number"
>>
>> foo : ℕ
>> foo = size-elimproved (λ s → ℕ{s}) (λ _ H → suc λ { {j} → H j } ) _
>>
>> is easily shown to be a successor of itself, which the definition of "natural numbers" forbids, hence the proof of False.
>>
>> Overall, I'm not sure it's worth a new bug report, as it is an elaboration of existing constructions. My main point in showing this is that one may easily "believe" that one is defining natural numbers with sizes e.g. for writing non-structural recursive functions over them (like integer division), while in effect writing something else, with unpleasant consequences.
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda