Convention for `f * g` and / or `fun x ↦ f x * g x`

Stream: mathlib4

[Sébastien Gouëzel]

The product of two functions can be written as f * g or fun x ↦ f x * g x. These are defeqs, but syntactically different, so rw with a lemma formulated using the first form will not apply for the second form, and conversely. The first form is nicer to read and to write, but often one ends up with the second one, so both have their advantages. In some parts of the library, a "solution" to this has been to write two forms for each lemma, one with f * g and one with fun x ↦ f x * g x (one of them being primed). This works pretty well, but leads to a lot of code duplication. Should we go on with the duplication, or settle on one form? (For instance, in probability theory, the product of two random variables X and Y will almost always be written in the first form X * Y).

This came up in the review of #21502.

[Ruben Van de Velde]

#22183 ran into this issue as well

[Antoine Chambert-Loir]

Does the same issue arise for sums, differences, powers?

[Eric Wieser]

For n-ary sums, the two are not defeq, but docs#Pi.sum_def can translate doesn't exist

[Edward van de Meent]

ideally, i think, we'd like simp normal form to reflect the right form for this, right?

[Edward van de Meent]

is there an issue with making the reverse of docs#Pi.mul_def a simp lemma?

[Ruben Van de Velde]

Would simp need to try that on every function it encounters?

[Edward van de Meent]

i don't know, that's why i'm asking :upside_down:

[Eric Wieser]

Yes, because #discr_tree_key prints *

[Eric Wieser]

Unless @Jovan Gerbscheid's discrtree rewrite is upstreamed, or we override simp in mathlib to use the downstream version

[Stefan Kebekus]

@Sébastien Gouëzel As the author of #21502, thanks for bringing this up here.

[Stefan Kebekus]

From a user's perspective, I believe that mathlib should support both f * g and fun x ↦ f x * g x. Both version have their use cases. If I had to choose, I would definitively take f * g, for the following reasons:

• The notation fun x ↦ f x * g x has a tendency to exponentially grow -- think fun y ↦ f y * (fun x ↦ g x * h x) y.
• In my (limited) experience, the simlifier is not nearly as good with complicated expressions of the form fun y ↦ f y * (fun x ↦ g x * h x) y as it is when treating functions as ring elements. When simplifying with messy computations, I started to constantly formulate (and apply) trivial lemmas (have : something = something else := by rfl; rw [this]; clear this), which quickly became quite painful.

[Stefan Kebekus]

From a contributor's perspective, I prefer the solution formulating relevant lemmas twice [unless some form of automatization exists], which reduces complexity and improves readability of my code at the expense of duplicating lemmas. On the other side, I do understand the concerns ("combinatorial explosion").

Personally, I could live with any decision, even if not my preferred one. However, I do feel strongly that we should have a policy here. As a newcomer, I found that mathlib is rather inconsistent in this respect and I have received conflicting advice how to proceed, which is of course a bit frustrating.

[Kevin Buzzard]

[off-topic: Re: have : X=Y := by rfl, rw [this], clear this: you might like the change tactic (although this approach can get very verbose). ]

[Etienne Marion]

Kevin Buzzard said:

[off-topic: Re: have : X=Y := by rfl, rw [this], clear this: you might like the change tactic (although this approach can get very verbose). ]

The combo conv + change can make it a bit less verbose

[Edward van de Meent]

also, possibly rw [show X=Y from rfl]

[Edward van de Meent]

a hack i've heard about is rw [(id rfl : X=Y)]

[Rémy Degenne]

With rw working how it does right now, I think we can't avoid having the form fun x ↦ f x * g x, since that's the way that multiplication appears most when inside more complicated expressions (and it's also the better form for tactics like fun_prop). So if we also want the f * g version because it's nicer in some contexts, we just need both.
A related issue is that Mathlib is inconsistent on which of the two lemmas should be primed.

[Sébastien Gouëzel]

So could the convention be: there should always be the version with fun x ↦ f x * g x, this is the main version, and it is without prime. And the PR author may add a primed version for f * g, but this is not mandatory.

[Stefan Kebekus]

@Kevin Buzzard @Etienne Marion @Rémy Degenne Thanks for the off-topic hints. I was not aware of these tricks.

[Sébastien Gouëzel]

@Stefan Kebekus , could you adapt #21502 to this convention? It means the primed and unprimed versions should be swapped.

[Stefan Kebekus]

@Sébastien Gouëzel Will do, tomorrow morning at the latest. [Update 25Feb25, 10:00: Done]

[Yaël Dillies]

I'm not super happy with this convention since it makes it sound like f * g is a second class citizen

[Eric Wieser]

Should our naming convention allocate a token to fun x =>, so as to avoid primes?

[Yaël Dillies]

That was my back-of-the-mind thought, yes

[Edward van de Meent]

so then fun x ↦ f x * g x would be something like fun_apply_mul_apply? i'm not sure that's better, tbh

[Sébastien Gouëzel]

Let's take a concrete example. In the lemmas

lemma applied_form (hf : AnalyticWithinAt 𝕜 f s z) (n : ℕ) :
    AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z

lemma unapplied_form (hf : AnalyticWithinAt 𝕜 f s z) (n : ℕ) :
    AnalyticWithinAt 𝕜 (f ^ n) s z

how would you name them? The proposal above is applied_form = AnalyticWithinAt.pow and unapplied_form = AnalyticWithinAt.pow'. I can start a poll once people give me some propositions. Since it seems most people agree that the normal form should be the applied one, I'd keep the shortest AnalyticWithinAt.pow for the applied form, but I'm all ears for other propositions.

[Eric Wieser]

Some existing precedent: docs#Finset.sum_add_distrib is stated as (s.sum fun x => f x + g x) = (s.sum fun x => f x) + (s.sum fun x => g x) not s.sum (f + g) = s.sum f + s.sum g.

[Jz Pan]

Kevin Buzzard said:

[off-topic: Re: have : X=Y := by rfl, rw [this], clear this: you might like the change tactic (although this approach can get very verbose). ]

It's said that there is a syntax change X with Y and change X with Y at h

[Jz Pan]

Another off-topic question: Do I need to open scoped Pointwise to use the notation f * g?

[Jz Pan]

Another off-topic question: Do I need to open scoped Pointwise to use the notation f * g?

[Eric Wieser]

No, open scoped Pointwise is only needed for pointwise operators on Sets and related objects

[Tomas Skrivan]

From the perspective of fun_prop:

1. stating a theorem as Continuous fun x => f x * g x talks about continuity of * in the first and the second argument
2. stating a theorem as Continuous (f * g) talks about continuity of * in the third argument

In a way they are just different theorems. Of course fun_prop could do some reduction a exploit the fact that fun x => f x * g x and f * g are defeq but currently this is not happening.

The proper way of formulating continuity of multiplication in all three arguments for fun_prop is:

import Mathlib

variable (f g : ℝ → ℝ) (hf : Continuous f) (hg : Continuous g)

example : Continuous (f * g) := by fun_prop -- fails

@[fun_prop]
theorem continuous_mul'''
    {X Y Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    [Mul Z] [ContinuousMul Z] (f g : X → Y → Z) (h : X → Y)
    (hf : Continuous ↿f) (hg : Continuous ↿g) (hh : Continuous h) :
    Continuous (fun x => (f x * g x) (h x)) := by simp; fun_prop

-- now these work
example : Continuous (f * g) := by fun_prop
example : Continuous (fun x : ℝ  => (((x * ·) ∘ f) * ((x + ·) ∘ g)) x) := by fun_prop

The current approach of fun_prop does not scale to arbitrary arity of * i.e. you need a separate theorem for every possible arity.

[Tomas Skrivan]

On the other hand this approach works even in cases where fun x => f x * g x is not defeq f * g. Which is in some sense true for Polynomial

example (f g : Polynomial ℝ) : (f * g).eval = (fun x : ℝ => f.eval x * g.eval x) := by rfl -- fail

In case we would have CoeFun (Polynomial ℝ) (fun _ => ℝ → ℝ) this would result in a confusing fact that f * g is not defeq to fun x => f x * g x.

[Sébastien Gouëzel]

I haven't got any other suggestions. Still, here is a poll. In the lemmas

lemma applied_form (hf : AnalyticWithinAt 𝕜 f s z) (n : ℕ) :
    AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z

lemma unapplied_form (hf : AnalyticWithinAt 𝕜 f s z) (n : ℕ) :
    AnalyticWithinAt 𝕜 (f ^ n) s z

how should we call the first lemma and the second lemma?

[Sébastien Gouëzel]

/poll
AnalyticWithinAt.pow and AnalyticWithinAt.pow'
AnalyticWithinAt.pow and AnalyticWithinAt.pow_unapplied
AnalyticWithinAt.pow' and AnalyticWithinAt.pow
AnalyticWithinAt.pow_applied and AnalyticWithinAt.pow
AnalyticWithinAt.pow_applied and AnalyticWithinAt.pow_unapplied
Other suggestions

[Sébastien Gouëzel]

There seems to be a consensus for "no prime for the applied version, prime the unapplied version if needed". I am therefore planning to add the following paragraph to the naming conventions. Comments and improvements welcome!

Applied and unapplied forms of functions

The product of two functions f and g can be denoted equivalently as
fun x ↦ f x * g x or f * g. These expressions are definitionally equal, but not syntactically, which
means that rw will not apply to one of them a theorem given with the other form. Therefore, it is
sometimes convenient to have variants of the statements using the two forms. The main form should always
be in terms of the applied version fun x ↦ f x * g x.
The other form can be given postfixing the name of the theorem with a prime.
For instance, the fact that the product of two continuous functions is continuous is

theorem Continuous.mul (hf : Continuous f) (hg : Continuous g) : Continuous fun x ↦ f x * g x

and one may also have

theorem Continuous.mul' (hf : Continuous f) (hg : Continuous g) : Continuous (f * g)

The same goes for addition, subtraction, negation and powers of functions.

[Eric Wieser]

I think probably "eta-expanded" is more accurate than "applied"

[Yaël Dillies]

Yes, mul_eta and mul seems like a good naming pair

[Yaël Dillies]

Sébastien, note that mobile Zulip users can't add options to polls, and I happen to have forcedly been a mobile Zulip user for the past five days

[Tomas Skrivan]

It it not just eta expansion! Eta expansion of f * g is fun x => (f * g) x which reduces to fun x => f x * g x with dsimp lemma Pi.mul_apply. This makes a big difference when writing a tactic that has to deal with this.

[Damiano Testa]

I am also not to thrilled to see eta appearing in user-facing names...

[Eric Wieser]

I wasn't suggesting it should appear in the name, merely that it should appear in the docs; I would argue that the description of the one we are assigning the unprimed name here is "use the eta expanded spelling" combined with "use the simp-normal form"

[Damiano Testa]

My comment was addressing Yaël's:

Yaël Dillies said:

Yes, mul_eta and mul seems like a good naming pair

[Tomas Skrivan]

If we don't use * notation. The expression fun x => HMul.hMul f g x(eta expanded f*g) is actually more similar(from lambda calculus perspective) to fun x => HMul.hMul c x(e.g. continuous_mul_left) or fun x => HMul.hMul x c(e.g. continuous_mul_right) rather than fun x => HMul.hMul (f x) (g x) (e.g. Continuous.mul)

[Floris van Doorn]

I'm not thrilled putting a naming convention with primes being formalized in our conventions, and would prefer something like AnalyticWithinAt.pow_unapplied, except that _unapplied is too long. Maybe AnalyticWithinAt.powFun or AnalyticWithinAt.powPi for the f ^ n version? (since it's the power operation on functions or on the Pi-type.)

[Sébastien Gouëzel]

Yaël Dillies said:

Sébastien, note that mobile Zulip users can't add options to polls, and I happen to have forcedly been a mobile Zulip user for the past five days

If you tell me an option you want me to add, I can do it myself!

[Jovan Gerbscheid]

The relevant rewrite lemma showing the equvalence of the two forms is Pi.mul_def. So a name with mulPi, mul_pi or mul_Pi in the place of mul seems reasonable for the version that multiplies the Π types.

[Sébastien Gouëzel]

Ok, let me run a new poll with these propositions (and discarding all those that got 0 in the first poll). In the lemmas

lemma applied (hf : Continuous f) (hg : Continuous g) : Continuous fun x ↦ f x * g x
lemma unapplied (hf : Continuous f) (hg : Continuous g) : Continuous (f * g)

how should the lemmas be named?

[Sébastien Gouëzel]

/poll
Continuous.mul and Continuous.mul'
Continuous.mul and Continuous.mul_pi
Continuous.mul and Continuous.mul_unapplied
Continuous.mul and Continuous.mulPi
Other propositions

[Yaël Dillies]

Wait, maybe we can't add options to polls anymore at all?

[Sébastien Gouëzel]

What would be the option you would like to add?

[Jovan Gerbscheid]

In terms of pi vs Pi capitalization, I presume docs#small_Pi is wrong and docs#deriv_pi correct?

[Yaël Dillies]

mul_eta/mul

[Sébastien Gouëzel]

Yes, I can't add another option to the poll. Let me do it below.

[Sébastien Gouëzel]

/poll
Continuous.mul_eta and Continuous.mul

[Sébastien Gouëzel]

The winner of the poll is Continuous.mul and Continuous.mul_pi.

[Sébastien Gouëzel]

Here is the text I will soon add to the naming convention. Comments welcome, again!

Expanded and unexpanded forms of functions

The product of two functions f and g can be denoted equivalently as
fun x ↦ f x * g x or f * g. These expressions are definitionally equal, but not syntactically, which
means that rw will not apply to one of them a theorem given with the other form. Therefore, it is
sometimes convenient to have variants of the statements using the two forms. The main form should always
be in terms of the expanded version fun x ↦ f x * g x.
The other form can be given postfixing the name of the theorem with _pi, as it corresponds to using
the operation defined on the Pi type instead of the pointwise operation.
For instance, the fact that the product of two continuous functions is continuous is

theorem Continuous.mul (hf : Continuous f) (hg : Continuous g) : Continuous fun x ↦ f x * g x

and one may also have

theorem Continuous.mul_pi (hf : Continuous f) (hg : Continuous g) : Continuous (f * g)

The same goes for addition, subtraction, negation and powers of functions.

[Jireh Loreaux]

What about composition? I.e., g ∘ f versus fun x ↦ g (f x)? I realize this isn't a pi issue, but we do have both versions running around in various places, e.g., docs#Continuous.comp and docs#Continuous.comp'.

[Yaël Dillies]

I think we really need to make the point-free version the default, and add a token that says "eta-expand, run dsimp"

[Jovan Gerbscheid]

@Yaël Dillies, are you saying that for f * g or for g ∘ f?

[Yaël Dillies]

Both

[Floris van Doorn]

Yaël Dillies said:

I think we really need to make the point-free version the default, and add a token that says "eta-expand, run dsimp"

Can you explain why you want the point free example as default?

Here is a (not super important) case why I like the expanded version better: If I have \all x, f x = f2 x then this is much easier to apply to fun x => f x * g x than to f * g.

[Floris van Doorn]

Somewhat related: it would be nice to have a tactic that eta-expands all partially applied functions in your goal (or a hypothesis). Maybe this already exists?

[Jovan Gerbscheid]

Besides the f + g vs fun x => f x + g x debate, there is also the f x + g x vs (f + g) x debate, see docs#MeasureTheory.integral_integral_add and docs#MeasureTheory.integral_integral_add'. What is the plan with naming these?

[Jovan Gerbscheid]

Floris van Doorn said:

Somewhat related: it would be nice to have a tactic that eta-expands all partially applied functions in your goal (or a hypothesis). Maybe this already exists?

It turns out there is an eta_expand tactic :tada:

Edit: looking at the implementation, it seems to not work perfectly, and only eta expand terms that are applications. So a free variable (f : a -> b) will not get expanded to fun x => f x :frown:

[Floris van Doorn]

I would like to make a comment on the mul_pi name: are we really certain that we want to call (· * ·) for functions mul_pi?
I am very strongly in favor of the Lean 4 convention where 1 operation has no underscores in it, and different operators names in a lemma name are separated by an underscore. The current suggestion is like calling (· + ·) on the natural numbers add_nat... And we decided a while ago that operations like Nat.cast should be named natCast in lemmas (when cast itself is ambiguous). This suggest piMul, which would also be fine by me.
(sorry for the bikeshedding)

[Yury G. Kudryashov]

BTW, the location of ' on prod lemmas is inconsistent too (encountered while working on #22195, not fixing in that PR).

[Floris van Doorn]

Jovan Gerbscheid said:

Besides the f + g vs fun x => f x + g x debate, there is also the f x + g x vs (f + g) x debate, see docs#MeasureTheory.integral_integral_add and docs#MeasureTheory.integral_integral_add'. What is the plan with naming these?

I would name (f + g) x the same way as what we decide for f + g. For integrals we just never write the eta-reduced form because of the notation, and fun x => (f + g) x is the same as f + g, without any unfolding.

[Floris van Doorn]

Jovan Gerbscheid said:

It turns out there is an eta_expand tactic :tada:

Edit: looking at the implementation, it seems to not work perfectly, and only eta expand terms that are applications. So a free variable (f : a -> b) will not get expanded to fun x => f x :frown:

This is not entirely right, since at least the following example works:

import Mathlib.Tactic.Common

example (f g : Nat → Nat) : f = g := by
  eta_expand
  guard_target =ₛ (fun a => f a) = (fun a => g a)
  sorry

[Jovan Gerbscheid]

@Floris van Doorn, I think the question here is whether (· * ·) for functions should be thought of as a separate operation to mul, or whether the pi is describing the arguments of mul.

e.g. mul_one multiplies a one, and mul_pi multiplies two pis.

[Yakov Pechersky]

Floris van Doorn said:

Here is a (not super important) case why I like the expanded version better: If I have \all x, f x = f2 x then this is much easier to apply to fun x => f x * g x than to f * g.

Perhaps that hypothesis would be better phrased point free / unfunext as well, as f = f2.

[Yakov Pechersky]

But in general, I agree that overall in the library, the prevalence of syntactic rewriting tools leads away from using things like partial applications via \. .

[Sébastien Gouëzel]

As Jovan says, in my mind mul_pi means that it's a mul (which refers to the symbol *), and it's on Pi objects (which refers to f and g), so that's why it has an underscore.

[Sébastien Gouëzel]

For composition, just for coherence I'd go for comp and comp_pi (although the argument is less compelling there)

[Yaël Dillies]

Sébastien Gouëzel said:

As Jovan says, in my mind mul_pi means that it's a mul (which refers to the symbol *), and it's on Pi objects (which refers to f and g), so that's why it has an underscore.

So now if you see x * y in a lemma you need to know whether x and y are functions and not

[Sébastien Gouëzel]

I'm not sure what you mean. If you see Continuous (f * g), it's obviously for functions, and then you use Continuous.mul_pi. Do you have a relevant example in mind where you think it could create confusion?

[Jireh Loreaux]

Yaël Dillies said:

I think we really need to make the point-free version the default, and add a token that says "eta-expand, run dsimp"

By "default", I interpret this to mean "the one that gets the name mul". I completely agree with Yaël here, and I think this is the key:

Yaël Dillies said:

So now if you see x * y in a lemma you need to know whether x and y are functions and not

I think we do need another token for the eta-expanded, dsimp'ed version. pi was reasonable idea except that it doesn't fit fun x ↦ g (f x)) at all.

[Sébastien Gouëzel]

The thing is that the expanded version is the one that is useful most of the time, so that's the one that should get the shortest name. The poll above shows that most people support this. Note that a typical function looks like fun x ↦ x * exp (- x^2 / 2), which is quite painful to write in a point-free way, so I don't think switching by default to the point-free version is a sensible move.

[Jireh Loreaux]

But because there is literally no other syntax in the unapplied form, it both:

1. forces us to use different conventions for x * y depending on whether these are functions or not (which is tremendously counterintuitive and I think will lead to much frustration for both reviewers and contributors)
2. makes it hard to come up with a good name for the unapplied version because there is no token for syntax that isn't present!

I think if we come up with a short enough token for the applied form it wouldn't be problematic.

Also, it's not entirely clear to me that the expanded for is always most useful, although in certain areas of the library that's definitely the case (e.g., integration). I do wonder if the original poll would reach the same consensus given these more recent comments, but I won't push for it unless someone other than Yaël or I agrees.

[Jireh Loreaux]

I would suggest simply:

1. fn_mul for fun x ↦ f x * g x
2. mul for f * g.

[Anatole Dedecker]

I have no strong opinion, but I agree that this option needs to be considered as it's the one that matches best with what we actually write

[Yaël Dillies]

Thank you Jireh for articulating my thoughts so well :folded_hands:

[Sébastien Gouëzel]

@Jireh Loreaux , do you think could you run another poll, keeping the options in the previous one that had some support, and explaining the new option and why you think it's better? Hopefully this will help everyone choose an option having all the information in mind.

[Jireh Loreaux]

I suggest a different naming convention:

1. fn_mul for fun x ↦ f x * g x (hereafter referred to as applied)
2. mul for f * g (hereafter referred to as unapplied)

A previous poll had concluded that the "default" version (i.e., unprimed / shorter name) should be the applied one because it is used more often. A later poll determined that the names for these should be mul (applied) and mul_pi (unapplied).

However, since that poll there has since been more discussion about some downsides of these choices. In particular, because there is literally no other syntax besides * in the unapplied form:

1. it forces us to use different conventions for f * g depending on whether these are functions or not (which is counterintuitive and I think will lead to much frustration for both reviewers and contributors)
2. it makes it hard to come up with a good name for the unapplied version because there is no token for syntax that isn't present!
3. related to (2), the pi naming convention doesn't accommodate things like fun x ↦ g (f x) vs. g ∘ f.

My suggested convention (fn_mul for applied, mul for unapplied), has some benefits:

1. matches the visible syntax reasonably well
2. is relatively short for both applied and unapplied versions
3. extends to other settings like ∘ (or even id for id vs. fn_self or fn_id for fun x ↦ x)
4. doesn't fracture the naming conventions for * based on whether or not the arguments are functions

So let's run another poll:

[Jireh Loreaux]

/poll What should the naming conventions be (applied and unapplied)
Continuous.mul and Continuous.mul'
Continuous.mul and Continuous.mul_pi
Continuous.mul and Continuous.mulPi
Continuous.fn_mul and Continuous.mul

[Kim Morrison]

I added an option, because I'm not sure why we would (confusingly?) refer to the fun token as fn.

[Kim Morrison]

Although there appears to be precedent, which may be enough to settle that.

[Sébastien Gouëzel]

There is overwhelming support for the last suggestion. This would give the following paragraph, to be added to the naming convention.

Expanded and unexpanded forms of functions

The product of two functions f and g can be denoted equivalently as
f * g or fun x ↦ f x * g x. These expressions are definitionally equal, but not syntactically, which
means that rw will not apply to one of them a theorem given with the other form. Therefore, it is
sometimes convenient to have variants of the statements using the two forms. To distinguish between them,
statements involving the first unexpanded form are written using just mul, while lemmas using
the second expanded form should instead use fun_mul.

For instance, the fact that the product of two continuous functions is continuous is

theorem Continuous.fun_mul (hf : Continuous f) (hg : Continuous g) : Continuous fun x ↦ f x * g x

and

theorem Continuous.mul (hf : Continuous f) (hg : Continuous g) : Continuous (f * g)

The same goes for addition, subtraction, negation, powers and composition of functions.

[Sébastien Gouëzel]

I am not specifying here if PR authors should use one form, or the other, or both, leaving that to the discretion of the authors. Does this sound reasonable?

[David Loeffler]

I am concerned about the amount of non-backward-compatible breakage (in mathlib & in downstream projects) that will arise if/when the definition of Continuous.mul gets changed to match this change to the style guide.

(Since the name Continuous.mul will remain in use, but won't mean the same as before, there is no way we can handle this with deprecations.)

[Sébastien Gouëzel]

Note that both statements are defeq, so in 99% of the situations nothing should break. For instance, if you were proving continuity with (hf.add hg).mul ha, the same proof will remain valid.

[David Loeffler]

Well, I guess the only way to find out is to try...

[Jireh Loreaux]

@Sébastien Gouëzel what you have written above looks pretty good, although can we pick an example other than Continuous (f * g)? Indeed, as you pointed out with the defeq comment, this particular issue will essentially never arise for Continuous.mul because one doesn't rewrite with this. Maybe docs#Topology.IsInducing.of_comp_iff would be slightly more relevant? Or other examples. I have some (like docs#cfc_mul), but they are too specialized for the naming conventions page.

[Jovan Gerbscheid]

Could you also mention the examples of identity and composition explicitly? My understanding is that we will write fun_id for fun x => x and fun_comp for fun x => f (g x)

[Sébastien Gouëzel]

I have yet another question: should we say that the use of fun_ is mandatory, or just useful to disambiguate when needed? For instance, in

theorem Continuous.comp₂ {g : X × Y → Z} (hg : Continuous g) {e : W → X} (he : Continuous e)
    {f : W → Y} (hf : Continuous f) : Continuous fun w => g (e w, f w)

I wouldn't rename it to Continuous.fun_comp₂ because we won't ever write the unexpanded version. No objection here?

[Jovan Gerbscheid]

Yes, I think the fun_comp can only be used for a (normal) composition of 2 functions.

[Jovan Gerbscheid]

I agree the fun_ is there for disambiguation. But my hope is that in (almost) all cases where the fun_ version of a lemma exist, there is also a regular version.

[Yaël Dillies]

I'd vote only for disambiguation

[Sébastien Gouëzel]

ok, another try:

Unexpanded and expanded forms of functions

The composition of two functions f and g can be denoted equivalently as
f ∘ g or fun x ↦ f (g x). These expressions are definitionally equal, but not syntactically, which
means that rw will not apply to one of them a theorem given with the other form. Therefore, it is
sometimes convenient to have variants of the statements using the two forms. If one needs to
distinguish between them, statements involving the first unexpanded form are written using just comp,
while lemmas using the second expanded form should instead use fun_comp. If there is no need to
disambiguate because a lemma is given using only the expanded form, the prefix fun_ is not required.

For instance, the fact that the composition of two functions is inducing (whatever that means) is

theorem IsInducing.fun_comp (hf : IsInducing f) (hg : IsInducing g) : IsInducing fun x ↦ f (g x)

and

theorem IsInducing.comp (hf : IsInducing f) (hg : IsInducing g) : IsInducing (f ∘ g)

The same goes for multiplication, addition, subtraction, negation and powers of functions.

[Jovan Gerbscheid]

It might be good to mention that Tactics like apply? and fun_prop, just like rw, do not apply one form to the other form, since the example isn't a rw lemma. And I'd suggest to also include the example with multiplication, as it is what this conversation started about.

[Sébastien Gouëzel]

ok, another try. I've switched back to the multiplication of two functions, as the fun_prop argument makes it clear why we need the two forms.

Unexpanded and expanded forms of functions

The multiplication of two functions f and g can be denoted equivalently as
f * g or fun x ↦ f x * g x. These expressions are definitionally equal, but not syntactically (and they don't
share the same key in indexing trees), which means that tools like rw, fun_prop or apply?
will not use a theorem with one form on an expression with the other form. Therefore, it is
sometimes convenient to have variants of the statements using the two forms. If one needs to
distinguish between them, statements involving the first unexpanded form are written using just mul,
while lemmas using the second expanded form should instead use fun_mul. If there is no need to
disambiguate because a lemma is given using only the expanded form, the prefix fun_ is not required.

For instance, the fact that the multiplication of two continuous functions is continuous is

theorem Continuous.fun_mul (hf : Continuous f) (hg : Continuous g) : Continuous fun x ↦ f x * g x

and

theorem Continuous.mul (hf : Continuous f) (hg : Continuous g) : Continuous (f * g)

Both theorems deserve tagging with the fun_prop attribute.

The same goes for addition, subtraction, negation, powers and compositions of functions.

[Thomas Zhu]

I think a caveat is that let's say I have a property P and write theorem P.mul (hf : P f) (hg : P g) : P fun x ↦ f x * g x. I don't need fun_ disambiguation per the convention above. (And for most properties, this is the form that should always exist first, because I can then rw/apply?/fun_prop using this form on more complicated expressions like fun x => f x * Real.exp (x + g x).) Then a month later someone wants to add the pointfree version theorem P.mul (hf : P f) (hg : P g) : P (f * g). They can't add this without renaming the existing P.mul to P.fun_mul, and you can't add a @[deprecated] alias for this rename either because P.mul is taken by the new form.

[Thomas Zhu]

Also, shouldn't there be a limit to how complicated something is before you should only write it in fun form? What about f * (g ∘ h)? f * (g ∘ (-h))? id * f? f ^ 2? 2 • f / g? -flip f? Real.exp ∘ f? id * (Real.exp ∘ (-f))? I am pretty sure at some extent, this form of pointfreeism is very discouraged. (I know the current version above is only a naming/token convention, and the discretion to use which is left to PR authors, so this would perhaps be a separate convention).

[Thomas Zhu]

Also related is id' vs id: by the convention above every id' should be named something like fun_self

[Sébastien Gouëzel]

For the first question: yes, that's true, but it's not so bad since both are defeq (and for apply? or fun_prop the new version will be picked up automatically). So I agree it's not perfect, but nothing is perfect!

For the second question, let's trust the PR authors and reviewers for making a good choice.

[Thomas Zhu]

You're right, they are defeq so shouldn't be that bad

[Jovan Gerbscheid]

Should id be names fun_self or fun_id? fun_id follows the fun_comp naming, but may be more confusing since there is no identity inside of the fun.

[Sébastien Gouëzel]

I would say fun_self, just following the symbols in the statement.

[Attila Vajda]

(deleted)