Equality of two functions

Question

I am wondering about definition of functions in Lean and proving equality (in some sense to be defined) of two functions.

Note: I have consulted the answer to the following related question but it does not answer my doubts: Definitional vs propositional equality.

Concretely, I am considering the following:

variables {X : Type}

def id1 (x : X) : X :=
x

def id2 : X → X := 
λ x, x

The commands print id1 and print id2 then return

def id1 : Π {X : Type}, X → X :=
λ {X : Type} (x : X), x

and

def id2 : Π {X : Type}, X → X :=
λ {X : Type} (x : X), x

My first question then is:

Does this mean that id1 and id2 are definitionally equal?

What I can do is prove

example : ∀ x : X, id1 x = id2 x := by {intro x, refl}

which suggests that id1 and id2 are indeed definitionally equal (because, as I understand, refl will only work on definitionally equal terms).

However, even if the above is correct, I am puzzled by the following: the command #check id1 = id2returns id1 = id2 : Prop but if I try

example : id1 = id2 := by {sorry}

I get a

don't know how to synthetize placeholder
context:
⊢ Type

and a

tactic failed, result contains meta-variables

so I guess that the statement id1 = id2 does not quite make sense. Hence my second question:

Is it possible to give meaning to the statement id1 = id2 and prove it?

Note: I believe this could be related to $\eta$-equivalence of terms, but I do really understand what this means.

Answer 1

This is because, since you have implicit arguments in your functions, Lean thinks you have left out the argument (that's what implicit means!), so it interprets your statement as

id1 {X = ??} = id2 {X = ??}

(This is not Lean syntax, it is just to demonstrate the problem.) And Lean then starts to figure out what the question marks should be. But of course it would fail, because there is absolutely no information that tells Lean what those are.

---

The above is likely not your real question, so what if we give the type X for Lean? We can do this by using @id1 X. The @ tells Lean to make all arguments explicit so you can provide them one by one. Let's check:

example : @id1 X = @id2 X := by refl

It passes! So id1 and id2 are indeed definitionally equal. Note that this is not what we conventionally call "function extensionality". This is called $\eta$-equality, it states that

If the body of two functions are definitionally equal, then they are definitionally equal.

What the Lean community calls "functional extensionality" states that

If for every $x$, $f(x)$ and $g(x)$ are propositionally equal, then $f$ and $g$ are propositionally equal.