2
$\begingroup$

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.

$\endgroup$

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
5
  • 2
    $\begingroup$ I'm nitpicking, but technically @id1 X = @id2 X := by refl only checks that once applied at a given type X, id1 and id2 are equal. But I guess that also @id1 = @id2 := by refl type-checks, which is really meaning that without giving them any further arguments, the two functions are (definitionally) equal. Although, because Lean's definitional equality contains η-equality, these two statement are equivalent (but this is a feature!). $\endgroup$ Commented Apr 3, 2023 at 8:27
  • $\begingroup$ Thanks also for the clarification about functional extensionality, I have removed the tag. $\endgroup$ Commented Apr 3, 2023 at 8:29
  • $\begingroup$ @MevenLennon-Bertrand You're right, I figured that the OP is asking about the case with X a fixed constant throughout the question. But that's a good addition. $\endgroup$
    – Trebor
    Commented Apr 3, 2023 at 9:31
  • $\begingroup$ Another nitpick, but η-equality is more commonly understood as the rule $t \equiv (\lambda x.\, t\ x)$. The rule you refer to is traditionally called the ξ-rule, or just congruence for abstraction. You can have a system with ξ but without η, that was e.g. the case in the old versions of Coq. $\endgroup$ Commented Apr 3, 2023 at 12:01
  • $\begingroup$ I'm sorry, I'm not familiar with the $\xi$-rule: does it mean that f = g implies that ∀ x, f x = g x? That's what I inferred from this answer, but I'm not sure I'm getting this right. $\endgroup$ Commented Apr 3, 2023 at 12:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.