Curry/Uncurry

Stream: new members

[me myself and I]

Hello.
I am working through "Theorem Proving in Lean" with only minimal background knowledge, so I am having trouble figuring out how to define curry and uncurry functions from the text:

def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := sorry

def uncurry (α β γ : Type) (f : α → β → γ) : α × β → γ := sorry

The core of my confusion is that I do not understand how the return types α → β → γ and α × β → γ can be expressed.
Am I supposed to def a new function inside the given function definition? Trying that gives an error.

If I start with lambda x y z g (for types alpha, beta, gamma, and function f), I get x : alpha, y : beta, z : ?m_1, and f : ?m_1.

Would you please instruct me how to define these functions?

Thank you.

[Edward Ayers]

Hi! The answer is def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := λ a b, f (a,b). In a def block, anything before the : is already in scope (so you don't need to lambda theα,β,γ or f ). If you replace sorry with an underscore _ and look at the lean output it will give you some hints about what is in scope and what the underscore needs to be replaced with.

[Edward Ayers]

So eg

def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := _

Gives:

α β γ : Type,
f : α × β → γ
⊢ α → β → γ

[Edward Ayers]

So it's telling you that you need to provide a function that takes a α and β and returns a γ.

[me myself and I]

OK; I understand now.
lambda x y, f(x,y) is actually returning a function with the required signature, yes?
Thank you for your wise and timely assistance!

[Edward Ayers]

yep

[Edward Ayers]

np