<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:DengXian;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"\@DengXian";
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:Menlo;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
p.gmail-p1, li.gmail-p1, div.gmail-p1
{mso-style-name:gmail-p1;
mso-margin-top-alt:auto;
margin-right:0in;
mso-margin-bottom-alt:auto;
margin-left:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.gmail-s1
{mso-style-name:gmail-s1;}
span.gmail-s2
{mso-style-name:gmail-s2;}
span.gmail-s3
{mso-style-name:gmail-s3;}
span.gmail-s4
{mso-style-name:gmail-s4;}
p.gmail-p2, li.gmail-p2, div.gmail-p2
{mso-style-name:gmail-p2;
mso-margin-top-alt:auto;
margin-right:0in;
mso-margin-bottom-alt:auto;
margin-left:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.gmail-s5
{mso-style-name:gmail-s5;}
span.gmail-s6
{mso-style-name:gmail-s6;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.25in 1.0in 1.25in;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-US" link="blue" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">Hi James,</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">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. </p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Thanks,<o:p></o:p></p>
<p class="MsoNormal">Jason Hu<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div style="mso-element:para-border-div;border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal" style="border:none;padding:0in"><b>From: </b><a href="mailto:james.smith.69781@gmail.com">James Smith</a><br>
<b>Sent: </b>Thursday, August 19, 2021 11:49 PM<br>
<b>To: </b><a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><br>
<b>Subject: </b>Re: [Agda] convenient induction on non-empty list?</p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal">Out of curiosity why is the library's nonempty length not what you want? Maybe there is another approach.<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="color:black">One observation is that there is some sneakiness in the </span><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">∷, </span><span style="color:black">this program is:</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="gmail-p1" style="margin:0in;font-variant-numeric:normal;font-variant-east-asian:normal;font-stretch:normal">
<span class="gmail-s1"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:mediumblue;background:#FD9E74">len</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">:</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s4"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">Data.List.NonEmpty.List⁺</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s4"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">ℕ</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">→</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s4"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">ℕ</span></span><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF"><o:p></o:p></span></p>
<p class="gmail-p2" style="margin:0in;font-variant-numeric:normal;font-variant-east-asian:normal;font-stretch:normal">
<span class="gmail-s5"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">len</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">(</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">x
</span></span><span class="gmail-s4"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428">Data.List.NonEmpty.∷</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s4"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428">Data.List.[]</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">)</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">=</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s6"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#D422FF">1</span></span><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428"><o:p></o:p></span></p>
<div>
<p class="MsoNormal"><span class="gmail-s5"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">len</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">(</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">x
</span></span><span class="gmail-s4"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428">Data.List.NonEmpty.∷</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black"> y
</span></span><span class="gmail-s4"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428">Data.List.∷</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black"> l</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">)</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">=</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s1"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:mediumblue;background:#FD9E74">len</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">(</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">y
</span></span><span class="gmail-s4"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428">Data.List.NonEmpty.∷</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black"> l</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">)</span></span> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">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.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">This pattern does work when the constructors match:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="gmail-p1" style="margin:0in;font-variant-numeric:normal;font-variant-east-asian:normal;font-stretch:normal">
<span class="gmail-s1"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">len2</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">:</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s1"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">Data.List.List</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s1"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">ℕ</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">→</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s1"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">ℕ</span></span><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF"><o:p></o:p></span></p>
<p class="gmail-p2" style="margin:0in;font-variant-numeric:normal;font-variant-east-asian:normal;font-stretch:normal">
<span class="gmail-s4"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">len2</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">(</span></span><span class="gmail-s1"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428">Data.List.[]</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">)</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">=</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s5"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#D422FF">0</span></span><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428"><o:p></o:p></span></p>
<p class="gmail-p2" style="margin:0in;font-variant-numeric:normal;font-variant-east-asian:normal;font-stretch:normal">
<span class="gmail-s4"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">len2</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">(</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">x
</span></span><span class="gmail-s1"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428">Data.List.∷</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s1"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428">Data.List.[]</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">)</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">=</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s5"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#D422FF">1</span></span><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428"><o:p></o:p></span></p>
<p class="gmail-p2" style="margin:0in;font-variant-numeric:normal;font-variant-east-asian:normal;font-stretch:normal">
<span class="gmail-s4"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">len2</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">(</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">x
</span></span><span class="gmail-s1"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428">Data.List.∷</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black"> y
</span></span><span class="gmail-s1"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428">Data.List.∷</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black"> l</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">)</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">=</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s5"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#D422FF">1</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s4"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">+</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s4"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#5C20FF">len2</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">
</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">(</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black">y
</span></span><span class="gmail-s1"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428">Data.List.∷</span></span><span class="gmail-s2"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:black"> l</span></span><span class="gmail-s3"><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#626262">)</span></span><span style="font-size:8.5pt;font-family:"Menlo",serif;color:#39A428"><o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">On Thu, Aug 19, 2021 at 7:08 PM Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com">matthewdaggitt@gmail.com</a>> wrote:<o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0in 0in 0in 6.0pt;margin-left:4.8pt;margin-right:0in">
<div>
<p class="MsoNormal">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.<o:p></o:p></p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">On Fri, Aug 20, 2021 at 6:45 AM Jason Hu <<a href="mailto:fdhzs2010@hotmail.com" target="_blank">fdhzs2010@hotmail.com</a>> wrote:<o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0in 0in 0in 6.0pt;margin-left:4.8pt;margin-right:0in">
<div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">Hi all,</p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"> </p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">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:</p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"> </p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-family:"Courier New"">open import Data.Nat</span></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-family:"Courier New"">open import Data.List</span></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-family:"Courier New"">open import Data.List.NonEmpty</span></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-family:"Courier New""> </span></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-family:"Courier New"">len : List</span><span style="font-family:"Cambria Math",serif">⁺</span><span style="font-family:"Courier New"">
</span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New""> →
</span><span style="font-family:"Cambria Math",serif">ℕ</span></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-family:"Courier New"">len (x
</span><span style="font-family:"Cambria Math",serif">∷</span><span style="font-family:"Courier New""> []) = 1</span></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-family:"Courier New"">len (x
</span><span style="font-family:"Cambria Math",serif">∷</span><span style="font-family:"Courier New""> y
</span><span style="font-family:"Cambria Math",serif">∷</span><span style="font-family:"Courier New""> l) = len (y
</span><span style="font-family:"Cambria Math",serif">∷</span><span style="font-family:"Courier New""> l)</span></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"> </p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">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.</p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"> </p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">Any idea is appreciated.</p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"> </p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">Thanks,</p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">Jason Hu</p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"> </p>
</div>
</div>
<p class="MsoNormal">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><o:p></o:p></p>
</blockquote>
</div>
</blockquote>
</div>
<p class="MsoNormal" style="margin-left:4.8pt">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>