Hello. Let me ask my question(s) of the day... Is there a way to give a fresh name `f`

to a term `x`

and add it to the proof context, like Ltac's `pose (f := x)`

would do, but with a fresh `f`

name? Is it possible to declare a new variable without giving its definition? Like having a new `x : nat`

in the context, not knowing anything about it?

I think the only way I have in mind is to generate a goal `forall x, forall f, f = blah -> G`

with `blah`

being the definition of `f`

and `G`

the old goal, then calling Ltac's `intros`

to put these `forall`

headers in the context. This looks like a workaround though, I wonder if something better exists.

There is not much "ltac" written in elpi, but you can find some code in examples/ and the app/eltac/ POC. Both tactics boil down to a call to 'refine' with a letin or a beta redex. About the "freshness" of the names, I would leave the problem on the side and use new_int as a start.

I managed to produce a small example, but this does not work as I expected in my use case... (Probably my bad.)

```
Elpi Tactic pose.
Elpi Accumulate lp:{{
solve [trm T] [G] GS :-
refine {{ let _ := lp:T in _ }} G GS.
}}.
Elpi Typecheck.
Goal False.
elpi pose (I).
```

```
Elpi Tactic pose.
Elpi Accumulate lp:{{
solve [str ID, trm T] [G] GS :-
coq.id->name ID N,
refine (let N _ T _) G GS.
}}.
Elpi Typecheck.
Goal False.
elpi pose "x" (I).
elpi pose "x" (I).
```

Here `N`

is a "hint", and elpi will not make the variable clash, but rather introduce a funny name instead, which you can't rely upon.

if you want you variable to be fresh and with a "predictable" name, I suggest you pick `x1`

... `xN`

and you call `pred new_int o:int`

which grants a fresh integer any time you call it.

FTR, the `{{ quotation }}`

do not let you specify an elpi variable for a name (only for terms). This is why I used the "raw" elpi term for the let in.

By "does not work as I expected", I meant that it does not introduce any assumption. Since it refines the goal with a bigger proof term, I'm having a hard time to identify the source of the issue.

It works here. Which version are you on?

```
pred assume-constraints i:(list term), i:term, o:term.
assume-constraints [] P P :- !.
assume-constraints (A :: Atoms) P Q :- !,
zify-atom A CA,
assume-constraints Atoms {{ let _ := lp:CA in lp:P }} Q.
```

The problem is that `P`

does not see `_`

.

You could write `{{ let x := lp:CA in lp:{{ P x }} }}`

to put `x`

in the scope of `P`

(or the shorter and equivalent `lp:(P x)`

) *but* here `P`

has the wrong elpi type, it should be `term -> term`

for `P x`

to typecheck.

You can also say that `P`

is a term of functional type in Coq, and write `{{ let x := lp:CA in lp:P x }}`

(this time the application is a Coq one, an `app`

node) but this proof term implements a cut anyway, so you don't see a let-in but a forall.

There is another little problem, you wrap the lets around the wrong hole. Here some code which "works". I don't what you really want to do, so I hope I did put you in some direction.

```
pred assume-constraints i:(list term), i:term, o:term.
assume-constraints [] P P :- !.
assume-constraints (A :: Atoms) P Q :- !,
zify-atom A CA,
assume-constraints Atoms {{ let x := lp:CA in lp:P x }} Q.
% TODO: apply Z-ification for hypotheses.
solve _ [(goal Ctx _ Ty _ as G)] GS :-
Ctx => std.do! [
zify-prop Ty _ _ Ty1->Ty_ Atoms,
close Atoms,
% FIXME: [ZifyProof] contains let-ins for constraints, but they do not
% appear in the goal.
assume-constraints Atoms P_ ZifyMissingProof,
ZifyProof = Ty1->Ty_ ZifyMissingProof,
std.assert-ok! (coq.typecheck ZifyProof _) "bad proof",
coq.say {coq.term->string ZifyProof},
refine ZifyProof G GS
].
```

the proof term you were generating was `(let H in ... (Ty1->Ty_ Kont))`

, IMO you want H to be visible (hence passed to) `Kont`

.

So this is the new term `(Ty1->Ty_ (let H : TH := .. in Kont H))`

and the new goal is `Kont : TH -> Z.of_nat .. = Z.of_nat ..`

.

Bottom line, if you type check (?e 3 : G) you infer for ?e : nat -> G, the same if you infer (let x := 3 in ?e 3 : G). If you want a let in the type of ?e you have to write it by yourself, since no type inference rule puts a let in the type. This makes a let instead of a forall in the resulting goal: `assume-constraints Atoms {{ (lp:P : let x := lp:CA in _) }} Q.`

I see. Thank you so much!

FTR, I managed to turn the function application `P x`

into Elpi one, so that constraints appear as assumptions after `refine`

. Here is my solution:

```
% [letins [T1, ..., Tn] U] states that U = {{ let x1 := T1 in ... let xn := Tn in _ }}.
pred letins i:(list term), o:term.
letins [] U :- !.
letins (T :: TS) (let _ _ T U) :- !, pi x\ letins TS (U x).
```

But, if I want to touch the innermost placeholder afterward, I don't see how to do that. (For now, it is OK for me.)

What do you mean by touch? You can match an evar if the argument is in input mode using the 'uvar' keyword, see the code of copy for example, or use the 'var' built-in.

I don't know about automatically introduction. Maybe it is good in your case, but is not very SSR style....

Last updated: Feb 05 2023 at 13:02 UTC