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 calc
s, but now that I've spelled out my expectation above, it seems reasonable to replace transitivity
by one-line calc
s 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