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?

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

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.

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)

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

Pierre Vial has marked this topic as resolved.

Last updated: Jun 06 2023 at 23:01 UTC