example of `positivity` tactic

Stream: new members

[rzeta0]

I can't seem to find an educational example of the positivity tactic online aside from these: https://leanprover-community.github.io/mathlib_docs/tactics.html

Here is a simple example I'm trying to construct:

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 -- error here

the error is

not a positivity goal

From the docs, goals of the form 0 ≤ x are valid.

help?!

[Ruben Van de Velde]

Well, it's not

[Ruben Van de Velde]

You're asking positivity to prove c^2 - a^2 - b^2 ≤ c^2 - a^2, which isn't in its scope

[Ruben Van de Velde]

My first thought was gcongr, but that goes off the rails, possibly because of the natural number subtraction (which is not well behaved). Maybe it could be made to work with some help, but it turns out omega handles it

[rzeta0]

Ruben Van de Velde said:

You're asking positivity to prove c^2 - a^2 - b^2 ≤ c^2 - a^2, which isn't in its scope

I'm a beginner so apologies for the errors. Isn't 0 ≤ c^2 - a^2 of the correct form 0 ≤ x ?

[Daniel Weber]

It is, and positivity works to prove it directly:

import Mathlib.Tactic

example {a c : ℕ} : 0 ≤ c^2 - a^2 := by
  positivity

However, that's probably not what you want - it sees that c^2 - a^2 is a natural number, and any natural number is nonnegative

[Daniel Weber]

It can't prove

import Mathlib.Tactic

example {a b c : ℤ} (h : c^2 = a^2 + b^2) : 0 ≤ c^2 - a^2 := by
  positivity

which is probably closer to what you want, but that's because it just doesn't manage to

[Ruben Van de Velde]

You may be misunderstanding how calc works - each line is a specific substep, and the proof at the end of the line applies to that substep, and the underscore at the start of the line stands in for the right hand side of the previous line

[Ruben Van de Velde]

So in your second step, you're asked to prove the goal I mentioned before, which doesn't have a zero anymore

[rzeta0]

Daniel Weber said:

It is, and positivity works to prove it directly:

import Mathlib.Tactic

example {a c : ℕ} : 0 ≤ c^2 - a^2 := by
  positivity

However, that's probably not what you want - it sees that c^2 - a^2 is a natural number, and any natural number is nonnegative

You're right it should be ℤ not ℕ - ive edited the question to reflect this.

[rzeta0]

Daniel Weber said:

which is probably closer to what you want, but that's because it just doesn't manage to

I want to check I understand. Are you saying the theorem is correct but the tactic as it is currently doesn't manage to prove it, and this is merely a function of the state of its development.

[rzeta0]

@Ruben Van de Velde - you are correct, I didn't fully understand calc so I will go away and think about how to make this work.

I'm keen on producing a simple educational example of positivity and if I can fit it into the framework of calc that would be great.