[Agda] Agsy vs Unifier

[Andreas Abel]

Just on
 > - Somewhat related: A way of expanding a resolved underscore to an
 > actual term would be neat.

A workaround is to replace the underscore by a question mark and after 
reloading use C-c C-s (solve).

On 27.09.2016 18:18, Guido Martínez wrote:
> Hi all,
>
> When doing transitivity reasoning on ≅, I used to use C-a to fill the
> first and last holes (since they're determined by the outer type of
> the equality), and every time I filled a justification, I could use
> C-a to fill the next hole, as the type of the justification (and the
> previous hole) perfectly determine the next.
>
> In the attached file, you can see this working great on the proof of
> comp-iso. One can delete any term and use C-a to fill it in, even when
> only one bordering justification is set (except for first and last,
> which always work). (My Agda version is 2.5.1).
>
> On some other examples, such as the composition of functors on the
> bottom of the file, this does not work anymore. Agsy is unable to fill
> any hole at all, even when the justifications are all in place and
> correct. What's more: writing "_" on every term hole works just fine,
> and one can work by filling justifications one by one (looking at the
> goal type to see the current term). Thus unification seems to beat
> Agsy in this situation. (underscores are actually resolved by
> unification, right?)
>
> So a few questions arise:
>
> - Why can't Agsy find these terms? They seem to be completely
> determined by the context, and can apparently be found by unification.
>
> - Shouldn't C-a try to unify too? I understand Agsy is a separate tool
> from Agda so maybe it cannot do unification itself, but I guess Agda
> could try to see if the hole is unifiable before calling Agsy. As a
> user I certainly expect C-a to be at least as strong as unification.
>
> - Somewhat related: A way of expanding a resolved underscore to an
> actual term would be neat.
>
> Hope I wasn't too confusing. I have more examples if required.
> Thanks!
> Guido
>
>
>
> _______________________________________________
> 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/