Inequality World

Stream: new members

[Debendro Mookerjee]

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.

[Kevin Buzzard]

cases hab with u hu,

[Kevin Buzzard]

will extract the u from hab

[Kevin Buzzard]

and the proof that it does the right thing is hu

[Kevin Buzzard]

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

[Debendro Mookerjee]

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

[Kevin Buzzard]

right

[Kevin Buzzard]

and then you've got what you need

[Debendro Mookerjee]

Thanks

[Kevin Buzzard]

np

[Debendro Mookerjee]

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?

[Kevin Buzzard]

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

[Debendro Mookerjee]

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]

Yes, that error looks good

[Kevin Buzzard]

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

[Kevin Buzzard]

what tactic caused that error?

[Debendro Mookerjee]

rw add_assoc

[Debendro Mookerjee]

Doesn't equality work in both directions?

[Kevin Buzzard]

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

[Debendro Mookerjee]

So what do I do here?

[Kevin Buzzard]

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

[Kevin Buzzard]

rw ← add_assoc

[Kevin Buzzard]

Is your background in maths or CS?

[Debendro Mookerjee]

Math

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and rw turns LHS into RHS

[Kevin Buzzard]

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]

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]

exactly the same reason?

[Debendro Mookerjee]

Wait do I use rw ← hu,?

[Kevin Buzzard]

give it a try :-)

[Debendro Mookerjee]

Oh I see it works

[Kevin Buzzard]

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

[Debendro Mookerjee]

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,

[Debendro Mookerjee]

Thanks.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Debendro Mookerjee]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Debendro Mookerjee]

So.....?

[Debendro Mookerjee]

what should I do

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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.

[Debendro Mookerjee]

I feel like I did not download something.

[Bryan Gin-ge Chen]

What error are you seeing, exactly?

[Debendro Mookerjee]

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

[Bryan Gin-ge Chen]

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

[Debendro Mookerjee]

I followed an youtube video and downloaded MATLIB and all.

[Bryan Gin-ge Chen]

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]

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]

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?

[Debendro Mookerjee]

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]

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]

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

[Reid Barton]

you're missing the :

[Bryan Gin-ge Chen]

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]

Thank you so much,

[Debendro Mookerjee]

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

[Debendro Mookerjee]

le_iff_exists_add (a b : mynat)
    a ≤ b ↔ ∃ (c : mynat), b = a + c

From the natural number game

[Bryan Gin-ge Chen]

Did you mean to write rw ge_iff_exists_add at hba,?

[Debendro Mookerjee]

Opps, thanks again

[Bryan Gin-ge Chen]

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

[Debendro Mookerjee]

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?

[Reid Barton]

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

[Debendro Mookerjee]

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]

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

[Bryan Gin-ge Chen]

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

[Debendro Mookerjee]

But file 'tatic' is not found in the LEAN_PATH

[Bryan Gin-ge Chen]

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

[Johan Commelin]

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]

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

[Kevin Buzzard]

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

[Debendro Mookerjee]

image.png

[Debendro Mookerjee]

image.png
I am using Windows

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

and you need to compile the project first

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Debendro Mookerjee]

What do mean by 'clone'?

[Debendro Mookerjee]

Like copy and save it?

[Kevin Buzzard]

You simply need to follow the instructions.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

I cannot help with Windows issues.

[Kevin Buzzard]

If you type leanproject what happens?

[Bryan Gin-ge Chen]

Try using git bash instead of the Windows command prompt.

[Debendro Mookerjee]

THis:
image.png

[Debendro Mookerjee]

Ok i will try

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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

[Debendro Mookerjee]

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]

Where issrc?

[Debendro Mookerjee]

Nevermind I found it.

[Debendro Mookerjee]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Debendro Mookerjee]

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?

[Kevin Buzzard]

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]

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