reassoc_of

Stream: mathlib4

[Joël Riou]

In category theory, we already have the reassoc tag in mathlib4. In mathlib, we also had the very convenient reassoc_of which translated a statement h : f = g into reassoc_of h : f ≫ _ = g ≫ _, and this was used in rewrites. Is there a hope that we may have the same in mathlib4? Is there a preferred way around this for the port? (e.g. using the slice tactic).

[Matthew Ballard]

I’ve been working around it but don’t have anything that I am happy with atm. I might just break down and implement reassoc_of

[Junyan Xu]

It would be nice to make it work for associative operations on a type ((*) in a semigroup, (+) in an add_semigroup, etc.). And maybe it can also be made to work for docs#function.comp, docs#linear_map.comp, docs#equiv.trans, etc.

[Matthew Ballard]

I am not sure how feasible something that unifies everything is at the moment. It would require some HAssoc class I think.

I did look a little at this but don't know the Lean 4 spelling of unify

[Thomas Murrills]

Is it just isDefEq? (Based on the doc strings I’d guess is_def_eq is now withNewMCtxDepth then isDefEq)

[Matthew Ballard]

I tried that though perhaps not correctly.

[Thomas Murrills]

Did you run into a specific issue with it? (I know there’s an issue where it won’t assign metavariables whose type is a Prop, just wondering if it’s that)

[Matthew Ballard]

Ah it could be that

[Thomas Murrills]

lean4#2054

[Matthew Ballard]

Specifically derive_reassoc_proof here is used in reassoc_of to get Lean to pass the equality directly to prove_reassocwhen generating the declaration.

[Matthew Ballard]

There may be a better way now in Lean 4 to generate declarations dynamically using tactics though

[Matthew Ballard]

I wouldn't know

[Eric Wieser]

#15738 uses the same strategy as reassoc_of, so I'd also be interested in knowing if there's a better pattern available

[Eric Wieser]

Does the existing pattern at least work in lean 4?

[Matthew Ballard]

If we can't unify with Prop, then I am skeptical

[Matthew Ballard]

Once I finish with abelian categories, I'll take another run at it

[Scott Morrison]

@Joël Riou, I've added the term elaborator in lean4#2765. Note I've called it reassoc_of%, in line with our naming for other term elaborators, although I don't feel strongly about this.

[Matthew Ballard]

Well, that was easy :)

[Scott Morrison]

That's what happens when tactics are written with their MetaM versions factored out. :-)

[Joël Riou]

Thanks very much @Scott Morrison !