Most convenient way to work with inequalities

Stream: new members

[Sabbir Rahman]

for inequalities that have only linear terms, linarith is the best weapon of choice. But what do in cases that involve multiplication or division of multiple variables. I find that I have to keep searching for the exact theorems and then use them. is there any better way, following are examples of situatio I am talking about

import Mathlib

variable (a b c : ℝ)

example (ha : 0 < a) (hb : 0 < b) : 0 < a * b := by sorry
example (h : a < b) (hc : 0 < c) : a * c < b * c := by sorry
example (h: a/c ≤ b/c) (hc: 0 < c) : a ≤ b := by sorry

-- and other similar

[Kevin Buzzard]

How does positivity do on these?

[Vasilii Nesterov]

Yes, for goals of the form 0 < something, the right choice is positivity (it repeatedly applies mul_pos, div_pos, etc.). For the second case, when you need to "cancel" something in the inequality, you can use gcongr. The last one can be solved with exact?.

[Kevin Buzzard]

The problem with exact? is that it's often the case that you're not presented with h and hc and a goal of a ≤ b, you have e.g. a hypothesis of (3t+2)/(1+x^2)<=(2t+3)/(1+x^2), the goal is something totally different, you want 3t+2<=2t+3, you know there will be an appropriate lemma, but you have to break out of your proof and write the exact line above and run exact? to get the name of the lemma and then go back in. Younger people can just memorise huge lists of lemmas but I find this really difficult to do, so I concentrate on learning the naming convention; a tactic is a much better solution because for slow people like me the workflow is so much easier.

[Sabbir Rahman]

Kevin Buzzard said:

How does positivity do on these?

I was not aware of positivity, thanks!

[Sabbir Rahman]

I agree with @Kevin Buzzard about exact. When I'm working on a proof in high level, it's not always that the situation is ideal for exact. So I have to write the lemma I'm searching for in a scratch file and use exact?. I also find it very difficult to remember theorems (even bad because the naming convention is still not natural to me). So tactics is the way I prefer, as they allow me to focus on higher level details.

[Sabbir Rahman]

Vasilii Nesterov said:

For the second case, when you need to "cancel" something in the inequality, you can use gcongr.

Thanks, I didn't know about gcongr either. gcongr easily handles second case, but I wouldn't call it a general solution. For example here, the example is actually that of inverting the direction due to negative multiplier. But gcongr expects goals b < a and 0 < c

import Mathlib

variable (a b c : ℝ)

example (h: a < b) (hc: c < 0) : a * c > b * c := by
    gcongr
    . sorry
    . sorry

[suhr]

Huge list of tactics could be replaced with a much smaller list of tactics + composition. Which is still annoying though, since it requires more thinking about minute details than necessary.

[Vasilii Nesterov]

Sabbir Rahman said:

Vasilii Nesterov said:

For the second case, when you need to "cancel" something in the inequality, you can use gcongr.

Thanks, I didn't know about gcongr either. gcongr easily handles second case, but I wouldn't call it a general solution. For example here, the example is actually that of inverting the direction due to negative multiplier. But gcongr expects goals b < a and 0 < c

import Mathlib

variable (a b c : ℝ)

example (h: a < b) (hc: c < 0) : a * c > b * c := by
    gcongr
    . sorry
    . sorry

Yes, there is no (at least efficient) general solution. gcongr just applies lemmas tagged with @[gcongr], and some of them have the assumption 0 < c instead of c < 0 because the former is more common.

[Vasilii Nesterov]

Sabbir Rahman said:

I agree with Kevin Buzzard about exact. When I'm working on a proof in high level, it's not always that the situation is ideal for exact. So I have to write the lemma I'm searching for in a scratch file and use exact?. I also find it very difficult to remember theorems (even bad because the naming convention is still not natural to me). So tactics is the way I prefer, as they allow me to focus on higher level details.

I use the following trick: if I feel some fact A can be derived from the current context using some library lemma, I write

have : A := by exact?

[Sabbir Rahman]

Vasilii Nesterov said:

I use the following trick: if I feel some fact A can be derived from the current context using some library lemma, I write

have : A := by exact?

I generally try apply? and when proofs are long, apply loses it's way and suggests irrelevant things. When I try apply? within a shorter example, that is better.