<div dir="ltr"><div><div>Thans to Andreas, Nils, and Andrea for the suggestions!<br></div>I'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"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></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't a restriction on the expressions you can scrutinize<br>
using "with" 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 <<a href="mailto:sanzhiyan@gmail.com">sanzhiyan@gmail.com</a>> wrote:<br>
> If you want to understand "with" better you can look at the "More in<br>
> depth" part of this:<br>
><br>
> <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>
><br>
> I find that with enough type dependencies the "with" construct only<br>
> makes sense if you think of its desugaring into an helper function. It<br>
> should also clarify the meaning of the "w" variables in the error<br>
> messages.<br>
><br>
> Cheers,<br>
> Andrea<br>
><br>
> On Tue, Oct 7, 2014 at 2:31 AM, Dan Krejsa <<a href="mailto:dan.krejsa@gmail.com">dan.krejsa@gmail.com</a>> wrote:<br>
>> Hi,<br>
>><br>
>> I'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<br>
>> produces<br>
>> an ordered list that is in fact a permutation of the original list).<br>
>> (The 'ordered' bit goes through pretty easy, but the 'permutation' bit<br>
>> is proving something of a pain to me. In particular, I'm developing all the<br>
>> permutation infrastructure myself...)<br>
>><br>
>> In any case, I notice that I'm structuring a lot of the more difficult<br>
>> proofs / functions as a long chain of 'with' patterns (here's a short one):<br>
>><br>
>> some_func : type<br>
>> some_func args with term1 | term 2<br>
>> ... | term1-deconstructed | term2-deconstructed with f x y<br>
>> ... | fxy with term4<br>
>> ... | term4 = ?<br>
>><br>
>> However, sometimes when I try to add a well-typed term to<br>
>> the values scrutinized via the 'with' , Agda complains of some type<br>
>> error 'when checking that the type <some long type> of the generated with<br>
>> function is well-formed'.<br>
>><br>
>> 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>
>> some_func : type<br>
>> some_func args with term1 | term 2<br>
>> ... | term1-deconstructed | term2-deconstructed with f x y | inspect (f x)<br>
>> y<br>
>> ... | fxy | [ fxydef ] with term4<br>
>> ... | term4 = ?<br>
>><br>
>> then I get a type error about the generated with-function. (That's just an<br>
>> example, other sorts of as-far-as-I-can-see good terms sometimes also cause<br>
>> similar problems.)<br>
>><br>
>> So, I don't really understand what the 'with function' is, and what are the<br>
>> restrictions on the terms that one can scrutinize using 'with'.<br>
>><br>
>> Or, if this is just a shortcoming/bug in current Agda, what would be a<br>
>> workaround for such a case?<br>
>><br>
>> Thanks,<br>
>><br>
>> - Dan<br>
>><br>
>> P.S. I could post my file, but it's pretty hairy still. (I could try to find<br>
>> 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<br>
>> practical Agda proving style & skills? I'm not in school and am learning<br>
>> mostly on my own out of personal interest. I'm hoping to improve my nose<br>
>> for 'code smells' in Agda, things like the 'green slime' mentioned in a<br>
>> recent Connor McBride paper ;-)<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" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>><br>
</div></div></blockquote></div><br></div>