<div dir="ltr"><div><div>Hi,<br><br></div>I&#39;m trying to work through a self-imposed exercise in Agda, proving<br>that a functional insertion sort algorithm on lists is correct (i.e., it produces<br>an ordered list that is in fact a permutation of the original list).<br></div><div>(The &#39;ordered&#39; bit goes through pretty easy, but the &#39;permutation&#39; bit<br>is proving something of a pain to me.  In particular, I&#39;m developing all the<br>permutation infrastructure myself...)<br><br></div><div>In any case, I notice that I&#39;m structuring a lot of the more difficult proofs / functions as a long chain of &#39;with&#39; patterns  (here&#39;s a short one):<br><br></div><div>some_func : type<br></div><div>some_func  args  with term1 | term 2<br></div><div>... | term1-deconstructed | term2-deconstructed  with f x y<br></div><div>... | fxy  with term4<br></div><div>... | term4 = ?<br><br></div><div>However, sometimes when I try to add a well-typed term to<br></div><div>the values scrutinized via the &#39;with&#39; , Agda complains of some type<br>error &#39;when checking that the type &lt;some long type&gt; of the generated with function is well-formed&#39;.<br><br></div><div>For instance, maybe the above example works fine, but if I also try to<br>get Agda to remember that fxy = f x y using inspect-on-steroids,<br><br><div>some_func : type<br></div><div>some_func  args  with term1 | term 2<br></div><div>... | term1-deconstructed | term2-deconstructed  with f x y | inspect (f x) y<br></div><div>... | fxy | [ fxydef ] with term4<br></div>... | term4 = ?<br><br></div><div>then I get a type error about the generated with-function.  (That&#39;s just an example, other sorts of as-far-as-I-can-see good terms sometimes also cause similar problems.)<br><br></div><div>So, I don&#39;t really understand what the &#39;with function&#39; is, and what are the restrictions on the terms that one can scrutinize using &#39;with&#39;.<br><br>Or, if this is just a shortcoming/bug in current Agda, what would be a workaround for such a case?<br><br></div><div>Thanks,<br><br></div><div>- Dan<br><br></div><div>P.S. I could post my file, but it&#39;s pretty hairy still. (I could try to find a small or minimal test case if this is not already a known problem.)<br><br>That reminds me: is there a good forum for asking for help improving practical Agda proving style &amp; skills?  I&#39;m not in school and am learning mostly on my own out of personal interest.  I&#39;m hoping to improve my nose for &#39;code smells&#39; in Agda, things like the &#39;green slime&#39; mentioned in a recent Connor McBride paper ;-)<br><br></div><div><br></div></div>