theorem foo (t : T) vs. theorem foo {t : T}

Stream: new members

[Isak Colboubrani]

When are the following two theorems not equivalent?

theorem foo₁ (a b c : G) (h : a * b = a * c) : b = c := by sorry
theorem foo₂ {a b c : G} (h : a * b = a * c) : b = c := by sorry

Of the theorems in Mathlib it seems like roughly 57 % are on the form theorem … (… : T) … and 43 % are on the form theorem … {… : T} ….

[Kevin Buzzard]

They're equivalent in the sense that they have the same mathematical content. They're not equivalent in the sense that foo1 is more irritating to use because h is an input and once Lean sees h it can figure out a, b, c, but foo1 wastes the user's time asking for them anyway.

[Damiano Testa]

And you can also verify what Kevin said about the lemmas being equivalent:

variable {G} [Mul G]
theorem foo₁ (a b c : G) (h : a * b = a * c) : b = c := sorry
theorem foo₂ {a b c : G} (h : a * b = a * c) : b = c := sorry

example : @foo₁ = @foo₂ := rfl

[Isak Colboubrani]

Thanks! I think I follow.

I'm trying to formulate a rule on when to use one over the other.

In the input case (h above): then it sounds like foo₂ {a b c : G} is always preferable over foo₁ (a b c : G)?

In the non-input case such as …

theorem bar₁ (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by sorry
theorem bar₂ {a b : G} : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by sorry

… then there is no ergonomic difference between the two?

The reason I'm asking is that I saw the different forms being mixed in files such as https://github.com/leanprover-community/lftcm2020/blob/master/src/exercises_sources/wednesday/algebraic_hierarchy.lean where we have:

lemma mul_left_cancel (a b c : G) (Habac : a * b = a * c) : b = c := …
lemma mul_eq_of_eq_inv_mul {a x y : G} (h : x = a⁻¹ * y) : a * x = y := …
theorem mul_one (a : G) : a * 1 = a := …

[Damiano Testa]

My point of view is that your initial examples foo_i had two "defensible" choices: either all of a b c should be implicit, or a should be explicit and b c implicit. The reason for possibly wanting a to be explicit is that, if you do not have h in context, by passing foo_i a Lean will produce the correct side-goal.

This is a subtlety, though, and it is not clear that the annoyance of using foo_i _ beats the few cases where having the explicit argument is useful.

[Kyle Miller]

You can write foo₂ (a := val) if you want to set a, though this isn't that great since the name a isn't necessarily intended to be part of the interface.