[Agda] Agsy vs Unifier

[Guido Martínez]

On Tue, Sep 27, 2016 at 1:36 PM, Andreas Abel <abela at chalmers.se> wrote:
> 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).
Ah! I wasn't familiar with C-c C-s. That definitely helps a lot in my
case, it seems to solve every "term" goal easily. Thanks!

So for trying to solve a goal one should try both C-s and C-a? Or is
the behaviour I described in the OP unexpected?



>
>
> 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/