## Stream: Elpi users & devs

### Topic: Definition of copy

#### Chantal Keller (Apr 11 2022 at 15:31):

Hi
In the definition of copy here:

• what is the predicate `name` in the first rule?
• what is the interest of having two `!` in the first rule?
(Just a remark: there is a typo in the initial comment l.106, a `"` is missing.)

#### Enrico Tassi (Apr 11 2022 at 18:11):

`name` is an Elpi builtin (not specific to Coq) so it is documented briefly here: https://github.com/LPCIC/coq-elpi/blob/master/elpi-builtin.elpi#L347 . The basic usage is to test if a term (of any type) is an eigenvariable, a name, aka a `pi` quantified constant.

Now that I have to explain it, I regret I wrote `copy` this way, but anyway, here it is.

The nicest version of copy is, for the lambda case, something like:

``````copy (fun N T B) (fun N T1 B1) :- copy T T1, pi x\ copy x x => copy (B x) (B1 x)
``````

since `x` is a fresh constant it is introduced with a specific rule, to say to copy it to itself.

As a speedup, I did add a

``````copy X X.
``````

clause, and omit the `copy x x =>` part when I cross a binder (that is the speedup).

Unfortunately `copy X X` is too rough, it also applies to non atomic terms for example, so I refined it to `copy X X :- name X` to ensure it is only used for names like `x`.

Now, the last detail is that I wrote it like

``````copy X Y :- name X, !, X = Y, !.
``````

this rule is operationally a bit more precise: first tests if `X` is a name, then commit to this rule with `!`, then say that `X` is `Y`, and finally take the first solution of the assignment.

About using `X = Y`, I think I wanted to be super sure that in case where the the input term is flexible but the user also gave an explicit second term, the behavior was OK. Imagine calling `copy (A x) x`, I'd like the rule for variables ("documentation" of `uvar`) of `copy` to apply (and fail), not this one. `copy X X` would work, set `A = y\y` and succeed, while I did not want this behavior (after all the first argument is an input, I should not touch it). Non linear heads, and input mode, is not exactly what one thinks.

About the last `!` I don't think it is really needed now that `=` is a builtin (hence the user cannot add clauses for `=`). But in the past `=` was, by chance/mistake/lazyness, a regular predicate and the user was able to write more rules for it (I'm afraid not intentionally).

Well, that was a bit of a mouthful ;-)

Thanks for the typo.

Last updated: Feb 04 2023 at 02:03 UTC