Ltac2: pose and exists

Developing plugins
1

Dear community,

I would like to create an Ltac2 function that does the equivalent of the following Coq tactics:
pose (ident := constr); exists ident.
An example of the above would be when proving a trivial statement of the form
forall n , exists m, n = m

I know that I can use the pose function from the Ltac2 Std.v file as Std.pose (Some s) t, but I do not know how to continue from here, as Std.pose (Some s) t is now of type unit, and the exists tactic from the Ltac2 Notations.v file takes as input a binding.

2

It is not recommended to use directly the low-level API to write such simple tactics. Instead, just use the corresponding built-in notations and quotations. You can do the following:

Require Import Ltac2.Ltac2.

Ltac2 mytac id c :=
  pose ($id := $c); let id := Control.hyp id in exists $id.

Goal exists m, m = 42.
Proof.
mytac @n constr:(21 + 21).

The only trick is to use Control.hyp to get a constr out of an identifier, but that is about it. (At some point it might be user-friendly to introduce a dedicated notation for this situation, since it is quite common.)

1 Like