Zulip Chat Archive

Stream: new members

Topic: Inequality World


view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:00):

Here is the theorem I have to prove:
theorem le_trans (a b c : mynat) (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c :=

Here is what I wrote so far:
rw le_iff_exists_add,

This gives me this output:
a b c : mynat,
hab : a ≤ b,
hbc : b ≤ c
⊢ ∃ (c_1 : mynat), c = a + c_1

I know that hab implies there exists c2 such that b = a +c2 and that hbc implies there exists c3 such that c = b + c3. That means I should use a statement like:
use c2+c3.

But how do I "summon" these c2 and c3? I do not know how to implement this lean. Please help.

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:01):

cases hab with u hu,

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:01):

will extract the u from hab

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:01):

and the proof that it does the right thing is hu

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:01):

Maybe you have to do rw le_iff_exists_add at hab first, but probably it doesn't matter

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:01):

And after that I use something like cases hbc with v hv?

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:01):

right

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:02):

and then you've got what you need

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:02):

Thanks

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:02):

np

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:13):

Another question. This what I did so far:

rw le_iff_exists_add at hab,
rw le_iff_exists_add at hbc,

cases hab with u hu,
cases hbc with v hv,
rw le_iff_exists_add,
use u+v,

Here is my output:
a b c u : mynat,
hu : b = a + u,
v : mynat,
hv : c = b + v
⊢ c = a + (u + v)

Now I want to use add_assoc to get c = (a+u)+v but I am getting an error. Why? and how to I fix it?

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:17):

rw add_assoc doesn't work? How about rw \l add_assoc? I always forget which way it goes :-)

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:19):

Still did not work. Here is the error message:

rewrite tactic failed, did not find instance of the pattern in the target expression
?m_1 + ?m_2 + ?m_3
state:
a b c u : mynat,
hu : b = a + u,
v : mynat,
hv : c = b + v
⊢ c = a + (u + v)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:20):

Yes, that error looks good

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:20):

that error says "I can't see (X + Y) + Z in the goal"

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:20):

what tactic caused that error?

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:20):

rw add_assoc

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:21):

Doesn't equality work in both directions?

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:21):

so if h is a proof that A = B then rw h looks for A's and changes them to B's

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:21):

So what do I do here?

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:21):

and you have B's which you want to change to A's so you need rw \l add_assoc

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:22):

rw ← add_assoc

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:22):

Is your background in maths or CS?

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:23):

Math

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:23):

well here's some news for you -- mathematicians can't tell the difference between A = B and B = A, but apparently computer scientists can!

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:24):

All of those lemmas like zero_add were always of the form (complicated thing) = (simpler thing)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:24):

and it turns out that's not a fluke, that's by design

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:24):

and rw turns LHS into RHS

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:25):

so it really matters which is which. In the earlier levels of the game, the job is to make stuff simpler, so you just keep rwing and you're going the right way. When it gets trickier you have to be more aware of what's actually going on

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:26):

So now the error is gone, but I cannot seem to use rw hu to replace a+u with b? why is that?

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:26):

exactly the same reason?

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:27):

Wait do I use rw ← hu,?

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:27):

give it a try :-)

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:27):

Oh I see it works

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:28):

rw turns LHS into RHS. Mathematicians just say "now use hu" but Lean is more fussy than that.

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:28):

It works:
rw le_iff_exists_add at hab,
rw le_iff_exists_add at hbc,

cases hab with u hu,
cases hbc with v hv,
rw le_iff_exists_add,
use u+v,
rw ← add_assoc,
rw ← hu,
rw ← hv,
refl,

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:28):

Thanks.

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:29):

I've just heard that I'm not going to work on Monday so I'm in a pretty good mood :-)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:29):

indeed I'm not going to work for quite some time :-)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:29):

I don't know what I'm talking about really, I love my job

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:37):

So now I am onto the next level where I am trying to prove anti-symmetry. Here is the theorem and the things I wrote so far:
theorem le_antisymm (a b : mynat) (hab : a ≤ b) (hba : b ≤ a) : a = b :=

rw le_iff_exists_add at hab,
rw le_iff_exists_add at hba,

cases hab with u hu,
cases hba with v hv,

rw hv,

Here is the output:
a b u : mynat,
hu : b = a + u,
v : mynat,
hv : a = b + v
⊢ b + v = b.

The hint says to use this theorem: eq_zero_of_add_right_eq_self (a b : mynat) : a + b = a → b = 0.

But when I use rw eq_zero_of_add_right_eq_self , I get an error again. Why?

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:37):

because you can't rewrite with this one, this is an implication

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:38):

rw h works when h is a proof of A = B. Then it changes all A's to B's. I suspect you want to do something else here.

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:38):

So.....?

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:38):

what should I do

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:38):

this is quite a tricky level and I don't really want to give away its secrets yet :-)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:39):

you can rw h1 at h2 if you like: if h1 : A = B then rw h1 at h2 will change all the A's in h2 to B`'s

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:54):

Slightly off topic: I am also getting an error when I do import data.nat.prime . Why is that?

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:56):

If you're playing in the web version of the game then you can't import anything

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:58):

Imports can only go at the beginning of a file and you don't have access to the beginning of the file. All you can do is use tactics. If you install lean and the mathlib tools and VS code onto your own computer then you will have much more flexibility to do imports

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 23:58):

Im not on the web version now. I am using Visual Studio Code. Trying to see if I can code off the web.

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:59):

Note however that the natural number game makes its own naturals, called mynat, and data.nat.prime is lots of primey facts about lean's actual natural numbers

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 00:00):

I trying to put this in Lean:

import data.nat.prime

open nat

example (n : ℕ) (hn : n > 1) (hp : ∀ p : ℕ, prime p ∧ p ∣ n → p > sqrt n) : prime n :=
begin
sorry
end

I am the same person from Prime Theorem Help. Just working bit by bit to prove this over Spring break.

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 00:01):

I feel like I did not download something.

view this post on Zulip Bryan Gin-ge Chen (Mar 14 2020 at 00:02):

What error are you seeing, exactly?

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 00:03):

file 'data\nat\prime' not found in LEAN_PATH

view this post on Zulip Bryan Gin-ge Chen (Mar 14 2020 at 00:03):

How are you creating the file in VS Code? Did you follow the instructions here?

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 00:05):

I followed an youtube video and downloaded MATLIB and all.

view this post on Zulip Bryan Gin-ge Chen (Mar 14 2020 at 00:07):

Note is that Lean files can't be opened / created on their own. They live in "projects" and you have to open the project directory in VS Code to get the imports to work properly. Try the instructions I linked above and see if you have any more luck.

view this post on Zulip Bryan Gin-ge Chen (Mar 14 2020 at 00:08):

If you followed a youtube video, it most likely doesn't have info about the latest version of the "mathlib tools". From your error message, I'm guessing you're using Windows, so you may need to go over these instructions first to get leanproject.

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 00:19):

Quick question: I am trying to mimic the proofs in Inequality world but this time for greater than in VS code. So in the Natural Number Game we have the theorem statement:
le_iff_exists_add (a b : mynat)
a ≤ b ↔ ∃ (c : mynat), b = a + c

Now in VS I am trying to implement a similar thing. This is what I wrote:

theorem ge_iff_exists_add (a b : N) a >= b ↔ ∃ (c : N), a= b + c := sorry

This is the error I am getting: invalid binder declaration... Why is that and how to I get rid of this?

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 00:21):

Basically, my goal for this evening is to prove that if b>=a and c>=a then bc>=a^2, very similar to some of the proofs in the Inequality World section of the Natural Number Game.

view this post on Zulip Bryan Gin-ge Chen (Mar 14 2020 at 00:23):

Lean doesn't know what >= is and that's screwing up the parsing. Try the unicode symbol instead (type it using \ge).

Edit: this was totally wrong, Lean does, in fact, know that >= is ge. Whoops!

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 00:23):

My bad, that's what I meant by >= (I used \ge in the VS code). Sorry about that

view this post on Zulip Reid Barton (Mar 14 2020 at 00:25):

you're missing the :

view this post on Zulip Bryan Gin-ge Chen (Mar 14 2020 at 00:25):

As Reid says, you're missing a colon:

theorem ge_iff_exists_add (a b : ) : a  b   (c : ), a= b + c := sorry

(Note that you can get syntax highlighting in Zulip by putting your code between ```lean and ``` (click the "A" icon to the bottom left of the edit box to see formatting tips).)

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 00:26):

Thank you so much,

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 00:32):

theorem example1 (a b c: \nat) (hba: b \ge a) (hca: c \ge a) : b*c \ge a*a :=
begin
        rw ge_iff_exists_add hba,
end

I get an error again. This is what I am trying to mimic, which I solved an hour ago in the Natural number game thanks to Kevin Buzzard:

theorem le_trans (a b c : mynat) (hab : a  b) (hbc : b  c) : a  c :=
begin
rw le_iff_exists_add at hab,
rw le_iff_exists_add at hbc,

cases hab with u hu,
cases hbc with v hv,
rw le_iff_exists_add,
use u+v,
rw  add_assoc,
rw  hu,
rw  hv,
refl,
end

I do not know why my thing in VS is not working

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 00:33):

le_iff_exists_add (a b : mynat)
    a  b   (c : mynat), b = a + c

From the natural number game

view this post on Zulip Bryan Gin-ge Chen (Mar 14 2020 at 00:35):

Did you mean to write rw ge_iff_exists_add at hba,?

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 00:36):

Opps, thanks again

view this post on Zulip Bryan Gin-ge Chen (Mar 14 2020 at 00:39):

As Kevin has said, pay careful attention to the error messages:

type mismatch at application
  ge_iff_exists_add hba
term
  hba
has type
  b ≥ a : Prop
but is expected to have type
  ℕ : Type

This is Lean saying "I can't apply ge_iff_exists_add to hba because I expect a natural number but I'm getting a proof of b ≥ a instead."

At this point you should realize: "hey wait, I didn't want to apply ge_iff_exists_add to hba at all! Oh, there's my typo..."

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 00:54):

Here is where I am at now:

theorem example1 (a b c :) (hba: b  a) (hca: c  a) : b*c  a*a :=
begin
    rw ge_iff_exists_add at hba,
    rw ge_iff_exists_add at hca,

    cases hba with u hu,
    cases hca with v hv,

    rw ge_iff_exists_add,


end

At this stage I believe I can use variables a,b,c,u,v just as in my Inequality world proof. But if I type in

use a*a+a*v+a*u+u*v,

but Lean is saying that u and v are undefined. Did I not define them when I used cases, both in my VS code and in my Inequality World proofs?

view this post on Zulip Reid Barton (Mar 14 2020 at 00:57):

Do u and v show up in the tactic state? Something must be wrong

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 00:58):

This is my tatic state without the use statement:

1 goal
a b c u : ,
hu : b = a + u,
v : ,
hv : c = a + v
  (c_1 : ), b * c = a * a + c_1

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 01:05):

When I type in use (let's say use 1) Lean gives this error: unknown identifier 'use'

view this post on Zulip Bryan Gin-ge Chen (Mar 14 2020 at 01:14):

You need to write import tactic at the top of your file since use is provided by mathlib.

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 01:16):

But file 'tatic' is not found in the LEAN_PATH

view this post on Zulip Bryan Gin-ge Chen (Mar 14 2020 at 01:16):

Then please see the instructions I linked above to set up your Lean project.

view this post on Zulip Johan Commelin (Mar 14 2020 at 05:08):

Bryan Gin-ge Chen said:

If you followed a youtube video, it most likely doesn't have info about the latest version of the "mathlib tools". From your error message, I'm guessing you're using Windows, so you may need to go over these instructions first to get leanproject.

@Scott Morrison Any chance you could add a message about leanproject to your tutorial videos?

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 19:56):

I followed the instructions on the link but still import tactic did not work.

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:02):

What OS are you on? Can you send a screenshot of VS Code in the exact state where the failure is occurring?

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 20:03):

image.png

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 20:03):

image.png
I am using Windows

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:04):

OK so your problem is that you have not made a Lean project as in the instructions. You can't just open a Lean file and hope it all works.

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:04):

You need to clone the example project and then File -> Open Folder and open the folder in VS Code.

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:04):

and you need to compile the project first

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:05):

https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:06):

You need to use the leanproject tool to make and compile a Lean project.

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 20:06):

What do mean by 'clone'?

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 20:06):

Like copy and save it?

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:06):

You simply need to follow the instructions.

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:08):

It's complicated I know, but so far I suspect that you have installed the tools but have not made a project. At the bottom of the installation instructions it tells you now to go onto the instructions about creating and working on Lean projects.

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 20:14):

So I typed source ~/.profile onto a terminal but I got this error:
image.png

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:15):

I cannot help with Windows issues.

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:16):

If you type leanproject what happens?

view this post on Zulip Bryan Gin-ge Chen (Mar 14 2020 at 20:16):

Try using git bash instead of the Windows command prompt.

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 20:16):

THis:
image.png

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 20:16):

Ok i will try

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:17):

Well it looks like you have leanproject installed which is great, but I would definitely follow Bryan's advice.

view this post on Zulip Bryan Gin-ge Chen (Mar 14 2020 at 20:18):

Yeah, if leanproject is working, then you should be in pretty good shape (once you switch to using git bash).

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 20:31):

What does this part mean:
In the file explorer on the left-hand side of VS Code, you can right-click on src, choose New file, and type a filename to create a file there.

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 20:31):

Where issrc?

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 20:32):

Nevermind I found it.

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 20:35):

It works!!!!
image.png
Thank you very much

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:37):

Sorry it's such a struggle. Lean is an experiment rather than finished code. We have tried really hard to write installation instructions but we do appreciate that it is still very complicated for people who are just used to the more standard "click here and it works" approach of the 21st century.

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:38):

Old people like me can remember when installing all software was like this :-)

view this post on Zulip Kevin Buzzard (Mar 14 2020 at 20:38):

(actually it was worse, you often had to compile it yourself!)

view this post on Zulip Debendro Mookerjee (Mar 14 2020 at 22:58):

Here is the code I have in VS:
theorem ge_iff_exists_add (a b: ℕ): a ≥ b ↔ ∃ (c: ℕ), a = b + c := sorry

theorem ge_refl(x : ℕ) : x ≥ x :=
begin
    rw ge_iff_exists_add,
    use 0,
    rw add_zero,
end

Here is what I want to prove:

theorem example2 (a b c : ℕ) (hba: c ≥ 1): a*b*c ≥ a*b :=
begin
    rw mul_comm,
    --Still Empty
end

After rw mul_comm, the lean tactic output is:

1 goal
a b c : ℕ
⊢ c * (a * b) ≥ a * b

However, if I substitute --Still Empty with rw ge_refl, I get the error:

rewrite tactic failed, lemma is not an equality nor a iff
state:
a b c : ℕ
⊢ c * (a * b) ≥ a * b

Since I have proven ab >= ab I want the goal to be c >=1. How do I achieve this?

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 08:11):

rw h only makes sense if h is a proof of A = B or A    BA\iff B. Then what it does is it takes all occurrences of A and changes them to B. ge_refl is not a proof of something of the form A = B or A    BA\iff B so rw ge_refl won't work.

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 08:14):

Oh I now see that you posted the exact same question in another thread where it was answered. Can you post questions precisely once?


Last updated: May 08 2021 at 04:14 UTC