Zulip Chat Archive

Stream: new members

Topic: proving pi >= 0


view this post on Zulip Mii Nguyen (Feb 27 2019 at 09:57):

I'm trying to prove 0 ≤ r^2 * pi. Here is my work

lemma pi_r_sq_pos (r : ) (H: 0  r): 0  r^2 * pi :=
have r^2  0, from pow_nonneg H 2,
have pi >  0, from pi_pos,
begin
    apply mul_nonneg,
end

I have to prove that pi ≥ 0 instead of pi > 0, but I still stuck in it.
Would someone help me with this? Thank you.

view this post on Zulip Patrick Massot (Feb 27 2019 at 09:59):

apply mul_nonneg ; linarith

view this post on Zulip Mii Nguyen (Feb 27 2019 at 10:00):

what is the role of linarith in this case? @Patrick Massot

view this post on Zulip Patrick Massot (Feb 27 2019 at 10:01):

The role of linarith is to blast away stupid equality and inequality problems

view this post on Zulip Patrick Massot (Feb 27 2019 at 10:01):

But you can also be explicit of course:

lemma pi_r_sq_pos (r : ) (H: 0  r): 0  r^2 * pi :=
have r^2  0, from pow_nonneg H 2,
have pi >  0, from pi_pos,
mul_nonneg r^2  0 (le_of_lt 0 < pi)

view this post on Zulip Patrick Massot (Feb 27 2019 at 10:02):

But in this case, the mathlib style is to be concise (because the result is trivial and wouldn't be even stated on paper):

lemma pi_r_sq_pos (r : ) (H: 0  r): 0  r^2 * pi :=
mul_nonneg (pow_nonneg H 2) (le_of_lt pi_pos)

view this post on Zulip Mii Nguyen (Feb 27 2019 at 10:17):

Would you explain the different of ‹ › and ( )? The first is for , say, exact argument and the second is for function? @Patrick Massot

view this post on Zulip Mii Nguyen (Feb 27 2019 at 10:18):

I can find the informations of it in which chapter of the book?

view this post on Zulip Patrick Massot (Feb 27 2019 at 10:18):

https://leanprover.github.io/logic_and_proof/propositional_logic_in_lean.html#additional-syntax

view this post on Zulip Mii Nguyen (Feb 27 2019 at 10:19):

Thank you @Patrick Massot

view this post on Zulip Patrick Massot (Feb 27 2019 at 10:19):

or https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html#more-on-the-proof-language

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 14:11):

le_of_lt is a proof that if a < b then a <= b; this is the answer to your original question, and it's in Patrick's code.

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 14:12):

You can guess it because you want to prove _ <= _ which is called le, and it's the conclusion, so le_of, and then you write le_of and hit things like ctrl-space until VS Code tells you the things it knows which have "le_of" in, and then you find it.


Last updated: May 10 2021 at 00:31 UTC