About alpha conversion in Lean 4

Stream: lean4

[Junseong O]

I am trying to understand Lean 4 as a formal system while reading The Type Theory of Lean by Mario Carneiro.
While reading the text, I came across a question.
In Lean 4, the statement fun x => x + 3 = fun y => y + 3 is provable by rfl.
As far as I know, this means that the Lean 4 kernel considers the two terms to be definitionally equal.
However, I cannot find any inference rule in the text that seems to account for this.
After searching, I learned that this kind of equality is called alpha conversion in lambda calculus.
Why can’t I find a rule corresponding to alpha conversion?

[Markus Himmel]

Lean represents bound variables using de Bruijn indices. See for example Wikipedia for an explanation.

[Junseong O]

I understand. Thank you!!

[Robin Arnez]

You can also use the inference rules from #leantt:

1. Γ, x : Nat ⊢ x + 3 : Nat -- easy enough
2. Γ ⊢ (fun x : Nat => x + 3) : ∀ x : Nat, Nat -- lambda typing with 1.
3. Γ ⊢ (fun y : Nat => (fun x : Nat => x + 3) y) ≡ fun x : Nat => x + 3 -- eta with 2.
4. Γ ⊢ (fun x : Nat => x + 3) ≡ fun y : Nat => (fun x : Nat => x + 3) y -- symmetry with 3.
5. Γ ⊢ Nat : Sort 1 -- definition of Nat
6. Γ, y : Nat ⊢ y : Nat -- variable typing with 5.
7. Γ, y : Nat ⊢ (fun x : Nat => x + 3) y ≡ y + 3 -- beta reduction with 1. and 6.
8. Γ ⊢ Nat ≡ Nat -- reflexivity with 5.
9. Γ ⊢ (fun y : Nat => (fun x : Nat => x + 3) y) ≡ fun y : Nat => y + 3 -- lambda congruence with 8. and 7.
10. Γ ⊢ (fun x : Nat => x + 3) ≡ fun y : Nat => y + 3 -- transitivity with 4. and 9.

[Robin Arnez]

I guess the text still assumes that you use a representation where names are irrelevant because I don't think you can do the same for ∀

[Kenny Lau]

@leannoob I would consider this part of the text to be the answer:
image.png

[Arthur Adjedj]

That isthe congruence rule of definitional equality for Pi types, this has little to do with alpha-conversion.

[Kenny Lau]

oh, my mistake

[Mario Carneiro]

Yes, the text assumes that the terms are written as de Bruijn and therefore alpha conversion is not necessary. I should have been more explicit about this (and variable conventions in general) in the paper.