[Agda] Restrictions on 'with' introductions?

[Dan Krejsa]

Thans to Andreas, Nils, and Andrea for the suggestions!
I'll try to add a test case to the issue report and then look
at the references suggested.

- Dan


On Fri, Oct 10, 2014 at 8:22 AM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> 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
> >>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141010/e869a4e7/attachment-0001.html