[Agda] Restrictions on 'with' introductions?

[Dan Krejsa]

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 ;-)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141006/aee84cdb/attachment.html