Zulip Chat Archive

Stream: new members

Topic: Inequalities in "calc"


Dan Grigsby (Jan 05 2024 at 20:38):

I'm working through "The Mechanics of Proof" by @Heather Macbeth'.

I have a question related to working with inequalities inside a "calc" proof. Here's an example from the book that I completed:

example {r s : } (h1 : s + 3  r) (h2 : s + r  3) : r  3 := by
  have h3 : r  3 + s :=
  calc
    r = r := by ring
    r  3 + s := by addarith[h1]
  have h4 : r  3 - s :=
  calc
    r = r := by ring
    r  3 - s := by addarith [h2]
  calc
    r = (r + r) / 2 := by ring
    _  (3 - s + (3 + s)) / 2 := by rel [h4, h3]
    _ = 3 := by ring

The first line in the last calc block makes sense to me. We are writing r in a form that can be then manipulated with rel in the next line. For the first two, I wrote what seems to be a correct proof by just saying r = r, but that feels wrong. Is there another way, perhaps something that is idiomatic?

Kevin Buzzard (Jan 05 2024 at 20:51):

Assuming that code compiles, and you want h3, why don't you just do have h3 : r <= 3 + s := by addarith[h1]?

Dan Grigsby (Jan 05 2024 at 20:58):

That works and is certainly simpler and better.

I think that generalizes - that anything that can be resolved with one tactic would work like that, and anything that requires more than one tactic would have an r = <something equal to r, but not directly/just r>.

^^^Does that sound right? Thanks for the help!

Heather Macbeth (Jan 05 2024 at 21:27):

Yup, calc blocks let you chain together two steps proved by different tactics ... if a statement can be proved in one step, you can generally just write the tactic without the scaffolding of a calc block.

Heather Macbeth (Jan 05 2024 at 21:29):

This seems to be a common place where beginners need to take a mental leap, e.g.
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Mechanics.20of.20Proof.20Ex

Patrick Massot (Jan 05 2024 at 21:34):

Yes, I have also seen this with my students. I was surprised but it simply seems to be a fact: people are tempted to write one line long calc. It would be nice to have at least a better error message.

Jireh Loreaux (Jan 05 2024 at 21:38):

It's a shame that calc actually errors with a single line and instead doesn't just provide an info with a Try this:

Jireh Loreaux (Jan 05 2024 at 21:39):

I guess this is implemented in core though?

Dan Grigsby (Jan 05 2024 at 21:48):

@Heather Macbeth you asked for typos and input. Looks like this is a common point of confusion. Adding a sentence somewhere in Ch1 (or 2?) would probably save headaches.

Heather Macbeth (Jan 05 2024 at 21:48):

Noted!

Patrick Massot (Jan 05 2024 at 21:50):

Jireh, it is implemented in core but overridden in Mathlib as soon as you import the calc widget.

Dan Grigsby (Jan 05 2024 at 22:00):

For calibration: I have recent freshman level linear algebra, calc and statistics experience. I'm 50, which makes me older than your target. I've written code for a long time, and have had the most success learning new math when I can come at it with either software tools (e.g.., learning calc and using sympy to check my work) or where there are computer-science adjacent things (e.g., familiarity doing matrix multiplications with numpy made linear algebra less intimidating.

Great community here. Really grateful for the help.

Notification Bot (Jan 05 2024 at 22:02):

Dan Grigsby has marked this topic as resolved.

Yaël Dillies (Jan 06 2024 at 07:15):

I actually have an urge of writing one-line calc blocks, and the reason for this is that I would expect

calc
  _ rel a := ?_

to be the same as

transitivity a

Yaël Dillies (Jan 06 2024 at 07:15):

It's a bit annoying right now because I need to add a dummy second line just to see what the new goals are.

Yaël Dillies (Jan 06 2024 at 07:15):

I was not planning on my finished code containing one-line calcs, but now that I've spelled out my expectation above, it seems reasonable to replace transitivity by one-line calcs completely. One less tactic to learn is always good.

Yaël Dillies (Jan 06 2024 at 09:14):

Sorry, this all got mixed up due to bad connection. The last message is supposed to be the first EDIT: Now reordered

Notification Bot (Jan 06 2024 at 09:14):

Yaël Dillies has marked this topic as unresolved.


Last updated: May 02 2025 at 03:31 UTC