Zulip Chat Archive

Stream: new members

Topic: partial transitivity


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 25 2020 at 00:24):

lt_of_le_of_lt

view this post on Zulip Lucas Viana (May 25 2020 at 00:26):

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

view this post on Zulip Kevin Buzzard (May 25 2020 at 00:27):

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

view this post on Zulip Lucas Viana (May 25 2020 at 00:28):

Two tactics! Or some way to toggle between them

view this post on Zulip Kevin Buzzard (May 25 2020 at 00:28):

Is apply lt_of_le_of_lt really that much trouble?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 25 2020 at 00:31):

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

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 25 2020 at 00:52):

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

view this post on Zulip Kevin Buzzard (May 25 2020 at 00:52):

#tpil will tell you all about tricks like @

view this post on Zulip Kevin Buzzard (May 25 2020 at 00:55):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 25 2020 at 00:56):

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

view this post on Zulip Kevin Buzzard (May 25 2020 at 00:56):

which I'll then show you how to solve

view this post on Zulip 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 :(

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 25 2020 at 01:16):

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

view this post on Zulip 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 () (<),

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (May 25 2020 at 04:03):

Maybe a mathlib issue?

view this post on Zulip 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