Reordering arguments of `Set.EqOn`

Stream: mathlib4

[Scott Morrison]

I'm wondering how people would feel about reordering the arguments of Set.EqOn, so the set comes before the function.

(Presumably, but not necessarily, we would want to make the same change to all the "functions on sets" predicates in file#Data/Set/Function.)

[Scott Morrison]

We're currently refactoring the trans tactic, and a cleanup proposed by @Kyle Miller doesn't like

@[trans]
theorem EqOn.trans (h₁ : EqOn f₁ f₂ s) (h₂ : EqOn f₂ f₃ s) : EqOn f₁ f₃ s := fun _ hx =>
  (h₁ hx).trans (h₂ hx)

because the s comes after the variables that trans is paying attention to.

Similarly there's a porting note just above, that @[refl] already doesn't like

theorem eqOn_refl (f : α → β) (s : Set α) : EqOn f f s := fun _ _ => rfl

This in itself isn't a reason to change the order --- I'm sure we can make the trans tactic more flexible to cope with things like this (although it would be nice if we didn't need to).

[Scott Morrison]

But it seems to me like all these functions would be more natural with the function coming last: they are all intended as predicates on functions, not predicates on sets.

[Kyle Miller]

One thing about the refactor is that it's putting more consistency checking into the @[trans] attribute -- I don't believe the current trans tactic is able to apply EqOn.trans due to the argument order anyway.

[Thomas Murrills]

Oh, btw: I also have an old branch that refactors rfl, symm, and trans! Specifically it handles reducible heads, but I also rewrote a bunch of trans in the process. (I wasn’t totally happy with where it was, and haven’t had the time to clean it up lately, so, not all choices endorsed.) If any of it is useful, it’s over at rfl-symm-trans-enhance—it also wouldn’t like EqOn.trans, though. :)

[Yaël Dillies]

I agree those arguments order inconsistencies are annoying. I am in favour of having it be set then function.

[Eric Rodriguez]

Option two - should it be Function.EqOn s?

[Eric Rodriguez]

Or does that not help the trans etc situation

[Eric Wieser]

Does the docs#Trans class work with the existing definition?

[Scott Morrison]

No, I tried that already.

[Eric Wieser]

Eric Rodriguez said:

Option two - should it be Function.EqOn s?

I think this will be more annoying for stating equality of morphisms on a set, as there dot notation won't work

[Eric Rodriguez]

that should be fixed instead of just working around it relentlessly

[Eric Rodriguez]

but it is a real shame about dot notation

[Eric Rodriguez]

it just lines up with how i'd write it on paper maths

[Scott Morrison]

I think reordering the arguments is the immediately available improvement. Is there anyone interested in doing that? I probably won't in the near future, and will just proceed with the refactoring of trans without worrying about getting it working with EqOn.

[Kyle Miller]

Eric Wieser said:

Does the docs#Trans class work with the existing definition?

I'm guessing you suggested this because trans has some support for the Trans class. Something that trans needs to be able to do is take the target expression p : Prop, identify the LHS and RHS from it, and then synthesize a p' and a p'' from p where the RHS of p' and the LHS of p'' have been replaced by a new intermediate value. The trans tactic assumes the last two explicit arguments in p are the LHS and RHS, but presumably this could be configured.

If there are examples that justify the need to have arguments that come after a LHS and RHS, it might be worth building this configuration infrastructure, but otherwise I think it's cleaner and easier to reorder arguments.

[Eric Wieser]

The obvious candidate is docs#MulEquiv, where morally the interesting LHS and RHS are not the last ones

[Eric Wieser]

(Though as it happens, Trans can still be made to work for that type)

[Kyle Miller]

@Eric Wieser I wasn't clear, I meant explicit arguments coming after the LHS and RHS. The implicit arguments to MulEquiv are the kind that (the refactoring of) trans can handle.

[Eric Wieser]

Does the code in #6509 still work after this refactor?

[Kyle Miller]

I don't think it affects #6509 at all since the refactor is just for the trans tactic and the @[trans] attribute, which doesn't touch the Trans class or the calc expression

[Kyle Miller]

By the way, the heuristic I added is that a relation is something of the form

(r ... any arguments ...) ... implicit arguments that LHS xor RHS depends on ... (LHS) ... implicit arguments ... (RHS) ... implicit arguments

Calling the three parenthesized expressions are R, LHS, and RHS, it checks that R LHS RHS can be elaborated (using mkAppM'), and when it applies @[trans] lemmas it swaps out values for LHS and RHS.

If you're wondering about the implicit arguments before LHS, this is to support relations like docs#HEq, even if it had both of its implicit type arguments come before the explicit arguments.

[Thomas Murrills]

I think that’s one major difference between our refactors: I eschew mkAppM' entirely, use forallMetaTelescope on the applied lemma, and rely on the isDefEq check between the resulting target type and the goal type to assign the mvars, without decomposing and recomposing the relation.

(Then I just extract the last two explicit arguments of the (type of the) R y z hypothesis to get ?y and either assign it or add it to the tactic state. I also extract the last two explicit arguments of the return type and the R x y hypothesis for consistency checking in the attribute, but not in the tactic itself.)

While in this case it seems like the best option is just to change EqOn, the non-mkAppM' approach might be more flexible in handling both implicit and explicit arguments in general. Also, we then don’t need to re-synthesize any instance arguments to the relation—we just get them by unification with the goal. But maybe there are caches helping with this anyway, I’m not sure.

Also, this approach only actually needs to use the relation-like nature of the target to extract y; this means one could easily, if required, instead just figure out the index at which y occurs as an argument to the lemma and store it in the extension data (e.g. via @[trans x y z], where x and z are only used during the consistency check and don’t need to be stored in any way); then we can get ?y by index from the array returned by forallMetaTelescope directly.

Anyway, just mentioning this approach in case it’s useful. :)

[Yaël Dillies]

Scott Morrison said:

I think reordering the arguments is the immediately available improvement. Is there anyone interested in doing that?

I'm happy to do it.

[Scott Morrison]

In the meantime I've made #7285 which just removes the (currently useless) @[trans] tag on EqOn.trans. It can be restored after the refactor discussed above (at which point it will actually have effect).