Check for evars in a tactic that returns a value

Question

I'm trying to write a tactic that returns a value, and in the course of doing so it needs to check if something is an evar.

Unfortunately, I can't use is_evar because then the tactic isn't deemed to return a value (but rather another tactic). An example is below.

Any suggestions?

Ltac reify_wrt values ls :=
  match ls with
  | nil => constr:(@nil nat)
  | ?a :: ?ls' => let i := lookup a values in
                 let idx := reify_wrt values ls' in
                 constr:(i :: idx)
  | ?e :: ?ls' => is_evar e; 
                  let i := constr:(100) in 
                  let idx := reify_wrt values ls' in
                  constr:(i :: idx)
  end.

Answer 1

There is a neat (or nasty) little trick that you can use to insert tactic execution into constr construction in Coq >= 8.5: wrap it in match goal.

Ltac reify_wrt values ls :=
  match ls with
  | nil => constr:(@nil nat)
  | ?a :: ?ls' => let i := lookup a values in
                 let idx := reify_wrt values ls' in
                 constr:(i :: idx)
  | ?e :: ?ls' => let check := match goal with _ => is_evar e end in
                  let i := constr:(100) in 
                  let idx := reify_wrt values ls' in
                  constr:(i :: idx)
  end.

---

Because programming language arcana fascinate me, I'll now tell you more than you probably ever wanted to know about the present and past execution models of Ltac.

There are two phases of tactic evaluation: there is tactic expression evaluation, and tactic running. During tactic running, sequencing, refine, rewrite, etc, are executed. During tactic expression evaluation, the following constructs are evaluated, if found in the head position of the tactic expressing:

• tactic calls are resolved/followed/inlined/unfolded
• let ... in ... binds the expression-evaluation of it's argument to the name, and does substitution
• constr:(...) is evaluated and type checked
• lazymaytch ... with ... end is evaluated (with back tracking), and returns the first matching branch which successfully expression-evaluates
• match ... with ... end is evaluated (with backtracking) and the branch is eagerly executed. Note that in this picture, match is strange, because it forces the execution of a tactic to come early. If you've ever seen "immediate match producing tactics not allowed in local definitions" in Coq < 8.5, that's an error message explicitly forbidding the behavior I'm exploiting above. I'm guessing it's because this strange behavior of match is a wart that the original devs implementing Ltac wanted to hide. So the only place you can notice it in Coq 8.4 is if you stick match inside of lazymatch and play with failure levels, and notice that lazymatch will backtrack across failures of tactic execution in the inner match when you would normally expect it to fail.

In Coq 8.5, the tactic engine was rewritten to handle dependent subgoals. This induced subtle changes in the semantics of ; which can only be observed when using evars that are shared between multiple goals. In the rewrite, the devs changed the semantics of lazymatch to mean "match without backtracking", and lifted the restriction on "immediate match producing tactics." Hence you can do strange things like:

let dummy := match goal with _ => rewrite H end in
constr:(true)

and have constr-producing tactics with side effects. However, you can no longer do:

let tac := lazymatch b with
                | true => tac1
                | false => tac2
                end in
tac long args.

because in Coq >= 8.5, lazymatch also eagerly evaluates it's branches.

Answer 2

This is a well-known limitation of Ltac: you cannot write a tactic that sometimes returns a value, and sometimes returns another tactic. The solution is to rewrite your tactic in continuation-passing style. I can't give you a detailed explanation on how to do this, unfortunately, but Adam Chlipala's CDPT has a chapter on Ltac that describes the problem; simply look for "continuation" in the text.