fun_prop for finite (multiplicative) support?

Stream: mathlib4

[Michael Stoll]

Context

I'm currently adding material on heights in arithmetic geometry to Mathlib (BTW, a review of #34330 would be very welcome...). The definition of the height involves a docs#finprod, and so in several places I have to deal with side goals of the form f.mulSupport.Finite (where f is some function). These goals can usually be easily proved by combining lemmas like docs#Set.Finite.subset or docs#Set.Finite.union with results expressing or bounding the docs#Function.mulSupport of some more complicated function in terms of the mulSupports of its constituents. This looks like something that one should be able to automate fairly easily, and the fun_prop framework seems to be the canonical choice for that.

Proposal

So I would like to extend fun_prop so that it can deal with these goals.

I don't think that fun_prop can be made to work with a composed predicate like fun f ↦ f.mulSupport.Finite, so one first has to define a dedicated predicate like

namespace Function

variable {α M : Type*} [One M]

/-- The function `f` has finite multiplicative support. -/
@[to_additive (attr := fun_prop)]
def HasFiniteMulSupport (f : α → M) : Prop := f.mulSupport.Finite

and then prove various lemmas using this predicate, e.g.,

@[to_additive (attr := fun_prop)]
lemma hasFiniteMulSupport_mul {M : Type*} [MulOneClass M] (f g : α → M)
    (hf : HasFiniteMulSupport f) (hg : HasFiniteMulSupport g) :
    HasFiniteMulSupport fun a ↦ f a * g a :=
  (hf.union hg).subset <| mulSupport_mul ..

This can fairly easily be done; see FiniteMulSupport.lean in the Heights repo.

But to reap the benefits, one then needs to replace all assumptions of the form f.mulSupport.Finite in Mathlib by f.HasFiniteMulSupport (loogle finds 37 for mulSupportand 55 for support). (One could perhaps even think of using by fun_prop as the default for these.)

Question

Would such an addition and change be welcome? If this is the case, I'll prepare a PR.

[Michael Stoll]

Michael Stoll said:

Would such an addition and change be welcome?

:ping_pong:

I think this would be helpful for my use case, but wouldn't want to spend time and energy to implement it when the maintainers think it's not wanted.

[Artie Khovanov]

If you don't want to do this refactor you could instead make a custom aesop ruleset.

[Jakub Nowak]

Can aesop "split" functions like fun_prop does?

[Artie Khovanov]

what do you mean by "split", sorry? If you have something like

theorem add_mulSupport_finite (hf : f.mulSupport.finite) (hg : g.mulSupport.finite) : (f + g).mulSupport.finite

you can tag it aesop 90% (or even aesop safe if you disable it downstream)

to do the thing I think you want it to do

see the SetLike aesop ruleset for an example

[Jakub Nowak]

I meant something like that but looks like it works with aesop too:

import Mathlib

variable {f g h : α → α} [Ring α]

@[aesop safe]
theorem add_mulSupport_finite (hf : f.mulSupport.Finite) (hg : g.mulSupport.Finite) : (fun x => f x + g x).mulSupport.Finite := by sorry

@[aesop safe]
theorem id_mulSupport_finite (hf : f.mulSupport.Finite) (hg : g.mulSupport.Finite) : (fun x : α => x).mulSupport.Finite := by sorry

example (hf : h.mulSupport.Finite) : (fun x => h x + h x + x).mulSupport.Finite := by
  aesop

Here, when applying add_mulSupport_finite Lean has to come up to use f = fun x => h x + h x and g = fun x => x. I thought that it was some special behaviour of fun_prop that it can do that. Though now I see that it is not the case, because even apply add_mulSupport_finite can do that.

[Michael Stoll]

I think the question is rather whether aesop can do it without adding extra API lemmas for _.mulSupport.Finite. I should experiment a bit to see whether it does, but didn't have time yet.

My original question is mainly whether the additional API would be welcome (and then it makes sense to have a definition for the combination and add the fun_prop tags).

(This is beside the point, but the two lemmas add_mulSupport_finite and id_mulSupport_finite are wrong.)

[Michael Rothgang]

In the Carleson project, we have classes BoundedCompactSupport and BoundedFiniteSupport. (We will probably only upstream one of these.) We're working on using fun_prop with them. In other words, adding fun_prop for such a property seems reasonable to me.

[Michael Stoll]

I take this to say that it also seems reasonable to you to add the predicate HasFiniteMulSupport (plus API). Correct?

[Michael Stoll]

By now, I have played with this a little bit. In #34658 I have added HasFiniteMulSupport, provided API and fun_prop tags, and changed most occurrences of Set.Finite (Function.mulSupport _) to HasMulSupport _ (and similarly for the additive version). I then simplified some proofs in NumberTheory.Height.Basic using the new fun_prop capabilities.

[Michael Stoll]

For comparison, in #34793 I just add API for Set.Finite (Function.mulSupport _)) and then use it to simplify the same two proofs.

[Michael Stoll]

Both PRs are marked "WIP" for the time being.

• The HasFiniteMulSupport option leads to nicer proofs (like fun_prop (disch := grind)), but feels a bit heavy when done consequently: there are many places where the new predicate can be used.
• The other option is more "minimally invasive", but also leads to less simplification.

Except for the material on heights (with more to come), it does not look like the existing API for docs#Function.mulSupport and its additive counterpart is used much in Mathlib. But this may well change in the future.

So the question is, which of the two options is preferable long-term? (If the answer should be "none", then a third option would be to add the API lemmas I need as private lemmas to the file where they are used.)

Your insights are appreciated!