## Stream: general

### Topic: transitivity

#### Johan Commelin (May 18 2019 at 05:11):

Could the transitivity tactic be enhanced, so that (here ≤ could be any transitive relation) if I have foo : b ≤ c and the goal is a ≤ c, then transitivity foo turns the goal into a ≤ b?
In other words, this could be a more readable version of refine le_trans _ foo.

#### Mario Carneiro (May 18 2019 at 05:49):

but what if you wanted to prove a <= foo and foo <= c instead? :P

#### Johan Commelin (May 18 2019 at 06:57):

Sorry, I don't understand what you mean...

#### Johan Commelin (May 18 2019 at 06:57):

The tactic could inspect the type of foo and be smart, right?

#### Johan Commelin (May 18 2019 at 06:58):

If foo is a Prop do what I suggest, if foo has the same type as a and c, do what Mario says (i.e. what it currently does).

#### Kevin Buzzard (May 18 2019 at 09:28):

If you have h1: b<=c and h2: d<=c and the goal is a<=c, then what? ;-)

#### Johan Commelin (May 18 2019 at 11:39):

I don't understand what the problem is here.... you would either write transitivity h1 or transitivity h2 depending on which one you want to use. I'm not asking for any automation here.

#### Reid Barton (May 18 2019 at 11:46):

transitivity e already means something (use e as the middle expression), but perhaps transitivity using e?

#### Johan Commelin (May 18 2019 at 11:47):

That would also work, yes.

#### Johan Commelin (May 18 2019 at 11:47):

I know that transitivity e already means something. But I thought that the tactic could nevertheless be smart, depending on the type of e. But your suggestion is even better

#### Simon Hudon (May 25 2019 at 14:05):

Has anyone noticed transitivity acting strange sometimes? Sometimes, I want to prove a ≤ b and transitivity will fail because it doesn't match ? ≤ ? -> ? ≤ ? -> ? ≤ ?. Right now, I'm working on a semilattice_inf_bot. Could it be a type class issue?

#### Koundinya Vajjha (May 25 2019 at 14:07):

I faced this issue yesterday.

#### Simon Hudon (May 25 2019 at 14:14):

Did you manage to solve it?

#### Koundinya Vajjha (May 25 2019 at 14:20):

No I couldn't figure it out so I just worked around it.

#### Simon Hudon (May 25 2019 at 14:22):

I'm thinking it might have something to do with apply. It manages to find the right lemma but then applying it goes wrong. If you replace transitivity with apply le_trans (or the appropriate lemma) does it also fail?

#### Koundinya Vajjha (May 25 2019 at 14:24):

apply le_trans fails, but convert le_trans _ _ seems to match something

#### Koundinya Vajjha (May 25 2019 at 14:24):

Which makes me think it's a type class issue?

#### Simon Hudon (May 25 2019 at 14:26):

refine le_trans _ _ would probably work too and apply le_trans _ _ also.

#### Koundinya Vajjha (May 25 2019 at 14:27):

yes they both work.

#### Simon Hudon (May 25 2019 at 14:27):

I'm thinking it has to do with type classes because le_trans is probably the most used transitivity lemma and people seem to be able to use it via transitivity pretty well in mathlib

#### Mario Carneiro (May 25 2019 at 14:31):

sounds like the apply bug

#### Mario Carneiro (May 25 2019 at 14:32):

is your <= definitionally a pi?

#### Koundinya Vajjha (May 25 2019 at 14:33):

it's the le on ennreal...

#### Mario Carneiro (May 25 2019 at 14:35):

which comes from with_top which is a pi

#### Simon Hudon (May 25 2019 at 14:35):

mine is the subset relation

Oh!

#### Simon Hudon (May 25 2019 at 14:36):

Do you have a fix for that?

#### Koundinya Vajjha (May 25 2019 at 14:36):

what does that mean?

#### Simon Hudon (May 25 2019 at 14:38):

The type of your lemma may look like: ? ≤ ? -> ? ≤ ? -> ? ≤ ? which would suggest that the head of the type is ? ≤ ? but that part is a pi too so you can keep applying arguments to it and apply does

#### Mario Carneiro (May 25 2019 at 14:38):

https://github.com/leanprover-community/mathlib/blob/master/src/order/bounded_lattice.lean#L503

#### Kevin Buzzard (May 25 2019 at 14:45):

sounds like the apply bug

What's "the apply bug"? Someone mentioned this the other day. The bug itself has passed me by though.

#### Mario Carneiro (May 25 2019 at 14:46):

It's stymied things like apply continuous.comp in the past

#### Mario Carneiro (May 25 2019 at 14:47):

basically apply foo gives an error even if foo applies, but the consequent of foo is a pi after completely reducing it

#### Kevin Buzzard (May 25 2019 at 14:48):

https://github.com/leanprover-community/mathlib/blob/master/src/order/bounded_lattice.lean#L503

This fancy-schmancy definition could be replaced with a simple case split.

#### Simon Hudon (May 25 2019 at 14:49):

But then it would get ugly

#### Mario Carneiro (May 25 2019 at 14:49):

yeah I knew that this suggestion would come up

#### Kevin Buzzard (May 25 2019 at 14:49):

What's wrong with it?

#### Mario Carneiro (May 25 2019 at 14:49):

I really don't like the idea of lean bugs changing the way I write my definitions

For sure

#### Kevin Buzzard (May 25 2019 at 14:50):

but the case split definition sounds easier to work with to me

#### Mario Carneiro (May 25 2019 at 14:50):

it's one case vs 4

#### Simon Hudon (May 25 2019 at 14:51):

Case splits have a way of multiplying

#### Simon Hudon (May 25 2019 at 14:52):

If I make a apply and transitivity that do not suffer from the same problems, should I call them apply' and transitivity'?

#### Simon Hudon (May 25 2019 at 14:53):

I think ideally, it should be a flag in apply_cfg but I think it needs to go into mathlib until we officially switch to 3.5.*c

#### Mario Carneiro (May 25 2019 at 14:56):

or we could just fix the bug

#### Simon Hudon (May 25 2019 at 15:12):

I'm not sure Leo sees it as a bug. I remember him introducing the feature and it seemed to be what he actually intended

#### Simon Hudon (May 25 2019 at 15:13):

But we can change Lean 3.5.*c. Do we not want a fix until then?

#### Mario Carneiro (May 25 2019 at 15:32):

It's clearly computing something wrong - it is unfolding in two different ways at different times and messes up the expected arity

#### Mario Carneiro (May 25 2019 at 15:33):

also the unfolding of irreducible definitions is extremely suspicious, given the lengths that Leo has gone to thread reducibility args through all the tactics

#### Johan Commelin (Jul 11 2020 at 13:33):

Can we make transitivity smarter? Currently transitivity 0 fails if I have a goal that is not about nat. But lean knows exactly which 0 I mean, because the goal is something like @has_le.le R _ _ _, so I'm talking about 0 : R.

Last updated: Aug 03 2023 at 10:10 UTC