Inequalities in "calc"

Stream: new members

[Dan Grigsby]

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]

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

[Dan Grigsby]

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]

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]

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]

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]

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]

I guess this is implemented in core though?

[Dan Grigsby]

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

Noted!

[Patrick Massot]

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

[Dan Grigsby]

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]

Dan Grigsby has marked this topic as resolved.

[Yaël Dillies]

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]

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]

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]

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

[Notification Bot]

Yaël Dillies has marked this topic as unresolved.