Basic inequalities

Stream: new members

[Emiel Lanckriet]

I want to show that y - x < e given abs(x - y) < e and x \leq y. I found a lemma

theorem abs_of_nonpos :
a ≤ 0 → abs a = -a

but I can't figure out how to get x - y \leq 0 from x \leq y.
Does anyone have any hints?

[Dan Stanescu]

Try linarith.

import tactic
import data.real.basic

example (x y : ℝ) (h : x - y ≤ 0) : x ≤ y := by linarith

[Ruben Van de Velde]

Other way around, I think, which can be solved with

example (x y : ℝ) (h : x ≤ y) : x - y ≤ 0 := sub_nonpos_of_le h

[Emiel Lanckriet]

Can you use linarith in the begin end-mode? Because each time I try it, the program seems to get stuck. When I make its own functions then it works.

[Ruben Van de Velde]

Alternatively,

example (x y : ℝ) (h : x ≤ y) : x - y ≤ 0 := by library_search

gives

Try this: exact sub_nonpos.mpr h

[Bryan Gin-ge Chen]

@Emiel Lanckriet Could you post an #mwe ? I don't know what you mean here:

Because each time I try it, the program seems to get stuck. When I make its own functions then it works.

[Dan Stanescu]

Emiel Lanckriet said:

Can you use linarith in the begin end-mode? Because each time I try it, the program seems to get stuck. When I make its own functions then it works.

Like this?

example (x y : ℝ) (h : x ≤ y) : x - y ≤ 0 :=
begin
    linarith, done
end

[Emiel Lanckriet]

Sorry, I must have wrongly identified the problem because I can't seem to reproduce it and the example works.

[Dan Stanescu]

Emiel Lanckriet said:

Sorry, I must have wrongly identified the problem because I can't seem to reproduce it and the example works.

No problem, remember to post minimal working examples:

https://leanprover-community.github.io/mwe.html

so we can help more effectively.

[Emiel Lanckriet]

Is there a function that has signature abs(x) < e -> x > 0 -> x < e? Also, is there a way to comb through mathlib using type signatures much like the searches you can do in Hoogle for Haskell commands?

[Eloi]

I have found #check (@abs_le ℤ _) I don't know if there is anything closer.

[Markus Himmel]

It looks like this function does not exist yet. Here is one way to write it:

lemma lt_of_abs_lt {α : Type*} [decidable_linear_ordered_add_comm_group α] {x e : α} : abs x < e → x < e :=
λ h, (abs_lt.mp h).right

[Scott Morrison]

If you state the result you want as an example library_search is often successful. (You can use library_search mid tactic block as well, but often it helps to state a cleaner version of the result you know you're after.)

[Scott Morrison]

There's also the #find command, but it's unusually pretty unsatisfactory.

[Scott Morrison]

The other strategy is to know the name ahead of time -- Markus's suggestion is pretty good. Using ctrl+space completion with the correct prefix is often useful.

[Kevin Buzzard]

This function has unused inputs so will be rejected by the maths linter :-) abs(x)<e -> x < e without any further assumptions.

[Emiel Lanckriet]

Kevin Buzzard said:

This function has unused inputs so will be rejected by the maths linter :-) abs(x)<e -> x < e without any further assumptions.

Ah, I see, thank you. I indeed made a mistake.

[Emiel Lanckriet]

Markus Himmel said:

It looks like this function does not exist yet. Here is one way to write it:

lemma lt_of_abs_lt {α : Type*} [decidable_linear_ordered_add_comm_group α] {x e : α} : abs x < e → x < e :=
λ h, (abs_lt.mp h).right

What does .mp mean in the solution? When I try it specifically for \R I get an error for this, I already found the solution in a slightly different way, but I was still wondering what .mp does.

[Markus Himmel]

mp converts an if-and-only-if to an implication from the left to the right side

[Markus Himmel]

What error do you get? The following works for me:

import data.real.basic

lemma lt_of_abs_lt {x e : ℝ} : abs x < e → x < e :=
λ h, (abs_lt.mp h).right

[Emiel Lanckriet]

It is probably because I tried to use the command in begin-end-mode.

[Markus Himmel]

If you post your code, I can help you fix it

[Emiel Lanckriet]

The problem I had before is gone, so now it works, thanks a lot for your help. I don't what I did wrong the first time, but it is apparently not a problem anymore.

[Scott Morrison]

mp is short for "modus ponens" if that helps you remember. (It doesn't help me. :-)

[Kevin Buzzard]

I like @Heather Macbeth 's take on it -- "iMPlies" :-)

[Mario Carneiro]

I find .1 and .2 easier to remember