partial transitivity

Stream: new members

[Lucas Viana]

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]

lt_of_le_of_lt

[Lucas Viana]

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

[Kevin Buzzard]

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

[Lucas Viana]

Two tactics! Or some way to toggle between them

[Kevin Buzzard]

Is apply lt_of_le_of_lt really that much trouble?

[Alex J. Best]

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

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

[Kevin Buzzard]

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]

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]

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

[Lucas Viana]

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

[Lucas Viana]

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

[Lucas Viana]

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]

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

[Kevin Buzzard]

#tpil will tell you all about tricks like @

[Kevin Buzzard]

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

[Lucas Viana]

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]

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

[Kevin Buzzard]

which I'll then show you how to solve

[Lucas Viana]

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]

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]

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]

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

[Kevin Buzzard]

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]

This is the example you want:

import data.real.basic

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

[Reid Barton]

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]

import data.real.basic

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

[Jeremy Avigad]

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]

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]

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]

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

[Yury G. Kudryashov]

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]

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

[Bryan Gin-ge Chen]

Maybe a mathlib issue?

[Mario Carneiro]

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