[Agda] convenient induction on non-empty list?

[Peter LeFanu Lumsdaine]

Dear Jason,

Non-empty lists *do* have a built-in induction/pattern-matching principle,
and the LHS of your definition is what that principle would accept.  But
like most primitive induction principles, it requires recursive calls to
have “structurally smaller” arguments, and in your second case

len (x ∷ y ∷ l) = len (y ∷ l)

the recursive call on the RHS is not structurally smaller than the LHS,
since as James Smith points out, the “y :: l” on the RHS is with the cons
for non-empty lists, while the “y :: l” on the LHS is the cons for plain
lists.

The thing that’s structurally decreasing in your example is the *list*
argument of the non-empty-cons constructor, not the whole non-empty list.
So you can make it acceptable by exposing that list as an argument of the
function:

len' : ℕ → List ℕ → ℕ

len' x [] = 1

len' x (y ∷ zs) = len' y zs


len : List⁺ ℕ → ℕ

len (x ∷ yz) = len' x ys

This is a kind of “helper function on lists” approach, so perhaps isn’t
what you hoped for.  But it’s a fairly non-intrusive one, and easy to apply
to more complicated definitions using the same “induction principle” — it
didn’t need any refactoring of the definition apart from splitting the
non-empty list argument into two separate arguments.

Best,
–Peter.


On Fri, Aug 20, 2021 at 4:54 AM Jason Hu <fdhzs2010 at hotmail.com> wrote:
>
> 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
> Sent: Thursday, August 19, 2021 11:49 PM
> To: 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>
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
>
>
>
> _______________________________________________
> 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/20210821/b9a99b14/attachment.html>