Now suppose that I have `f : A -> B`

and I need to rename a subterm `f x`

into a variable `y : B`

. The following predicate fails and I think that I know why:

```
rename (app [E, X]) Y :-
target-typ E Ty,
pi y\
decl y _ Ty =>
Y = y.
```

It fails because `Y = y`

makes the newly created `y`

"leak" outside of the `pi`

rule, whereas the predicate you gave me was using recursion under a binder, never "going out". What would be the idiomatic solution for renaming?

You got it right, the problem is the scope of y. The slogan is "there is not such a thing as a free variable".

Here you need y to exist before rename is called, otherwise `Y`

cannot see it. In some sense you need to allocate `y`

in advance. It is hard to suggest any other solution without seeing more code.

I think I can imagine what you are trying to do, see for example the reification example https://github.com/LPCIC/coq-elpi/blob/master/examples/example_reflexive_tactic.v . There the `y`

are not real bound variable, but rather numbers. You could also go this way.

I am exploring the AST of a Coq term and I want to hide some subtrees behind names, so I need to introduce new variables. I'm checking your link right now.

So, either you do it in 2 passes, first you see how many you need, then you create binders for all of them and rename... but it depends what you really have to do, without knowing more I can't be more precise. Well, I've to go now.

Thank you very much for all the help!

I wrote a silly example of another way to skin the cat, hope it helps.

```
From elpi Require Import elpi.
Elpi Command generalize.
Elpi Accumulate lp:{{
% we add a new constructor to terms
type abs int -> term.
% the rule we want
gen {{ 1 }} (abs M) N M :- !, M is N + 1.
% boring fold
gen (app L) (app L1) A A1 :- !, gen-list L L1 A A1.
gen T T A A.
gen-list [] [] A A.
gen-list [X|XS] [Y|YS] A A2 :- gen X Y A A1, gen-list XS YS A1 A2.
% bind back abstracted subterms
bind 0 T T1 :- copy T T1.
bind M T {{ fun x => lp:(B x) }} :-
N is M - 1,
pi x\ copy (abs M) x => bind N T (B x).
main [trm T] :- std.do! [
gen T T1 0 M,
bind M T1 T2,
coq.say {coq.term->string T} "===>" {coq.term->string T2},
].
}}.
Elpi generalize (3 + 7).
```

It prints

```
(3 + 7) ===> (fun (x : ?e) (x0 : ?e0) => S (S x0) + S (S (S (S (S (S x))))))
```

So every `1`

encountered in the term is changed to an abstraction `abs`

with a counter, then after the first run, another predicate runs replacing every abstraction with the correct variable according to the number encoded in this `abs`

constructor. I think I understand the idea; I'll give it a try on my problem and see if it fits. Thank you for the additional idea.

Last updated: Jun 23 2024 at 01:02 UTC