Hello,

my goal is to produce a tactic with elpi, which, given:

- a (non-dependent) function
`Fu`

of the form`fun (a1 : A1) .... (a : An) => expr : B`

- an expression
`Te`

of type B

produces the statement:

`forall (a1 : A1) .... (a : An), expr = Te`

For now, I'm doing like this:

```
Elpi Tactic tryftp.
Elpi Accumulate lp:{{
pred funtoprod i : term, i : term, o : term.
funtoprod (fun Na Ty Fu1) Te (prod Na Ty Fu2) :- pi x\ decl x Na Ty => funtoprod (Fu1 x) Te (Fu2 x).
funtoprod Fu Bo Re :- coq.unify-eq (app [{{ @eq }}, _ , Fu , Bo]) Re ok.
solve (goal _ _ _ _ [trm L] as G) GL :-
funtoprod L ( {{1}}) Re, coq.ltac.say Re.
}}.
Tactic Notation "tryftp" constr(l) := elpi tryftp (l).
Goal False.
tryftp 0.
tryftp 2.
tryftp (fun (a : nat) => a ).
tryftp (fun (a b : nat) => 0) .
```

but all the examples fail. For instance, `tryftp 0`

fails with the following error message:

```
Unification problem outside the pattern fragment. ((Data.Term.App (global, (Data.Term.App (indc, (Data.Term.CData «O»), [])),
[])) == (Data.Term.AppArg (2, [(Data.Term.Arg (5, 0))]))) Pass -delay-problems-outside-pattern-fragment (elpi command line utility) or set delay_outside_fragment to true (Elpi_API) in order to delay (deprecated, for Teyjus compatibility).
```

What does this error indicate? And how to fix this?

Replacing `coq.ltac.say`

with `coq.say`

makes the code work on my machine.

with `coq.say {coq.term->string Re}`

```
0 = 1
2 = 1
forall a : nat, a = 1
forall H H0 : nat, 0 = 1
```

I think it's what you expected

(unrelated) btw I think your call to `coq.unify-eq`

is useless, because `Re`

is still an unconstrained variable when unification is called, so `Re`

will always be equal to the first argument you gave (`app[{{ @eq }} ...`

). In this case you can directly use equality (`Re = ...`

) or put your left hand side term directly in the head of the clause

Ok, my bad! :sweat:

I'll try with `=`

. At first, I tried it with `Re is ...`

but it didn't work though, so I thought I needed some unification to evaluate the `elpi`

hole

it does work!

Last updated: Apr 20 2024 at 23:01 UTC