0

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

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 : Prop 但预计具有类型 Prop : Type

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

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

4

1 回答 1

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。“相反”，如果你想让 Lean 自己弄清楚，Y你可以写一个下划线：quux _ y.

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

于 2019-04-23T09:39:46.737 回答