request - simple example with positivity

Stream: new members

[rzeta0]

The following task requires the notion of a squared number being always positive (naturals, integers, reals).

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

Yesterday I ran into a wall trying to use the positivity tactic to show this: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/example.20of.20.60positivity.60.20tactic

The online (lean 3) docs have examples that are much smaller than what I want to show above: https://leanprover-community.github.io/mathlib_docs/tactics.html#positivity

Overnight I had a think and concluded that it just wasn't possible within the calc proof structure that I have learned about thus far and want to explore further. Am I wrong about this?

My request is for a simple calc proof example that proves the above task, or something similar to it.

The aim is to create an educational example that I can write up on my blog - which I do to help me learn better. ( https://leanfirststeps.blogspot.com/p/contents.html )

Note: You may be asking why I want to stick to the calc structure. It is because I want to develop a good diverse set of examples within calc before moving onto other structures eg have.

[rzeta0]

PS - the tactic doens't have to be positivity - they key point I want to use is that $a^2 \geq 0$

[Riccardo Brasca]

Did you write ≥ instead of ≤?

[rzeta0]

Riccardo Brasca said:

Did you write ≥ instead of ≤?

my error, i've edited the original post

[Yaël Dillies]

Something like

import Mathlib

example {a b c : Real} (h : c ^ 2 = a ^ 2 + b ^ 2) : a ^ 2 \le c ^ 2 :=
  calc
    a ^ 2 = a ^ 2 + 0 := by ring
    _ \le a ^ 2 + b ^ 2 := by gcongr; positivity
    _ = c ^ 2 := by rw [h]

maybe?

[Yaël Dillies]

(untested, written on a phone)

[Riccardo Brasca]

Something like the following?

import Mathlib

example (a b c : ℝ) (h : c ^ 2 = a ^ 2 + b ^ 2) : c ^ 2 ≥ a ^ 2 :=
  calc c ^ 2 = a ^ 2 + b ^ 2 := by rw [h]
  _ ≥ a ^2 := by simp [sq_nonneg]

[Edward van de Meent]

import Mathlib
example {a b c: ℝ} (h:c ^ 2 = a ^ 2 + b ^ 2): a ^ 2 ≤ c ^ 2 := calc
    a ^ 2
      = a ^ 2 + 0 := (add_zero (a ^ 2)).symm
    _ ≤ a ^ 2 + b ^ 2 := add_le_add (le_refl (a ^ 2)) (sq_nonneg b)
    _ = c ^ 2 := h.symm

[rzeta0]

Thanks Yaël, Riccardo and Edward for the examples.

As a beginner, I don't know about simp [sq_nonneg] or add_le_add etc yet .. I only know ring, rw, rel, and norm_num .. and was hoping positivity was the only extra I needed. I think gcongr is related to rel so I'll see if I can make that work.

[rzeta0]

Having struggled with this for 2 days I've come to the conclusion that I can't create a proof using only: rel, rw, ring and norm_num, and positivity.