## Stream: Elpi users & devs

### Topic: ✔ Problem of unifying evars?

#### Pierre Vial (Sep 13 2022 at 09:29):

Hello,
I'm trying to write a tactic which, given a term `m` which is of the form:

``````match e with
| C0 .... => f_0
| C1 x1 .... xn =>  f1
| .... end.
``````

produces the statement : `forall (x1 : A1) ... (xn : An), e = C1 x1 ... xn -> m = f1`
Right now, I'm doing this:

``````Elpi Accumulate lp:{{
pred essai i : term, i : list term, i : term, i : term, i : term, o : term.
essai (fun X Ty F) L M E C  (prod X Ty Re) :- !, pi x\ decl x _ Ty =>  essai (F x) [x | L ] M E C  (Re x).
essai F L M E C (prod _ (app [{{ @eq }}, _ , E , app [C | L] ]) (c\ app [{{@eq}}, _ , M , F ]) ).
}}.

Elpi Query lp:{{.     %%% This query produces an untypable term, but it succeeds
essai (fun _ X0 c0\ fun _ (X1 c0) c1\ {{ true}}) []
{{(match 2 with
| 0 => true
| S k => false
end) }}
{{2}} {{S}} P.
}}.

Elpi Tactic mytac.
Elpi Accumulate lp:{{
solve (goal _ _ _ _ [trm M] as G) GL :-
M  = (match E _ LCases),  coq.typecheck E Ty Ok,
(global (indt I)  = Ty ; app [global (indt I) | _ ] = Ty),  coq.env.indt I _ _ P TyI Ks KTs,
std.map Ks (x\ y\ y = global (indc x)) LCtors, %coq.say LCtors,
std.nth 1 LCtors C,  std.nth 1 LCases F,   coq.mk-n-holes P H,
coq.say "Ty is" Ty "\n\nF is " F  "\n\nM is" M  "\n\nE is" E "\n\nC is" C,
essai F [] M E C Re, coq.say Re.        %%% If this line is commented, the queries below succeed
Elpi Typecheck.

Tactic Notation "mytac" constr(l) := elpi mytac (l).
Goal 2 +2 = 5.
mytac
(match 2 with
| 0 => true
| S k => false
end).
mytac (match [1 ; 2] with
| [] => false
| _ :: _ => true
end
).
Abort.
``````

For some reason, the two last queries fail (without a specific message error). I dont' understand what does not work, since the tactic type-checks, and the parameters, which are printed, seem of the good form. So is this some problem of unifying an elpi variable?

#### Pierre Vial (Sep 13 2022 at 20:03):

What is very mysterious is that if I replace the last query of the tactic `mytac` (i.e. the line `essai F [] M E C Re, coq.say Re`) with the query

``````essai (fun _ X0 c0\ fun _ (X1 c0) c1\ {{ true}}) []
{{(match 2 with
| 0 => true
| S k => false
end) }}  {{2}} {{S}} P.
``````

the calls of `mytac` below also fail.
I really don't understand why it should be so. I guess the problem is neither with unification nor with typechecking

#### Enrico Tassi (Sep 14 2022 at 06:14):

I'm sorry I don't have much time today. One mistake is that the third argument of coq.typecheck is `Ok` which is a variable, and not the constant `ok`.
The idiomatic way of calling it is `std.assert-ok! (coq.typecheck T Ty) " some message"` which tests if the result is ok, if not it prints the error message produced by Coq and prefixes it with some message.

#### Pierre Vial (Sep 14 2022 at 07:38):

Unfortunately, it does not seem that the problem was with `ok`, which I just corrected (actually, the printing commands below ensured that the type was correctly read)

#### Pierre Vial (Sep 14 2022 at 09:26):

OK, thanks to @Chantal Keller and @Louise Dubois de Prisque , I understood where the problem was: the predicate `essai` should have been between `Elpi Tactic mytac.` and `Elpi Typecheck.`
I was mistaken into thinking that accumulation would pass through `Elpi` tactics, commands and programs

#### Notification Bot (Sep 14 2022 at 10:38):

Pierre Vial has marked this topic as resolved.

Last updated: Jun 06 2023 at 23:01 UTC