Proving two functions are equivalent

Stream: new members

[Fingy Soupy]

Hello, I'm wondering how to prove the following:

inductive foo
| A
| B
def I := nat -> foo
def I_eq (a b : I) (p : ∀ x : nat, (a x) = (b x)) : a = b := sorry

I'm not really sure how to prove = without using rw and I don't see how rw could be applied here

[Notification Bot]

This topic was moved here from #general > Proving two functions are equivalent by Kyle Miller.

[Kyle Miller]

@Fingy Soupy You need to use function extensionality in some way to prove a = b from equality on values.

Here's one way using tactics:

def I_eq (a b : I) (p : ∀ x : nat, (a x) = (b x)) : a = b :=
begin
  ext,
  apply p,
end

[Kyle Miller]

You can also do this using a term proof:

def I_eq (a b : I) (p : ∀ x : nat, (a x) = (b x)) : a = b := funext p

[Kyle Miller]

(I hope you don't mind I moved your question to "new members".)

[Fingy Soupy]

Awesome, thanks :) I have not heard of 'function extensionality' before. I'll do some reading into it. I don't mind, I didn't see that was a stream, sorry.

[Eric Wieser]

by library_search should have been able to answer this question for you :)

[Kyle Miller]

In general, "extensionality" refers to an idea where things are considered to be equal if they're externally indistinguishable. The only thing you can do with a function is evaluate it, and in Lean we (more-or-less) define function equality by extensionality. (The hedge there is just because function extensionality is actually a consequence of some other axioms.)

Similarly, the extensionality property for sets is that they're equal if they have the same elements. In ZFC, that's taken as an axiom. In Lean, that's actually funext but with special notation for sets.

tactic#ext looks in a database of extensionality lemmas to retrieve one that applies to the given situation. Lemmas are added to this database by giving them the ext attribute.

[Fingy Soupy]

Oh wow, I wasn't aware of library_search. This is great, thank you! :)
This is very informative thanks :)