Zulip Chat Archive

Stream: new members

Topic: Anonymous "have"


view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (May 22 2020 at 16:13):

What are the types of a and b?

view this post on Zulip Bryan Gin-ge Chen (May 22 2020 at 16:13):

#mwe

view this post on Zulip Syx Pek (May 22 2020 at 16:15):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Syx Pek (May 22 2020 at 16:25):

Give me 5 minutes and Ill bash out the rest.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 22 2020 at 16:31):

and all imports.

view this post on Zulip Patrick Massot (May 22 2020 at 16:31):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Bryan Gin-ge Chen (May 22 2020 at 16:54):

Sorry if we seem somewhat prickly about this.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 22 2020 at 16:56):

That page should contain the word sorry

view this post on Zulip Jalex Stark (May 22 2020 at 16:59):

#mwe now has a sentence explaining that sorries are fine

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Jalex Stark (May 22 2020 at 17:09):

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

view this post on Zulip Patrick Massot (May 22 2020 at 17:10):

merged

view this post on Zulip Jalex Stark (May 22 2020 at 17:11):

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

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 22 2020 at 19:41):

Testing new linkifier: #mwe

view this post on Zulip Jalex Stark (May 22 2020 at 19:41):

yay! too bad github hasn't built the latest merge yet though

view this post on Zulip Patrick Massot (May 22 2020 at 19:43):

It's sad we can't deploy by hand


Last updated: May 07 2021 at 00:30 UTC