## Stream: new members

### Topic: inequality golf request

#### Bryan Gin-ge Chen (Nov 21 2018 at 18:56):

I'm curious to see how simple a lean proof of this can be:

-- Thm 1.3 in Hopcroft, Motwani and Ullcroft's book
example (x : ℕ) (h : x ≥ 4) : 2 ^ x ≥ x ^ 2 := sorry


For comparison, here's my ugly rewrite proof:

import tactic.linarith

open nat

lemma h4 : (4 : ℚ) = ↑(4 : ℕ) := by simp
lemma h5 : (5 : ℚ) = ↑(5 : ℕ) := by simp

lemma hne {a : ℕ} : 0 < (↑((a+4)^2) : ℚ) :=
begin
-- simp, ring,
rw [nat.cast_pos],
exact pow_pos (succ_pos _) _
end

lemma this'' {a : ℕ} : (5 : ℚ)^2 / (4 : ℚ)^2 ≥ (↑((a+5)^2) / ↑((a+4)^2): ℚ) :=
begin
refine (div_le_iff hne).2 _,
rw [mul_comm_div, ←mul_div_assoc],
refine (le_div_iff (by norm_num)).2 _,
-- simp, ring, simp,
rw [h4, h5, cast_pow, cast_pow, ←_root_.mul_pow, ←_root_.mul_pow, ←cast_mul, ←cast_mul],
refine _root_.pow_le_pow_of_le_left _ _ _,
{ exact nat.cast_nonneg _ },
{ rw [nat.cast_le], linarith }
end

lemma this' {a : ℕ} : 2 ≥ (↑((a+5)^2) / ↑((a+4)^2): ℚ) :=
calc 2 ≥ (5 : ℚ)^2 / (4 : ℚ)^2 : by norm_num
... ≥ _ : this''

example (x : ℕ) (h : x ≥ 4) : 2 ^ x ≥ x ^ 2 :=
match x, h with
| 0, _ := dec_trivial
| 1, _ := dec_trivial
| 2, _ := dec_trivial
| 3, h := by norm_num at h
| 4, _ := dec_trivial
| (a+5), hₐ :=
begin
have : 2 ^ (a + 4) ≥ (a + 4) ^ 2 := _match (a+4) dec_trivial,
have thisQ : (↑(2 ^ (a+4)) : ℚ) ≥ (↑((a+4)^2) : ℚ) :=
nat.cast_le.2 this,
have goalQ : (↑(2 ^ (a+5)) : ℚ) ≥ (↑((a+5)^2) : ℚ) :=
begin
rw [nat.pow_succ, mul_comm, cast_mul, mul_mul_div (↑((a+5)^2)) (ne_of_gt hne)],
conv_rhs { rw [mul_comm, ←mul_assoc, mul_comm_div, one_mul] },
exact mul_le_mul this' thisQ (le_of_lt hne) (by norm_num)
end,
exact nat.cast_le.1 goalQ
end
end


I tried using linarith at the commented lines but it didn't seem to know how to deal with coercions from nat, even after I put ↑a ≥ 0 as a hypothesis. A related question: what's the easiest way to turn a goal like this:

(160 + 16 * ↑a) * ↑a ≤ (200 + 25 * ↑a) * ↑a


into an inequality over nats (e.g. by getting it into a form where I can use nat.cast_le)?

#### Kevin Buzzard (Nov 21 2018 at 19:31):

import data.nat.basic
import tactic.ring

lemma helpful {d : ℕ} (h4 : 4 ≤ d) : 2 * d + 1 ≤ d * d :=
calc 2 * d + 1 ≤ 2 * d + d : nat.add_le_add_left (le_trans dec_trivial h4) _
... = (2 + 1) * d : by rw [add_mul,one_mul]
... ≤ d * d : nat.mul_le_mul_right _ (le_trans dec_trivial h4)

example (x : ℕ) (h : x ≥ 4) : 2 ^ x ≥ x ^ 2 :=
begin
induction x with d Hd,exact dec_trivial,
cases nat.eq_or_lt_of_le h with h4 h5,
rw ←h4,exact dec_trivial,
have h4 : 4 ≤ d := nat.le_of_lt_succ h5,
exact calc 2 ^ (d + 1) = 2 ^ d * 2 : by rw nat.pow_succ
... ≥ d ^ 2 * 2 : nat.mul_le_mul_right 2 (Hd h4)
... = d * d + d * d : by rw [mul_two,nat.pow_two]
... = (d + 1) ^ 2 : by ring
end


#### Kevin Buzzard (Nov 21 2018 at 19:31):

Did I misunderstand the question? I don't understand why you are using rationals.

#### Bryan Gin-ge Chen (Nov 21 2018 at 19:33):

Yeah, in hindsight that strategy wasn't so smart (I was following the proof from that book which first showed that $2 \geq (x+1)^2/x^2$ for $x\geq4$).

#### Kevin Buzzard (Nov 21 2018 at 19:33):

For (160 + 16 * ↑a) * ↑a ≤ (200 + 25 * ↑a) * ↑a I would try proving the things you want to rewrite with simp. I wrote some stuff about this sort of thing here https://github.com/leanprover/mathlib/blob/master/docs/extras/casts.md , maybe that helps.

#### Kevin Buzzard (Nov 21 2018 at 19:34):

I showed that goal too, but I kept everything in nat and showed 2x^2>=(x+1)^2

#### Bryan Gin-ge Chen (Nov 21 2018 at 19:35):

I was looking at that doc but it didn't say anything about inequalities. But maybe you're saying that I'll have to transform the numbers individually.

#### Bryan Gin-ge Chen (Nov 21 2018 at 19:37):

Or I guess I can probably get simp to do the LHS / RHS all at once.

#### Kevin Buzzard (Nov 21 2018 at 20:41):

I mean you could try things like rw (show (160 + 16 * ↑a) * ↑a = ((160 + 16 * a) * a : nat), by simp)

#### Kevin Buzzard (Nov 21 2018 at 20:47):

import data.rat

example (a : ℕ) (H : ((160 : ℚ) + 16 * ↑a) * ↑a ≤ (200 + 25 * ↑a) * ↑a) :
(160 + 16 * a) * a ≤ (200 + 25 * a) * a :=
begin
rw (show ((160 : ℚ) + 16 * ↑a) * ↑a = ((160 + 16 * a) * a : nat), by simp) at H,
rw (show ((200 : ℚ) + 25 * ↑a) * ↑a = ((200 + 25 * a) * a : nat), by simp) at H,
rw nat.cast_le at H,
assumption
end


#### Kevin Buzzard (Nov 21 2018 at 20:48):

I had to deal with a gazillion of these sorts of things when I was doing my own undergraduate example sheets, and ended up with what I hope is a robust set of techniques. I still sometimes think about a typeclass solution though.

#### Bryan Gin-ge Chen (Nov 22 2018 at 01:31):

Thanks, this has been very helpful!

#### Kevin Buzzard (Nov 22 2018 at 08:17):

So here's a question that came up on my undergraduate example sheets. "Show that the rationals are unbounded above in the reals". In maths we would perhaps say "it's a standard result that for all real x there exists a natural n with n > x, so done". As you can imagine, porting this proof to Lean is a great example of how things are harder than they look here (or how they should be)? @Bryan Gin-ge Chen you might want to try proving theorem rationals_unbounded (r : ℝ) : ∃ s : ℚ, r < s from exists_nat_gt : ∀ (x : ℝ), ∃ (n : ℕ), x < ↑n. It's just the same sort of kerfuffle. Some idle coding from earlier in the week:

import algebra.archimedean

import data.real.basic

class is_nat (r : ℝ) : Prop :=
(pf : ∃ n : ℕ, r = n)

class is_rat (r : ℝ) : Prop :=
(pf : ∃ q : ℚ, r = q)

definition S : set ℝ := {r : ℝ | is_rat r}

instance nat_is_rat (r : ℝ) [H : is_nat r] : is_rat r :=
begin
tactic.unfreeze_local_instances,
rcases H with ⟨⟨n,Hn⟩⟩,
refine ⟨⟨n,_⟩⟩, -- some stupid refining happening here out of the way
rw Hn, simp
end

-- better than exists_nat_gt
-- can it be written by a machine?
theorem real.exists_nat_gt' (x : ℝ) :
∃ (n : ℝ) [is_nat n], x < n :=
let ⟨n,Hn⟩ := exists_nat_gt x in ⟨n,⟨⟨⟨n,rfl⟩⟩,Hn⟩⟩

theorem rationals_unbounded (r : ℝ) : ∃ s : S, r < s :=
let ⟨n,Hn,Hx⟩ := real.exists_nat_gt' r in
begin
haveI := Hn,
refine ⟨⟨n,show is_rat n, by apply_instance⟩,_⟩,
assumption,
end


There's some noise earlier on, but the main proof at the end there is very short, and probably could be shorter (it was one of the things that started me off on the use rant on another thread). I've always wondered whether there is something in these typeclasses I'm setting up here.

#### Mario Carneiro (Nov 22 2018 at 08:58):

I'm confused. What's the difference between exists_nat_gt and what you want?

#### Kevin Buzzard (Nov 22 2018 at 08:59):

I want a version of exists_nat_gt which only uses real numbers. The problem which I as a number theorist run into is having to switch between nat, rat and real all the time in a way which is very non-intuitive to a mathematician. I am proposing putting nat and rat (and int) typeclasses on real, meaning that you can reason only with real numbers and avoid having to deal with all the casts.

#### Kevin Buzzard (Nov 22 2018 at 09:00):

The issue is not exists_nat_gt, the issue is proving (r : ℝ) : ∃ s : ℚ, r < s using it, which is more than one line in Lean and only one line in maths.

#### Kevin Buzzard (Nov 22 2018 at 09:01):

import algebra.archimedean

import data.real.basic

definition S : set ℝ := {r : ℝ | ∃ q : ℚ, r = q}

theorem rationals_unbounded : ∀ r : ℝ, ∃ s : S, r < s :=
begin
intro r,
have H := exists_nat_gt r,
cases H with n Hn,
refine ⟨⟨n,_⟩,_⟩,
refine ⟨n,_⟩,
simp,
show r < n,
assumption
end


That is sort-of horrible.

#### Mario Carneiro (Nov 22 2018 at 09:01):

perhaps you should use exists_rat_gt then

#### Mario Carneiro (Nov 22 2018 at 09:02):

also notice that the proof of that is a one liner

#### Kevin Buzzard (Nov 22 2018 at 09:02):

These one-liners are hard for beginner mathematicians to write. Of this I am certain.

#### Kevin Buzzard (Nov 22 2018 at 09:02):

That's the problem.

#### Kevin Buzzard (Nov 22 2018 at 09:03):

You can say "well, that's the nature of dependent type theory" or "mathematicians are cheats", but at the end of the day they struggle to see what the issue is.

#### Kevin Buzzard (Nov 22 2018 at 09:04):

My typeclass suggestion, which clearly needs work and may never fly, is just an idea I had for trying to make it easier for mathematicians.

#### Mario Carneiro (Nov 22 2018 at 09:04):

that's probably true, but you've already written lots of documentation about it. What more are you going for?

#### Kevin Buzzard (Nov 22 2018 at 09:04):

I want to make it easy for beginners.

#### Kevin Buzzard (Nov 22 2018 at 09:05):

I want the proof of rationals_unbounded (r : ℝ) : ∃ s : rat, r < s to be exists_nat_gt rather than being this plus several lines of faffing around.

#### Kevin Buzzard (Nov 22 2018 at 09:06):

:= by standard_typeclass_faff using [exists_nat_gt]

#### Mario Carneiro (Nov 22 2018 at 09:06):

they aren't literally the same thing, so you can't completely eliminate the faffing, but you can get it down to one line

#### Mario Carneiro (Nov 22 2018 at 09:06):

well, you can if you use the library lemma :)

#### Kevin Buzzard (Nov 22 2018 at 09:06):

They are literally the same thing to a mathematician, and whilst I completely understand that they are not the same thing at all, I want to make this transparent.

#### Mario Carneiro (Nov 22 2018 at 09:07):

no they are not the same to a mathematician either... one is talking about nats and the other is talking about rats

#### Mario Carneiro (Nov 22 2018 at 09:07):

clearly not the same

#### Kevin Buzzard (Nov 22 2018 at 09:07):

And my conclusions were that when it suits them, mathematicians redefine the rationals to be the subset of the reals which are rational

#### Kevin Buzzard (Nov 22 2018 at 09:08):

and similarly they redefine the naturals. Mathematicians only work with objects up to canonical isomorphism so they don't even notice that this is happening.

#### Mario Carneiro (Nov 22 2018 at 09:08):

In that case you have to make an analogous observation that nat is a subset of rat ... it's not zero step no matter how you do it

#### Kevin Buzzard (Nov 22 2018 at 09:09):

I know it's not zero step, but it's perhaps one tactic.

#### Kevin Buzzard (Nov 22 2018 at 09:10):

Ultimately I'll just say the same thing one more time -- if in a maths lecture you prove that for all reals x there exists a natural n with n > x, and then you want to deduce that for all reals x there exists a rational q with q > x, the proof in a maths lecture is "what are you talking about? We just did this!" It's 0 lines.

#### Kevin Buzzard (Nov 22 2018 at 09:11):

Because conveniently at this point in the lecturer's brain, a natural is a rational.

#### Kevin Buzzard (Nov 22 2018 at 09:11):

I am hoping that one day we'll have an interface which will enable mathematicians to keep this pretence up.

#### Mario Carneiro (Nov 22 2018 at 09:11):

definition S : set ℝ := {r : ℝ | ∃ q : ℚ, r = q}

theorem rationals_unbounded (r : ℝ) : ∃ s : S, r < s :=
let ⟨q, h⟩ := exists_rat_gt r in ⟨⟨_, ⟨q, rfl⟩⟩, h⟩


#### Kevin Buzzard (Nov 22 2018 at 09:12):

you cheated, you used exists_rat_gt. And already that line is hard for beginners, who work in tactic mode, to write.

#### Mario Carneiro (Nov 22 2018 at 09:12):

theorem rationals_unbounded (r : ℝ) : ∃ s : S, r < s :=
let ⟨n, h⟩ := exists_nat_gt r in ⟨⟨_, n, rfl⟩, by simpa⟩


#### Kevin Buzzard (Nov 22 2018 at 09:13):

Can we get rid of all pointy brackets?

#### Kevin Buzzard (Nov 22 2018 at 09:13):

With my type class idea, I wanted to get pointy bracket usage down to 0

#### Mario Carneiro (Nov 22 2018 at 09:13):

you have to inhabit an exists

#### Kevin Buzzard (Nov 22 2018 at 09:13):

I wanted the output to be a real with a typeclass proving it's a nat.

#### Kevin Buzzard (Nov 22 2018 at 09:14):

Right. So I want to use use to inhabit the exists.

#### Mario Carneiro (Nov 22 2018 at 09:16):

theorem rationals_unbounded (r : ℝ) : ∃ s : S, r < s :=
begin
cases exists_nat_gt r with n h,
split, swap,
{ split, split,
{ refl },
{ exact n } },
{ simpa }
end


#### Kevin Buzzard (Nov 22 2018 at 09:16):

This basically is the culmination of my thoughts so far on this silly issue. That's why I wanted use and that's why I'm thinking about [is_rat r]. But we've moved on from least upper bounds now, so next week I'll be fussing about something else :-) It was just some thoughts on how this part of my course was more difficult than I wanted it to be in Lean, and Bryan's post is another indication of this -- his original post in this thread is a clear indication that mathematicians find it difficult to work with this extra layer of difficulty when nat, rat and real all become different objects, because we are not used to thinking of them like this.

#### Mario Carneiro (Nov 22 2018 at 09:16):

arguably that is more like a newbie proof

#### Mario Carneiro (Nov 22 2018 at 09:17):

just lots of splitting and bashing

#### Kevin Buzzard (Nov 22 2018 at 09:17):

This simpa proof is my favourite so far. I still don't know what simpa does. Whenever I read the description I still get confused. First we simplify the hypotheses, then the conclusion using some hypotheses, then we look for the conclusion in the hypotheses, or something. Maybe I should work on my simpa understanding.

#### Kevin Buzzard (Nov 22 2018 at 09:18):

Thanks for the simpa proof. I will look at it.

#### Mario Carneiro (Nov 22 2018 at 09:20):

simpa using h simplifies h with the lemmas, then simplifies the goal using the lemmas, then applies assumption to match h with the goal

#### Mario Carneiro (Nov 22 2018 at 09:20):

here I never said to use h, so it actually just simplified the goal and then applied assumption

#### Mario Carneiro (Nov 22 2018 at 09:21):

so it is identical to simp; assumption in this case

#### Patrick Massot (Nov 22 2018 at 12:06):

@Kevin Buzzard I'm not sure I understand what you want. It seems to me that

theorem rationals_unbounded (r : ℝ) : ∃ s : ℚ, r < s :=
begin
rcases exists_nat_gt r with ⟨n, _⟩,
use n,
simpa
end


#### Patrick Massot (Nov 22 2018 at 12:53):

I played a bit with your ideas and, of course, I don't have a really nice answer. Something not too bad that may be worth thinking about:

import data.real.basic

@[class] def is_rat (r : ℝ) : Prop := ∃ q : ℚ, r = q

instance nat_is_rat (n : ℕ) : is_rat n := ⟨n, by simp⟩

meta def come_on : tactic unit := [repeat { assumption <|> apply_instance <|> split}]

theorem rationals_unbounded (r : ℝ) : ∃ s : ℝ, is_rat s ∧ r < s :=
begin
cases exists_nat_gt r with n H,
use n,
come_on
end


#### Patrick Massot (Nov 22 2018 at 12:54):

I'm a bit disappointed that none of our general purpose automation tactic seem to be able to replace my ad hoc one.

#### Kevin Buzzard (Nov 22 2018 at 13:34):

Because none of them ask type class inference for any help? Surely the type class system is supposed to fix these problems before the user sees them?

#### Kevin Buzzard (Nov 22 2018 at 13:34):

I guess the challenge now is to prove Bryan's lemma using his proof strategy!

#### Kevin Buzzard (Nov 22 2018 at 13:38):

Of course it's a theorem about a rational number x with [is_nat x] or [is_int x] (changing the choice should not change the proof at all) and the hypothesis x ge 4. Ideally no actual nats should show up in the proof at all other than those buried in the typeclass system

#### Kevin Buzzard (Nov 22 2018 at 13:39):

That's the question. I shouldn't be telling Bryan "don't use rat" -- we should be making rat easier to use in this context.

#### Kevin Buzzard (Nov 22 2018 at 13:39):

Because that's what mathematicians do instinctively

#### Scott Morrison (Nov 24 2018 at 08:24):

Blech, dealing with inequalities is so awful. :-) I have been avoiding it for a long time!

#### Scott Morrison (Nov 24 2018 at 08:24):

lemma le_pred_of_lt {n m : ℕ} (h : n < m) : n ≤ m - 1 := sorry

#### Scott Morrison (Nov 24 2018 at 08:28):

ok...

lemma le_pred_of_lt {n m : ℕ} (h : n < m) : n ≤ m - 1 :=
pred_le_pred (succ_le_of_lt h)
`

#### Kevin Buzzard (Nov 24 2018 at 09:11):

One reason this is annoying is that it's the CS minus there, which doesn't behave as nicely as our minus

#### Kenny Lau (Nov 24 2018 at 09:13):

I think the horse is long dead...

#### Kevin Buzzard (Nov 24 2018 at 09:36):

I'm just saying that one reason it's hard is that nat minus is poorly behaved, you're in a situation where (a-b)+b isn't a and this will surely make automation harder to write.

#### Kevin Buzzard (Nov 24 2018 at 09:36):

All the lemmas you need should be there somewhere -- the library does a really good job of being complete. Don't forget to import data.nat.basic .

#### Mario Carneiro (Nov 24 2018 at 09:42):

in a lot of ways, automation for nat subtraction is similar to automating stuff involving division - you have well definedness conditions that are generated by your statement and they have to be maintained when you rewrite the expression

#### Kevin Buzzard (Nov 24 2018 at 09:46):

Yes, that's an insightful comment. Mathematicians know that dividing by zero is something one "never does" so we're always prepared to supply that proof that the denominator is non-zero. But it's easy for us to forget the corresponding precondition for nat subtraction, because nat subtraction just doesn't exist in maths. You define division to be random where we don't define it, but you define nat subtraction to be the wrong thing when we have a perfectly good answer which just happens to be a number which is not a nat.

Last updated: May 16 2021 at 20:13 UTC