[Agda] Restrictions on 'with' introductions?

[Andreas Abel]

Dan this may well be a bug in Agda.  This might be a related issue:

   https://code.google.com/p/agda/issues/detail?id=745

If you have test case that exhibits the problem, please add it to the 
issue tracker.

Cheers,
Andreas

On 07.10.2014 02:31, Dan Krejsa 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
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/