using positivity with limited (beginner) tactics

Stream: new members

[rzeta0]

I have asked about this before and went away to think / learn more.. but I have failed.

My aim is to construct a simple educational example of a Lean proof that shows

$$c^2 = a^2 + b^2 \implies c^2 \geq a^2$$

using only some/all of the following tactics: ring, rw, rel, num_norm.

This is because the content I am creating has not introduced more advanced tactics / lemmas.

I've been following Heather Macbeth's "Mechanics of Proof" course but she creates her own tactic called extra which does the job but I am trying to follow vanilla Lean4.

The following is an outline of a broken proof, but I present it here to give a flavour of how simple. the code needs to be.

import Mathlib.Tactic

example {a b : ℤ} (h1 : a^2 + b^2 = c^2) : 0 ≤ c^2 - a^2 :=
  calc
    0 = c^2 - a^2 - b^2 := by linarith [h1]
    _ ≤ c^2 - a^2 := by positivity

It may be impossible, to do with just those tactics, no-one had confirmed that for me thus far.

You may reasonably ask "why" - my aim is to develop educational examples that are approachable for newcomers and beginners (like myself) and no scare them away with unfamiliar methods and code. I am hoping it is possible to "do easy tasks easily in code".

[Michal Wallace (tangentstorm)]

For the first step, repeatedly choosing suggestions from rw? leads me to this:

example {a b : ℤ} (h1 : a^2 + b^2 = c^2) : 0 ≤ c^2 - a^2 :=
  calc
    0 = c^2 - a^2 - b^2 := by rw [← h1]; rw [Int.sub_sub]; rw [Int.sub_eq_zero_of_eq rfl]
    _ ≤ c^2 - a^2 := sorry

[Michal Wallace (tangentstorm)]

I know neither of these are on your current list of tactics, but, the least scary proof I've found so far is this:

example {a b : ℕ} (h1 : a^2 + b^2 = c^2) : 0 ≤ c^2 - a^2 :=
  calc
    0 = c^2 - a^2 - b^2 := by omega
    _ ≤ c^2 - a^2 := by simp[sq_nonneg]

I first tried omega for both lines, but on the second line, it complains:

omega could not prove the goal:
a possible counterexample may satisfy the constraints
  d ≤ -1
where
 d := b ^ 2

So I tried to give it the information it needs:

example {a b : ℤ} (h1 : a^2 + b^2 = c^2) : 0 ≤ c^2 - a^2 :=
  calc
    0 = c^2 - a^2 - b^2 := by omega
    _ ≤ c^2 - a^2 := by
      have : 0 ≤ b^2 := by exact?
      omega

... and this told me about sq_nonneg.

[Michal Wallace (tangentstorm)]

Using exact? and omega for search, I found this proof of your exact LaTeX statement:

example {a b : ℤ} (h1 : c^2 = a^2 + b^2) : c^2 ≥ a^2 := by
  calc c^2
    _ = a^2 + b^2  := h1
    _ ≥ a^2        := by
      have : 0 ≤ b^2 := sq_nonneg b
      exact Int.le_add_of_nonneg_right this

or just:

example {a b : ℤ} (h1 : c^2 = a^2 + b^2) : c^2 ≥ a^2 := by
  calc c^2
    _ = a^2 + b^2  := h1
    _ ≥ a^2        := Int.le_add_of_nonneg_right (sq_nonneg b)

[rzeta0]

Thanks @Michal Wallace (tangentstorm) I really appreciate your efforts on this.

I think, given several people have tried to provide un-scary proofs, but none have managed to only use the small list of beginner tactics, then this may be an impossible task - and may be what drove Heather Macbeth to write a custom tactic for her course.

( i will find out in future what omega does, as well as simp and exact and the question marks too ... )

[Yaël Dillies]

Didn't I already provide you with a proof that only used your small list of beginner tactics?

[Yaël Dillies]

I mean, not with rel but gcongr instead

[rzeta0]

I'm going through my messages history and can't seem to find it? my apologies if you have and I missed it

[Yaël Dillies]

I mean this

[rzeta0]

I had missed that. I will print it out and study it. Thank you.