[Agda] Question on `unify` function in Reflection API

[Kenichi Asai]

Dear all,

To add a bit more background information, Chiaki wants to write a
tactic using Reflection API that can automatically search for the next
reduction step for a calculus.  As a first step, she considers the
addition calculus:

E = number | E + E

with the reduction rules:

left_ : e1 + e2 -> e1' + e2  if e1 -> e1'
right_: n1 + e2 -> n1  + e2' if e2 -> e2'
plus_ : n  + m  -> r         if n + m is r

Then, given (1 + 2) + 3, we know that the first rule to be applied
must be left_, and given 0 + 1, the first rule to be applied must be
plus_.  For now, she writes a macro, runTC, in the file nat.agda that
fills the goal with plus_ and observes that it works for 0 + 1.

So far, so good.

What she wants to formalize is the lambda calculus, and she wants to
employ PHOAS by Chlipala for variable binding.  When she writes the
same thing for the lambda calculus with PHOAS, however, she encounters
a mysterious error.  The example file, nat-param.agda, is the
(extremely) simplified version of it, where she considers only the
addition calculus whose terms are parameterized by a type, Typ, which
is present but not used at all.

Then, the same macro no longer works.  Why not?  If she enters plus_
in the goal and refine it (C-c C-r), it is accepted.  Why doesn't
unifying the goal with plus_ in runTC work?

Thanks for any help!

Sincerely,

-- 
Kenichi Asai


On Fri, Oct 11, 2019 at 04:34:23PM +0900,
 Chiaki Ishio wrote:

> Hello all,
> 
> I have a question on the `unify` function in Reflection API.
> I got two minimal examples of multi-step addition of natural numbers
> (nat.agda, nat-param.agda).
> 
> In the first example (nat.agda), the goal of the fourth argument is
> dependent on the second argument, but I can unify the desired constructor.
> 
> multi-step : Reduce* (E (V 0) (V 1)) (V 1)
> multi-step = trans* (E (V 0) (V 1))
>                     {!!} -- 2nd arg
>                     (V 1)
>                     {!runTC!} -- 4th arg, runTC succeeds
>                     {!!}
> 
> In another example (nat-param.agda), datatype definitions are
> parameterized, but those parameters don't have any real meanings.
> When I try the following code, `unify` function in Reflection API fails
> unless I fill up the second argument.
> 
> multi-step : (v : Typ) → Reduce* v (E (V 0) (V 1)) (V 1) -- we have a
> parameter `v`
> multi-step v = trans* (E (V 0) (V 1))
>                       {!!} -- 2nd arg
>                       (V 1)
>                       {!runTC!} -- 4th arg, runTC fails
>                       {!!}
> 
> I am not sure why this happens, and not sure of any difference between the
> `unify` function and the refine command in Emacs Mode.
> 
> Any comments would be appreciated.
> 
> Best,
> 
> Chiaki Ishio
> chiaki.ishio at gmail.com