## Stream: new members

### Topic: Anonymous "have"

#### Syx Pek (May 22 2020 at 16:05):

Lets say I want to prove something but I need to show 0 < 1, one way is to use the syntax have h : 0 < 1, by norm_num, I was wondering if I can avoid introducing a name for it.

#### Jalex Stark (May 22 2020 at 16:08):

did you try have : 0 < 1 := by norm_num or show 0 < 1, norm_num
(also : post code, post code, post code. you'll get more interesting responses, including answers to questions you didn't think to ask, if you post code)

#### Alex J. Best (May 22 2020 at 16:09):

It depends on the context but you can put by norm_num inline , i.e rw add_lt_left (by norm_num : 0 < 1)

#### Alex J. Best (May 22 2020 at 16:10):

or even

lemma silly (h : 0 < 1) : 1 = 1 := by refl

example : 1 = 1 :=
begin
exact silly (by norm_num)
end


#### Syx Pek (May 22 2020 at 16:13):

Well basically I am stuck here:

example : abs (a*b) ≤ (a^2 + b^2) / 2 :=
begin
have h₁ : 0 ≤ a^2 - 2*a*b + b^2,
calc a^2 - 2*a*b + b^2
= (a - b)^2 : by ring
... ≥ 0         : by apply pow_two_nonneg,
have h₂ : 0 ≤ a^2 + 2*a*b + b^2,
calc a^2 + 2*a*b + b^2
= (a + b)^2 : by ring
... ≥ 0         : by apply pow_two_nonneg,
have h₃ : (0 : ℝ) ≤ 2, by norm_num,
apply abs_le_of_le_of_neg_le,
end


I thought h₃ was unweildy to "initialize" and was hoping to "inline it" but to be honest, I don't know how to proceed from here.

#### Bryan Gin-ge Chen (May 22 2020 at 16:13):

There's also using "French" quotes (though I seem to recall this name not being accurate), see https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html#more-on-the-proof-language

#### Bryan Gin-ge Chen (May 22 2020 at 16:13):

What are the types of a and b?

#mwe

#### Syx Pek (May 22 2020 at 16:15):

Oh I don't noticed variables a b : ℝ , they are real.

#### Jalex Stark (May 22 2020 at 16:18):

okay, so now you know why your post doesn't work. Edit your post to make it work. Did you follow the #mwe link to see what we're asking for?

#### Syx Pek (May 22 2020 at 16:22):

My question was not this. It was on

example : abs (a*b) ≤ (a^2 + b^2) / 2 :=
begin
have h₁ : 0 ≤ a^2 - 2*a*b + b^2,
calc a^2 - 2*a*b + b^2
= (a - b)^2 : by ring
... ≥ 0         : by apply pow_two_nonneg,
have h₂ : 0 ≤ a^2 + 2*a*b + b^2,
calc a^2 + 2*a*b + b^2
= (a + b)^2 : by ring
... ≥ 0         : by apply pow_two_nonneg,
have h₃ : (0 : ℝ) < 1, by norm_num,
have h₄ : (0 : ℝ) < 2, by norm_num,
apply abs_le_of_le_of_neg_le,
rw ←div_one (a*b),
rw div_le_div_iff h₃ h₄,
sorry
end


Can I not give names to h₃ h₄, for that line to work.

#### Kevin Buzzard (May 22 2020 at 16:24):

Can you post fully working code that I can just cut and paste? It would make it much easier to help.

#### Syx Pek (May 22 2020 at 16:25):

Give me 5 minutes and Ill bash out the rest.

#### Kevin Buzzard (May 22 2020 at 16:26):

Instead of defining h_3 can't you just replace the unique place it occurs with (by norm_num)? Is that the answer to your question?

#### Alex J. Best (May 22 2020 at 16:30):

Syx Pek said:

Give me 5 minutes and Ill bash out the rest.

by fully working we just mean define all variables, not that it can't have a sorry at the end.

and all imports.

#### Bryan Gin-ge Chen (May 22 2020 at 16:33):

This is what Alex and Kevin suggested. I couldn't get it to work without the type ascriptions:

import data.real.basic

variables (a b : ℝ)

example : abs (a*b) ≤ (a^2 + b^2) / 2 :=
begin
have h₁ : 0 ≤ a^2 - 2*a*b + b^2,
calc a^2 - 2*a*b + b^2
= (a - b)^2 : by ring
... ≥ 0         : by apply pow_two_nonneg,
have h₂ : 0 ≤ a^2 + 2*a*b + b^2,
calc a^2 + 2*a*b + b^2
= (a + b)^2 : by ring
... ≥ 0         : by apply pow_two_nonneg,
-- have h₃ : (0 : ℝ) < 1, by norm_num,
-- have h₄ : (0 : ℝ) < 2, by norm_num,
apply abs_le_of_le_of_neg_le,
rw ←div_one (a*b),
rw div_le_div_iff (by norm_num : (0 : ℝ) < 1) (by norm_num : (0 : ℝ) < 2),
sorry
end


#### Alex J. Best (May 22 2020 at 16:35):

You can also just let the rewrite spawn new goals for what it needs and then fill them later.

example (a b : ℝ): abs (a*b) ≤ (a^2 + b^2) / 2 :=
begin
have h₁ : 0 ≤ a^2 - 2*a*b + b^2,
calc a^2 - 2*a*b + b^2
= (a - b)^2 : by ring
... ≥ 0         : by apply pow_two_nonneg,
have h₂ : 0 ≤ a^2 + 2*a*b + b^2,
calc a^2 + 2*a*b + b^2
= (a + b)^2 : by ring
... ≥ 0         : by apply pow_two_nonneg,
apply abs_le_of_le_of_neg_le,
rw ←div_one (a*b),
rw div_le_div_iff,
sorry,
norm_num, norm_num,
end


#### Syx Pek (May 22 2020 at 16:44):

Alright, I filled out the sorry, I apologize for the bad example:

variables a b : ℝ

-- BEGIN
example : abs (a*b) ≤ (a^2 + b^2) / 2 :=
begin
have h₁ : 0 ≤ a^2 - 2*a*b + b^2,
calc a^2 - 2*a*b + b^2
= (a - b)^2 : by ring
... ≥ 0         : by apply pow_two_nonneg,
have h₂ : 0 ≤ a^2 + 2*a*b + b^2,
calc a^2 + 2*a*b + b^2
= (a + b)^2 : by ring
... ≥ 0         : by apply pow_two_nonneg,
have h₃ : (0 : ℝ) < 1, by norm_num,
have h₄ : (0 : ℝ) < 2, by norm_num,
apply abs_le_of_le_of_neg_le,
rw [←div_one (a*b), div_le_div_iff h₃ h₄],
calc a*b*2
≤ 0 + a*b*2                    : by exact le_of_eq (eq.symm (zero_add _))
...≤ a^2 - 2*a*b + b^2 + a*b*2    : by exact add_le_add h₁ (le_refl (a*b*2))
...= (a^2 + b^2) *1               : by ring,

rw [← div_one (-(a*b)), div_le_div_iff h₃ h₄],
calc -(a*b)*2
≤ 0 + -(a*b)*2                 : by exact le_of_eq (eq.symm (zero_add _))
...≤ a^2 + 2*a*b + b^2 + -(a*b)*2 : by exact add_le_add h₂ (le_refl (-(a*b)*2))
...= (a^2 + b^2) *1               : by ring,
end


I am actually curious how to avoid defining  h₃ h₄ and this was adequately answered above. Thanks!

#### Bryan Gin-ge Chen (May 22 2020 at 16:52):

Note that the last thing you posted still doesn't qualify as a MWE because you didn't include import data.real.basic at the top.

#### Bryan Gin-ge Chen (May 22 2020 at 16:53):

In particular, you should test this by making a new Lean file, pasting your code snippet into it, and seeing if you get the expected behavior. This is exactly what people who try to help you will do!

#### Jalex Stark (May 22 2020 at 16:55):

we did not ask you to fill in the sorry, we only asked you to make a #mwe. When you read the content after following the #mwe link, did it leave you with the impression that sorrys are disallowed?

#### Patrick Massot (May 22 2020 at 16:56):

That page should contain the word sorry

#### Jalex Stark (May 22 2020 at 16:59):

#mwe now has a sentence explaining that sorries are fine

#### Syx Pek (May 22 2020 at 17:01):

Ah, when I read it I interpreted "correct imports" as _not the wrong ones" rather than a complete list of the imports one have to make.
Also, in my head, I've been playing around with the problem for quite a bit, and just implicitly assumed all my variables are real, so I didn't realise it was a significant part of the program.

#### Jalex Stark (May 22 2020 at 17:03):

hmm i don't know what you mean by "not the wrong ones" but anyway, you can always check whether your code is a MWE by pasting it into a blank file and seeing if you get what you expect

#### Patrick Massot (May 22 2020 at 17:04):

Oh, but this is the wrong page. This should now be a link to https://leanprover-community.github.io/mwe.html, and you haven't updated the right file.

#### Jalex Stark (May 22 2020 at 17:04):

that way you can have the computer tell you what's important instead of trying to figure it out yourself :)

#### Bryan Gin-ge Chen (May 22 2020 at 17:05):

So we need to copy the wiki page to the community website and @Mario Carneiro needs to update the #mwe linkifier so it points there as well.

#### Jalex Stark (May 22 2020 at 17:06):

I just did the copying (well I guess it's sitting as a PR waiting to be merged), and now
https://github.com/leanprover-community/mathlib/wiki/Minimum-Working-Example-(MWE)
is blank except for a link to the real page

#### Patrick Massot (May 22 2020 at 17:07):

I don't see any PR at https://github.com/leanprover-community/leanprover-community.github.io/pulls

#### Jalex Stark (May 22 2020 at 17:08):

(the first time I only made a branch and forgot to press the "make a PR" button)

#### Jalex Stark (May 22 2020 at 17:09):

https://github.com/leanprover-community/leanprover-community.github.io/pull/25/files

merged

#### Jalex Stark (May 22 2020 at 17:11):

@Syx Pek , do you still have a question that we haven't answered?

#### Bryan Gin-ge Chen (May 22 2020 at 17:15):

sadly, github is experiencing errors again so the page didn't build: https://www.githubstatus.com/

#### Syx Pek (May 22 2020 at 17:18):

No. Thanks for the reply! It is pretty frustrating when you want to prove stuff "obviously true" but it is quite enjoyable.