simp and simpNF

Stream: mathlib4

[Johan Commelin]

I have a question about simp normal forms and the mathlib simp set. I will just focus on an example, while trying to understand this.

We have decided that f (x + y) = f x + f y should be a simp lemma, instead of f x + f y = f (x + y). Intuitively, I am still very happy with this choice. But from a (CS) theoretical perspective this is not clear at all. Because we are introducing an extra copy of f, instead of removing one.
So I think the reason we like our definition is because in practice we hope that x or y will be in the kernel of f and so we can simplify even further. And in practice it is just much more likely that x or y will be in the kernel than that some complicated expression like x + y is in the kernel.
But that's a very vague and imprecise argument.

So my question is: after 5 years of mathlib, and 5 decades of ITP more generally, do we have a good understanding of why f (x + y) = f x + f y is the "correct" simp direction?

[Damiano Testa]

My internal reasoning is that it is likelier that you have a result about f applied to something "atomic", than to a sum of stuff. The kernel is an example, but you might also have other values of a that simp can simplify. :shrug:

[Eric Wieser]

Another case like "in the kernel" is "is a constructor"; often f (mk x) = g x, where g is simpler, and you want to get there from f (mk x + y + 0)

[Johan Commelin]

Yup, that's a nice one.
I wonder if we can somehow come up with an abstract principle.

[Vincent Beffara]

Perhaps a more naive reason is that the usual direction is sure to fire while for simplifying f x + 0 + f y one needs to shuffle things around, so proving an equality with simp is more likely to work the way it is?

[Eric Wieser]

A similar argument: some types of induction turn P z into P x -> P y -> P (x + y), and for those it's helpful if simp can separate the x and y in the goal

[Jireh Loreaux]

Johan, here is one fascinating counterexample. The continuous functional calculus for an element a : A in a C⋆-algebra is a monomorphism cfc : C(spectrum ℂ a, ℂ) →⋆ₐ[ℂ] A. And it satisfies a composition property cfc (f ∘ g) = cfc f (cfc g) (please ignore that this is not well-typed). In practice, I have found that, when working with cfc, we almost always rewrite with the usual lemmas (e.g., map_mul, map_add, etc.) backwards. The reason is essentially this: to show two expressions involving the cfc are equal, pull cfc all the way out (i.e., from the leaves of the expression to the head) of both, then argue that the functions are equal.

Because of the way we implemented cfc, we don't technically use map_mul and friends, we have docs#cfc_mul, but I wrote cfc_mul in the same direction and only later realized that somehow it is the "wrong" direction.

[Johan Commelin]

Interesting! Thanks for sharing

[Kevin Buzzard]

If f is a cast between numeric types then humans want to freely go in both directions in proofs and this is why we have norm_cast and push_cast. So it's not clear that there can be an argument which unambiguously concludes that one way is more helpful than the other.

[Tomas Skrivan]

In SciLean I have simp sets add_push, add_pull, smul_push, smul_pull, ... and command that takes a proof of IsLinearMap k f and generates all the relevant theorems for a concrete f.

Lots of my proofs end with simp [smul_push, add_push].

[Violeta Hernández]

My intuition is that f can be a very complicated function, and it can be very unclear what it does when applied to some large term. Splitting it up allows you to think about its behavior on each specific portion of the term.