Inequality World 2

Stream: new members

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

[Reid Barton]

Is ge_refl a real thing?

[Reid Barton]

oh I see, you defined it above. But you could never use it here

[Reid Barton]

You need a lemma that says: if c >= 1, then c * x >= x

[Debendro Mookerjee]

Just curious, how would I prove this lemma. And how would I call this lemma into my theorem?

[Reid Barton]

Somehow (depending on your exact definitions and already existing lemmas) you would want to show if c >= 1 then you can write c = d + 1, and then (d + 1) * x = d * x + x >= x because hopefully you know y + x >= x for any y

[Reid Barton]

The second question you can do first: define

lemma my_lemma (c x : \N) : c >= 1 -> c * x >= x := sorry

then in your proof,

  apply my_lemma,

[Reid Barton]

I suggest you do this first and finish your main proof, then prove the lemma

[Debendro Mookerjee]

Ok thanks I will do that.

[Debendro Mookerjee]

I got this error:

invalid apply tactic, failed to unify
  c * (a * b) ≥ a * b
with
  ?m_1 * ?m_2 ≥ ?m_2
state:
a b c : ℕ,
hba : c ≥ 1
⊢ c * (a * b) ≥ a * b

[Debendro Mookerjee]

Wait, I think I can write it backwards.

[Debendro Mookerjee]

Nevermind I think I got it. Thanks for the help

[Debendro Mookerjee]

This is my tactic state after using apply,

1 goal
a b c : ℕ,
hba : c ≥ 1
⊢ c ≥ 1

But if I say rw hba I get an error. Why and how do I fix it?

[Bryan Gin-ge Chen]

You can only rw with equalities or iff statements. Try exact hba.

[Debendro Mookerjee]

I got it: I used apply hba

[Debendro Mookerjee]

I guess its the same thing, right?

[Bryan Gin-ge Chen]

They both work, but exact and apply do different things in general.

[Debendro Mookerjee]

Another question. To prove my_lemma defined by Reid Barton I want to use induction starting from 1. Is that possible in lean, and if so how?

[Bryan Gin-ge Chen]

Use exact H when H has the type of the goal. Use apply H when H : a -> b to turn a goal b to a goal a.

[Debendro Mookerjee]

Ok thanks. The clarification indeed helps. I changed it to exact ba. To prove my_lemma defined by Reid Barton I want to use induction starting from 1. Is that possible in lean, and if so how?

[Marc Huisinga]

you can use regular induction. you will get a hypothesis 0 >= 1, which is false, and can hence be used to prove the base case.

[Debendro Mookerjee]

But how to I show that this is false (what lean code shows this)---I see why it is false and why it proves the base case.

[Marc Huisinga]

i'm not sure what the intended way in NNG is since i haven't played it

[Marc Huisinga]

i'd probably do something like

intro h,
exact (nat.not_succ_le_zero 0 h).elim

[Marc Huisinga]

in the inductive case you'll also see that you can only apply the induction hypothesis if you make an additional case distinction, which is where you have to prove the actual base case for 1 :)

[Debendro Mookerjee]

Here is my tatic state:

1 goal
case nat.succ
x d : ℕ,
hd : x + d ≥ x
⊢ x + d + 1 ≥ x

How do I apply hd into the goal?

[Debendro Mookerjee]

Here's the rest of my code (base case complete)

lemma my_lemma_helper (x y: ℕ) : y+x ≥ x :=
begin
    induction y with d hd,
    rw zero_add,
    apply ge_refl,

    rw add_comm,
    rw nat.add_succ,
    rw add_comm at hd,
    rw succ_eq_add_one,

end

[Debendro Mookerjee]

Still was not able to make progress on lemma my_lemma_helper stated above. Any Help?

[Kevin Buzzard]

What do you mean by "how do I apply hd to the goal?"

[Kevin Buzzard]

hd is not equal to the goal, and it's not a function so you can't apply it to anything.

[Debendro Mookerjee]

Nevermind, I realized my mistake and it works now

[Debendro Mookerjee]

This might be a silly question, but here it is anyway:

This is the theorem I am trying to prove:

theorem ge_cancel (a b : ℕ) (ha : a*b ≥ a) : b ≥ 1 :=
begin
    rw ge_iff_exists_add at ha,

    cases ha with u hu,

    ----more work needs to be done-------
end

Here is the tactic state:

1 goal
a b u : ℕ,
hu : a * b = a + u
⊢ b ≥ 1

How do I achieve this goal?

[Bryan Gin-ge Chen]

ge_cancel is false when a = 0 and b = 0.

[Debendro Mookerjee]

Same question, but here is my corrected theorem:

theorem ge_cancel (a b : ℕ) (ha : a*b ≥ a) (hb: a ≥ 1) : b ≥ 1 :=
begin
    rw ge_iff_exists_add at ha,

    cases ha with u hu,

    ----more work needs to be done-------
end

[Kevin Buzzard]

If you're now using Lean and mathlib, rather than doing natural number game stuff, you should use <= not >=, i.e. wherever you have a >= b you should change it to b <= a. <= is much better supported in mathlib.

[Kevin Buzzard]

Are you asking for a maths proof or a Lean proof?

[Debendro Mookerjee]

Lean proof

[Kevin Buzzard]

Then first explain a maths proof and we can think about how to turn it into a Lean proof.

[Debendro Mookerjee]

Claim: If ab >= a where a is >=1 and a,b are positive integers then b >= 1.
Proof:
Assume ab >= a where a is >=1, but that b < 1. Then there exists a positive integer c such that b = 1 - c. Thus ab = a*(1 - c) = a - ac.
Thus there exists a positive integer k such that ab = a - k. Thus ab < a. Contradiction

[Debendro Mookerjee]

I only know a contradiction math proof, and I do not know how to write a contradiction proof in Lean. How do I start writing a contradiction proof in Lean if I am to translate the above math proof?

[Kevin Buzzard]

What is your definition of the subtraction you're using? We should be able to simplify this proof. Did you play the natural number game? Subtraction is never defined in this game, and this is for a good reason.

[Kevin Buzzard]

And do you really mean "a,b are positive integers"? What type do the terms a and b have?

We need to be 100% clear on the maths proof before we can start the Lean proof.

[Debendro Mookerjee]

(a b : \nat) (ha: a \ge 1) (hb : b \ge 1)

For substaction, I just used the regular paper-pencil proof definition: subtraction is addition by negative number (I just wrote the proof if this were a class homework question)

[Kevin Buzzard]

PS if you cannot do basic logic like contradiction yet then you should work through the exercises in Theorem Proving In Lean. There is a ton of stuff to learn, and just asking every time you get stuck on a random question might not be the most efficient way to proceed. I spent a lot of time reading that website above and would only ask questions here if I was really stuck.

[Kevin Buzzard]

What is your definition of a negative number?

[Kevin Buzzard]

I am pretending to be Lean here. We have two terms a and b of type nat. If you've played the natural number game then you know the definition of addition and multiplication. Can you see that there is a problem with defining subtraction?

[Kevin Buzzard]

And if you haven't played the natural number game, then you should learn to walk before you can run.

[Debendro Mookerjee]

Yeah I do, but I only know the paper pencil proof done in math class for this one

[Debendro Mookerjee]

I played the Natural number game from the stream Inequality World

[Kevin Buzzard]

Well the pencil and paper proof unfortunately seems to assume that negative numbers exist, and this is problematic because introducing negative numbers will mean that we have to import the entire question into a question about terms in a new type, namely the integers.

[Kevin Buzzard]

and this will make the formal proof much more complicated.

[Debendro Mookerjee]

So how do I avoid subtraction ?

[Kevin Buzzard]

Good question! Try and figure out a solution which doesn't use subtraction. If you play the natural number game you will begin to understand exactly what you can and cannot do with natural numbers.

[Debendro Mookerjee]

The last two lines of my tactic state is bothering me; I do not know how to go around it?

1 goal
a b u : ℕ,
hu : a * b = a + u
⊢ b ≥ 1

[Debendro Mookerjee]

I did play the natural number game (in the stream Inequality World) so that's why I started to avoid substraction in my original lean proof, where I got the above tactic state. I do not know how to use hu to satisfy the goal

[Kevin Buzzard]

Can you prove that that goal is impossible to solve?

[Kevin Buzzard]

This stuff is hard. Your original question basically says "how do I work inductive types, and how do I do basic logic stuff like proof by contradiction in Lean".

[Kevin Buzzard]

I am a teacher. I have been a teacher for over 20 years.

[Debendro Mookerjee]

Here is the theorem I am trying to prove: (from an old stream called Prime Theorem Help)

Let n > 1. If n has no positive prime factor less than or equal to sqrt(n), then n is prime.

Here is a proof from Hungerford's Abstract Algebra:
Suppose n has the given property but assume that n is not prime. Then n has at least two positive prime factors, say p1 and p2, so that n = p1p2k for some positive integer k. By hypothesis, n has no positive prime divisors less than or equal to sqrt(n). Hence p1 > sqrt(n) and p2 > sqrt(n). Hence n = p1p2k >= p1*p2 >n. Contradiction.

And here are the things I have proved so far thanks to you and others in Zulip:
image.png
image.png
image.png
image.png
image.png

These theorems and lemmas are needed to prove things in the main proof in Hungerford's Algebra. I was curious about the contradiction proof because Hungerford's proof uses it and I want to mimic it.

[Kevin Buzzard]

My answer to you is "go and read Theorem Proving In Lean. You are thinking like a mathematician. If you want to learn how to use Lean you need to learn to think more like a computer scientist. Chapters 3 and 4 tell you a lot about how to use logic in Lean. Chapter 7 tells you how to use inductive types. These chapters tell you the answer to not only your question, but also the next 5 questions which you will ask me if I just tell you how to do this one."

[Debendro Mookerjee]

Ok I will start

[Kevin Buzzard]

This stuff is hard, and you are just choosing random arithmetical statements which might be currently beyond your abilities. You need to step back and do some self study and learn about the basics. Do all of the exercises in the first seven chapters in Theorem Proving In Lean and feel free to ask if you are stuck.

[Kevin Buzzard]

But Hungerford will have to wait a while.

[Debendro Mookerjee]

Here is a Lean code from Chapter 3 Section 4

variables p q : Prop

example (h : p ∧ q) : q ∧ p :=
have hp : p, from and.left h,
have hq : q, from and.right h,
show q ∧ p, from and.intro hq hp

What exactly do the lines :

have hp : p, from and.left h,
have hq : q, from and.right h,

mean? Am I dividing up the hypothesis or the goal?

[Bryan Gin-ge Chen]

Not sure what you mean by "dividing up", but have is a way to introduce a new named hypothesis.

[Debendro Mookerjee]

So if my tactic state is:

1 goal
n v u : ℕ,
hu : n = v * u ∧ v ≤ u
⊢ n = v * u ∧ v * v ≤ n

I have two goals: n = v * u and v * v ≤ n. I am guessing that have allows me to focus on these two individually right?

[Andrew Ashworth]

The next paragraph after that section you posted says exactly what it is under the hood... "Internally, the expression have h : p, from s, t produces the term (λ (h : p), t) s. In other words, s is a proof of p, t is a proof of the desired conclusion assuming h : p, and the two are combined by a lambda abstraction and application. This simple device is extremely useful when it comes to structuring long proofs, since we can use intermediate have’s as stepping stones leading to the final goal."

[Debendro Mookerjee]

But I do not know what those words mean

[Debendro Mookerjee]

So I am trying to learn by example

[Andrew Ashworth]

Did you skip chapter 2 :)

[Debendro Mookerjee]

I read ch 2 but I felt ch 3 would give concrete applications of ch 2 stuff

[Andrew Ashworth]

Hah, but there are exercises in Ch2 that explain lambda notation

[Andrew Ashworth]

I know it's boring and not related to the thing you actually want to do

[Andrew Ashworth]

but it's necessary

[Chris Hughes]

have is for when you want to prove a lemma on the way to your theorem.

So have hp : p, from and.left h introduces a proof of p into your context, and the proof is and.left h.

Personally I don't find the explanation about have in terms of lambdas very helpful.

[Debendro Mookerjee]

And what does and.left h actually do?

[Andrew Ashworth]

suppose and is a structure with two members, left and right

[Andrew Ashworth]

and.left is just the first element

[Debendro Mookerjee]

And and.right is the second element?

[Andrew Ashworth]

yup

[Debendro Mookerjee]

But then it seems that have is breaking up my hypothesis; is that right?

[Debendro Mookerjee]

Since p is part of my hypothesis p and q

[Reid Barton]

I think it will become clearer as you look at more examples.

[Bryan Gin-ge Chen]

It's used here to introduce proofs of each of the parts of your hypothesis, but it's not breaking it up as I understand it.

[Debendro Mookerjee]

Thanks

[Debendro Mookerjee]

Is it possible to define Propositions of the form h1 \and h2 within a proof.

[Yury G. Kudryashov]

You can say have h1 : ..., from ..., then have h2 : ..., from ..., then have h := h1 ∧ h2 (in tactic mode; in term mode the idea is the same but the syntax is slightly different).

[Debendro Mookerjee]

I read ch.2 and am in still in Ch.3. I don't see what the assume statement does? Can anyone explain with a concrete example?

[Bryan Gin-ge Chen]

It's the same as λ, see Section 3.2.

Example:

constants p q : Prop

theorem t1 : p → q → p := assume hp : p, assume hq : q, hp

[Daniel Keys]

I had some trouble with this myself. In Lean, assume has a very well-defined meaning, while we as mathematicians use it in a more encompassing way.

[Andrew Ashworth]

yes, the assume is there to make mathematicians feel at home... but it is exactly the lambda calculus' lambda operator. I do not know if it makes people more or less confused

[Debendro Mookerjee]

Can we say:

constants p q : Prop

theorem t1 : p → q → p := assume hp : p, assume hq :\not q, hp

[Andrew Ashworth]

no, because the lambda operator doesn't work that way

[Debendro Mookerjee]

Ok I see.

[Debendro Mookerjee]

So it only works with the hypotheses we have

[Daniel Keys]

Look for the stream "Understanding assume" under new members to see more. I don't exactly know how to send you a link, but you can search for it.

[Debendro Mookerjee]

Thanks