## Stream: Lean for teaching

### Topic: Real analysis

#### Heather Macbeth (May 08 2020 at 17:35):

If I understand correctly, @Patrick Massot has taught a whole real analysis course in Lean. I would like to do this someday, but as a test last semester I had two real analysis students do some optional exercises:

#### Heather Macbeth (May 08 2020 at 17:37):

(By the way, since it was just two students, I could give just a few more difficult problems, rather than working up to them with large numbers of easier problems.)

#### Patrick Massot (May 08 2020 at 17:38):

This is not quite the situation. Students have a whole real analysis course during the first semester with zero Lean (or any proof assistant). They see epsilons during lectures, but the exams are 100% about calculating stuff. During the second semester they have twelve weeks with me, doing two hours of Lean with me. What we cover in those 12 weeks is a strict subset of the first semester course.

#### Heather Macbeth (May 08 2020 at 17:40):

project 1: I wrote a proof that

Lemma limitX : limit (fun (n:nat) =>  ((-1)^n * (INR n) + 5) / ((INR n)^4 - 3 * (INR n) + 3 )) 0.


Lemma limitX : limit (fun (n:nat) =>  (1 + (3*INR n^2 + INR n) / (2*INR n^2 -1))) (5/2).


#### Heather Macbeth (May 08 2020 at 17:42):

project 2: I wrote a proof that

Lemma limit_plus :  forall (Xn Yn:nat -> R) (x y:R), limit Xn x -> limit Yn y -> limit (fun n:nat => Xn n + Yn n) (x + y).


Lemma limit_mult : forall (Xn Yn:nat -> R) (x y:R), limit Xn x -> limit Yn y -> limit (fun n:nat => (Xn n) * (Yn n)) (x * y).


#### Heather Macbeth (May 08 2020 at 17:45):

project 3: I indicated this section of the textbook and had them formalize it themselves:

Definition monotone_incr (Xn:nat -> R) := forall n:nat, (Xn n) <= (Xn (S n)).

Lemma monotone_conv : forall (Xn:nat -> R), monotone_incr Xn -> bound (fun y:R => (exists n:nat, Xn n = y)) -> exists x:R, limit Xn x.


#### Kevin Buzzard (May 08 2020 at 17:45):

INR n is the real number corresponding to the natural number n?

#### Heather Macbeth (May 08 2020 at 17:46):

Yes. (For those new to the thread, this is Coq, not Lean.)

#### Heather Macbeth (May 08 2020 at 17:46):

I am sure there is a clever way to do type conversions in Coq, but since I was new to it myself, I only knew the clunky way.

#### Heather Macbeth (May 08 2020 at 17:47):

I am new to Lean but I have already discovered that it has nice type conversion commands!

#### Kevin Buzzard (May 08 2020 at 17:50):

You can just coerce in Lean: given n : ℕ you can just talk about n : ℝ. It's great that you're showing mathematicians formal proof verification systems! I use Lean in my undergraduate lectures but it's 100% optional; I run a club on Thursday evenings where people can talk to me about it.

#### Kevin Buzzard (May 08 2020 at 17:51):

Did anyone manage to do project 3? It looks pretty tough. Are there good introductions to mathematics in Coq? We're frantically trying to make Lean teaching materials for mathematicians.

#### Heather Macbeth (May 08 2020 at 17:52):

It was a good experience and the students seemed to learn a lot from it (as did I). I think real analysis is a very good playground for formalized proof: the proof structures are complicated (all those for-alls and there-exists), but also more or less the same every time, so the students can get the hang of it fast.

#### Heather Macbeth (May 08 2020 at 17:52):

Yes, they did all 3 projects! I spent a lot of time helping, but they took the big steps themselves.

#### Kevin Buzzard (May 08 2020 at 17:53):

I guess I can prove these things in Lean but I have no idea how these things would look like in Coq. Are there specialised tools for solving this sort of thing? For the first lemma I would just show that for n sufficiently large the abs value of the numerator was at most 2n and the abs value of the denominator was at least 1/2*n^4, which would be a bit of a kerfuffle

#### Heather Macbeth (May 08 2020 at 17:55):

For me, the mess of absolute values and epsilons is the point -- I think this is what introductory real analysis course should teach them :)

#### Heather Macbeth (May 08 2020 at 17:56):

I hesitate to say "Coq can't do this or that", because I am also fairly new to Coq -- but I do not know how to do the analogue of a calc proof or library_search in Coq.

#### Heather Macbeth (May 08 2020 at 17:56):

These are both great features of Lean, which make it more natural. I plan to switch to Lean if/when I do this again.

#### Kevin Buzzard (May 08 2020 at 17:56):

But conversely you could envisage a more conceptual proof along the lines of "by a tactic, $(n^4-3n+3)/n^4$ tends to 1, so by a theorem we can replace the denominator by $n^4$ etc

#### Kevin Buzzard (May 08 2020 at 17:57):

But such a tactic doesn't exist in Lean (although the theorem does) so one would have to work in a more low-level manner. It would not surprise me if one could solve all these questions with a tactic in Isabelle/HOL

#### Kevin Buzzard (May 08 2020 at 17:58):

But on the other hand, did you say you were a differential geometer? Trying to define tangent bundles in Isabelle/HOL would be a nightmare, that's why I am using a system with dependent types

#### Heather Macbeth (May 08 2020 at 18:00):

Indeed, it would be possible to write tactics to do all these problems. But I think the experience of doing them "on paper" as a beginning analysis student is better replicated by typing out the proofs by hand, rather than by invoking a tactic. My dream is to set a homework assignment full of epsilon-delta problems, and have the computer grade it!

#### Kevin Buzzard (May 08 2020 at 18:00):

It would take some guts to do this sort of thing in a differential geometry course though :-) I taught algebraic geometry last term and I formalised about 1/3 of the course but then I got bogged down by the Nullstellensatz and eventually got so far behind that I put the entire thing on hold

#### Kevin Buzzard (May 08 2020 at 18:01):

Heather Macbeth said:

My dream is to set a homework assignment full of epsilon-delta problems, and have the computer grade it!

Right! The problem is that I don't think my university would at this point buy the idea of forcing 1st years to learn a system such as this. Course they're doing this sort of thing in computer science departments everywhere!

#### Heather Macbeth (May 08 2020 at 18:02):

Though Coq does have one lower-level tactic that helps with these -- it's called nra, "nonlinear real arithmetic", and it's a (limited) nonlinear version of Lean's linarith. Great for inequalities.

#### Kevin Buzzard (May 08 2020 at 18:03):

I spent some time today grading Richard Thomas' 1st year analysis exam, and in Q2 he divides by zero! If he'd formalised his solutions in Lean he would have noticed :-)

#### Kevin Buzzard (May 08 2020 at 18:03):

So it's not just the teachers who get a better deal if the students are formalising solutions in Lean, the students would also not have to deal with annoying typos in an exam situation

#### Kevin Buzzard (May 08 2020 at 18:04):

"2(b): For $n\geq0$ show that $\sqrt{n+1}-\sqrt{n}\leq\frac{1}{2\sqrt{n}}$"

#### Kevin Buzzard (May 08 2020 at 18:04):

Fortunately I was marking Q3 so I don't get to see what the students thought of that...

#### Kevin Buzzard (May 08 2020 at 18:05):

In Lean 1/0=0 so the question is actually false :-)

#### Heather Macbeth (May 08 2020 at 18:05):

One more lower-level tactic that does not exist in Coq, so far as I know, but would be great: something like ring or linarith but which also manipulates absolute values (at least $|ab|=|a||b|$, but maybe also $|a+b|\leq |a|+|b|$). Maybe Lean's simp does this?

#### Kevin Buzzard (May 08 2020 at 18:05):

I formalised my exam! But I am a bit of an extremist...

#### Kevin Buzzard (May 08 2020 at 18:05):

simp only rewrites equalities, so it won't use the triangle inequality

#### Heather Macbeth (May 08 2020 at 18:06):

Oh dear. That hits close to home, I just corrected an in-progress exam (we are teaching remotely and asynchronously) with a sign error.

#### Kevin Buzzard (May 08 2020 at 18:06):

and I don't think linarith uses the triangle inequality either. But I've formalised a bunch of stuff like this in Lean (and got students to formalise more at my club) and the trick is that there are lemmas called things like abs_le and you rewrite those first

#### Kevin Buzzard (May 08 2020 at 18:07):

You replace $|x|\leq a$ by $-a\leq x\leq a$ and then linarith can do its magic

!!!

#### Kevin Buzzard (May 08 2020 at 18:09):

It's pretty cool what undergraduates can do if you encourage them; he's doing basic stuff with differentiability and continuity in Lean, just formalising the lectures himself -- I taught him Lean and he just decided to go for it. There is a bunch of elementary analysis there.

#### Kevin Buzzard (May 08 2020 at 18:10):

It's things like this that make me think that this has a real role to play in education.

#### Kevin Buzzard (May 08 2020 at 18:11):

and you probably saw the same sort of things too, some students just get good. This place is a really good place for beginners to ask Lean questions, it's a lot more efficient than googling

Yes, indeed.

#### Kevin Buzzard (May 08 2020 at 18:16):

Did some of the students manage to do the exercises? How hard is it to get Coq up and running? The community have tried to make it really easy to install Lean but it's still a fair amount of work for an 18 year old Windows user who is not used to having to type commands into the command line.

#### Heather Macbeth (May 08 2020 at 18:20):

This was just a couple of students, who volunteered to be my guinea pigs. They did all 3 projects, but I spent a lot of time helping, everything from installation help onwards.

#### Kevin Buzzard (May 08 2020 at 18:21):

Yeah that's how it is until you reach some basic minimum of competent users.

#### Kevin Buzzard (May 08 2020 at 18:22):

The first year I ran my Thursday evening club it was hard work and I lost a lot of people early on. The second time I had a bunch of competent 2nd years and it went much better.

#### Heather Macbeth (May 08 2020 at 18:23):

But I see that Patrick Massot set up his exercises so they run in a browser; I plan to try that next time.

#### Kevin Buzzard (May 08 2020 at 18:25):

Yeah, he also wrote tools which mix well-typeset mathematics and Lean, e.g. here

#### Kevin Buzzard (May 08 2020 at 18:25):

you can click on a line in a proof and then on a grey rectangle to see Lean's tactic state.

That's great!

#### Kevin Buzzard (May 08 2020 at 18:26):

I think there is huge potential here, for crazy formalised books etc

#### Kevin Buzzard (May 08 2020 at 18:26):

I just have no idea why software like this has been around for 30+ years but mathematicians haven't adopted it for teaching.

#### Kevin Buzzard (May 08 2020 at 18:27):

It would be interesting to re-do the proofs you gave your students in Lean to see if they're more or less painful

#### Heather Macbeth (May 08 2020 at 18:30):

I'm pretty sure they'll be less painful. My naive understanding is that Lean has better type conversion, and it has unicode and calc proofs and library_search, and these more than make up for the loss of nra.

#### Heather Macbeth (May 08 2020 at 18:32):

Anyway, yes, this is the future of teaching! But it's not quite clear when the future will really arrive.

#### Kevin Buzzard (May 08 2020 at 18:35):

I want nra anyway. What does it do? The trick is to persuade one of the CS people to write it :-)

#### Heather Macbeth (May 08 2020 at 18:41):

nra : all I know is this (1 paragraph of documentation) plus this (source code). The documentation says it's experimental, but it works well!

#### Patrick Massot (May 08 2020 at 19:39):

@Heather Macbeth thanks a lot for your explanations. I'm sorry I had to leave for family duty while you were chatting with Kevin.

#### Patrick Massot (May 08 2020 at 19:40):

About the Coq/Lean comparison: for that kind of mathematics there is clearly no foundational difference at all. It's all about being less user unfriendly (you cannot really hope for the general tool to be really user-friendly) and the surrounding tooling.

#### Patrick Massot (May 08 2020 at 19:41):

I think that unicode + absence of iron curtain is already a big advantage for students. And ongoing work will make things even more friendly. This include Ed Ayers's tactic state widget efforts and of course the whole Lean 4 project. For instance I really look forward to customizable pretty-printing.

#### Patrick Massot (May 08 2020 at 19:44):

My students used Lean is pretty diverse setups. Before the lock-down they had access to computer rooms running Lean + VScode locally. Since the beginning they also have bundle like what I link to at the beginning of this page (first three links). These are single zip file having everything in one folder (Lean+VScode+extension+library, everything) but without any flexibility to create project or update Lean or mathlib. They also used Lean i the browser as you saw, and Lean on CoCalc.

#### Patrick Massot (May 08 2020 at 19:47):

My work also involved very very careful choice of exercises to make sure students see almost only the best parts of dependent types. For instance your first project is the opposite of what I did, because it mixes natural number with real numbers. My only exception to this is the sequence $1/(n+1)$ that is used in several places, but I give all required lemmas about it. My student didn't even prove it goes to zero.

#### Patrick Massot (May 08 2020 at 19:47):

Your projects 2 to 4 are in my course.

#### Heather Macbeth (May 08 2020 at 19:48):

Thanks! CoCalc looks like another good option. Do you have an institutional subscription? I may try to get one.

#### Heather Macbeth (May 08 2020 at 19:50):

Regarding project 1: I agree, the switching back and forth between $\mathbb{N}$ and $\mathbb{R}$ is very painful. I had already decided that if I were to give the same projects again, I would reverse the order of (1) and (2).

#### Johan Commelin (May 08 2020 at 19:50):

Luckily we now have norm_cast and push_cast

#### Patrick Massot (May 08 2020 at 19:52):

I know we have norm_cast, and this would be a very important part of a course about learning Lean. But I wanted to avoid it at all cost in a course about regular maths using a proof assistant as a tool only.

#### Heather Macbeth (May 08 2020 at 19:53):

I guess, I think that doing exercises like project 1 (on paper) is really pedagogically very useful for beginning students. I set exams that mostly consist of such problems!

#### Patrick Massot (May 08 2020 at 19:56):

If you want to know more about the big picture here, it's probably useful to know that proof assistants don't have to make limit computation difficult. You can watch @Manuel Eberl 's great talk about computing limits in Isabelle.

#### Patrick Massot (May 08 2020 at 19:59):

For such tasks mathlib is currently light years behind the automation available in Isabelle. In this case there is no fundamental reason. You only need someone with Manuel's skills and enough motivation. One major problem is that those people are academics so they need papers. The first people doing such a thing can get a paper about it. But then the people porting it to other proof assistants still have a lot of work to do without having a paper. I'm exaggerating a bit, but this is a very real issue. Sometimes the solution is to get a MSc student porting things, and learning along the way, but sometimes it's too hard (or there aren't enough students).

#### Heather Macbeth (May 08 2020 at 19:59):

This is very interesting to me, though maybe it's a separate discussion ... Yes, I had seen this work of Manuel Eberl. But when I do analysis (in research), I really do flail around with inequalities, until some quantity is bounded in some Banach space norm. It feels much closer to "by-hand" epsilon-delta analysis than to big-O notation.

#### Patrick Massot (May 08 2020 at 19:59):

Yes, it's a completely separate discussion.

#### Heather Macbeth (May 08 2020 at 20:00):

For me, I am more excited about tools to manipulate inequalities (see the discussion with Kevin above about nra and my imagined tactic for the absolute value) than about tools which spit out the limit of any of a specialized class of sequences.

#### Johan Commelin (May 08 2020 at 20:01):

Patrick Massot said:

For such tasks mathlib is currently light years beyond the automation available in Isabelle.

You mean "behind", I guess

#### Heather Macbeth (May 08 2020 at 20:01):

But probably I am not understanding the full scope of Eberl's work.

#### Patrick Massot (May 08 2020 at 20:02):

Yes, my English is crappy. Let me edit my post so that less people will be confused.

#### Patrick Massot (May 08 2020 at 20:02):

What a silly idea to have those opposite words so close alphabetically

#### Patrick Massot (May 08 2020 at 20:15):

As I wrote on the general stream, the nra tactic seems like one hour of work by someone knowing how to do that kind of things. What would you want the absolute value tactic to do?

#### Heather Macbeth (May 08 2020 at 20:21):

Wow, I did not know that this chat room was "ask and you shall receive" :)

#### Patrick Massot (May 08 2020 at 20:23):

Sometimes it works surprisingly well

#### Patrick Massot (May 08 2020 at 20:23):

Sometimes it fails completely

#### Heather Macbeth (May 08 2020 at 20:23):

I would like a tactic that works in (say) normed spaces, that will verify facts of the form $\lVert 2a + b\rVert\leq 3\lVert a\rVert + \lVert b-a\rVert$.

#### Heather Macbeth (May 08 2020 at 20:24):

Do I have two wishes left?

#### Heather Macbeth (May 08 2020 at 20:25):

So, combining features of ring and nra, but also dealing with norms.

#### Patrick Massot (May 08 2020 at 20:29):

It needs quite a bit more cleverness than ring and nra, unless I'm missing a trick here.

#### Patrick Massot (May 08 2020 at 20:30):

You need to have the idea of rewriting $2a+ b = 3a + (b-a)$. ring doesn't require any idea

#### Patrick Massot (May 08 2020 at 20:30):

ringcan check this identity, but not come up with the statement

#### Heather Macbeth (May 08 2020 at 20:31):

I think that's right -- I thought about it briefly a while back, couldn't see a deterministic algorithm, so it has to be a matter of writing a good, tailored search.

#### Patrick Massot (May 08 2020 at 20:32):

Of course we can specifically detect goals of the form $\|| x \|| \le \lambda \||y\|| + \mu \||z\||$, but that would be a really specialized tactic

#### Patrick Massot (May 08 2020 at 20:32):

and not good for teaching IMO, since I want students to come up with the idea, and Lean to do automatically things that we wouldn't write on paper.

#### Patrick Massot (May 08 2020 at 20:33):

From that point of view linarith is already too smart sometimes. It closes goals that students would have a hard time doing on paper, especially when there are many inequalities floating around

#### Kevin Buzzard (May 08 2020 at 21:10):

On the other hand I'd love a Groebner basis tactic and that would definitely prove things which non-puzzle-minded undergraduates would find tricky. Sometimes you just want to get on though

#### Heather Macbeth (May 08 2020 at 21:14):

Patrick Massot said:

and not good for teaching IMO, since I want students to come up with the idea, and Lean to do automatically things that we wouldn't write on paper.
From that point of view linarith is already too smart sometimes. It closes goals that students would have a hard time doing on paper, especially when there are many inequalities floating around

Thank you for writing this, I had been thinking this but had not quite put it into words. For teaching, I would like to have a set of tactics, which automate everything that the undergraduate finds obvious (let's say, chains of 3 combinations of the field axioms, the ordering axioms, and $|ab|=|a||b|$), and nothing else.

#### Heather Macbeth (May 08 2020 at 21:24):

Back to this point ...

Heather Macbeth said:

I would like a tactic that works in (say) normed spaces, that will verify facts of the form $\lVert 2a + b\rVert\leq 3\lVert a\rVert + \lVert b-a\rVert$.

Patrick Massot said:

Of course we can specifically detect goals of the form $\|| x \|| \le \lambda \||y\|| + \mu \||z\||$, but that would be a really specialized tactic

I think you understood what I meant (you are an analyst too), but my dream tactic would not just verify that $\lVert 2a + b\rVert\leq 3\lVert a\rVert + \lVert b-a\rVert$, but would invent that fact itself, when faced with hypotheses $\lVert c\rVert \leq \lVert 2a + b\rVert$ and $\lVert a\rVert\leq \lVert ef\rVert$ (let's say we're in a normed algebra), in order to prove the goal $\lVert c\rVert \leq 3\lVert e\rVert\lVert f\rVert + \lVert b-a\rVert$. But I know there is no algorithm for this.

#### Johan Commelin (May 08 2020 at 21:29):

I think that a mix of simp, norm_num, linarith and rewrite_search (not yet in mathlib) would get quite far with such a goal. But it would also be slow.

#### Johan Commelin (May 08 2020 at 21:30):

The nice thing is that some of these tactics can print a tactic script that is longer and less elegant, but faster.

#### Jeremy Avigad (May 08 2020 at 21:37):

This very nice paper may be of interest: https://arxiv.org/abs/0904.3482.

#### Heather Macbeth (May 08 2020 at 21:53):

@Jeremy Avigad, thank you for the link. I am not used to reading logic papers, but is this paper saying that there exists an algorithm which determines the truth of statements like
$\forall a,b,c,d\in V,(\lVert c\rVert \leq \lVert 2a+b\rVert\land\lVert a\rVert\leq \lVert d\rVert )\Rightarrow (\lVert c\rVert\leq 3\lVert d\rVert +\lVert b-a\rVert)$
? If so that's everything I asked for except the extension from vector spaces to algebras.

#### Chris Hughes (May 08 2020 at 23:35):

I think it does suggest that, but it reduces it to the theory of real closed fields, and this is a highly non trivial thing to implement.

#### Jalex Stark (May 09 2020 at 00:32):

In addition to being hard to implement, it's also like doubly exponentially slow, right?

#### Jalex Stark (May 09 2020 at 00:34):

(on the topic of proving inequalities, this paper has a nice algorithm for a broad class of cauchy-schwartz-like inequalities)

#### Chris Hughes (May 09 2020 at 00:34):

Yeah, but e^e^3 still isn't very big, and the examples in practice are only that big.

#### Chris Hughes (May 09 2020 at 00:35):

I don't think humans are any better than double exponential.

#### Jalex Stark (May 09 2020 at 00:37):

I think it would be magical (and I don't see any limitation other than engineer hours, which is to say it's not happening anytime soon) to have a server that runs an expensive algorithm like this and memorizes all the queries it's received together with a witness that is much cheaper to check than running the algorithm

#### Heather Macbeth (May 09 2020 at 01:02):

Instructive, thanks!

#### Mario Carneiro (May 09 2020 at 05:12):

@Jalex Stark Are there good witnesses for real closed fields? If you use terms to inhabit the existentials, you can probably bring it down to the quantifier free part but I think it's still pretty hard from there

#### Patrick Massot (May 09 2020 at 11:17):

Patrick Massot said:

Wow, I did not know that this chat room was "ask and you shall receive" :)

Sometimes it works surprisingly well

https://github.com/leanprover-community/mathlib/issues/2637

(deleted)

#### Jalex Stark (May 09 2020 at 11:55):

hmm. I guess I come from a world where every proof can be made exponentially shorter by using a PCP.
but I guess we need deterministic proofs, and I don't have any particular ideas here.

#### Mario Carneiro (May 09 2020 at 11:58):

I like nondeterministic proofs

#### Mario Carneiro (May 09 2020 at 12:00):

To put it another way, I'm specifically interested in whether there is an NP algorithm for real closed fields that is faster than double exponential

#### Jalex Stark (May 09 2020 at 12:32):

Okay, so we have a doubly-exponential NP-type proof, which is just a transcript of the deterministic algorithm. Standard pcp machinery can give us a pcp of the same length. That's a doubly-exponentially long proof string such that if the theorem is false, then you can find a hole with constant probability by checking only a constant number of random locations. Of course, checking a random location in a doubly-exponentially long string requires exponentially much randomness.

#### Mario Carneiro (May 09 2020 at 12:34):

what does pcp stand for here? I thought it was post correspondence problem but I don't see the relation

#### Jalex Stark (May 09 2020 at 12:35):

Probabilistically checkable proof

#### Jalex Stark (May 09 2020 at 12:36):

I edited out the false thing above, which makes the already-not-good-enough thing a bit worse

#### Mario Carneiro (May 09 2020 at 12:37):

Oh I see. I think these aren't good enough for lean, even with an oracle (the human, or mathematica, etc)

#### Jalex Stark (May 09 2020 at 13:01):

okay, that's sad but also what I expected

#### Heather Macbeth (May 09 2020 at 17:28):

Patrick Massot said:

Wow, I did not know that this chat room was "ask and you shall receive" :)

Sometimes it works surprisingly well

https://github.com/leanprover-community/mathlib/issues/2637

So cool, thank you!!

#### Kevin Buzzard (May 10 2020 at 15:31):

I keep meaning to do these Coq projects in Lean but marking keeps getting in the way :-(. I think the way I would do the first one would be to prove that the limit of $\frac{n^4-3n+3}{n^4}$ is 1 and then use the calculus of limits to reduce the question to finding the limit of $\frac{(-1)^nn+5}{n^4}$. In general I think I would want a lemma saying that if $p(x)\in\R[x]$ has degree $d$ then the limit of $\frac{p(n)}{n^d}$ is the leading term of $p$. If these things aren't in the library I'm going to have to start getting my hands dirty. But this seems to be a nice way to a "conceptual" proof of the projects.

#### Kevin Buzzard (May 10 2020 at 15:32):

@Kenny Lau how would you do this https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for.20teaching/topic/Real.20analysis/near/196926867 in Lean?

#### Patrick Massot (May 12 2020 at 10:49):

Heather Macbeth said:

https://github.com/leanprover-community/mathlib/issues/2637

So cool, thank you!!

It would be nice if you could give us a list of half a dozen goals the Coq version can solve (and you find useful if possible) so they can be added as tests to the Lean version.

#### Heather Macbeth (May 12 2020 at 21:56):

@Patrick Massot , how is this for a start? Adapted from my student's proof that products preserve limits. Let me know if the tests should be more or less focused than this (eg is it useful to have irrelevant hypotheses, random function applications that the parser has to treat as blocks, etc? Or should the examples be truly minimal?)

In Coq, using nra, I can do

Lemma test (u v x y A B : R) : (0 < A) -> (A <= 1) -> (1 <= B)
-> (x <= B) -> ( y <= B)
-> (0 <= u ) -> (0 <= v )
-> (u < A) -> ( v < A)
-> (u * y + v * x + u * v < 3 * A * B).
Proof.
nra.
Qed.


The best I can figure out in Lean (without the new nlinarith) is

example (u v x y A B : ℝ) : (0 < A) → (A ≤ 1) → (1 ≤ B)
→ (x ≤ B) → ( y ≤ B)
→ (0 ≤ u ) → (0 ≤ v )
→ (u < A) → ( v < A)
→ (u * y + v * x + u * v < 3 * A * B) :=
begin
intros,
have h1 : 0 ≤ B := by linarith,
have h2 : 0 ≤ A := by linarith,
calc u * y + v * x + u * v
= u * y + ( v * x + u * v ) : by ring
... ≤ u * B + ( v * x + u * v ) : add_le_add_right' (mul_le_mul_of_nonneg_left a_4 a_5)
... ≤ A * B + ( v * x + u * v ) : add_le_add_right' (mul_le_mul_of_nonneg_right (le_of_lt a_7) h1)
... = v * x + (A * B + u * v ) : by ring
... ≤ v * B + (A * B + u * v ) : add_le_add_right' (mul_le_mul_of_nonneg_left a_3 a_6)
... ≤ A * B + (A * B + u * v ) : add_le_add_right' (mul_le_mul_of_nonneg_right (le_of_lt a_8) h1)
... = u * v + 2 * A * B: by ring
... ≤ A * v + 2 * A * B : add_le_add_right' (mul_le_mul_of_nonneg_right (le_of_lt a_7) a_6)
... ≤ 1 * v + 2 * A * B : add_le_add_right' (mul_le_mul_of_nonneg_right a_1 a_6)
... < 1 * A + 2 * A * B : by linarith
... ≤ B * A + 2 * A * B : add_le_add_right' (mul_le_mul_of_nonneg_right a_2 h2)
... = 3 * A * B : by ring,
end


(I would also be interested to hear if there are any tricks that would shorten the above proof.)

#### Patrick Massot (May 12 2020 at 22:05):

Yes, this is a very good start.

#### Heather Macbeth (May 12 2020 at 22:06):

(a few edits to the above, as

The best I can figure out in Lean

improves)

#### Patrick Massot (May 12 2020 at 22:07):

I don't know if you noticed, but you can follow the conversation at https://github.com/leanprover-community/mathlib/pull/2637

#### Patrick Massot (May 12 2020 at 22:09):

About your Lean code, you probably missed the fact you can feed linarith a list of facts to use.

#### Heather Macbeth (May 12 2020 at 22:10):

So linarith would replace the explicit add_le_add_right' invocations, is that correct?

Yes

#### Patrick Massot (May 12 2020 at 22:11):

For instance you can begin your calc with

  calc u * y + v * x + u * v
≤ v * x + (A * B + u * v ) :  by linarith [mul_le_mul_of_nonneg_left a_4 a_5, mul_le_mul_of_nonneg_right (le_of_lt a_7) h1]


#### Patrick Massot (May 12 2020 at 22:11):

But this is still crappy. We really need that new tactic here

#### Heather Macbeth (May 12 2020 at 22:12):

Still, that's better, thanks!

#### Heather Macbeth (May 12 2020 at 22:19):

Here's what I can reduce to using the trick you told me. It's interesting to me that two invocations of ring cannot be removed. I had thought that linarith subsumed ring, but it seems not.

begin
intros,
have h1 : 0 ≤ B := by linarith,
have h2 : 0 ≤ A := by linarith,
calc u * y + v * x + u * v
≤ u * B + (v * x + u * v) : by linarith [mul_le_mul_of_nonneg_left a_4 a_5]
... ≤ A * B + (v * x + u * v) : by linarith [mul_le_mul_of_nonneg_right (le_of_lt a_7) h1]
... ≤ v * B + (A * B + u * v) : by linarith [mul_le_mul_of_nonneg_left a_3 a_6]
... ≤ A * B + (A * B + u * v) : by linarith [mul_le_mul_of_nonneg_right (le_of_lt a_8) h1]
... = u * v + 2 * A * B: by ring
... ≤ A * v + 2 * A * B : by linarith [mul_le_mul_of_nonneg_right (le_of_lt a_7) a_6]
... ≤ 1 * v + 2 * A * B : by linarith [mul_le_mul_of_nonneg_right a_1 a_6]
... < B * A + 2 * A * B : by linarith [mul_le_mul_of_nonneg_right a_2 h2]
... = 3 * A * B : by ring,
end


#### Rob Lewis (May 12 2020 at 22:19):

Coq's nra is clearly doing more than it claims in the documentation. There's no comparison between y and 0, so its preprocessing shouldn't learn anything new about u*y. This should just be treated as an atom that it knows nothing about, and it shouldn't find a proof.

#### Rob Lewis (May 12 2020 at 22:22):

I had thought that linarith subsumed ring, but it seems not.

I'm surprised linarith doesn't solve the first ring goal. In the second, linarith won't know to identify B*A with A*B.

#### Rob Lewis (May 12 2020 at 22:23):

Oh, it's because 2*A*B is (2*A)*B.

#### Heather Macbeth (May 12 2020 at 22:23):

Conjecture: The tactic family containing nra also contains psatz, which has the same purpose (nonlinear arithmetic) but uses a different algorithm. Perhaps at some point psatz was determined to be better and nra now just is an alias for psatz.

#### Rob Lewis (May 12 2020 at 22:25):

Could be! I can dig a little deeper tomorrow.

#### Heather Macbeth (May 12 2020 at 22:26):

Here's the source code; I couldn't make head nor tail of it, but you surely can.

#### Mario Carneiro (May 12 2020 at 22:30):

I've made it as far as here, which seems to be where the actual work is

#### Rob Lewis (May 12 2020 at 22:30):

example (u v x y A B : ℝ) : (0 < A) → (A ≤ 1) → (1 ≤ B)
→ (x ≤ B) → ( y ≤ B)
→ (0 ≤ u ) → (0 ≤ v )
→ (u < A) → ( v < A)
→ (u * y + v * x + u * v < 3 * A * B) :=
begin
intros,
have h1 : 0 ≤ B := by linarith,
have h2 : 0 ≤ A := by linarith,
calc u * y + v * x + u * v
≤ u * B + (v * x + u * v) : by linarith [mul_le_mul_of_nonneg_left a_4 a_5]
... ≤ A * B + (v * x + u * v) : by linarith [mul_le_mul_of_nonneg_right (le_of_lt a_7) h1]
... ≤ v * B + (A * B + u * v) : by linarith [mul_le_mul_of_nonneg_left a_3 a_6]
... ≤ u * v + 2 * (A * B) : by linarith [mul_le_mul_of_nonneg_right (le_of_lt a_8) h1]
... ≤ A * v + 2 * (A * B) : by linarith [mul_le_mul_of_nonneg_right (le_of_lt a_7) a_6]
... ≤ 1 * v + 2 * (A * B) : by linarith [mul_le_mul_of_nonneg_right a_1 a_6]
... < 3 * (A * B) : by linarith [mul_le_mul_of_nonneg_right a_2 h2, mul_comm A B]
... = 3 * A * B : by ring,

end


#### Mario Carneiro (May 12 2020 at 22:31):

Aha, nlinear_preprocess is the preprocessor

#### Rob Lewis (May 12 2020 at 22:34):

Not claiming this is really better, but

example (u v x y A B : ℝ) : (0 < A) → (A ≤ 1) → (1 ≤ B)
→ (x ≤ B) → ( y ≤ B)
→ (0 ≤ u ) → (0 ≤ v )
→ (u < A) → ( v < A)
→ (u * y + v * x + u * v < 3 * A * B) :=
begin
intros,
have h1 : 0 ≤ B := by linarith,
have h2 : 0 ≤ A := by linarith,
have := mul_le_mul_of_nonneg_left a_4 a_5,
have := mul_le_mul_of_nonneg_right (le_of_lt a_7) h1,
have := mul_le_mul_of_nonneg_left a_3 a_6,
have := mul_le_mul_of_nonneg_right (le_of_lt a_8) h1,
have := mul_le_mul_of_nonneg_right (le_of_lt a_7) a_6,
have := mul_le_mul_of_nonneg_right a_1 a_6,
have := mul_le_mul_of_nonneg_right a_2 h2,
have := mul_comm A B,
have : 3 * A * B = 3 * (A * B) := by ring,
linarith
end


#### Mario Carneiro (May 12 2020 at 22:35):

I think what they failed to mention is that constraints are already normalized to 0 <= x, 0 < x or 0 = x

#### Heather Macbeth (May 12 2020 at 23:08):

One more quick example, also solved by nra in Coq:

example (A B : ℝ) : (0 < A) → (1 ≤ B) → (0 < A / 8 * B) :=
begin
intros,
have h1 : 0 < A / 8 := by linarith,
have h2 : 0 < B := by linarith,
exact mul_pos' h1 h2,
end


#### Kevin Buzzard (May 12 2020 at 23:24):

import data.real.basic

example (A B : ℝ) (hA : 0 < A) (hB : 1 ≤ B) : (0 < A / 8 * B) :=
by apply mul_pos'; linarith


#### Mario Carneiro (May 12 2020 at 23:41):

If my mental model of nra is correct, it should be doing this:

example (A B : ℝ) : (0 < A) → (1 ≤ B) → (0 < A / 8 * B) :=
begin
intros,
have := mul_nonneg (le_of_lt a) (sub_nonneg_of_le a_1),
linarith,
end


but evidently that doesn't work

#### Mario Carneiro (May 12 2020 at 23:57):

Actually, I think it's also doing normalization into monomials first as well. So it's more like

example (A B : ℝ) : (0 < A) → (1 ≤ B) → (0 < A / 8 * B) :=
begin
intros,
have := mul_nonneg (le_of_lt a) (sub_nonneg_of_le a_1),
rw [mul_sub] at this,
rw show A / 8 * B = (A * B) * 1 / 8, by ring,
linarith,
end


which does work

#### Mario Carneiro (May 12 2020 at 23:58):

I don't think it's going to be possible to support this without getting into the weeds of linarith

#### Heather Macbeth (May 13 2020 at 02:29):

I guess the point is that Coq's lra behaves differently from linarith? In particular, as we discussed earlier, it subsumes ring, whereas linarith does not. For example, if I directly translate to Coq the code written by @Rob Lewis above, I can cut the two lines

  have := mul_comm A B,
have : 3 * A * B = 3 * (A * B) := by ring,


i.e., just the following works:

Require Import Rbase.
Require Import Psatz.
Local Open Scope R_scope.

Lemma test (u v x y A B : R) : (0 < A) -> (A <= 1) -> (1 <= B)
-> (x <= B) -> ( y <= B)
-> (0 <= u ) -> (0 <= v )
-> (u < A) -> ( v < A)
-> (u * y + v * x + u * v < 3 * A * B).
Proof.
intros a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8.
assert (h1 : 0 <= B) by lra.
assert (h2 : 0 <= A) by lra.
pose proof Rmult_le_compat_l _ _ _ a_5 a_4.
pose proof Rmult_le_compat_r _ _ _ h1 (Rlt_le _ _ a_7).
pose proof Rmult_le_compat_l _ _ _ a_6 a_3.
pose proof Rmult_le_compat_r _ _ _ h1 (Rlt_le _ _ a_8).
pose proof Rmult_le_compat_r _ _ _ a_6 (Rlt_le _ _ a_7).
pose proof Rmult_le_compat_r _ _ _ a_6 a_1.
pose proof Rmult_le_compat_r _ _ _ h2 a_2.
lra.
Qed.


#### Rob Lewis (May 13 2020 at 09:51):

Yep. Coq clearly does some kind of normalization of atoms in lra.

Require Import  Psatz Rbase.
Open Scope R_scope.

Lemma test2 (u v : R) : (0 < u*v) -> 0 < 3*u*v.
Proof.
lra.
Qed.


* associates to the left, so it figures out that (3*u)*v is actually 3*(u*v) where u*v is the atom it cares about.

#### Rob Lewis (May 13 2020 at 09:53):

linarith could actually be adapted to do that one pretty easily, but this one is more surprising:

Lemma test2 (u v : R) : (0 < u*v) -> 0 < 3*v*u.
Proof.
lra.
Qed.


#### Rob Lewis (May 13 2020 at 09:55):

It must be calling ring on the atoms? This sounds super expensive.

#### Rob Lewis (May 13 2020 at 09:58):

@Mario Carneiro is there an API for ring-without-proofs? Like, I give it an expr and get a ring-normalized expr back without a proof that they're equal.

#### Rob Lewis (May 13 2020 at 11:22):

I have a partially working linarith that handles this at least. It needs efficiency improvements to be used in practice, and should become part of the more expensive linarith!. But there's a bug in ring:

import tactic.ring

-- loops
example (A B : ℕ) : A * B = 2 :=
begin
-- ring,
end


Haven't investigated yet.

#### Patrick Massot (May 13 2020 at 15:15):

I'm now marking my Lean exam. I didn't teach them the assumption tactic because that's one more tactic to learn and exact is good enough. Hence they use linarith instead of assumption. :shrug:

#### Heather Macbeth (May 13 2020 at 15:35):

Students are efficient, they do what works! After my ones learned that nra did effectively anything, I think I saw them use it to prove that 2 * u = u + u :)

#### Kevin Buzzard (May 13 2020 at 15:38):

I prove 0<1 with norm_num because it's fewer characters than exact zero_lt_one and exact dec_trivial.

#### Rob Lewis (May 13 2020 at 15:39):

When I give advice to people writing new tactics, I tell them that their users will abuse them in every way possible. They need to be foolproof. This is why the new norm_cast figures out attributes for you automatically.

#### Patrick Massot (May 13 2020 at 15:40):

Both those uses are fair. I don't want to waste student neurons on remembering the names of whatever specifically prove 2 * u = u + u or 0 < 1.

#### Rob Lewis (May 13 2020 at 15:40):

Kevin Buzzard said:

I prove 0<1 with norm_num because it's fewer characters than exact zero_lt_one and exact dec_trivial.

This doesn't sound like abuse though, that's exactly the situation norm_num is designed for!

#### Mario Carneiro (May 13 2020 at 17:05):

Rob Lewis said:

Mario Carneiro is there an API for ring-without-proofs? Like, I give it an expr and get a ring-normalized expr back without a proof that they're equal.

No, but why would you want that? If you are normalizing the context, you will probably want to associate proofs during that phase too

#### Rob Lewis (May 13 2020 at 17:38):

Linarith works using ring for verification. It does ~no proving of its own, including in the step where it identifies atoms. So that step just needs to ask "are these exprs syntactically eq or defeq or ring-eq" depending on the context. Then it builds the linear problem, computes the coefficients, and if ring claimed that things were equal before, it should normalize them away in the end.

#### Rob Lewis (May 13 2020 at 17:40):

But there's a related "issue," the order of appearance of arguments to ring affects the normal form. This is kind of expected, since you need a deterministic term order. But A*B and B*A don't normalize to the same thing if you normalize them separately.

#### Mario Carneiro (May 13 2020 at 17:42):

You should be operating in the ring_m monad

#### Mario Carneiro (May 13 2020 at 17:42):

that way you can share atoms between invocations

#### Rob Lewis (May 13 2020 at 17:45):

Okay, that solves one issue. But I still can't get the normal form without a proof, right?

#### Rob Lewis (Jun 08 2020 at 20:22):

I have an update to linarith that makes some progress here, effectively doing normalization of monomials+. It handles @Mario Carneiro 's example

example (A B : ℝ) : (0 < A) → (1 ≤ B) → (0 < A / 8 * B) :=
begin
intros,
have := mul_nonneg (le_of_lt a) (sub_nonneg_of_le a_1),
linarith,
end


and @Heather Macbeth 's example cutting the two ugliest lines from the ugly proof. But in combination with Mario's nonlinear preprocessing it still doesn't match nra -- Heather's example still fails.

#### Rob Lewis (Jun 08 2020 at 20:23):

AFAICT linarith is now comparable to lra, and nlinarith does everything the documentation of nra claims. So nra must be doing something extra.

#### Rob Lewis (Jun 08 2020 at 20:27):

This fails:

example (A B : ℚ) : (0 < A) → (1 ≤ B) → (0 < A / 8 * B) :=
begin
intros,
nlinarith,
end


but this succeeds:

example (A B : ℚ) : (0 < A) → (1 ≤ B) → (0 < B) → (0 < A / 8 * B) :=
begin
intros,
nlinarith,
end


so maybe nra is working with a bit more than just comparisons with 0?

#### Rob Lewis (Jun 08 2020 at 20:27):

New linarith is here, btw: https://github.com/leanprover-community/mathlib/tree/linarith-update

#### Heather Macbeth (Jun 08 2020 at 22:00):

Rob Lewis said:

Heather Macbeth 's example cutting the two ugliest lines from the ugly proof.

Thanks for the update! What do you mean by the "two ugliest lines", is it the two I could cut from a Lean/linarith proof here while preserving a working Coq/lra proof?

#### Rob Lewis (Jun 08 2020 at 22:07):

Yep! This works now, the Lean equivalent of your lra proof.

example (u v x y A B : ℝ) : (0 < A) → (A ≤ 1) → (1 ≤ B)
→ (x ≤ B) → ( y ≤ B)
→ (0 ≤ u ) → (0 ≤ v )
→ (u < A) → ( v < A)
→ (u * y + v * x + u * v < 3 * A * B) :=
begin
intros,
have h1 : 0 ≤ B := by linarith,
have h2 : 0 ≤ A := by linarith,
have := mul_le_mul_of_nonneg_left a_4 a_5,
have := mul_le_mul_of_nonneg_right (le_of_lt a_7) h1,
have := mul_le_mul_of_nonneg_left a_3 a_6,
have := mul_le_mul_of_nonneg_right (le_of_lt a_8) h1,
have := mul_le_mul_of_nonneg_right (le_of_lt a_7) a_6,
have := mul_le_mul_of_nonneg_right a_1 a_6,
have := mul_le_mul_of_nonneg_right a_2 h2,
linarith
end


#### Heather Macbeth (Jun 08 2020 at 22:10):

As for the secret sauce of nra, one trivial possibility. There was this discovery of Mario's:
Mario Carneiro said:

I think what they failed to mention is that constraints are already normalized to 0 <= x, 0 < x or 0 = x

Is your nlinarith doing the same?

#### Rob Lewis (Jun 08 2020 at 22:20):

I didn't update nlinarith beyond what Mario did, but no, I don't think it's doing that. At a glance I don't think that's what's going on, but maybe..

#### Mario Carneiro (Jun 09 2020 at 04:46):

@Rob Lewis I think that normalizing should be sufficient, but I think linarith is currently blocked by lack of normalization in cases like this:

example (A B : ℚ) (h : 0 < A * B / 8) : 0 < A / 8 * B := by linarith -- fail


which would be normalized by ring but are probably being treated as distinct by linarith

#### Mario Carneiro (Jun 09 2020 at 04:51):

Assuming that linarith is able to normalize both of these terms to 1/8 * atom(A*B), it should be sufficient to normalize inequalities to 0 <= x to prove

example (A B : ℚ) : (0 < A) → (1 ≤ B) → (0 < A / 8 * B) := by nlinarith


because the preprocessing will produce

example (A B : ℚ) (h1 : 0 < A) (h2 : 0 ≤ B - 1) (h3 : 0 < A * (B - 1)) :
0 < A / 8 * B := by linarith


and I can confirm that after monomial processing linarith is able to prove this goal:

example (A B : ℚ) (h1 : 0 < A) (h2 : 0 ≤ B - 1) (h3 : 0 < A * B - A) :
0 < 1/8 * (A * B) := by linarith --works


#### Rob Lewis (Jun 09 2020 at 07:39):

@Mario Carneiro did you see the linarith update I mentioned above? #2995

#### Rob Lewis (Jun 09 2020 at 07:40):

It proves

example (A B : ℚ) (h : 0 < A * B / 8) : 0 < A / 8 * B := by linarith


#### Rob Lewis (Jun 09 2020 at 07:40):

But not

example (A B : ℚ) : (0 < A) → (1 ≤ B) → (0 < A / 8 * B) := by nlinarith


#### Mario Carneiro (Jun 09 2020 at 07:40):

I saw it after this message; I saw that you noticed something similar

#### Mario Carneiro (Jun 09 2020 at 07:41):

Note that you have to be able to reduce A * (B - 1) to A * B - A * 1 during monomial processing

#### Rob Lewis (Jun 09 2020 at 09:06):

Okay, yeah, I think you're right. Normalizing hypotheses to 0 < and running the current nlinarith preprocessing creates a problem that lra can solve. In principle linarith should solve it too, but it hits an implementation bottleneck. Fixable in theory, lra is more or less instant.

#### Rob Lewis (Jun 09 2020 at 09:06):

(This is on the more complicated example.)

#### Rob Lewis (Jun 09 2020 at 09:08):

It did give me a stack overflow in JSCoq but the native version has no trouble, heh.

#### Mario Carneiro (Jun 09 2020 at 09:10):

ooh, how have I not heard about jscoq before

#### Rob Lewis (Jun 09 2020 at 12:18):

Confirmed. I refactored linarith to avoid a very expensive comparison between rb_maps. Surprised that didn't turn up as a bottleneck earlier. It now solves this (~8 seconds on my laptop, so still room for improvement).

lemma test7 (u v x y A B : ℚ)
(a : 0 < A)
(a_1 : 0 <= 1 - A)
(a_2 : 0 <= B - 1)
(a_3 : 0 <= B - x)
(a_4 : 0 <= B - y)
(a_5 : 0 <= u)
(a_6 : 0 <= v)
(a_7 : 0 < A - u)
(a_8 : 0 < A - v) :
u * y + v * x + u * v < 3 * A * B :=
begin
intros,
nlinarith
end


#### Rob Lewis (Jun 09 2020 at 12:19):

So the nlinarith preprocessing just needs to normalize things to 0 < before running, and we're there.

#### Mario Carneiro (Jun 09 2020 at 12:31):

Doesn't linarith already have to do this preprocessing? Perhaps linarith can split this processing out as a separate function so that nlinarith can insert itself after this processing but before the main work

#### Rob Lewis (Jun 09 2020 at 12:37):

Yes, this can be part of a refactor of the whole linarith frontend.

#### Patrick Massot (Jun 09 2020 at 12:37):

Thank you very much Rob and Mario for taking time to work on this.

Last updated: Dec 20 2023 at 11:08 UTC