[Agda] convenient induction on non-empty list?

[Jason Hu]

Hi James,

Len is just an example, not the problem I am working on. I am actually defining an interpretation of certain non-empty lists, and my definitions are irrefutable on paper, but it is just I can’t punch in as is in Agda. The fact that non-empty list doesn’t have a builtin induction principle is rather strange.

Thanks,
Jason Hu

From: James Smith<mailto:james.smith.69781 at gmail.com>
Sent: Thursday, August 19, 2021 11:49 PM
To: agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>
Subject: Re: [Agda] convenient induction on non-empty list?

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