Real analysis

Stream: Lean for teaching

[Heather Macbeth]

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]

(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]

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]

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.

and had them adapt it to a proof that

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

[Heather Macbeth]

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).

and had them adapt it to a proof that

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]

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]

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

[Heather Macbeth]

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

[Heather Macbeth]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Heather Macbeth]

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]

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

[Kevin Buzzard]

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

[Heather Macbeth]

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]

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]

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

[Kevin Buzzard]

One of my undergraduates got quite into it and made this

[Heather Macbeth]

!!!

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Heather Macbeth]

Yes, indeed.

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Heather Macbeth]

That's great!

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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

[Heather Macbeth]

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]

@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]

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]

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]

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]

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]

Your projects 2 to 4 are in my course.

[Heather Macbeth]

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

[Heather Macbeth]

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]

Luckily we now have norm_cast and push_cast

[Patrick Massot]

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]

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]

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]

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]

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]

Yes, it's a completely separate discussion.

[Heather Macbeth]

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]

Patrick Massot said:

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

You mean "behind", I guess

[Heather Macbeth]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Patrick Massot]

Sometimes it works surprisingly well

[Patrick Massot]

Sometimes it fails completely

[Heather Macbeth]

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]

Do I have two wishes left?

[Heather Macbeth]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Heather Macbeth]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Jeremy Avigad]

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

[Heather Macbeth]

@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]

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]

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

[Jalex Stark]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Jalex Stark]

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]

Instructive, thanks!

[Mario Carneiro]

@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]

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

[Patrick Massot]

(deleted)

[Jalex Stark]

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]

I like nondeterministic proofs

[Mario Carneiro]

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]

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]

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

[Jalex Stark]

Probabilistically checkable proof

[Jalex Stark]

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

[Mario Carneiro]

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

[Jalex Stark]

okay, that's sad but also what I expected

[Heather Macbeth]

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]

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]

@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]

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]

@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]

Yes, this is a very good start.

[Heather Macbeth]

(a few edits to the above, as

The best I can figure out in Lean

improves)

[Patrick Massot]

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

[Patrick Massot]

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

[Heather Macbeth]

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

[Patrick Massot]

Yes

[Patrick Massot]

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]

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

[Heather Macbeth]

Still, that's better, thanks!

[Heather Macbeth]

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]

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]

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]

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

[Heather Macbeth]

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]

Could be! I can dig a little deeper tomorrow.

[Heather Macbeth]

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

[Mario Carneiro]

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

[Rob Lewis]

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]

Aha, nlinear_preprocess is the preprocessor

[Rob Lewis]

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]

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

[Heather Macbeth]

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]

import data.real.basic

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

[Mario Carneiro]

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]

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]

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

[Heather Macbeth]

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]

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]

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]

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

[Rob Lewis]

@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]

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]

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]

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]

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

[Rob Lewis]

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]

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]

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]

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]

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]

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]

You should be operating in the ring_m monad

[Mario Carneiro]

or in your own monad that extends it

[Mario Carneiro]

that way you can share atoms between invocations

[Rob Lewis]

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

[Rob Lewis]

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]

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]

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]

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

[Heather Macbeth]

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]

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]

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]

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]

@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]

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]

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

[Rob Lewis]

It proves

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

[Rob Lewis]

But not

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Rob Lewis]

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]

(This is on the more complicated example.)

[Rob Lewis]

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

[Mario Carneiro]

ooh, how have I not heard about jscoq before

[Rob Lewis]

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]

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

[Mario Carneiro]

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]

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

[Patrick Massot]

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