在精益定理证明器中定义`curry`

Question

我正在阅读精益 3 的官方教程。我陷入了第 2 章中的第二个练习：

完成以下定义，其中“curry”和“uncurry”是一个函数。

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

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

我目前的尝试是

def curry (α β γ : Type*) (f : α × β → γ) (x : α) (y : β) : γ := f (x, y)

这并不令人满意，因为我修改了练习中的类型，而不是仅仅用一些代码替换“抱歉”。在保持类型相同的情况下采取什么更好的方法？我希望得到一些提示，为我指明正确的方向，而不是完整的解决方案。

Answer 1

我想我会为遇到这个问题的人分享一个完整且可读的答案，以及精益 3 和精益 4 中柯里化的示例。所有功劳都归功于@jmc 以及他们对原始正确答案的评论。

-- Lean 3

def curry {α β γ : Type*} (f: α × β -> γ) : α -> β -> γ :=
λ x y, f (x, y) 

def add (ns : ℕ × ℕ) : ℕ := ns.1 + ns.2

#check add            -- ℕ × ℕ -> ℕ
#check curry add      -- ℕ -> ℕ -> ℕ

#eval add (2, 2)      -- 4
#eval (curry add) 2 2 -- 4 

在lean3 Web编辑器上实时运行它

-- Lean 4

def curry (f: α × β -> γ) : α -> β -> γ :=
λ x y => f (x, y) 

def add (ns : Nat × Nat) : Nat := ns.1 + ns.2

#check add            -- Nat × Nat -> Nat
#check curry add      -- Nat -> Nat -> Nat

#eval add (2, 2)      -- 4
#eval (curry add) 2 2 -- 4