定理中命题的大括号和圆括号之间的区别

Question

我对定理中用大括号表示命题感到非常困惑。请参阅以下四个代码段：

theorem contrapositive_1 : ∀ (P Q : Prop),
(P -> Q) -> (¬ Q -> ¬ P) := sorry
theorem contrapositive_2 (P Q : Prop) : 
(P -> Q) -> (¬ Q -> ¬ P) := sorry
theorem contrapositive_3 : ∀ {P Q : Prop},
(P -> Q) -> (¬ Q -> ¬ P) := sorry
theorem contrapositive_4 {P Q : Prop} : 
(P -> Q) -> (¬ Q -> ¬ P) := sorry

我想，它们都是一样的，但显然它们不是，因为当我想在另一个定理的证明中使用contraprositive_1和contraprositive_2时，lean显示了类型不匹配的错误：

术语 h1 具有类型 P → Q ： 道具，但预期具有类型 道具 ： 类型

另一方面，contraprositive_3和contraprositive_4工作正常。

大括号和圆括号有什么区别？

Answer 1

区别在于参数是显式的()还是隐式{}。通常，您希望参数是明确的，除非可以从后面的参数中找出它们。例如

lemma foobar {X : Type} (x : X) : x = x := sorry

在这种情况下，X是隐式的，因为一旦你告诉 Lean 关于x，它就可以弄清楚X本身(它是x的类型)。换句话说，如果你想将引理应用于y : Y你可以写foobar y。 相反，如果你会做

lemma quux (X : Type) (x : X) : x = x := sorry

您必须将其称为quux Y y.

如果在名称之前放置一个@，则会将所有隐式参数转换为显式参数。所以你可以打电话给@foobar Y y."相反"如果你想让精益自己弄清楚Y你可以写一个下划线：quux _ y。

TPIL中的相关部分：https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#implicit-arguments

Answer 2

• ()括号中的参数是您需要自己传递给函数的内容。

  这些就是所谓的显式参数。

• {}和⦃⦄括号中的参数由 Lean's 计算统一系统。

  当 Lean 可以推导出 { 参数 } 到函数时，我们使用{}基于(我们提供的另一个参数)。{}和⦃⦄在统一程序的时间上有所不同。

• []括号中的参数由 Lean 的类型类推理系统计算出来。

  当精益可以根据 mathlib 的事实推导出 [ 参数] 时，我们使用[]。

---

凯文·巴扎德(Kevin Buzzard)关于精益括号的好文章：https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2022/Part_B/brackets.html。