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

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显示类型不匹配错误：

term h1 has type P → Q : Prop but is expected to have type Prop : Type

另一方面，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

()括号中的参数是你需要自己传递给函数的。

These are so called explicit arguments.
{} 和 ⦃⦄ 括号中的参数由 Lean 计算得出 统一系统.

We use {} when Lean can deduce { argument } to the function based on ( another argument we provided ). {} and ⦃⦄ differ in timing of the unifier.
[] 括号中的参数由 Lean 的 type class 推理系统计算得出 .

We use [] when Lean can deduce [ argument ] based on facts from mathlib.

Kevin Buzzard 撰写的一篇关于精益中括号的好文章：https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2022/Part_B/brackets.html。

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

Difference between the curly and round brackets for propositions in a theorem

lean