[Agda] Restrictions on 'with' introductions?

[Andrea Vezzosi]

Oh, and the standard workaround is to try to come up with an helper
function yourself.
Sometimes you can be smarter about where you turn the expression you
want to match into a variable, or maybe you can work around type
dependencies by proving something more general.

Also, there isn't a restriction on the expressions you can scrutinize
using "with" per se, it all depends on how they appear in the goal and
context type, i.e. whether the helper function generated as described
on the wiki can be given a well-formed type.

On Fri, Oct 10, 2014 at 5:11 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
> If you want to understand "with" better you can look at the "More in
> depth" part of this:
>
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.With-expression
>
> I find that with enough type dependencies the "with" construct only
> makes sense if you think of its desugaring into an helper function. It
> should also clarify the meaning of the "w" variables in the error
> messages.
>
> Cheers,
> Andrea
>
> On Tue, Oct 7, 2014 at 2:31 AM, Dan Krejsa <dan.krejsa at gmail.com> wrote:
>> Hi,
>>
>> I'm trying to work through a self-imposed exercise in Agda, proving
>> that a functional insertion sort algorithm on lists is correct (i.e., it
>> produces
>> an ordered list that is in fact a permutation of the original list).
>> (The 'ordered' bit goes through pretty easy, but the 'permutation' bit
>> is proving something of a pain to me.  In particular, I'm developing all the
>> permutation infrastructure myself...)
>>
>> In any case, I notice that I'm structuring a lot of the more difficult
>> proofs / functions as a long chain of 'with' patterns  (here's a short one):
>>
>> some_func : type
>> some_func  args  with term1 | term 2
>> ... | term1-deconstructed | term2-deconstructed  with f x y
>> ... | fxy  with term4
>> ... | term4 = ?
>>
>> However, sometimes when I try to add a well-typed term to
>> the values scrutinized via the 'with' , Agda complains of some type
>> error 'when checking that the type <some long type> of the generated with
>> function is well-formed'.
>>
>> For instance, maybe the above example works fine, but if I also try to
>> get Agda to remember that fxy = f x y using inspect-on-steroids,
>>
>> some_func : type
>> some_func  args  with term1 | term 2
>> ... | term1-deconstructed | term2-deconstructed  with f x y | inspect (f x)
>> y
>> ... | fxy | [ fxydef ] with term4
>> ... | term4 = ?
>>
>> then I get a type error about the generated with-function.  (That's just an
>> example, other sorts of as-far-as-I-can-see good terms sometimes also cause
>> similar problems.)
>>
>> So, I don't really understand what the 'with function' is, and what are the
>> restrictions on the terms that one can scrutinize using 'with'.
>>
>> Or, if this is just a shortcoming/bug in current Agda, what would be a
>> workaround for such a case?
>>
>> Thanks,
>>
>> - Dan
>>
>> P.S. I could post my file, but it's pretty hairy still. (I could try to find
>> a small or minimal test case if this is not already a known problem.)
>>
>> That reminds me: is there a good forum for asking for help improving
>> practical Agda proving style & skills?  I'm not in school and am learning
>> mostly on my own out of personal interest.  I'm hoping to improve my nose
>> for 'code smells' in Agda, things like the 'green slime' mentioned in a
>> recent Connor McBride paper ;-)
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>