Example 1.4.6 of The Mechanics of Proof

Stream: general

[Hanson Char]

I've been working through Example 1.4.6 of The Mechanics of Proof,

import Mathlib.Data.Real.Basic
import Library.Basic

math2001_init

example {n : ℤ} (hn : n ≥ 5) : n ^ 2 > 2 * n + 11 :=
  calc
    n ^ 2 = n * n := by ring
    _ ≥ 5 * n := by rel [hn]
    _ = 2 * n + 3 * n := by ring
    _ ≥ 2 * n + 3 * 5 := by rel [hn]
    _ > 2 * n + 11 := by numbers  ; <= this failed

But I got the following error:

Numbers tactic failed. Maybe the goal is not in scope for the tactic (i.e. the goal is not a pure numeric statement), or maybe the goal is false?

Am I misunderstanding how numbers works here? (Here is the git repository).

[Hanson Char]

Oh never mind, I figured it out. Use norm_num instead of numbers and it checks out, even though the book hasn't yet mentioned norm_num up to that point.

Oops, turns out I need to read the next example:

In fact, while writing up the correct solution, you probably had difficulty justifying the last step. Come back to that step after you have studied the next example.

[Notification Bot]

Hanson Char has marked this topic as resolved.

[Notification Bot]

Hanson Char has marked this topic as unresolved.

[Notification Bot]

Hanson Char has marked this topic as resolved.

[Kyle Miller]

Can I ask what's your motivation for using numbers here? The error message suggests that numbers is only for purely numeric statements:

Hanson Char said:

Maybe the goal is not in scope for the tactic (i.e. the goal is not a pure numeric statement)

The goal you are trying to prove here is 2 * n + 3 * 5 > 2 * n + 11, which is not a purely numeric statement (note the n).

Hanson Char said:

Oh never mind, I figured it out. Use norm_num instead of numbers and it checks out even though the book hasn't yet mentioned norm_num up to that point.

Yes, using a more powerful tactic can do that, however: the book never uses norm_num. The only real mention of it is in the very last chapter, Transitioning to mainstream Lean. You shouldn't consider norm_num to be a solution here.

[Kyle Miller]

Oh, I just saw that you edited your last message and you noticed the hint to look at the next exercise.

[Hanson Char]

Right, thanks. I've been wondering. I'll retry with the extra introduced in the next example.

[Notification Bot]

Hanson Char has marked this topic as unresolved.

[Hanson Char]

I've resolved this example using extra. However, in an earlier attempt I tried the following and thought it would be a valid step:

example {n : ℤ} (hn : n ≥ 5) : n ^ 2 > 2 * n + 11 :=
  calc
    n ^ 2  > n ^ 2 - 4 := by extra  -- <= fails

Yet this resulted in an error:

out of scope: extra proves relations between a LHS and a RHS differing by some neutral quantity for the relation

I wonder why.

[Kenny Lau]

@Hanson Char probably because they aren't "differing by some neutral quantity", try making the LHS n^2-0 first

[Kenny Lau]

to a mathematician n^2 and n^2-0 are obviously the same, but not to a computer

[Hanson Char]

Aha! Yup, that works. Thanks.

[Notification Bot]

Hanson Char has marked this topic as resolved.

[Hanson Char]

I’ve been experimenting with the extra tactic and found this works as expected:

example (p: ℝ) (hp: p ≥ 0) : 2 * p ≥ p := by
calc
  2 * p = p + p := by ring
  _ ≥ p := by extra

However, this similar-looking example fails:

example (q: ℝ) (hq: q ≤ 0) : 2 * q ≤ q := by
calc
  2 * q = q + q := by ring
  _ ≤ q := by extra

Is it correct that extra only works when the term being “removed” is known to be non-negative? The documentation doesn’t seem to clarify this case.

[Notification Bot]

Hanson Char has marked this topic as unresolved.

[Hanson Char]

I’ve been further experimenting with the extra tactic and found that it works as expected in this case:

example (p: ℝ) (hp: p ≥ 0) : 2 * p ≥ p := by
calc
  2 * p = p + p := by ring
  _ ≥ p := by extra

But this similar-looking example doesn’t work:

example (q: ℝ) (hq: q ≤ 0) : 2 * q ≤ q := by
calc
  2 * q = q + q := by ring
  _ ≤ q := by extra

Is it correct that extra only works when the term being “removed” is known to be non-negative? The documentation doesn’t seem to clarify this case.

[Aaron Liu]

I have no idea.

[Notification Bot]

Aaron Liu has marked this topic as unresolved.

[Hanson Char]

On more thoughts, for these two cases there is no need to use extra, since rel suffices.

example (p: ℝ) (hp: p ≥ 0) : 2 * p ≥ p := by
calc
  2 * p = p + p := by ring
  _ ≥ p + 0 := by rel [hp]
  _ = p := by ring

example (q: ℝ) (hq: q ≤ 0) : 2 * q ≤ q := by
calc
  2 * q = q + q := by ring
  _ ≤ q + 0 := by rel [hq]
  _ = q := by ring

However, extra comes in handy when there is square involved, e.g.

example (n: ℝ) : 0 ≤ n ^ 2 := by extra