Section 3 : functions

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 write f x in Lean instead of f(x) (which doesn’t actually work in Lean at all). Brackets can be used – but you have to leave a space (so f (x)) and they are optional anyway.

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. In the second one I explain how to make types with finitely many terms, and how to make functions from these types. In the last sheet I show how to use these to make counterexamples to various assertions about injective and surjective functions.