trans attribute

Stream: mathlib4

[Kevin Buzzard]

In Mathlib4,

@[trans]
theorem trans_left (hab : TransGen r a b) (hbc : ReflTransGen r b c) : TransGen r a c := by

gives me an error:

 @[trans] attribute only applies to lemmas proving x ∼ y → y ∼ z → x ∼ z, got ∀ {α : Type u_1} {r : α → α → Prop}
  {a b c : α}, TransGen r a b → ReflTransGen r b c → TransGen r a c

The issue here is that it's not the same relation being used three times, but two relations are involved. In Lean 3 it looks like we could be more liberal with our trans tagging -- IIRC this was the trick that made calc allow things like a < b ... <= c ..., because lt_of_lt_of_le What do I do here? I'm in no position to make trans work more generally, but am I missing an import which does this, and if not then should I just add a TODO or open an issue or what?

[Kevin Buzzard]

PS my imports are

import Mathlib.Tactic.Basic
import Mathlib.Logic.Relator
import Mathlib.Init.Propext
import Mathlib.Tactic.Relation.Rfl
import Mathlib.Tactic.Use
import Mathlib.Tactic.LibrarySearch

[Mario Carneiro]

Note that calc doesn't use the @[trans] attribute anymore, it uses the Trans typeclass which does allow non-uniform relations

[Mario Carneiro]

the @[trans] attribute is only used by the trans tactic (previously transitivity) which does require uniform relations since it has to make something up for the subgoals

[Mario Carneiro]

so you can just not tag it as @[trans] and add a Trans instance instead

[Kevin Buzzard]

If I have a relation which is transitive and I prove this and attach @[trans], should the system automatically make the Trans instance?

[Mario Carneiro]

it could (and probably should). It doesn't right now

[Yury G. Kudryashov]

@Mario Carneiro @Siddhartha Gadgil , could you please expand docs on this attribute / trans tactic? Namely, how does it interact with Trans class?

[Yury G. Kudryashov]

E.g.,

• Does it create a Trans instance?
• Does it use Trans instances?

I mean, is it enough to have one of @[trans]/Trans? If yes, which one?

[Siddhartha Gadgil]

I'll check and document, but the intention is that it uses the Trans class

[Yury G. Kudryashov]

Then we can drop some @[trans] attrs.

[Yury G. Kudryashov]

At least after I add an instance [IsTrans α r] : Trans r r r.

[Yury G. Kudryashov]

IMHO, we should either drop @[trans] or make it generate a Trans instance instead of using its own data.

[Yury G. Kudryashov]

Because in mathlib3, @[trans] was used both by trans and calc.

[Yury G. Kudryashov]

Then trans tactic can be just apply IsTrans.trans.

[Siddhartha Gadgil]

I agree that in principle a better design will be to have @[trans] generate a Trans instance and having the trans tactic use Trans classes only. The one thing to be wary off is that there may be instances of @[trans] labelled lemmas that do not have a corresponding Trans class. In lean 3 the attributes sym and trans could be applied very liberally.

[Yury G. Kudryashov]

Any specific examples that work with Lean 3 calc?

[Siddhartha Gadgil]

I don't know examples. I have to think through this: figure out what is needed to make a Trans instance and then see if adding these breaks any @[trans] labels.

[Siddhartha Gadgil]

I just checked the definition of the Trans class and using one way is not that easy, and I do not know if it is even valid in all cases. The issue is that in many cases @[trans] is applied to a family of transitivity relations. So we will have to map to a similar family of instances, which will take some work. And, as I mentioned, there is no check in mathlib that the attribute is only applied to families of a certain shape.

Initially I had assumed that symm and trans attributes were only for the standard shapes and this led to errors during the port, i.e., the test while adding the attribute failing (which was not desired). As I said, one can try to add a parametrized collection of Trans instances for the attribute and give an error if this fails. But as this is a bit fiddly, if the present dual approach is not harmful we should consider living with it.