## Stream: new members

### Topic: Inequality World

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

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.

#### Kevin Buzzard (Mar 13 2020 at 23:01):

cases hab with u hu,

#### Kevin Buzzard (Mar 13 2020 at 23:01):

will extract the u from hab

#### Kevin Buzzard (Mar 13 2020 at 23:01):

and the proof that it does the right thing is hu

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

#### Debendro Mookerjee (Mar 13 2020 at 23:01):

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

right

#### Kevin Buzzard (Mar 13 2020 at 23:02):

and then you've got what you need

Thanks

np

#### Debendro Mookerjee (Mar 13 2020 at 23:13):

Another question. This what I did so far:

cases hab with u hu,
cases hbc with v hv,
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?

#### 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 :-)

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

#### Kevin Buzzard (Mar 13 2020 at 23:20):

Yes, that error looks good

#### Kevin Buzzard (Mar 13 2020 at 23:20):

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

#### Kevin Buzzard (Mar 13 2020 at 23:20):

what tactic caused that error?

#### Debendro Mookerjee (Mar 13 2020 at 23:21):

Doesn't equality work in both directions?

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

#### Debendro Mookerjee (Mar 13 2020 at 23:21):

So what do I do here?

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

#### Kevin Buzzard (Mar 13 2020 at 23:22):

rw ← add_assoc

#### Kevin Buzzard (Mar 13 2020 at 23:22):

Is your background in maths or CS?

Math

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

#### Kevin Buzzard (Mar 13 2020 at 23:24):

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

#### Kevin Buzzard (Mar 13 2020 at 23:24):

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

#### Kevin Buzzard (Mar 13 2020 at 23:24):

and rw turns LHS into RHS

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

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

#### Kevin Buzzard (Mar 13 2020 at 23:26):

exactly the same reason?

#### Debendro Mookerjee (Mar 13 2020 at 23:27):

Wait do I use rw ← hu,?

#### Kevin Buzzard (Mar 13 2020 at 23:27):

give it a try :-)

#### Debendro Mookerjee (Mar 13 2020 at 23:27):

Oh I see it works

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

#### Debendro Mookerjee (Mar 13 2020 at 23:28):

It works:

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

Thanks.

#### 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 :-)

#### Kevin Buzzard (Mar 13 2020 at 23:29):

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

#### Kevin Buzzard (Mar 13 2020 at 23:29):

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

#### 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 :=

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?

#### Kevin Buzzard (Mar 13 2020 at 23:37):

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

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

So.....?

what should I do

#### 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 :-)

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

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

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

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

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

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

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

#### Bryan Gin-ge Chen (Mar 14 2020 at 00:02):

What error are you seeing, exactly?

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

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

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

#### 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:
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?

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

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

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

#### Reid Barton (Mar 14 2020 at 00:25):

you're missing the :

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

#### Debendro Mookerjee (Mar 14 2020 at 00:26):

Thank you so much,

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

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


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

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

#### Bryan Gin-ge Chen (Mar 14 2020 at 00:35):

Did you mean to write rw ge_iff_exists_add at hba,?

#### Debendro Mookerjee (Mar 14 2020 at 00:36):

Opps, thanks again

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

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

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

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?

#### Reid Barton (Mar 14 2020 at 00:57):

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

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


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

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

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

#### Debendro Mookerjee (Mar 14 2020 at 19:56):

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

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

image.png

#### Debendro Mookerjee (Mar 14 2020 at 20:03):

image.png
I am using Windows

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

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

#### Kevin Buzzard (Mar 14 2020 at 20:04):

and you need to compile the project first

#### Kevin Buzzard (Mar 14 2020 at 20:05):

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

#### Kevin Buzzard (Mar 14 2020 at 20:06):

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

#### Debendro Mookerjee (Mar 14 2020 at 20:06):

What do mean by 'clone'?

#### Debendro Mookerjee (Mar 14 2020 at 20:06):

Like copy and save it?

#### Kevin Buzzard (Mar 14 2020 at 20:06):

You simply need to follow the instructions.

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

#### Debendro Mookerjee (Mar 14 2020 at 20:14):

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

#### Kevin Buzzard (Mar 14 2020 at 20:15):

I cannot help with Windows issues.

#### Kevin Buzzard (Mar 14 2020 at 20:16):

If you type leanproject what happens?

#### Bryan Gin-ge Chen (Mar 14 2020 at 20:16):

Try using git bash instead of the Windows command prompt.

THis:
image.png

Ok i will try

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

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

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

#### Debendro Mookerjee (Mar 14 2020 at 20:31):

Where issrc?

#### Debendro Mookerjee (Mar 14 2020 at 20:32):

Nevermind I found it.

#### Debendro Mookerjee (Mar 14 2020 at 20:35):

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

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

#### Kevin Buzzard (Mar 14 2020 at 20:38):

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

#### Kevin Buzzard (Mar 14 2020 at 20:38):

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

#### 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
use 0,
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?

#### Kevin Buzzard (Mar 15 2020 at 08:11):

rw h only makes sense if h is a proof of A = B or $A\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\iff B$ so rw ge_refl` won't work.

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