what is (deterministic) timeout at 'isDefEq' ?

Stream: new members

[rzeta0]

Continuing to work through "The Mechanics of Proof", I am doing the exercise to prove:

example (x y : ℚ) (h : x * y = 1) (h2 : x ≥ 1) : y ≤ 1 := by
  sorry

My attempt at a solution is as follows

example (x y : ℚ) (h : x * y = 1) (h2 : x ≥ 1) : y ≤ 1 := by
  have h4 :=
  calc
    x * y = 1 := by rw [h]
    _ ≤ x := by addarith [h2]
    _ = x * 1 := by ring
  cancel x at h4

However this gives an error:

(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

What does this mean? What caused it?

The error refers rot the line with cancel on it.

---

If I comment out the cancel line and put the cursor at the end, info view reports

h4 : x * y ≤ x * 1

which looks cancellable, especially since x ≥ 1 by hypothesis h2

[rzeta0]

I've googled but found nothing helpful.

Should I interpret this as "the proof is so bad the internal engine broke" ?

[Kevin Buzzard]

You are asking a question about a bespoke tactic which only exists in the mechanics of proof repo, which greatly decreases the number of people who are able to answer the question.

[rzeta0]

Understood Kevin - I was directed to this site by Heather Macbeth but I understand the limited interest in non-standard tactics. I will restrict my future questions to those that apply to lean/mathlib.

[Kevin Buzzard]

The question should be answered at some point! You might have to wait though :-)

[Adam Kurkiewicz]

@rzeta0 , which chapter of "The Mechanics..." is it?

[Adam Kurkiewicz]

I've gone through most of that book so maybe I have the solution lying somewhere

[Adam Kurkiewicz]

OK @rzeta0 so this is how I solved it:

example (x y : ℚ) (h : x * y = 1) (h2 : x ≥ 1) : y ≤ 1 := by
  have h3: x ≥ x * y := by rw [← h] at h2; exact h2
  have h4 : x - x * y ≥ 0 := by addarith [h3]
  have h5: x * (1 - y) ≥ 0 := calc
    x * (1 - y) ≥ x * (1 - y) := by rfl
    _ = x - x * y := by ring
    _ ≥ 0 := by exact h4
  have h6: (1 - y) ≥ 0 := by cancel x at h5
  have h7: y ≤ 1 := by addarith[h6]
  exact h7

Let me have a look at your solution

[Kyle Miller]

Let's work through each part of this message:

(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

• isDefEq is the algorithm that checks whether two expressions are definitionally equal to one another
• Lean measures time in a deterministic way rather than using a clock, using the "heartbeat clock". At various points in the algorithm, the heartbeat clock is incremented.
• the algorithm timed out because it reached the maximum number of heartbeats. You can follow the suggestion to add the command set_option maxHeartbeats NNN before the example with a larger value of NNN to see if it will succeed if you wait long enough. Setting it to 0 turns off the timer.

This does not mean the error is because of isDefEq to be sure. Rather, it's isDefEq that happened to be running when the timer went off. We can infer that the cancel tactic uses definitional equality inside the algorithm. Maybe it has a bug, maybe it doesn't, but it seems worth someone looking into why your example causes it to time out.

[Adam Kurkiewicz]

So @rzeta0, it looks like cancel indeed should work and indeed it doesn't work for me either.

But there's still a way to finish your proof.

So, you might have heard about it already, there's a website that can help you find standard libarary proofs.. I've used it to search for mul_le_mul (although I think my first search was le_mul, after which I narrowed down to mul_le_mul. le stands for less than or equal, mul stands for multiplication, these are both standard abbreviations in lean).

Using this approach, I found mul_le_mul_left, which is a function that can take a proof of 0 < x and spit out a proof of x * y ≤ x * 1 ↔ y ≤ 1. Since it is an implication, and we want to go forward we have to do .mp and then we feed it the proof you've got already, h4, to get y ≤ 1

Putting this all together (I'm leaving showing 0 < x as an exercise):

example (x y : ℚ) (h : x * y = 1) (h2 : x ≥ 1) : y ≤ 1 := by
  have h4 :=
  calc
    x * y = 1 := by rw [h]
    _ ≤ x := by addarith [h2]
    _ = x * 1 := by ring
  have x_le_0 : 0 < x := sorry
  exact (mul_le_mul_left x_le_0 : x * y ≤ x * 1 ↔ y ≤ 1).mp h4

[rzeta0]

Thanks Adam and Kyle - I appreciate you trying to help.

Given the course "Mechanics of Proof" is a linear course for beginners, at this early point in the book we don't know about "exact" or "mul_le_mul" so I will keep searching for a solution using only the few things we have learned.

I conclude from the comment earlier that "cancel" might have a bug as we can't find a reason it should fail here.

[rzeta0]

This seems to work (but doesn't seem to need 0<y as suggested bt the course author):

example (x y : ℚ) (h : x * y = 1) (h2 : x ≥ 1) : y ≤ 1 := by
  -- have h3 : 0 < x * y := by addarith [h]
  -- cancel x at h3 -- h3: 0 < y
  have h4 :=
  calc
    y * x = x * y := by ring
    _ = 1 := by rw [h]
    _ ≤ x := by rel [h2]
    _ = 1 * x := by ring
  cancel x at h4

I think the problem was that cancel can only right-cancel, not left-cancel....

[Adam Kurkiewicz]

I think very highly of Heather's course, and I benefited from doing parts of it myself, but I think it can be a little bit slow, and and I think it has an additional agenda besides just teaching people lean. I think this additional agenda is some kind of compliance with curriculum guidelines in an American university. Or maybe it's the fact that it needs to build up towards future maths courses. I'm not sure if I have a correct read on this, we would have to ask her.

If your objective is to learn lean as fast as possible, a good material to learn from is Kevin's Natural Number Game:

https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/

It has the added benefit of being really, really fun to play!

But I think in the current state of the educational materials for lean, your best bet is probably doing both Heather's course and playing Kevin's game. The course covers more ground.

Of course if your objective is getting a good grade in Math 2001, you might want to just keep cracking with the "Mechanics..." -- it can be a bit of a grind at times -- but it will be good for you!

Best of luck!

[Patrick Massot]

Teaching how to use Lean is clearly not the main goal of this book. Teaching mathematics is the main goal. I don't think it was ever meant to be a general introduction to Lean.

[Adam Kurkiewicz]

Sure, but if you're trying to learn lean without too much prior computer science/ mathematics background, you have limited options. "Mechanics of proof" is one of the available options, so regardless of the intended purpose, it will fulfil that role on occasion. Natural Numbers Game is the other option. Other options that I'm aware of are targeted at a more advanced reader.

[Adam Kurkiewicz]

One of the things I might do some day is essentially extend NNG to work up to the proof of infinitely many primes. I think that would fill a nice niche in the introductory material for lean.

[Patrick Massot]

I was only commenting on your "additional agenda" comment. I feel you made it sound way more mysterious than it is.

[Adam Kurkiewicz]

@Patrick Massot , this is pretty much ancient history at this point (I disappeared from the field for many years to create and exit a biotech software startup), but this thread on teaching lean to high schoolers is still very much of interest to me. I think both Mechanics of proof and Natural Number Game moved us in the right direction since then, but I think there's still work to do to make it easier for learners that are early on in their mathematical/ compsci journey.

No mystery intended with the "additional agenda" :)

[Patrick Massot]

I very much agree that trying to find something suitable for high school students is very worthwhile. The mechanics of proof is targeting the right level of mathematical sophistication here. It probably wouldn’t work for your still of workshop because it assumes more available time.

[Patrick Massot]

I also fear this book will be frustrating to rzeta0 who seems to be interested in understanding more about what Lean is doing under the hood, and asks questions going in the direction of a formal specification of the grammar etc. This is simply not what this great book is about.

[rzeta0]

Thanks everyone for helping.

I am an adult who went to university 25+ years ago but didn't study mathematics (I did physics, then a masters in computer science). That means I didn't learn about proofs and logic. I am learning those now by working through Terence Tao's Analysis I - including attempting all the exercises (https://analysis-solutions.blogspot.com - caution they might be wrong). I previously read through JD Hawkins Proof and the Art of Mathematics and J Cummings Proofs : A Long Form Textbook.

So I am self-teaching basic mathematics which most undergraduates would learn - and I thought learning Lean at a beginner-medium level would help make my mathematical thinking more robust. The aim isn't to learn a new language. If I ask about its internals or design it is because over 25 years in tech and gazillions of programming languages I have learned the importance of user-centric design.

So far I am benefiting from Heather's course because it isn't too fast for me - I am a slow learner!

I do create courses (youtube, blog, sometimes printed books) for topics I feel could benefit from more accessible and friendly content than is currently available. I did this previously and people seem to like it. I'm not sure if I'll get to that point with Lean but it is an idea. The audience would be the someone with maths to age 18 or someone with a numerate degree but not mathematics but with an interest.

My long term learning objectives are to understand number theory better - and as someone with no mathematics education beyond age 18, I have to teach myself logic, proof, and then topics like analysis and complex analysis - eventually.

I previously embarked on this journey ( https://www.youtube.com/@PrimesToRiemann/videos ) but stopped when I realised I would have to learn maths more deeply!

[Adam Kurkiewicz]

Sounds like an interesting journey @rzeta0!

I'm also interested in formalising elementary number theory. Currently I'm working on formalising solutions to IMO problems, which I'm contributing here:

https://github.com/dwrensha/compfiles

In addition to being good fun, there is a hope this will help with development of reasoning capabilities of AI models.

[Adam Kurkiewicz]

Ah one more thing @rzeta0,

If you've got a lot of experience with programming languages, you could also work with Theorem Proving in Lean 4. I worked through half of the book (until chapter 7) in ~2017/2018. It got a bit too hard for me after that. The resource covers lean more from first principles and I think is generally targeted at a more advanced reader than Mechanics of proof or Natural Number Game.

Again, best of luck!