Zulip Chat Archive

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?

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

#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.

Kevin Buzzard (May 22 2020 at 16:31):

and all imports.

Patrick Massot (May 22 2020 at 16:31):

Like: read the #mwe link that was posted several times...

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!

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

Sorry if we seem somewhat prickly about this.

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