transitivity

Stream: general

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

That would also work, yes.

[Johan Commelin]

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]

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]

I faced this issue yesterday.

[Simon Hudon]

Did you manage to solve it?

[Koundinya Vajjha]

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

[Simon Hudon]

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]

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

[Koundinya Vajjha]

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

[Simon Hudon]

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

[Koundinya Vajjha]

yes they both work.

[Simon Hudon]

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]

sounds like the apply bug

[Mario Carneiro]

is your <= definitionally a pi?

[Koundinya Vajjha]

it's the le on ennreal...

[Mario Carneiro]

which comes from with_top which is a pi

[Simon Hudon]

mine is the subset relation

[Simon Hudon]

Oh!

[Simon Hudon]

Do you have a fix for that?

[Koundinya Vajjha]

what does that mean?

[Simon Hudon]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

But then it would get ugly

[Mario Carneiro]

yeah I knew that this suggestion would come up

[Kevin Buzzard]

What's wrong with it?

[Mario Carneiro]

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

[Kevin Buzzard]

For sure

[Kevin Buzzard]

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

[Mario Carneiro]

it's one case vs 4

[Simon Hudon]

Case splits have a way of multiplying

[Simon Hudon]

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

[Simon Hudon]

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]

or we could just fix the bug

[Simon Hudon]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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.