Enzo Crance (Feb 08 2021 at 17:02): Enzo Crance (Feb 08 2021 at 17:02):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?
Enrico Tassi (Feb 08 2021 at 17:08):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.
Enrico Tassi (Feb 08 2021 at 17:12):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.
Enzo Crance (Feb 08 2021 at 17:15):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.
Enrico Tassi (Feb 08 2021 at 17:20):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.
Enzo Crance (Feb 08 2021 at 17:21):Thank you very much for all the help!
Enrico Tassi (Feb 09 2021 at 11:03):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: Oct 13 2024 at 01:02 UTC