Brackets in function inputs =========================== This is about the different types of brackets which we see in Lean's functions. If we type ``#check @mul_assoc`` into Lean (assuming we've done ``import tactic`` or some other import which imports group theory) then we get the following output: .. code-block:: mul_assoc : ∀ {G : Type u_1} [_inst_1 : semigroup G] (a b c : G), a * b * c = a * (b * c) At first glance, this makes some kind of sense: ``a * b * c`` means by definition ``(a * b) * c`` so we can see that this is some sort of claim that multiplication is associative. Looking more carefully, what is going on is that ``mul_assoc`` is a function, which takes as input a type ``G``, a semigroup structure ``_inst_1`` on ``G`` and three terms ``a``, ``b`` and ``c`` of ``G``, and returns a proof that ``(a * b) * c = a * (b * c)``. But what's with all the different kinds of brackets? We can see `{}`, `[]` and `()`. There's even a fourth kind, although it's rarer: try ``#check @mul_one_class.ext`` to even see some ``⦃⦄`` brackets. These are the four kinds of brackets which you can use for function input variables. Here's a simple explanation of what they all mean. ``()`` brackets --------------- These brackets are the easiest to explain. An input to a function in ``()`` brackets is an input which the user is expected to apply. For example, if we have a theorem ``double (x : ℕ) : 2 * x = x + x`` then ``double 37`` is the theorem that ``2 * 37 = 37 + 37``. ``{}`` and ``⦃⦄`` brackets -------------------------- These brackets exist because Lean's type theory is dependent type theory, meaning that some inputs to functions can be completely determined by other inputs. For example, the term ``subgroup.mul_mem`` is a proof of the theorem stating that if two elements of a group are in a given subgroup, then their product is also in this subgroup. The type of this term is the following: .. code-block:: ∀ {G : Type} [_inst_1 : group G] (H : subgroup G) {x y : G} (hx : x ∈ H) (hy : y ∈ H) : x * y ∈ H So ``subgroup.mul_mem`` takes as input the following rather long list of things. First it wants a type ``G``. Then it wants a group structure on ``G``. Next it wants a subgroup ``H`` of ``G``, then two elements ``x`` and ``y`` of ``G``, and finally two proofs; first a proof that ``x ∈ H`` and second a proof that ``y ∈ H``. Given all of these inputs, it then outputs a proof that ``x * y ∈ H``. Now let's imagine we're actually going to use this proof-emitting function to prove some explicit statement. We have some explicit group, for example the symmetric group :math:`S_5`, and some explicit subgroup `H` and some explicit permutations ``x`` and ``y`` in :math:`S_5`, and proofs ``hx`` and ``hy`` that ``x ∈ H`` and ``y ∈ H``. At the point where we feed in the input ``hx`` into ``subgroup.mul_mem``, Lean can look at ``hx`` and see immediately what ``x`` is (by looking at the type of ``hx``) and what ``G` is (by looking at the type of ``x``). So, when you think about it, it's a bit pointless asking the user to explicitly supply those inputs, because actually the type of the input ``hx`` (namely ``x ∈ H``) contains enough information to uniquely determine them. Calculations like are what Lean's *unifier* does, and the ``{}`` and ``⦃⦄`` brackets are for this purpose; they mean that they are inputs to the function which the user need not actually supply at all; Lean will figure them out. Technical note: The difference between ``{}`` and ``⦃⦄`` is that one is more *eager* than the other; this is all about the exact timing of the unifier. Basically if you have ``f (a : X) {b : Y} (c : Z)`` and ``g (a : X) ⦃b : Y⦄ (c : Z)`` then the unifier will attempt to figure out ``b`` in ``f`` the moment you have given it ``f a``, but it will only start worrying about ``b`` in ``g`` when you have given it ``g a c``. For an example where this matters, see `section 6.5 of Theorem Proving In Lean `_ . If you want a rule of thumb: use ``{}``. ``[]`` brackets --------------- Like ``{}`` brackets, these square brackets are inputs which the user does not supply, but which the system is going to figure out by itself. The ``{}`` brackets above were figured out by Lean's unification system. The ``[]`` brackets in this section are figured out by Lean's type class inference system. Lean's type class inference system is a big list of facts. For example Lean knows that the reals are a field, that the natural numbers are an additive monoid, that the rationals have a 0 and a 1, etc etc. Which facts does this system know? The facts it knows are "instances of classes", or "instances of typeclasses" to give them their full name. Let's take a look at ``add_comm``. You can see its type with ``#check @add_comm``. Its type is this: .. code-block:: add_comm : ∀ {G : Type} [_inst_1 : add_comm_semigroup G] (a b : G), a + b = b + a An ``add_comm_semigroup`` is something a bit weaker than an additive commutative group; any abelian group with group law ``+`` is an ``add_comm_semigroup``. The only inputs in round brackets to this proof are ``a`` and ``b``. Here's a short script which gives ``add_comm`` all the inputs it needs. .. code-block:: import data.real.basic def a : ℝ := 37 def b : ℝ := 42 #check add_comm a b -- add_comm a b : a + b = b + a The ``add_comm`` function was given ``a``, and Lean knows that ``a`` has type ``ℝ`` because that's part of the definition of ``a``. So the unifier figures out that ``G`` must be ``ℝ``. The one remaining input to the function is a variable with the weird name of ``_inst_1``, whose type is ``add_comm_semigroup ℝ``; you can think of it as "a proof that the reals are an additive commutative semigroup" but it's actually more than just a proof -- it's all the data of the addition and identity element as well; the functions and constants as well as the proofs. Where does Lean get this variable ``_inst_1`` from? The answer is that in ``mathlib`` somewhere, someone proved that the real numbers were a field, and they tagged that result with the ``@[instance]`` attribute, meaning that the typeclass inference system now knows about it. The typeclass inference system knows that every field is an additive commutative group, and that every additive commutative group is an additive commutative semigroup. So the system throws this package together and fills in the ``_inst_1`` input automatically for you. Basically this system is in charge of keeping all the group and ring proofs which we don't want to bother about ourselves. You can add new facts into the typeclass system. Here's a way of telling Lean that you want to work with an abstract additive commutative group ``G``. .. code-block:: import tactic variables (G : Type) [add_comm_group G] (x y : G) #check add_comm x y -- add_comm x y : x + y = y + x Instead of using concrete types like the reals, we make a new abstract type ``G``, give it the structure of an additive commutative group, and let ``x`` and ``y`` be abstract elements of ``G`` (or more precisely terms of type ``G``). The ``variables`` line has square brackets in too -- this means "add the fact that ``G`` is an additive commutative group to the typeclass system". Then when ``add_comm`` runs, the system will supply the proof that ``G`` is an additive commutative semigroup, so the function ``add_comm x y`` runs successfully and outputs a proof that ``x + y = y + x``. Overriding brackets ------------------- You may well never need to do this in this course, but I put it here for completeness. Sometimes the system goes wrong, and Lean cannot figure out the inputs it was supposed to figure out by itself. If this happens, you can override all the systems by using the ``@`` symbol in front of the function. In Lean 3 it's all or nothing -- either the system is left alone, or the user supplies every single input (including the ones which the system could have done itself). Here are some examples. Note that `_` means "get the system to do it anyway". .. code-block:: import tactic variables (G : Type) [add_comm_group G] (x y : G) /- add_comm : ∀ {G : Type} [_inst_1 : add_comm_semigroup G] (a b : G), a + b = b + a -/ -- override `{}` and `[]` inputs with `@` #check @add_comm _ _ x y -- get the system to work out `G` and the group structure #check @add_comm G _ x y -- user supplies `G`, Lean figures out group structure #check @add_comm _ (by apply_instance) x y -- Lean figures out `G`, user supplies group structure I say "the user supplies the group structure", on the last line, but I do it by just running the ``apply_instance`` tactic, which tells the typeclass inference system to do it anyway. For fun examples of the system failing, search for things like `_ _ _ _ _` in mathlib. In Lean 4 there will be a way of supplying only those inputs which Lean was having problems with. However when the system is failing, it can sometimes be an indication that the user's definitions are not optimal.