Does Coq do alpha conversion on it's own?

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?


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

  Print l.


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

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

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.