Working with evars and goals · Ltac2

Stream: Ltac2

Topic: Working with evars and goals

Patrick Nicodemus (Feb 03 2024 at 19:44):

I am having trouble understanding how to practically work with evars and goals in Ltac2. I will ask a number of specific questions but I would appreciate any general advice to help me reformulate my approach.

A basic point of confusion I have is that tactics which create evars often create them as a side effect, such as eexists, econstructor, eapply, etc. rather than returning them to the user. However, it is not clear to me how to inspect the environment in order to understand what the evars are that must be resolved to conclude the proof. Similarly, because most tactics operate implicitly on "the" single focused goal and panic if such a goal does not exist, it is not clear how to say "solve this goal."

For example, here is a basic problem which I do not know how to solve with Ltac2: Assume there is a currently focused goal, and I decide that it would be helpful to prove a lemma, L. I would like to construct a new goal corresponding to L, solve it by calling a designated tactic, and bind the resulting proof term to an Ltac2 constr variable. I do not want to use the assert tactic or anything else that would result in the proof having a Gallina let-binding in it for the proof of the lemma, because I want to prove things about the term I'm defining later and it is annoying if there are let-bindings in the term that prohibit simple syntactic pattern matching. (For example if my term is let a := t in f a and I write an Ltac2 match statement match goal with | [ |- f _ ] => ... this will fail.)

The Ltac2 documentation states that "[a thunk] can access a backtracking proof state, consisting among other things of the current evar assignment and the list of goals under focus." I am aware of the following constructs in Ltac2 for managing goals and evars.

Ltac2 @ external focus : int -> int -> (unit -> 'a) -> 'a
Ltac2 @ external shelve : unit -> unit
Ltac2 @ external shelve_unifiable : unit -> unit
Ltac2 @ external new_goal : evar -> unit
Ltac2 @ external with_holes : (unit -> 'a) -> ('a -> 'b) -> 'b
Ltac2 @ external equal : evar -> evar -> bool

I understand what most of these do with some exceptions (What is the meaning of the two integer arguments to focus? What is the difference between shelve and shelve_unifiable?)

Can I actually access and inspect the list of goals as a data structure? The focus command brings a single goal into view, but how do I know how many goals there are? How do I know a priori if "focus on the nth goal" is legal or will fail?
What is the semantics of shelving? If I shelve a goal in Ltac2, where does it "go" and how do I access it later?
Why is there no unshelve command, as in Ltac1? Would this be somehow incompatible with the way Ltac2 models goals?
How can I retrieve, a list of all the current unification variables that have yet to be assigned?
Why does the new_goal command append an evar to the end of the list of goals, rather than the beginning?
with_holes is intended to take an argument f : 'a -> 'b whose job is to solve the evars created as a side effect by the first argument u: unit -> 'a. If u is a term I can imagine just inspecting the argument, finding the holes and figuring out how to solve them, but if u: unit -> unit is just an effectful tactic like econstructor than how can f understand what the unification variables were created by it? How can it inspect the proof state to understand what its job is?

Ike Mulder (Feb 04 2024 at 09:55):

I don't have a complete answer, but here are some partial ones.

For counting the number of goals, I use Control.enter and some mutable state. See here. If there is a better solution I would also like to know :)
For the assert-without-let-binding problem, maybe you could write something like:

let myterm : constr := '(ltac2:(tactic_proving_L) : $L) in ...

(I don't recall exactly how this should be escaped.) Above should Ltac2-let-bind some Coq constr of type L, and you produce that term with an inner ltac2:(..). I am not sure how to pass information to that inner ltac2 function though.

Gaëtan Gilbert (Feb 04 2024 at 10:14):

Why is there no unshelve command, as in Ltac1? Would this be somehow incompatible with the way Ltac2 models goals?

When some API isn't there, usually it's because nobody implemented it.
https://github.com/coq/coq/pull/18604

with_holes is intended to take an argument f : 'a -> 'b whose job is to solve the evars created as a side effect by the first argument u: unit -> 'a. If u is a term I can imagine just inspecting the argument, finding the holes and figuring out how to solve them, but if u: unit -> unit is just an effectful tactic like econstructor than how can f understand what the unification variables were created by it? How can it inspect the proof state to understand what its job is?

The typical use of with_holes is something like apply term, u produces term and f does the unification. Unification is not expected to always solve all new evars, rather we want to produce an error when it doesn't.

Gaëtan Gilbert (Feb 04 2024 at 10:15):

For counting the number of goals, I use Control.enter and some mutable state. See here. If there is a better solution I would also like to know :)

The better solution is to use your definition for now and make a feature request on Coq so you can remove it later.

Gaëtan Gilbert (Feb 04 2024 at 10:28):

let myterm : constr := '(ltac2:(tactic_proving_L) : $L) in ...

This may not be ideal as tactic backtracking doesn't work through open_constr:() (ie '(foo)).
something like this should work I think

Ltac2 solve_with_tac ty tac :=
  let c := '(_ :> $ty) in (* :> means no cast node is produced in the term *)
  match Constr.Unsafe.kind c with
  | Constr.Unsafe.Evar ev _ =>
      Control.new_goal ev > [ .. | tac ()]
  | _ => Control.throw Assertion_failure
  end
  c.

(used like

Import Printf.

Goal True.
  printf "%t" (solve_with_tac 'nat (fun () => exact 42)).
  (* prints 42 *)

)

Patrick Nicodemus (Feb 04 2024 at 14:21):

Thanks, I will try these out!

Last updated: Oct 12 2024 at 12:01 UTC