Kevin Buzzard (Oct 30 2020 at 14:58):
At Imperial the students have just been learning about the definition of integers as modulo the equivalence relation . This is after the naturals have all been set up from first principles from Peano's axioms. It was claimed (not by me!) that the standard axioms of a commutative ring could be proved "easily" for the integers and everything was left as an exercise :D
So I did this exercise in Lean, and by far the hardest thing, at least for me, was to prove that multiplication was well-defined, i.e. descends to the quotient. When the dust clears, the problem is the following (thank you
extract_goal :-) )
example (i j k l m n p q : ℕ) (h₁ : i + n = m + j) (h₂ : k + q = p + l) : i * k + j * l + (m * q + n * p) = m * p + n * q + (i * l + j * k) := begin admit, end
omega doesn't work because the goal involves multiplication, and because we don't have Groebner bases I just rolled my eyes, added some carefully-chosen thing to both sides and did a big
calc proof. I labelled this as "boss level" :-) and students (from Imperial and elsewhere) have been working on it (and rather easier stuff!) this afternoon on the discord.
@Shing Tak Lam tried
hint pointed out that
nlinarith solves the goal!
I was surprised. What the heck is
nlinarith doing here? This goal seems to me to be a tricky goal about naturals, out of scope for
omega. Kudos to @Rob Lewis for this!
Reid Barton (Oct 30 2020 at 15:05):
I'm guessing what's happening is effectively turning everything into statements about , solving
k and plugging them in, and finishing with
ring. Note that the first statement uses the fact that we already know the original statement you were trying to prove.
Rob Lewis (Oct 30 2020 at 15:38):
nlinarith is roughly
linarith plus "squares and products of nonnegative things are nonnegative." You can
set_option trace.linarith true to see the linear problem it ends up solving. I don't know exactly what proof it finds, but it isn't solving
h2 as a preprocessing step.
Rob Lewis (Oct 30 2020 at 15:39):
But as Reid points out this is definitely circular in one way or another.
Rob Lewis (Oct 30 2020 at 15:39):
You can't use
linarith to define the integers because it immediately casts
Rob Lewis (Oct 30 2020 at 15:40):
omega I believe.
Kevin Lacker (Oct 30 2020 at 15:45):
what a weird way to define the integers. I guess this is natural if you consider set products and equivalence relations to be a more basic thing than integers?
Bryan Gin-ge Chen (Oct 30 2020 at 15:50):
This is the definition I was taught when I was first learning that things like the integers needed to be formally defined. The idea of the construction here also generalizes well to turning other commutative monoids into abelian groups.
Kevin Lacker (Oct 30 2020 at 16:09):
interesting. i would have guessed people would do it like, for every positive number x you have both +x and -x
Mario Carneiro (Oct 30 2020 at 18:10):
this is uglier to get right; I mean, what about 0?
Floris van Doorn (Oct 30 2020 at 18:37):
I remember doing this back in Lean 0.1: https://github.com/leanprover/lean2/blob/148d475421d4512df3015758275def59238458ad/library/standard/data/int/basic.lean#L631-L633
Lean was... less convenient to use back then.
Kevin Buzzard (Oct 30 2020 at 21:01):
@Kevin Lacker today I finished teaching a 4 week intensive introduction to university mathematics to the 1st years at my university. Part 1 of the course (my part) involves defining sets, functions and equivalence relations, and we don't mention the integers at all! I prove things like composite of injective functions is injective and equivalence relations = partitions etc. Part 2 starts with the natural numbers defined by Peano's axioms and then uses the tools I've developed to define the integers and rationals as equivalence classes.
Kevin Lacker (Oct 30 2020 at 22:02):
recently I taught my 7-year-old about negative numbers. I did not use the strategy of, first define injective functions and equivalence relations
Kevin Buzzard (Oct 30 2020 at 22:05):
:-) I taught my 4 year old nephew about negative numbers; we started with the "what's the number before this one?" game, and then when we got stuck at 0 we moved onto localisation of monoids.
Kevin Lacker (Oct 30 2020 at 22:10):
okay, i literally laughed out loud
Kevin Buzzard (Oct 30 2020 at 22:11):
OK so I am bending the truth a little. But it was a productive session! At the end I told him to go and ask his mother what the number before negative 9 was. She got it wrong :D
Bryan Gin-ge Chen (Oct 30 2020 at 22:26):
I really enjoyed the blog post that Kevin wrote about it: https://xenaproject.wordpress.com/2020/06/27/teaching-dependent-type-theory-to-4-year-olds-via-mathematics/
Kevin Buzzard (Oct 30 2020 at 22:51):
There really is something which annoys me about Lean's definition of
int, as a mathematician. I am in no position to say anything about implementation issues, and perhaps the definition is a stroke of genius, but having one constructor for and one constructor for somehow implicitly announces that the centre of symmetry of the integers is at the point . With the definition of one can see the symmetry at 0. What I have learnt from many conversations here is that I really should not worry about the actual definition, because if I want a certain structure on the integers I can simply make it myself. Looking at the mathlib proofs of things like being a group homomorphism makes me die a little inside; my conclusion really is that I just shouldn't be looking. With the definition this comes out really naturally. From a type-theoretic perspective perhaps the opposite is true -- why use some zany quotient type when it's just a simple inductive type with two constructors?
Kevin Buzzard (Oct 30 2020 at 22:51):
Perhaps as a mathematician I am just constantly on the look out for symmetry? shrug
Mario Carneiro (Oct 31 2020 at 05:04):
By the way, there is actually a really nice way to see as a symmetry: it's the same as bitwise NOT in two's complement arithmetic (but on an infinite bit width). Put another way, I think you can take as a subset of , the 2-adic numbers, and mapping on every digit yields the function .
Johan Commelin (Oct 31 2020 at 05:12):
Right, so we should set up our maths curriculum in a different way:
- First define (Peano style)
- Then teach them modular arithmatic:
- Time for projective limits! We can now build , and call this (??)
- After some careful study, we see that there is a really interesting subring, obtained by the invariants under some natural involution.
- Call this subring .
Let's go for it!
Mario Carneiro (Oct 31 2020 at 05:19):
This approach also matches the modular reasoning of this kid:
John Cremona said:
I tried out the “what comes before” game with my 5-year old granddaughter, starting with 6 (“how old will you be on your next birthday?”). No hesitation at all right down to “what comes before 1?” “Zero!” and then to “what comes before zero?” she said “One hundred!” instantaneously. I asked her why and she said something like “the numbers are in a circle so it has to be the biggest number in the whole world!”
Last updated: May 09 2021 at 10:11 UTC