[Agda] convenient induction on non-empty list?

[James Smith]

Out of curiosity why is the library's nonempty length not what you want?
Maybe there is another approach.

One observation is that there is some sneakiness in the ∷, this program is:

len : Data.List.NonEmpty.List⁺ ℕ → ℕ

len (x Data.List.NonEmpty.∷ Data.List.[]) = 1
len (x Data.List.NonEmpty.∷ y Data.List.∷ l) = len (y Data.List.NonEmpty.∷ l
)

So the RHS is not "obviously" smaller because it's a different constructor
than the pattern match. The system is missing that there's a semantic
relationship between the two cons'es that we see intuitively.

This pattern does work when the constructors match:

len2 : Data.List.List ℕ → ℕ

len2 (Data.List.[]) = 0

len2 (x Data.List.∷ Data.List.[]) = 1

len2 (x Data.List.∷ y Data.List.∷ l) = 1 + len2 (y Data.List.∷ l)

On Thu, Aug 19, 2021 at 7:08 PM Matthew Daggitt <matthewdaggitt at gmail.com>
wrote:

> That is weird. I don't have any concrete suggestions apart from the one
> you've already mentioned, apologies, but I'd definitely advise filing a bug
> report on the Agda repo.
>
> On Fri, Aug 20, 2021 at 6:45 AM Jason Hu <fdhzs2010 at hotmail.com> wrote:
>
>> Hi all,
>>
>>
>>
>> It sounds like a stupid question but it seems to me there isn’t a
>> convenient way to do it. What I want to do is to do induction on a
>> non-empty list as defined in the stdlib in a “standard” way. To illustrate
>> the problem, consider the following program:
>>
>>
>>
>> open import Data.Nat
>>
>> open import Data.List
>>
>> open import Data.List.NonEmpty
>>
>>
>>
>> len : List⁺ ℕ → ℕ
>>
>> len (x ∷ []) = 1
>>
>> len (x ∷ y ∷ l) = len (y ∷ l)
>>
>>
>>
>> As of 2.6.2, Agda doesn’t like this definition and complains that len
>> does not terminate. What I am looking for is a solution that does not
>> require defining a “helper” which handle the underlying list, and the
>> “main” function which does the job separately.
>>
>>
>>
>> Any idea is appreciated.
>>
>>
>>
>> Thanks,
>>
>> Jason Hu
>>
>>
>> _______________________________________________
>> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210819/137fc149/attachment.html>