What does the error `Not a variable after goal`

mean?

I'm tinkering with `elpi`

recursive predicates, and I encounter this message during a recursive call.

Apparently, it's related to this line of `ml`

code, but I don't really get its meaning

Hum, it is likely a bug but I need your code in order to reproduce it.

Well, this example is quite long.

The idea is the following:

Assume that `m`

is a `Coq`

term of the form

``match e with

...

| C_i x_1 .... x_{k_i} => f_i

...

end.

```
where the match contains `n` cases (i.e. there are`n` constructors : no deep pattern-matching).
Then `pm_in_goal M` is supposed to assert and prove in the local context the following `n` obviously valid statements:
```

forall x_1 ... x_{k_i}, e = C_i x_1 ... x_{k_i} -> m = f_i

```
Now, the code. Search for !!! to get the salient parts: I think it's a problem on how I'm currently binding the goals in the recursive call of `pm_in_goal_case`, which is the main predicate of the tactic
```

Ltac intro_inv := (let HProd := fresh "H" in

intro HProd ; inversion HProd ; reflexivity).

Elpi Tactic pm_in_goal.

Elpi Accumulate lp:{{

% fun_to_prod L M E C (fun (x1 : A1) ... (xn : An ) => f)

% outputs

% forall (x1 : A1) ... (xn : An ), E = C [x1 ; ... ; xn L] -> M = f

% where the x1 ... xn may occur in the expression f

% In practice, when fun_to_prod is called, M is a match on the expression E and C is a constructor of the type of E and L = [] (L is an accumulator)

pred fun_to_prod i : list term, i : term, i : term, i : term, i : term, o : term.

fun_to_prod L M E C (fun X Ty F) (prod X Ty Re) :- !, coq.say "fun", pi x\ decl x _ Ty =>

fun_to_prod [x | L ] M E C (F x) (Re x).

fun_to_prod L M E C F (prod _ (app [{{ @eq }}, _ , E , app [C | L] ]) (c\ app [{{@eq}}, _ , M , F ]) ).

% readmatch M E Ty LCa P Ks H has for only input M, which is supposed to be a term of the form

% match E with

% ...

% | C_i x_1 .... x_n => f_i

% ... end

% Then E is the matched expression, whose type is Ty

% LCa is the list of cases of [match]

% P is the number of (type) parameters of Ty %%% \Q is P useful?

% Ls is the list of the constructors of Ty (elpi type [constructor])

% H is a list of P holes

pred readmatch i : term, o : term, o : term, o : list term, o : int, o : list constructor, o : list term.

readmatch M E Ty LCa P Ks H :-

M = (match E _ LCa),

coq.typecheck E Ty ok,

(global (indt I) = Ty ; app [global (indt I) | _ ] = Ty),

coq.env.indt I _ _ P _ Ks _,

coq.mk-n-holes P H.

% pm_in_goal_case M E H [K1 , ... , Kn ] [F1 , ... , Fn ] G GL succesively asserts

% and proves Pro_1, ..., Pro_n where fun_to_prod [] L M E (app [C_i | H]) Pro_i

% and C_i is the 'term' associated to the 'constructor' K_i

% Notes:

% * H is supposed to be a list of p holes representing the p parameters of

% the inductive datatype of M

% * the proof of each Pro_i is obtained with a call to the tactic 'intro_inv'

pred pm_in_goal_case i : term, i : term, i : list term, i : list constructor, i : list term, i : goal, o : list sealed-goal.

pm_in_goal_case M E H [] [] G [seal G] :- coq.say "fin assblut". % should we just have _ instead of [seal G]?

pm_in_goal_case M E H [K | TK] [F | TLCa ] G GL :- % GL remplaçable par [seal G] ?

app [global (indc K) | H] = C, coq.say "pm_in_goal_case 2", fun_to_prod [] M E C F Pro,

coq.typecheck Pro _ ok,

coq.ltac.call "myassert" [trm Pro] G [seal GPro | LSG ], %seal G],

coq.ltac.call "intro_inv" [] GPro [],

pm_in_goal_case M E H TK TLCa G [seal G0]. %%% !!! if this line is commented, the example below does not fail (but one has only 1 statement instead of 2)

solve (goal _ _ _ _ [trm M] as G) GL :-

coq.say "solve 1", readmatch M E Ty LCa P Ks H, coq.say "solve 2",

pm_in_goal_case M E H Ks LCa G GL.

}}.

Elpi Typecheck.

Goal nat.

Elpi Query lp:{{ coq.say "THE TEST". }}.

elpi pm_in_goal (match 2 with

| 0 => true

| S k => false.

end). %% !!! Here is the error

exact 0.

Abort.

```
```

```
Elpi Tactic match_to_eqn.
Elpi Accumulate lp:{{
pred mkeqbo i:term, i:term, i:term, i:term, o:term.
mkeqbo {{ fun x => lp:(Bo x) }} K E M {{ fun x => lp:(Bo1 x) }} :- !,
@pi-decl `x` _ x\
mkeqbo (Bo x) {coq.mk-app K [x]} E M (Bo1 x).
mkeqbo B K E (match _ RTy Bs as M) {{ fun h : lp:E = lp:K => lp:Proof h : lp:Ty }} :-
Proof = {{ @eq_ind_r _ lp:K lp:Pred (refl_equal lp:B) lp:E }},
Pred = {{ fun x => lp:{{ match {{ x }} RTy Bs }} = lp:B }},
Ty = {{ lp:M = lp:B }}.
pred mkeqn i:list term, i:list term, i:term, i:term, o:term.
mkeqn [] [] _ _ {{ _ }}.
mkeqn [B|Bs] [K|Ks] E M {{ let h := lp:Bo in lp:(R h) }} :-
mkeqbo B K E M Bo,
@pi-def `h` _ Bo h\
mkeqn Bs Ks E M (R h).
solve (goal _ _ _ _ [trm (match E _ Bs as M)] as G) GL :- std.do! [
std.assert-ok! (coq.typecheck M _) "illtyped input",
coq.typecheck E Ty ok,
coq.safe-dest-app Ty (global (indt I)) Args,
coq.env.indt I _ _ Pno _ Ks _,
std.take Pno Args Params,
std.map Ks (x\r\ coq.mk-app (global (indc x)) Params r) KPs,
mkeqn Bs KPs E M T,
%BUG: coq.say "M=" M "T=" {coq.term->string T},
std.assert! (refine T G GL) "bug in term generation",
].
}}.
Elpi Typecheck.
Lemma foo : nat.
elpi match_to_eqn (match 2 with
| 0 => true
| S k => false
end).
```

Thanks for sharing your code. I had to rewrite it, and finally the bug is caused by a debug print. What a shame. I'll look into fixing it.

Last updated: Jun 06 2023 at 22:01 UTC