Section 4 : functions

Note to future Kevin: this needs to be moved to section 3; it’s easier than groups. We want functions section 3, sets section 4, groups section 5.

This short section is an introduction to “abstract” functions in Lean. We’ve seen functions from the naturals to the reals, but here we’ll be talking about functions between types X and Y.

Lean is a functional programming language, and functional programmers realised a long time ago that brackets which mathematicians put into their work are often not necessary. If f : X  → Y and x : X then we can write f x in Lean instead of f(x) and it works just as well. Brackets can be used – they are just optional.

Be warned though – functions in Lean are greedy: they will eat the next thing they see. For example f n + 1 means (f n) + 1 and not f (n + 1). If you want f(n+1) then you need to use the brackets. Similarly, composite of functions f : X  → Y and g : Y  → Z evaluated at x : X needs to be written g (f x) otherwise g would eat f and then choke because f doesn’t have the right type.

The problem sheets

For the first sheet you should be able to get away with what you already know. For the second one I introduce a method for making finite types and explain how to define functions from these finite types to other types. This is needed because in the first sheet we are proving theorems, but in the second sheet we are expected to give counterexamples.