generalised distributivity in mathlib4

Stream: general

[Matthew Pocock]

I've been skimming through the sources for mathlib4. There seem to be an absolute ton of theorems of the form: G (F x y) ↔ F (G x) (G y) for some function-like things F and G. I get that there's a usability/maintainability/readability win in writing these out long-hand a lot of the time. However, is there a concept in the library of this relation between an F and G? Is there anything to be gained by treating this in the abstract rather than in all the individual special cases?

The types are obvious while we're using just the one, as in G: a→a and F: a×a→a, but otherwise I guess you need some typeclass trickery to summon the F, G that work where the LHS uses F: a×a→b, G: b→d and the RHS uses G: a→c, F: c×c→d. Distributive arrows? I'm guessing there's some monad/category thingies that do this? Perhaps it isn't a useful abstraction for authoring or tactically applying theorems.

[Jireh Loreaux]

Can you list some of the lemmas you're thinking of? It might help to have a few specific examples of the abstraction.

[Bolton Bailey]

Not OP but:

• docs#apply_ite
• docs#AddMonoidHom (the map_add' condition)
• docs#himp_inf_distrib
• docs#min_mul_distrib'

Really, most theorems with distrib in their name.

[Bolton Bailey]

The main thing I think about with distrib lemmas is that they are usually not simp lemmas, but that I bet sometimes there are simp calls that would close with particular distrib lemmas added to the simp set. OTOH, if we add @[simp] to these willy nilly, simp it would make a lot of other simp calls more complicated.

[Bolton Bailey]

My hope would be that a smarter search method like rw_search or aesop would be able to identify this kind of thing and make a good choice for how far to simplify.

[Yaël Dillies]

Bolton Bailey said:

The main thing I think about with distrib lemmas is that they are usually not simp lemmas, but that I bet sometimes there are simp calls that would close with particular distrib lemmas added to the simp set. OTOH, if we add @[simp] to these willy nilly, simp it would make a lot of other simp calls more complicated.

@Kyle Miller has a rule for which distributivity lemmas are fine to be tagged by simp: If the RHS contains no more occurrence of a free variable than the LHS, then it's a good simp lemma (or at least not obviously a bad one).

[Bolton Bailey]

docs#List.replicate_add another example

[Bolton Bailey]

This is a case where I'd actually like the symm of the lemma to be @[simp] @Yaël Dillies , what are the criteria for that?

[Bolton Bailey]

(That is, if the are multiple occurences in the RHS, when should we symm the lemma and simp tag it?)

[Yaël Dillies]

None that I can think of. If you add replicate a m ++ replicate a n = replicate a (m + n) as a simp lemma then you also need to add replicate a n ++ [a] = replicate a (n + 1), [a] ++ replicate a n = replicate a (1 + n), etc... The problem with making a reverse distributivity lemma simp is that you also need to add a lemma for each possible simplification of each summand, in order to preserve confluence.

[Yaël Dillies]

If you really want it to be simp, I'd suggest tagging it simp locally to the file, or putting it in a custom simp set.

[Bolton Bailey]

Ok, I won't tag it then

[Eric Wieser]

Just to note that #7323 is related to this comment about replicate_add