<div dir="ltr"><div><div>Thans to Andreas, Nils, and Andrea for the suggestions!<br></div>I&#39;ll try to add a test case to the issue report and then look<br>at the references suggested.<br><br></div>- Dan<br><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Oct 10, 2014 at 8:22 AM, Andrea Vezzosi <span dir="ltr">&lt;<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Oh, and the standard workaround is to try to come up with an helper<br>
function yourself.<br>
Sometimes you can be smarter about where you turn the expression you<br>
want to match into a variable, or maybe you can work around type<br>
dependencies by proving something more general.<br>
<br>
Also, there isn&#39;t a restriction on the expressions you can scrutinize<br>
using &quot;with&quot; per se, it all depends on how they appear in the goal and<br>
context type, i.e. whether the helper function generated as described<br>
on the wiki can be given a well-formed type.<br>
<div class="HOEnZb"><div class="h5"><br>
On Fri, Oct 10, 2014 at 5:11 PM, Andrea Vezzosi &lt;<a href="mailto:sanzhiyan@gmail.com">sanzhiyan@gmail.com</a>&gt; wrote:<br>
&gt; If you want to understand &quot;with&quot; better you can look at the &quot;More in<br>
&gt; depth&quot; part of this:<br>
&gt;<br>
&gt; <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.With-expression" target="_blank">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.With-expression</a><br>
&gt;<br>
&gt; I find that with enough type dependencies the &quot;with&quot; construct only<br>
&gt; makes sense if you think of its desugaring into an helper function. It<br>
&gt; should also clarify the meaning of the &quot;w&quot; variables in the error<br>
&gt; messages.<br>
&gt;<br>
&gt; Cheers,<br>
&gt; Andrea<br>
&gt;<br>
&gt; On Tue, Oct 7, 2014 at 2:31 AM, Dan Krejsa &lt;<a href="mailto:dan.krejsa@gmail.com">dan.krejsa@gmail.com</a>&gt; wrote:<br>
&gt;&gt; Hi,<br>
&gt;&gt;<br>
&gt;&gt; I&#39;m trying to work through a self-imposed exercise in Agda, proving<br>
&gt;&gt; that a functional insertion sort algorithm on lists is correct (i.e., it<br>
&gt;&gt; produces<br>
&gt;&gt; an ordered list that is in fact a permutation of the original list).<br>
&gt;&gt; (The &#39;ordered&#39; bit goes through pretty easy, but the &#39;permutation&#39; bit<br>
&gt;&gt; is proving something of a pain to me.  In particular, I&#39;m developing all the<br>
&gt;&gt; permutation infrastructure myself...)<br>
&gt;&gt;<br>
&gt;&gt; In any case, I notice that I&#39;m structuring a lot of the more difficult<br>
&gt;&gt; proofs / functions as a long chain of &#39;with&#39; patterns  (here&#39;s a short one):<br>
&gt;&gt;<br>
&gt;&gt; some_func : type<br>
&gt;&gt; some_func  args  with term1 | term 2<br>
&gt;&gt; ... | term1-deconstructed | term2-deconstructed  with f x y<br>
&gt;&gt; ... | fxy  with term4<br>
&gt;&gt; ... | term4 = ?<br>
&gt;&gt;<br>
&gt;&gt; However, sometimes when I try to add a well-typed term to<br>
&gt;&gt; the values scrutinized via the &#39;with&#39; , Agda complains of some type<br>
&gt;&gt; error &#39;when checking that the type &lt;some long type&gt; of the generated with<br>
&gt;&gt; function is well-formed&#39;.<br>
&gt;&gt;<br>
&gt;&gt; For instance, maybe the above example works fine, but if I also try to<br>
&gt;&gt; get Agda to remember that fxy = f x y using inspect-on-steroids,<br>
&gt;&gt;<br>
&gt;&gt; some_func : type<br>
&gt;&gt; some_func  args  with term1 | term 2<br>
&gt;&gt; ... | term1-deconstructed | term2-deconstructed  with f x y | inspect (f x)<br>
&gt;&gt; y<br>
&gt;&gt; ... | fxy | [ fxydef ] with term4<br>
&gt;&gt; ... | term4 = ?<br>
&gt;&gt;<br>
&gt;&gt; then I get a type error about the generated with-function.  (That&#39;s just an<br>
&gt;&gt; example, other sorts of as-far-as-I-can-see good terms sometimes also cause<br>
&gt;&gt; similar problems.)<br>
&gt;&gt;<br>
&gt;&gt; So, I don&#39;t really understand what the &#39;with function&#39; is, and what are the<br>
&gt;&gt; restrictions on the terms that one can scrutinize using &#39;with&#39;.<br>
&gt;&gt;<br>
&gt;&gt; Or, if this is just a shortcoming/bug in current Agda, what would be a<br>
&gt;&gt; workaround for such a case?<br>
&gt;&gt;<br>
&gt;&gt; Thanks,<br>
&gt;&gt;<br>
&gt;&gt; - Dan<br>
&gt;&gt;<br>
&gt;&gt; P.S. I could post my file, but it&#39;s pretty hairy still. (I could try to find<br>
&gt;&gt; a small or minimal test case if this is not already a known problem.)<br>
&gt;&gt;<br>
&gt;&gt; That reminds me: is there a good forum for asking for help improving<br>
&gt;&gt; practical Agda proving style &amp; skills?  I&#39;m not in school and am learning<br>
&gt;&gt; mostly on my own out of personal interest.  I&#39;m hoping to improve my nose<br>
&gt;&gt; for &#39;code smells&#39; in Agda, things like the &#39;green slime&#39; mentioned in a<br>
&gt;&gt; recent Connor McBride paper ;-)<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; _______________________________________________<br>
&gt;&gt; Agda mailing list<br>
&gt;&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;<br>
</div></div></blockquote></div><br></div>