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

Question

I'm very confused by the use of braces for propositions in a theorem. See the following four snippets:

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

I thought, they were all the same, but clearly they are not, because when I want to use contraprositive_1 and contraprositive_2 in the proof of another theorem, lean shows an error for type mismatch:

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

On the other hand, contraprositive_3 and contraprositive_4 work fine.

What is the difference between the curly and round brackets?

Answer 1

The difference is whether the argument is explicit () or implicit {}. In general, you want arguments to be explicit, unless they can be figured out from arguments that come later. For example

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

In this case X is implicit, because once you tell Lean about x, it can figure out X itself (it is the type of x). In other words, if you want to apply the lemma to y : Y you can just write foobar y. If instead you would make

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

you would have to call it as quux Y y.

If you place an @ before a name you turn all the implicit arguments into explicit arguments. So you can call @foobar Y y. “Conversely” if you want Lean to figure out Y by itself you can write an underscore: quux _ y.

The relevant section in TPIL: https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#implicit-arguments