## Stream: new members

### Topic: partial transitivity

#### Lucas Viana (May 25 2020 at 00:23):

I know what the transitivity tactic does, but I want a weaker version of it: if I have a goal a < c, how can I split it into two goals a ≤ b and b < c?

#### Kevin Buzzard (May 25 2020 at 00:24):

lt_of_le_of_lt

#### Lucas Viana (May 25 2020 at 00:26):

Wouldn't it be handy if there was a tactic like transitivity for that?

#### Kevin Buzzard (May 25 2020 at 00:27):

How would the tactic know whether you want to reduce to $a\leq b$ and $b, or to $a and $b\leq c$?

#### Lucas Viana (May 25 2020 at 00:28):

Two tactics! Or some way to toggle between them

#### Kevin Buzzard (May 25 2020 at 00:28):

Is apply lt_of_le_of_lt really that much trouble?

#### Alex J. Best (May 25 2020 at 00:28):

You could use a calc for this, iirc it supports doing

calc a \le b : by blah
... < c : by blah2


#### Kevin Buzzard (May 25 2020 at 00:29):

If a \le b and b < c are already in the context (i.e. are assumptions) then the linarith tactic will solve a<c.

#### Lucas Viana (May 25 2020 at 00:30):

Kevin Buzzard said:

Is apply lt_of_le_of_lt really that much trouble?

how can I make it use b instead of dummy?m_1?

#### Kevin Buzzard (May 25 2020 at 00:31):

Either tell it b using @ or tell it one of the proofs.

#### Lucas Viana (May 25 2020 at 00:47):

Sorry, I tried and searched around but I just don't know how to use @ :oh_no:

#### Lucas Viana (May 25 2020 at 00:48):

Search engines are not very friendly of symbols, and searching for at symbol did not give me much

#### Lucas Viana (May 25 2020 at 00:51):

I would find it nice if I could split it into two goals, but I may end up proving everything before and applying lt_of_le_of_lt then

#### Kevin Buzzard (May 25 2020 at 00:52):

If you post me an example, I'll post a solution

#### Kevin Buzzard (May 25 2020 at 00:52):

#tpil will tell you all about tricks like @

#### Kevin Buzzard (May 25 2020 at 00:55):

For some reason, @ seems to be explained in section 6.2

#### Lucas Viana (May 25 2020 at 00:56):

Kevin Buzzard said:

If you post me an example, I'll post a solution

I know how to prove it with apply, I was just wondering if I could use it to split the goal into two goals where the b is a variable I have around, like the transitivity tactic

#### Kevin Buzzard (May 25 2020 at 00:56):

I know, and I'm challenging you to turn it into a little two-line example

#### Kevin Buzzard (May 25 2020 at 00:56):

which I'll then show you how to solve

#### Lucas Viana (May 25 2020 at 00:57):

Kevin Buzzard said:

For some reason, @ seems to be explained in section 6.2

Thank you, if I just search for @ in the search box it gives me no results :(

#### Kevin Buzzard (May 25 2020 at 00:57):

The skill of knocking up little minimal working examples is a really important one; it helps people learn to ask much better questions

#### Lucas Viana (May 25 2020 at 01:03):

lemma blah (a b c : ℝ) (a ≤ b) (b < c) : a < c :=
begin
apply lt_of_le_of_lt, -- split into two goals?
end


#### Lucas Viana (May 25 2020 at 01:03):

I know it is stupid to split into two goals here, I'm just asking if it is possible

#### Kevin Buzzard (May 25 2020 at 01:04):

This one is too easy -- you already have the inequalities you want so you can do

import data.real.basic

lemma blah (a b c : ℝ) (h1 : a ≤ b) (h2 : b < c) : a < c :=
begin
exact lt_of_le_of_lt h1 h2,
end


#### Kevin Buzzard (May 25 2020 at 01:05):

This is the example you want:

import data.real.basic

lemma blah (a b c : ℝ) : a < c :=
begin
sorry
end


#### Reid Barton (May 25 2020 at 01:05):

You can use the calc block from above with the parts after the :s replaced by _s, and they will make new goals

#### Kevin Buzzard (May 25 2020 at 01:06):

import data.real.basic

lemma blah (a b c : ℝ) : a < c :=
begin
apply @lt_of_le_of_lt _ _ _ b,
repeat {sorry},
end


#### Jeremy Avigad (May 25 2020 at 01:06):

For the @ symbol, see also the end of Section 2.9 (https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#implicit-arguments).

#### Lucas Viana (May 25 2020 at 01:13):

Following @Reid Barton advice, I think this is the most elegant way to do it:

lemma blah (a b c : ℝ) : a < c :=
begin
calc a ≤ b : _
... < c : _,
-- Two goals!
repeat { sorry }
end


#### Bryan Gin-ge Chen (May 25 2020 at 01:15):

Writing calc blocks that create multiple goals can be confusing, since it may not be clear which of the new goals is currently active unless you write show.

#### Kevin Buzzard (May 25 2020 at 01:16):

Of course you can just prove the goals along the way :-)

#### Yury G. Kudryashov (May 25 2020 at 03:24):

My 5¢: it would be nice to have an optional (keyword?) argument to transitivity that will allow me to write

transitivity b with (≤) (<),


#### Yury G. Kudryashov (May 25 2020 at 03:26):

But this "nice" is not "nice" enough for me to dig into the source of transitivity.

#### Bryan Gin-ge Chen (May 25 2020 at 04:03):

Maybe a mathlib issue?

#### Mario Carneiro (May 25 2020 at 04:18):

You can also write

import data.real.basic

lemma blah (a b c : ℝ) : a < c :=
begin
apply lt_of_le_of_lt (_ : _ <= b),
end


or variations with more or less explicitness

Last updated: May 14 2021 at 22:15 UTC