Error `Not a variable after goal` · Elpi users & devs

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

Enrico Tassi (Oct 02 2022 at 21:46):

Pierre Vial (Oct 03 2022 at 15:19):

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:

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).

% 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.

Enrico Tassi (Oct 04 2022 at 14:19):

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.

Stream: Elpi users & devs

Topic: Error `Not a variable after goal`

Pierre Vial (Oct 02 2022 at 16:29):

Enrico Tassi (Oct 02 2022 at 21:46):

Pierre Vial (Oct 03 2022 at 15:19):

Enrico Tassi (Oct 04 2022 at 14:19):