## Stream: new members

### Topic: Basic inequalities

#### Emiel Lanckriet (Jul 16 2020 at 14:51):

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 (Jul 16 2020 at 14:59):

Try linarith.

import tactic
import data.real.basic

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


#### Ruben Van de Velde (Jul 16 2020 at 15:31):

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 (Jul 16 2020 at 15:31):

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 (Jul 16 2020 at 15:32):

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 (Jul 16 2020 at 15:33):

@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 (Jul 16 2020 at 15:35):

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 (Jul 16 2020 at 15:37):

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

#### Dan Stanescu (Jul 16 2020 at 15:42):

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 (Jul 18 2020 at 08:56):

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 (Jul 18 2020 at 09:09):

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

#### Markus Himmel (Jul 18 2020 at 09:16):

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 (Jul 18 2020 at 09:19):

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 (Jul 18 2020 at 09:19):

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

#### Scott Morrison (Jul 18 2020 at 09:20):

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 (Jul 18 2020 at 09:25):

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

#### Emiel Lanckriet (Jul 18 2020 at 09:35):

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 (Jul 18 2020 at 09:53):

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 (Jul 18 2020 at 09:55):

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

#### Markus Himmel (Jul 18 2020 at 09:56):

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 (Jul 18 2020 at 09:57):

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

#### Emiel Lanckriet (Jul 18 2020 at 09:59):

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 (Jul 18 2020 at 10:00):

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

#### Kevin Buzzard (Jul 18 2020 at 10:28):

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

#### Mario Carneiro (Jul 18 2020 at 17:27):

I find .1 and .2 easier to remember

Last updated: Dec 20 2023 at 11:08 UTC