<div dir="ltr">Dear Jason,<div><br></div><div>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<br><br><span style="font-family:"Courier New"">len (x<span class="gmail-Apple-converted-space"> </span></span><span style="font-family:"Cambria Math",serif">∷</span><span style="font-family:"Courier New""><span class="gmail-Apple-converted-space"> </span>y<span class="gmail-Apple-converted-space"> </span></span><span style="font-family:"Cambria Math",serif">∷</span><span style="font-family:"Courier New""><span class="gmail-Apple-converted-space"> </span>l) = len (y<span class="gmail-Apple-converted-space"> </span></span><span style="font-family:"Cambria Math",serif">∷</span><span style="font-family:"Courier New""><span class="gmail-Apple-converted-space"> </span>l)</span><br></div><div><br></div><div>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.</div><div><br></div><div>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:</div><div><br></div><div><p class="MsoNormal"><span style="font-family:"Courier New"">len' : </span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New""><span class="gmail-Apple-converted-space"> </span>→ </span><span style="font-family:"Courier New"">List</span><span style="font-family:"Courier New""><span class="gmail-Apple-converted-space"> </span></span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New""><span class="gmail-Apple-converted-space"> </span>→<span class="gmail-Apple-converted-space"> </span></span><span style="font-family:"Cambria Math",serif">ℕ</span></p><p class="MsoNormal"><span style="font-family:"Courier New"">len' x<span class="gmail-Apple-converted-space"> </span></span><span style="font-family:"Courier New"">[] = 1<u></u><u></u></span></p><p class="MsoNormal"><span style="font-family:"Courier New"">len' x<span class="gmail-Apple-converted-space"> (</span></span><span style="font-family:"Courier New"">y<span class="gmail-Apple-converted-space"> </span></span><span style="font-family:"Cambria Math",serif">∷</span><span style="font-family:"Courier New""><span class="gmail-Apple-converted-space"> zs</span>) = len' y<span class="gmail-Apple-converted-space"> zs</span></span></p><p class="MsoNormal"><span style="font-family:"Courier New""><span class="gmail-Apple-converted-space"><br></span></span></p><p class="MsoNormal"><span style="font-family:"Courier New"">len : List</span><span style="font-family:"Cambria Math",serif">⁺</span><span style="font-family:"Courier New""><span class="gmail-Apple-converted-space"> </span></span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New""><span class="gmail-Apple-converted-space"> </span>→<span class="gmail-Apple-converted-space"> </span></span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New""><u></u><u></u></span></p><p class="MsoNormal"><span style="font-family:"Courier New"">len (x<span class="gmail-Apple-converted-space"> </span></span><span style="font-family:"Cambria Math",serif">∷</span><span style="font-family:"Courier New""><span class="gmail-Apple-converted-space"> yz</span>) = len' x ys</span></p><div><br></div>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.</div><div><br></div><div>Best,</div><div>–Peter.</div><div><br></div><div><br>On Fri, Aug 20, 2021 at 4:54 AM Jason Hu <<a href="mailto:fdhzs2010@hotmail.com">fdhzs2010@hotmail.com</a>> wrote:<br>><br>> Hi James,<br>><br>>  <br>><br>> 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.<br>><br>>  <br>><br>> Thanks,<br>><br>> Jason Hu<br>><br>>  <br>><br>> From: James Smith<br>> Sent: Thursday, August 19, 2021 11:49 PM<br>> To: <a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><br>> Subject: Re: [Agda] convenient induction on non-empty list?<br>><br>>  <br>><br>> Out of curiosity why is the library's nonempty length not what you want? Maybe there is another approach.<br>><br>>  <br>><br>> One observation is that there is some sneakiness in the ∷, this program is:<br>><br>>  <br>><br>> len : Data.List.NonEmpty.List⁺ ℕ → ℕ<br>><br>> len (x Data.List.NonEmpty.∷ Data.List.[]) = 1<br>><br>> len (x Data.List.NonEmpty.∷ y Data.List.∷ l) = len (y Data.List.NonEmpty.∷ l) <br>><br>>  <br>><br>> 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.<br>><br>>  <br>><br>> This pattern does work when the constructors match:<br>><br>>  <br>><br>> len2 : Data.List.List ℕ → ℕ<br>><br>> len2 (Data.List.[]) = 0<br>><br>> len2 (x Data.List.∷ Data.List.[]) = 1<br>><br>> len2 (x Data.List.∷ y Data.List.∷ l) = 1 + len2 (y Data.List.∷ l)<br>><br>>  <br>><br>> On Thu, Aug 19, 2021 at 7:08 PM Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com">matthewdaggitt@gmail.com</a>> wrote:<br>><br>> 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.<br>><br>>  <br>><br>> On Fri, Aug 20, 2021 at 6:45 AM Jason Hu <<a href="mailto:fdhzs2010@hotmail.com">fdhzs2010@hotmail.com</a>> wrote:<br>><br>> Hi all,<br>><br>>  <br>><br>> 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:<br>><br>>  <br>><br>> open import Data.Nat<br>><br>> open import Data.List<br>><br>> open import Data.List.NonEmpty<br>><br>>  <br>><br>> len : List⁺ ℕ → ℕ<br>><br>> len (x ∷ []) = 1<br>><br>> len (x ∷ y ∷ l) = len (y ∷ l)<br>><br>>  <br>><br>> 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.<br>><br>>  <br>><br>> Any idea is appreciated.<br>><br>>  <br>><br>> Thanks,<br>><br>> Jason Hu<br>><br>>  <br>><br>> _______________________________________________<br>> Agda mailing list<br>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>> <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>><br>> _______________________________________________<br>> Agda mailing list<br>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>> <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>><br>>  <br>><br>> _______________________________________________<br>> Agda mailing list<br>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>> <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a></div></div>