Zulip Chat Archive
Stream: maths
Topic: Teaching functions
Gihan Marasingha (Oct 17 2020 at 16:45):
For those using Lean for teaching mathematics, how do you treat the notion of function?
Until this year, I've taught my beginning undergraduates that a function is a triple $(A, B, C)$ of sets where $C \subseteq A \times B$ with the properties:

$\forall a \in A, \exists b \in B, (a,b) \in C$ and

$\forall a \in A, \forall b_1 b_2 \in B, (a,b_1) \in C \land (a,b_2) \in C \to b_1 = b_2$.
The typetheoretic notion of a function as a named lambda abstraction does away with the distinction between functions that have the same 'map' but different domains or codomains. I see that data.set.function
provides, for example, inj_on
to define what it means for a (typetheoretic) function to be injective on a set. But this moves the notion of domain of a function to the definition of injectivity, rather than treating it as part of the definition of the function. That's fine, but it isn't the same notion of function as that given above.
My question to those teaching undergraduate maths with Lean is: do you just work with the typetheoretic definition? If not, do you use inj_on
to define injectivity, or do you do something else entirely?
Yury G. Kudryashov (Oct 17 2020 at 16:47):
In Lean each function knows its domain: f : α → β
has domain α
.
Yury G. Kudryashov (Oct 17 2020 at 16:47):
If we want to study this function on a subset of its domain, then we introduce an auxiliary s : set α
and define docs#set.inj_on etc
Yury G. Kudryashov (Oct 17 2020 at 16:48):
docs#function.injective does not use any set
s
Gihan Marasingha (Oct 17 2020 at 17:11):
OK, so is the best solution not to worry about the distinction between sets and types?
When we use inj_on
to look at a function on a subset of its domain, then the new domain is not part of the function, but has been moved into the position of being an argument of inj_on
. To me, this is a different definition of function than that which I'm used to, but I accept that it's the most natural definition as far as Lean is concerned.
My view would be that α
and β
aren't domains and codomains in the traditional sense, as they aren't sets. Rather, to reconcile with the settheoretic notion of function, a function would consist of a triple A : set α
, B : set β
, C : set α × β
with the above properties, but this seems overly complicated and hard to work with in Lean.
Reid Barton (Oct 17 2020 at 17:12):
For most (math) purposes the correct mapping is "set" = Type
, "subset" = set
Floris van Doorn (Oct 17 2020 at 17:12):
When I explain functions, I like to explain that a function is a mathematical procedure that takes a certain class of inputs to an output. A function "knows" what its inputs can be (its domain), and what its potential outputs can be (its codomain).
The definition you gave is an encoding of that idea in set theory. I don't think what you wrote has to be the definition, it just the most convenient encoding of the mathematical idea of a function in set theory. In type theory there is a different encoding (which is hardly an encoding, since functions are a primitive notion in type theory).
The idea that functions have the same 'map' but different domains and codomains looks a little different in type theory than in set theory, but you can find analogues of everything in one theory in the other theory. In type theory, two maps cannot be "the same" without having the same domain and codomain, but I don't think that is an essential feature of function.
If you have A → B
and C ⊆ A
you can still restrict your function to C
in both set theory and type theory. In set theory, the "map" of your new function will be a subset, in type theory it will use subtype.rec
, if we encode C
as a subtype of A
.
Reid Barton (Oct 17 2020 at 17:13):
e.g. "A group is a set $G$ equipped with a binary operation $m : G \times G \to G$ and ..." > (G : Type) (m : G > G > G)
"A subgroup $H$ of a group $G$ is a subset $H \subset G$ such that ..." > (H : set G) ...
Reid Barton (Oct 17 2020 at 17:16):
(This works better with a "structural" idea of what a set is, e.g., "an object of the category of sets", rather than a "material" one as in a set theory like ZFC)
Gihan Marasingha (Oct 17 2020 at 17:19):
Thanks everyone. That makes sense and will save a lot of faffing about. I suspect students will find the typetheoretic notion to be more natural that the settheoretic one anyway.
Patrick Massot (Oct 17 2020 at 17:47):
@Gihan Marasingha did you have a look at the tutorials project? It's almost only a translation into English of the Lean files I use with first year undergrads (double major in math and computer science). The only differences are a couple of efficiency optimizations (saving a couple of lines of Lean code using rintros
instead of intros
followed by cases
, things like that). The question you asked here simply do not arise. Functions in (dependent) type theory is just way closer to actual mathematical intuition that the set theory bullshit we sometimes have to pretend to believe when teaching.
Yury G. Kudryashov (Oct 17 2020 at 17:47):
E.g., the typetheoretic notion corresponds to function types in programming languages:
double sqr (double x) { return x * x; }
corresponds to
def sqr : double → double := λ x, x * x
Kevin Buzzard (Oct 17 2020 at 18:33):
Floris said
When I explain functions, I like to explain that a function is a mathematical procedure that takes a certain class of inputs to an output. A function "knows" what its inputs can be (its domain), and what its potential outputs can be (its codomain).
I shy away from saying exactly what kind of procedure it is  if I prove that for all f :R > R, if f is differentiable then it is continuous, the f in that argument is not something defined by a mathematical procedure
Kevin Buzzard (Oct 17 2020 at 18:36):
But just to add to the chorus Gihan  the A and B you have in your definition are definitely types in Lean. All the intuition goes through.
Gihan Marasingha (Oct 17 2020 at 19:12):
@Patrick Massot yes, I really enjoyed the tutorial project! I learned much about Lean (including rintros
) from it. Fortunately, my highschool French was sufficient to understand the only text that remained untranslated: "Ce n'est pas cela. Essayez encore".
@Kevin Buzzard: according to Liebeck, 'A function from $S$ to $T$ is a rule that assigns to each $s \in S$ a single element of $T$'. Is 'rule' different from 'procedure' or has M1F changed since the 1990s? ;)
All: I like the typetheoretic approach and I agree that it's more natural in many ways (the definition of function being a case in point) than the settheoretic approach. I'm lucky to have the freedom to try this, but not all of my colleagues are sold on teaching mathematics formally (one said 'Buzzard can do this at Imperial, but...'). That's one of the reasons for raising the set / type issue as it relates to functions.
I hope others will come round eventually. This is reminiscent of the Bourbakiinfluenced changes in teaching last century.
Johan Commelin (Oct 17 2020 at 19:19):
People are still bashing Bourbaki, right?
Patrick Massot (Oct 17 2020 at 20:20):
Gihan Marasingha said:
yes, I really enjoyed the tutorial project! I learned much about Lean (including
rintros
) from it. Fortunately, my highschool French was sufficient to understand the only text that remained untranslated: "Ce n'est pas cela. Essayez encore".
Good catch! I just translated it. But really, the message is that good (but not elite) first year students can handle those exercises.
Patrick Massot (Oct 17 2020 at 20:21):
Gihan Marasingha said:
I'm lucky to have the freedom to try this, but not all of my colleagues are sold on teaching mathematics formally (one said 'Buzzard can do this at Imperial, but...').
You can tell them "Massot can do that at Orsay too".
Patrick Massot (Oct 17 2020 at 20:23):
Actually I use Lean for teaching much more than Kevin since I have 50 students each year which have a mandatory mathematics course using Lean.
Patrick Massot (Oct 17 2020 at 20:24):
Johan Commelin said:
People are still bashing Bourbaki, right?
Some people like to do that, but they will never undo the effect that Bourbaki had on mathematics.
Last updated: May 09 2021 at 11:09 UTC