Choosing the appropriate level of implicitness/explicitness

Stream: new members

[Isak Colboubrani]

Based on my observations, the following four styles are equivalent (with the last one being a slight exception).

If you were teaching Lean, which style would you choose to teach?

More generally, is there an idiomatic rule of thumb for selecting between styles 1, 2, 3, and 4?

import Mathlib

-- Style 1.
set_option autoImplicit true
example (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (h₁ : P → Q) (h₂ : Q → P) : [P, Q].TFAE := by tfae_finish

-- Style 2.
set_option autoImplicit false
example (α) (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (P Q) (h₁ : P → Q) (h₂ : Q → P) : [P, Q].TFAE := by tfae_finish

-- Style 3.
example (α : Type) (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (P Q : Prop) (h₁ : P → Q) (h₂ : Q → P) : [P, Q].TFAE := by tfae_finish

-- Style 4.
universe u
example (α : Type u) (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (P Q : Prop) (h₁ : P → Q) (h₂ : Q → P) : [P, Q].TFAE := by tfae_finish

[Edward van de Meent]

The idiomatic rule would be to use variable for these kinds of assumptions, since you're likely to use these multiple times in the same section/file

[Edward van de Meent]

Also, note that a second difference is if the Type and Prop arguments are implicit as arguments. They are in (2,3,4), which tends to be nicer for lemmas

[Daniel Weber]

Just a note that in Mathlib you should usually not use style 3 or 4, and instead use Type* to be universe general

[Isak Colboubrani]

Great points! I've also added Type* as a fifth option. While there are solid arguments for avoiding styles 1, 3, and 4 in certain contexts, are there also good reasons to avoid styles 2 and 5 in some cases?

The five styles:

import Mathlib

-- Style 1.
set_option autoImplicit true
example (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (h₁ : P → Q) (h₂ : Q → P) : [P, Q].TFAE := by tfae_finish

-- Style 2.
set_option autoImplicit false
example (α) (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (P Q) (h₁ : P → Q) (h₂ : Q → P) : [P, Q].TFAE := by tfae_finish

-- Style 3.
example (α : Type) (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (P Q : Prop) (h₁ : P → Q) (h₂ : Q → P) : [P, Q].TFAE := by tfae_finish

-- Style 4.
universe u
example (α : Type u) (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (P Q : Prop) (h₁ : P → Q) (h₂ : Q → P) : [P, Q].TFAE := by tfae_finish

-- Style 5.
example (α : Type*) (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (P Q : Prop) (h₁ : P → Q) (h₂ : Q → P) : [P, Q].TFAE := by tfae_finish

[Daniel Weber]

The main reason I can see to avoid 5 is that the definitions become long and cluttered

[Daniel Weber]

One problem in style 2 is probably a problem you have when using Type _ instead of Type*, where it can sometimes unexpectedly unify to a specific value

[Isak Colboubrani]

Then it seems that style 5 might be the best choice—at least in the context of Mathlib.

Also, in an example where the choice between (…) and {…} doesn't affect functionality, which is considered more idiomatic: style 5a or 5b?

import Mathlib

-- Style 5a.
example (α : Type*) (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (P Q : Prop) (h₁ : P → Q) (h₂ : Q → P) : [P, Q].TFAE := by tfae_finish

-- Style 5b.
example {α : Type*} {xs ys : List α} : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example {P Q : Prop} {h₁ : P → Q} {h₂ : Q → P} : [P, Q].TFAE := by tfae_finish

[Edward van de Meent]

if the purpose is to educate people unfamiliar with lean, 5a, since then you don't introduce unnecessary complexity. if the purpose is to educate people familiar with lean, 5b, to give an idea as to what the lemma would look like

[Edward van de Meent]

(also, i think i'd have h1 and h2 explicit in 5b, although i haven't worked with TFAE statements)

[Isak Colboubrani]

Like this?

import Mathlib

-- Style 5a.
example (α : Type*) (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (P Q : Prop) (h₁ : P → Q) (h₂ : Q → P) : [P, Q].TFAE := by tfae_finish

-- Style 5b.
example {α : Type*} {xs ys : List α} : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example {P Q : Prop} (h₁ : P → Q) (h₂ : Q → P) : [P, Q].TFAE := by tfae_finish

[Kevin Buzzard]

FWIW I go with Style 3 when teaching maths undergraduates because most of them have no reason to know about universes, so I just tell them that Type is the universe of all sets.