Equality part 1: definitional equality.

I keep meaning to write something about equality in Lean, and on the tube home today I just managed to understand it a little bit better, so perhaps now is the time (although I won’t get to today’s revelation until part 2).

My post on building the natural numbers from first principles , written when I had had been learning Lean for only a few months, is a popular post. I explain how the natural numbers are defined in Lean, and also how addition of natural numbers is defined. As mathematicians we do not think twice about the facts that 0 + n = n and n + 0 = n, but in Lean these two equalities have a different status, because of the definition of addition.

The definition of addition in Lean is “by induction on the second variable” — or more precisely by recursion on the second variable. Every natural number is either 0, or the “successor” S(n) of a previously-defined natural number. Lean defines x+0 to be x, and if we have defined x+n already, then Lean defines x+S(n) to be S(x+n). If you like, we can now prove by induction that x+y has been defined for all x and y, by induction on y. Lean’s notation for S(n) is succ n or more precisely nat.succ n .

I highlight “defines” in the preceding paragraph because we now see some examples of so-called “definitional equality”. The equality x+0=x for x a natural number is a definitional equality — it is true by definition. However the equality 0+x=x is certainly true, but it is not true by definition — it is true because of a theorem. Indeed, one proves 0 + x = x by induction on x, as is done fairly early on in the post linked to above.

As a mathematician I never really had to distinguish between these two kinds of equality. However, when writing Lean code, it is a good idea to keep track of which equalities should be true by definition and which ones are true because of some extra content. One very simple reason for this is that if your goal is an equality which is true by definition, however complicated the definitions involved may be, there is every chance that Lean will be able to prove it using the refl tactic (or, in term mode, the rfl term). This might sound silly but it is absolutely not — several times in the past I found myself stuck trying to prove something which felt obvious to me but for which I could not find the right lemmas in Lean’s library to do the job, and then it was pointed out to me that refl would solve the goal.

Over the last few months I worked intensely on the perfectoid project and during this time I had to work with equivalence classes. I have a traditional model of equivalence classes in my head — if S is a set and \sim is an equivalence relation on S then the set Q of equivalence classes for \sim is, by definition, a set of subsets of S, equipped with the canonical map S\to Q sending s\in S to its equivalence class [s]. It was Patrick Massot who pointed out to me that in some sense this construction is misleading — one does not really need Q to be precisely this set, in fact the main thing one needs is the universal property for Q, namely that if f:S\to T is a function such that s_1\sim s_2\implies f(s_1)=f(s_2) then f descends to a function \overline{f}: Q\to T satisfying \overline{f}([s])=f(s) for all s\in S. Now all this is in Lean of course, but its implementation was something which I always found mysterious until recently, for the reasons I shall now explain.

The first, completely dumb, thing is that the descent \overline{f} of f is called the lift of f in Lean. This huge change of notation disoriented me for a long time. A related piece of notation: the universal property \overline{f}([s])=f(s) mentioned above has a name — it’s called “the computation principle” in Lean — and I had never heard it being called this before, which was an obstruction to my understanding when people were talking about this sort of thing on the Lean Zulip chat.

The second reason was that whilst Lean is completely capable of forming subsets of S and making them into a new type Q, Lean did not use this approach at all, using instead a new quotient axiom to make Q which is explicitly added to the system, and then a certain amount of fuss is made about it right the end of Theorem Proving In Lean. For a long time I could not see the point of this quotient axiom at all; the only thing it seemed to do was to provide a second method for making quotient types which was not the standard way taught in undergraduate mathematics classes.

However, when actually working with equivalence relations and equivalence classes in a technical setting, the penny finally dropped: the computational principle is a definitional equality. In other words, the proof that \overline{f}([s])=f(s) is refl. This really does change your workflow in practice; indeed I was very excited on a few occasions that what looked like some very complicated goal involving quotients turned out to be provable with refl. To appreciate the power of this, imagine how one would go about defining \overline{f} using the traditional approach. We have some equivalence class C, which is non-empty by definition. We want to define \overline{f}(C). How do we do this? Well we apply the computer scientists’ axiom of choice, which gives us an element c\in C, and then we just return f(c). Now it is certainly a theorem that \overline{f}([s])=f(s), however the chances are that the c\in [s] that we chose was not s, and the fact that f(c)=f(s) is true because it is a theorem that f is constant on equivalence classes! In particular, \overline{f}([s])=f(s) would not be true by definition with this approach.

Definitional equality is a powerful tool. If x=y is true by definition, and h is a function, then h(x)=h(y) is also true by definition. If however x and y are only equal because of a theorem, then one is going to have to use Lean’s rewrite tactic with the theorem to prove that h(x)=h(y) and in particular one is going to have to do some work. Seeing a gigantic goal disappear completely with the proof being refl is very satisfying, and when I understood the difference between definitional equality and equality-because-of-a-theorem I realised that refl is a powerful tool for finishing proofs. In fact I have even claimed in the past that refl is my favourite tactic, although I guess on occasion I have to confess that ring can be pretty useful too…

Advertisements
Posted in Learning Lean | Tagged , | Leave a comment

Perfectoid spaces!

Patrick Massot, Johan Commelin and I finished our definition of a perfectoid space in Lean! The home page of our project is here (check out Patrick’s graph, representing how Lean thinks about perfectoid spaces!) and the source code is here. We ultimately wrote around 12,000 lines of code.

What does this all mean? Well, one way of thinking about it, following the theme of this blog, might be: my virtual undergraduate Xena, who did not even know the definition of the complex numbers 18 months ago, now knows some really complicated things! Perfectoid spaces were discovered/invented by Peter Scholze in 2011, and used by him to prove new cases of the weight-monodromy conjecture and Langlands’ conjectures. Scholze was awarded the Fields Medal, one of the highest honours in mathematics, for this work.

But in my mind, the important thing is this. We all know, and indeed computer scientists have known for decades, that computer proof assistants like Lean are capable of working with undergraduate-level mathematics; indeed in my previous post I link to Abhimanyu Pallavi Sudhir’s solutions to last May’s M1F exam (the 1st year “introduction to proof” course which I teach at Imperial), and over the last 18 months I have blogged about many other achievements of Imperial’s undergraduates, and in particular the work of Chris Hughes and Kenny Lau formalising many proofs of results on our undergraduate curriculum and beyond. Ramon Mir’s MSc thesis formalised schemes in Lean in a robust way, and these are MSc level objects. But what I did not really feel I knew, until now, was whether Lean was capable of handling genuinely complex objects which are of actual interest to research mathematicians. Now we know that it is. In particular, I now see no theoretical obstruction stopping Tom Hales’ Formal Abstracts project from succeeding. In the long term, I believe that projects such as Hales’ have a real chance of changing the way humans do mathematics, and some chance of ultimately changing the way computers do mathematics.

It would still require many person-years of work to formally verify, for example, Scholze’s tilting correspondence for perfectoid spaces in Lean. But the crucial thing is that it would require far less work to formally state the correspondence. Here in 2019, formalising deep human proofs in computer proof verification systems is still a hugely non-trivial problem, which computers cannot do and which takes humans a very long time to do. But now I am sure that we are in a position where we can start telling computers the statements of precisely what we humans believe that we have achieved in pure mathematics. What computers can do with this information — well, that’s a question for the computer scientists. Given that so much effort has been put into search algorithms over the last 10 years, I should think that this would be a good place to start. I remember as a PhD student paging through a book on algebraic spaces desperately hoping to spot facts which would enable me to progress with my thesis. Can this process be automated in such a way as to be practical and useful to the 21st century PhD student?

The success of Hales’ project will involve a culture change amongst mathematicians. Ultimately it will rely on mathematicians formalising statements of their theorems, once their papers are accepted, and uploading the formalised statements to Hales’ database. We are not ready for this now, for several reasons. Firstly, we do not have enough mathematical objects formalised in Lean (we still don’t have manifolds [written May 2019]! But we will do soon, they are certainly on the way). And secondly, most mathematicians do not know the appropriate formal language which Lean understands. If my project to educate undergraduates to speak this language succeeds, and if Imperial students and others continue to get on board and formalise more and more mathematical objects, then I believe that progress will be inevitable. Imperial’s new mathematics curriculum launches in October and I will be pushing hard to digitise all the pure mathematics courses — definitions, theorems, proofs, example sheets, everything. After 25 years of teaching mathematics to undergraduates in the standard way, I am both surprised and excited to now be doing things in a completely different and new way.

Posted in Uncategorized | Tagged , , , , , | 4 Comments

M1F, Imperial undergraduates, and Lean

M1F is the “introduction to proof” course which I have taught for the last few years at Imperial College London. When I started this blog just over one and a half years ago, one of my goals was to see whether Lean could handle the solutions to an M1F exam. At the time it was pretty clear that it wasn’t ready — a random sample of M1F exams showed that most of them mentioned either the complex numbers, or functions such as the exponential, sine and cosine function. None of these were in Lean at the time.

I wrote some basic complex number code myself, and PR’ed it to the maths library; it was my first serious PR. A team led by Chris Hughes (at the time a first year) did sines and cosines and the exponential function. And now the inevitable has occurred: Abhimanyu Pallavi Sudhir, a current first year, has formalised the solutions to last year’s M1F final exam! Many thanks to Abhi — I was pretty sure this sort of thing should be accessible, but this is the proof. Apologies to Abhi for taking so long to get around to looking at his work. I believe that having concrete goals like this are a good way of driving Lean’s maths library in the direction which I want it to go in — formalising mathematics which is actually used by mathematicians. One reason I took so long to look at it was that I have been very focussed on the perfectoid project recently — but more of that in another post.

Funnily enough, one of the things in the exam which was the trickiest to do in Lean was the proof that 0.71 has no 8’s in its decimal expansion! Lean still does not have a theory of decimal expansions, although Calle Sönne and I will eventually get around to writing one (after exams). In the mean time, I wrote a definition from first principles which does the trick. Another irritating issue is the question about a set with two elements, which a mathematician can start with “WLOG the set is \{0,1\}“. I believe you — but this actually takes a few lines to justify in Lean. Something is missing here — a transport tactic of some kind. We’ll get there one day — the computer scientists are on the case.

20 months ago, formalising the solutions to an M1F exam seemed like a dream away. I’ve already mentioned three undergraduates who were involved in one way or another in realising this dream. All this made me start wondering about which Imperial undergraduates have contributed to Lean’s maths library, and what they have done. At the top we have Chris Hughes and Kenny Lau, who have made many many contributions. Kenny made a robust theory of localisations of commutative rings, essential for our work on schemes, and Chris proved the law of quadratic reciprocity and the fundamental theorem of algebra, amongst many other achievements. Both Chris and Kenny wrote their first year projects in Lean, and Chris is now a maintainer for Lean’s maths library! But here are a whole bunch of other Imperial undergraduates who have managed to get namechecked in Lean’s maths library as well:

  • Ellen Arlt (matrices)
  • Sangwoo Jo (number theory)
  • Guy Leroy (number theory)
  • Jean Lo (analysis, irrationals, operator norms)
  • Rohan Mitta (topology)
  • Blair Shi (matrices)
  • Abhimanyu Pallavi Sudhir (irrationals, analysis, hyperreals)
  • Calle Sönne (analysis, irrationals)
  • Andreas Swerdlow (algebra)

I must also mention Guillermo Barajas Ayuso, Luca Gerolla, Clara List, Amelia Livingston, Elliott Macneil, Ramon Mir and Ali Sever, all of whom wrote a substantial amount of Lean code which they did not PR; Clara on primes of the form x^2+ny^2 (completely solving the problem for n\leq 3), Luca on fundamental groups, Guillermo on analysis, Elliott on group theory and number theory, Amelia on group theory and Ali on Tarski’s formulation of 2d geometry. Ramon Fernandez Mir has written his MSci project in Lean! And last but not least, Keji Neri, who did a bunch of algebra over the summer with the Imperial summer students, even though he is a Cambridge undergraduate — the only one to have contributed to Lean’s maths library as far as I know. Oxford, Warwick, UCL, Bristol — where are you? Lean’s maths library is ready to digitise a huge chunk of your curriculum. Let’s do it — it will scare the grown-ups.

Finally, some news on Athina Thoma. Athina is the post-doc who has been observing the Imperial undergraduates and trying to figure out whether Lean helps them to learn proofs better. First great piece of news: she has had her contract renewed for another six months! Second great piece of news: slowly she and Paola Iannone are beginning to make sense of all the data they collected. I await with interest the paper they are writing, and the conclusions they will draw.

Posted in M1F, undergrad maths | Tagged , , , | Leave a comment

Happy pi day

Yesterday was pi day, and discussion of Lean’s support of pi came up on the chat. The discussion of pi is I think a great way of illustrating what Lean can and cannot do.

To start with, “Lean has pi”. Here it is in the source code.

lemma exists_cos_eq_zero : ∃ x, 1 ≤ x ∧ x ≤ 2 ∧ cos x = 0 :=      real.intermediate_value'       
(λ x _ _, continuous_iff_continuous_at.1 continuous_cos _)
(le_of_lt cos_one_pos)
(le_of_lt cos_two_neg) (by norm_num)

noncomputable def pi : ℝ := 2 * classical.some exists_cos_eq_zero

If you have ever thought about how pi might be defined formally, then maybe you can see what is going on here. The lemma cos_one_pos is the lemma that cos(1)>0 and the lemma cos_two_neg is the lemma that cos(2)<0. Cosine is defined as a power series and these are grotty power series computations. Now using the fact that cosine is continuous, and the intermediate value theorem, we can prove that cos(x) has a zero between x=1 and x=2. We define \pi to be two times an arbitrary zero of the cosine function between 1 and 2 (we choose a random one, using the computer science version of the axiom of choice, which says that you can choose an element from a non-empty set — just don’t get me started on this). The library then goes on to prove that in fact the cosine function has a unique zero in this range (because the cosine function is decreasing in this range) and now we have an unambiguous definition of \pi in Lean.

One has to constrast this approach with an approach taken by, say, a hand calculator, or a programming language like python or C++. In these languages, a value for pi will either be hard coded, or there will be an algorithm implemented which will generate pi to an arbitrary precision in as quick a time as possible. So, for example, a calculator can typically produce the value of \pi to ten decimal places (and a computer to far more if necessary), and then one could compute the value of \sin(\pi) to ten decimal places (or to far more) and see that it is 0.000000\dots.

But Lean is different. Lean is not a calculator. Lean is a theorem prover. It is true by definition that \cos(\pi/2)=0 in Lean, and it is a theorem in Lean that \sin(2\theta)=2\sin(\theta)\cos(\theta) and hence it is a theorem in Lean that \sin(\pi)=0. Note however that Lean has not done any numerical computation to prove this, it has deduced it from theorems and definitions. For this kind of question, one could regard Lean as performing better than the traditional “computational” model of a computer that we have — a computer can check that \sin(\pi) is zero to 10 or 1000000 decimal places, and the more places you want, the longer it would take. But it cannot prove the answer is zero. Lean can prove that \sin(\pi)=0 with no numerical computation at all.

But what if one did want to do a numerical computation of \pi? Well, this is the flip side of the story. Lean is not designed for this sort of question at all! It is a computer program which “knows \pi“, but actually what does it know about the value of \pi? Well, by definition, \pi is twice a number between 1 and 2, so we get

Theorem. 2<\pi<4.

So as you can see, in this regard Lean is lagging a bit behind the a hand calculator. It seemed like pi day was a good day to make things better.

And by the end of it, things had got about an order of magnitude better! Thanks to the efforts of Floris van Doorn, with some help by others, we now have

Theorem. 3.14<\pi<3.15.

Ongoing work by Kenny Lau might give us even more decimal places within the next day or so. But how might one go about proving such a theorem, given only a bunch of standard theorems about sine and cosine, and the facts that \cos(\pi/2)=0 and 2<\pi<4? Floris used the following trick:

\cos(x)^2=\frac{1+\cos(2x)}{2}.

Using this standard fact, and the fact that \cos(\pi/2)=0, he could deduce exact values for \cos(\pi/4),\ \cos(\pi/8),\ \cos(\pi/16),\ldots. Because \sin(x)^2+\cos(x)^2=1 he could deduce exact values for \sin(\pi/4),\ \sin(\pi/8),\ \sin(\pi/16),\ldots. He could also prove that if x>0 then \sin(x)<x (by using the power series for x\le 1 and the fact that \sin(x)\le 1 when x>1) and as a consequence could prove lower bounds for \pi! By using two terms of the power series for sine we can also prove that \sin(x)>x-x^3/6 for 0<x<1 and this gives us upper bounds.

Taking a random rational number and then squaring it, doubling it and subtracting one (which one has to do to get from \cos(x) to \cos(x)^2 can get a bit hairy once one has done it a few times. Lean had to prove intermediate goals such as

(2 : ℝ) ≤ ((((2 - (157 / 50 / 2 ^ (4 + 1)) ^ 2) ^ 2 - 2) ^ 2 - 2) ^ 2 - 2) ^ 2

and these are real numbers, which in Lean are big complicated equivalence classes of Cauchy sequences, so this looked a bit daunting at first — another reminder that Lean is designed to do proofs, not numerical computations. The norm_num algorithm strained a bit with these checks, however Mario Carneiro pointed out that with judicious approximations one can make life easier: the trick is to constantly replace fractions with large numerators and denominators with approximately equal fractions with smaller numerators and denominators before you square again. These dirty hacks got us through in the end.

The festivities are documented on the pi day thread at the Zulip chat (login required) or the archive of the Zulip chat (no login required), and Floris’ code is here (permalink) or get it at https://github.com/fpvandoorn/mathlib/blob/pi/src/data/real/pi.lean .

Using the decimal expansions library currently being developed by Calle Sonne and myself at Imperial, we can now prove that the first two digits of \pi after the decimal point are 1 and 4. We still have some way to go before we can catch up with Emma Haruka Iwao, but what if her code contains bugs? We have proofs 🙂

In fact in 2017, Bertot, Rideau and Thery did much better — they use Coq to get a million decimal places of pi, formally verified. Doing this work today made me understand far better what an achievement that was.

Posted in Uncategorized | Tagged , | 2 Comments

2+2=4

I am interested in teaching and outreach, and often get asked to give talks to schoolkids. I gave one today, to a room full of year 10 kids (aged 14-15), and I showed them Lean. This was the youngest group of students I’ve ever attempted to show Lean to. I decided to show them a proof that 2 + 2 = 4, starting from definitions of 2 and +. However by year 10 the students have not seen induction yet, so I started by showing them parts of a YouTube video with stuff in a line falling over (e.g. dominoes, humans). I then defined the naturals (I called them “numbers”) as an inductive type in Lean, showed how to define recursively the function which adds two to a number, and finally we proved 2 + 2 = 4 by unwrapping the definitions of 2 and + and so on.

I really didn’t know how it was going to go. But, to my relief, when we were doing the big calculation, I asked the audience to fill in the next line for all seven lines, and these kids managed to do it! I was very pleased.

Here are the pdf slides. In the actual talk the text appeared slowly (there were beamer pauses) and there were times when I spent a minute or two talking to the kids about what was going on.

On page 12 of the pdf I say “Let’s go and make some numbers using Lean” and this is what I coded up live. I finish by trying to formalise the statement that 2+2=4 but there’s a problem because although I’ve defined two and four I’ve not yet defined addition. We then go back to the pdf, and on page 15 I return to Lean and define addition like this. Then comes the moment of truth: the calculation on line 16 (which appears line by line in the actual presentation) and which I got them to do. Having made it through, I then showed how Lean could prove it with rfl, and claimed that this was because even though we’d only just taught it numbers it was already an expert in numbers. I then asked the audience what other kinds of maths did they think it was possible to teach Lean and immediately one kid said “all of it”. I agreed. I then made some provocative statements about why people like my daughter should not be forced to learn about cosines, and then asked if there were any questions. The first one was “How do I learn more about this stuff?”. But I did feel that I’d lost plenty of people in the room.

I think that age 14-15 is a little too young for this talk. These kids had self-selected — they were at Imperial for an open day (during a UK school holiday) so were probably interested in science. But I wonder if the material presented here would be a little more suited to kids a little older. I’m giving a couple more school talks in the future, so maybe I’ll find out soon enough.

Posted in Uncategorized | 4 Comments

Lean in LaTeX

Patrick Massot wrote a formatter, which can turn Lean code into beautiful LaTeXxy html. The undergraduates and I have been formalising Imperial’s first real analysis course M1P1 in Lean. Put them together and you get a 21st century proof of the sandwich theorem.

That last link is a link to a proof of the theorem that says that if three real-valued sequences (a_n), (b_n), (c_n) with a_n\leq b_n\leq c_n satisfy a_n\to\ell and c_n\to\ell, then b_n\to\ell. If you click on a line in the proof then it opens up the Lean code (which is probably incomprehensible if you don’t know any Lean) but the beauty is that if you then click on one of the grey rectangles either side of that line of Lean code then you get to see the tactic state, which a mathematician might well find easy to understand because it is written in standard mathematical language. This way a mathematician who does not know any Lean can still step through the formal proof, and can figure out how to get from each line to the next themselves, because each individual step is typically very short.

Ultimately this means that we can write formally-verified course notes for the Imperial analysis course which the first year undergraduates are currently attending, and the notes could be of use even to students who do not know the technicalities of how to use Lean and do not have Lean installed on the computers they have access to.

Posted in Imperial, undergrad maths | Tagged , | 2 Comments

A word on BIDMAS

Maybe it’s not called that in other countries, but in the UK BIDMAS (which I swear was “BODMAS” when I was at school, or maybe I just went to a weird school) was the rule that was used to figure out how to work out what things like 1+2*3-4/(5+6-7*8-9) meant. The BIDMAS rule was that B for Brackets came first, and then there’s this I which might stand for “indices” i.e. ^, and then division, multiplication, addition and subtraction. There seemed to be some disagreement amongst my own children (all of whom have learnt this at school over the last few years) as to whether the “DM” in BIDMAS meant that division had to be done before multiplication, or whether division and multiplication had equal “strength”. I ultimately realised that I was not entirely sure I understood this BIDMAS thing myself! I am pretty sure that BIDMAS doesn’t mean that addition must be done before subtraction, otherwise a-b+c would come out to be a-(b+c), whereas I am almost certain that it is supposed to mean (a-b)+c. [Interestingly though, it seemed to me that doing all divisions before all multiplications, from left to right, seems to give the same answer as treating division and multiplication with the same weight.]

We see from this discussion that these pieces of notation like + and *, and of course other symbols such as , and had better also have some sort of BIDMAS rule. Furthermore, we had also better know whether we evaluate them from left to right or from right to left, because sometimes this matters and sometimes it depends on the operator! For example 10-5-4 is (10-5)-4=1 and not 10-(5-4)=9, however if you type 2^1^2 into your favourite computer algebra package (or 2**1**2 if you’re using python) then the chances are you’re going to get 2^(1^2)=2^1=2 rather than (2^1)^2=2^2=4. Indeed, you can check that Lean thinks it’s 2:


#eval 2 ^ 1 ^ 2 -- Lean says 2
#reduce 2 ^ 1 ^ 2 -- still 2

How does this actually work then?

For any piece of notation like -, we need to know two things: First, its power (in the sense that BIDMAS says that * has more power than -; the power of an operator is a natural number) and secondly we need to know its associativity (we need to know whether a-b-c means (a-b)-c or a-(b-c)). It turns out that this is all you need to know. Lean’s parser is a so-called Pratt parser but all you really need to know is how Lean figures out the power (technically called the “left binding power”) and associativity of all the operators you run into. These operators include functions like nat.add, and notation like + (note in particular that even though nat.add 2 3 means the same as 2 + 3, the parser treats them differently). Note also that even though (a+b)+c=a+(b+c), Lean still has to know exactly which one is meant by a+b+c; the fact that they are equal is a theorem rather than being true by definition.

The first rule you need to know is that functions have very high power — they eat the next thing they see and that’s it.


#eval nat.add 3 nat.add 4 5 -- error

Functions are greedy. They eat the next thing presented to them and only afterwards check that it has the right flavour. The first nat.add eats 3, and then it eats the second nat.add and chokes because nat.add isn’t a natural number. You have to fix it with brackets, which have the highest power of all:


#eval nat.add 3 (nat.add 4 5) -- evaluates to 12

So that’s brackets and functions. Now what about notation? When notation is defined, its power is also defined. You can see the power of some notation by looking at at the numbers printed out with Lean’s #print notation command. For example


#print notation +
-- _ `+`:65 _:65 := has_add.add #1 #0

It’s the 65’s we need to understand here. The first number 65 tells you that `+` has power 65. The second number 65 tells you that + is left associative, that is, a+b+c=(a+b)+c by definition. Why? Well, in practice that second number is either equal to the first one (meaning the notation is left associative) or one less (meaning right associative). For example


#print notation ^
-- _ `^`:80 _:79 := has_pow.pow #1 #0

The power notation has a higher power than addition, as expected, but 79 is one less than 80, meaning that it’s right associative, as we saw above. Functions and brackets have power over 1000, by the way.

To learn more about left binding power and how Pratt parsers really work, e.g. to learn what the second number actually means and why it’s either equal to or one less than the first number, try the links on the Wikipedia website. But for Lean users who just want to figure out how things are being parsed, this trick should pretty much always tell you what you need to know. It’s worth just typing


#print notation

and looking at all the output — you’ll learn that ^ has power 80, * and / have power 70, and + and - have power 65, which tells you that Lean knows BIDMAS (and that addition and subtraction do indeed have the same power). Interestingly, we also learn that = has power 50. Had it ever occurred to you that = also needed a binding power? Lean also needs to know what P = Q = R means! It turns out that = is left associative, so 1 = 2 = (1 = 2) is true, by reflexivity.

If anyone has run into Lean’s (or Haskell’s) $ as an alternative for brackets, the way it works is that f $ x is just defined to be f x, but $ has power 1, which is so low that everything else gets evaluated first. For example


#eval nat.add 3 $ nat.add 4 5

works! Lean evaluates the $ at the very end, after it’s figured out that nat.add 4 5 is 9, so this time the addition succeeds.

The one gotcha I have run into is that the comma in ∀ (x : X), P x also has a super-low power (it has power 0 in fact), meaning that the innocent-looking


example (P Q : ℕ → Prop) :
∀ x, P x ∧ Q x → ∀ x, Q x ∧ P x := sorry

doesn’t mean what I would instinctively think it meant: Lean brackets it as ∀ x, (P x ∧ Q x → ∀ x, Q x ∧ P x), because has power 25, bigger than the power of the comma. To get this:


example (P Q : ℕ → Prop) :
(∀ x, P x ∧ Q x) → ∀ x, Q x ∧ P x := sorry

you have to add those brackets in explictly.

Posted in Learning Lean, Uncategorized | Leave a comment