28
$\begingroup$

In Lean, explicit function arguments are enclosed in round brackets and implicit ones in curly brackets, as in this example:

lemma surjective.comp {g : β → φ} {f : α → β} (hg : surjective g) (hf : surjective f) :
  surjective (g ∘ f) := ...

However, occasionally we see some strange double curly brackets like this:

def injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂

I'm sure I once read an explanation of this, but my attempts to search for it now have failed. What do the double curly brackets mean?

$\endgroup$
1
  • $\begingroup$ Implicit parameters I guess $\endgroup$
    – ice1000
    Feb 8 at 20:30

1 Answer 1

30
$\begingroup$

Single braces{⋯} indicate a maximally inserted implicit argument and {{⋯}} a weakly inserted implicit argument, as explained in the manual.

Consider the definition of the identity map in which the first argument is implicit:

def id {α : Type u} (x : α) : α := x

In an expression such as id 3 Lean will figure out the implicit argument α to be . But what will it do when faced just with id, not applied to anything? There are two options:

  1. It could create a new meta-variable ?M (also known as an existential variable) and convert the lone id to id ?M. The value of ?M will be determined later as more information becomes available. This is known as a maximally inserted implicit argument, because it is inserted whenever possible. The above definition does so.

  2. Indicate that the argument should not be maximally inserted by using {{⋯}} instead:

    def id {{α : Type u}} (x : α) : α := x
    

    Now, when faced with id, Lean will read it precisely as id without inserting anything. This strategy is known as weakly inserted implicit arguments.

Let's try it out:

universe u

def id₁ {α : Type u} (x : α) : α := x

#check id₁
-- output: id₁ : ?M_1 → ?M_1

def id₂ {{α : Type u}} (x : α) : α := x

#check id₂
-- output: id₂ : Π ⦃α : Type u_1⦄, α → α

In most cases the difference between the maximally and weakly inserted arguments does not matter. But when it does matter it becomes very annoying if only the wrong one is available. For example, the OP shows the definition of injective map using {{⋯}}. They are there, because with {⋯} the expression injective f would mean injective f ?a₁ ?a₂ which reads “for some fixed but yet to be determined a₁ and a₂, if f a₁ = f a₂ then a₁ = a₂". That's not what “f is injective“ means.

$\endgroup$
2
  • 1
    $\begingroup$ I find the explanation in Theorem Proving In Lean to also be quite helpful; it gives an explicit example related to equivalence relations that this can solve. $\endgroup$ Feb 8 at 22:27
  • $\begingroup$ Minor amendment: injective f would not be interpreted as injective f ?a₁ ?a₂ (which is not type correct), but rather if you have hf : injective f then it would be interpreted as hf ?a₁ ?a₂ when referenced (which could be annoying if you are trying to pass hf to another lemma expecting something of type injective f). It is also useful to know that if for whatever reason you can't change the type of hf and it uses {} brackets, you can cancel this behavior at the use site by writing @hf instead. $\endgroup$ Feb 18 at 6:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.