Does Coq do alpha conversion on it's own?

Using Coq
1

I recently discovered the Eval cbv in term strategy for reduction but I noticed that my terms were already printed with unique names (alpha-conversion). Does Coq already do alpha-conversion on it’s own?

e.g.

  Definition l := forall x y : nat, x = y \/ forall x:nat, x < y.

  Print l.

displays:

l = forall x y : nat, x = y \/ (forall x0 : nat, x0 < y)
     : Prop
2

Coq performs a form of α-conversion to avoid confusion between identifiers. Here for instance x is already bound when it is encountered again in the second forall, and so it is renamed. But maybe what you had in mind was

Definition l := (forall x y ; nat, x = y) \/ (forall x : nat, x < y).

? In that case, Coq would be perfectly happy keeping x twice, as there is no risk of confusion.

1 Like
3

To be precise, internal representation of coq terms use DeBuijn Indices for bound variables so alpha conversion is not even necessary there. Names are only there for the user and on-the-fly renaming is performed at printing for readiness.

3 Likes