[Agda] Restrictions on 'with' introductions?

[Andrea Vezzosi]

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
>