Modelling non-commutative products, CenterDot problem

Question

I am trying to model certain non-commutative, but associative, structures with Mathematica. As a notation for the product I take CenterDot and add the attribute Flat since the product is associative. Then, I would like to realize certain relations, e.g. $$ a \cdot f[b,c]=f[a\cdot b,c]+f[a,b\cdot c] $$ for a function $f[b,c]$. I thought that this can be done systematically with a simple replace rules

$$a \cdot f[b,c]\,/. a\_ \cdot f[b\_,c\_]\rightarrow f[a\cdot b,c]+f[a,b\cdot c]$$

However, the output of such an operation is (the second term is ok)

$$f[\text{CenterDot}[a],b\cdot c]+f[a\cdot b,c]$$

If I use BlankSequence, $a\_\_$ instead of Blank, the output is exactly I want, but then the rule fails to give the right answer when there are several factors on the left (ideally, I would use the rule as many times as to remove all factors from the left. For example,

$$u\cdot a \cdot f[b,c]$$

is transformed to (in the second term it generates extra arguments, which is meaningless) $$f[u\cdot a\cdot b,c]+f[u,a,b\cdot c]$$

Ironically, the first rule (with Blank) works here and gives the desired

$$f[u\cdot a,b\cdot c]+f[u\cdot a\cdot b,c]$$

Answer 1

The OneIdentity attribute will help:

SetAttributes[CenterDot, {Flat, OneIdentity}];

a_ \[CenterDot] f[b_,c_] := f[a \[CenterDot] b, c] + f[a, b \[CenterDot] c]

Then:

a \[CenterDot] f[b, c] //TeXForm

$f(a,b\cdot c)+f(a\cdot b,c)$

And your second example:

CenterDot[u, a, f[b,c]] //TeXForm

$f(u\cdot a,b\cdot c)+f(u\cdot a\cdot b,c)$

Addendum

Why does OneIdentity help?

When pattern matching, note the way Flat works:

ClearAll[CenterDot]
SetAttributes[CenterDot, Flat]

CenterDot[x, y] /. CenterDot[a_, b_] :> {a,b}

{CenterDot[x], CenterDot[y]}

The arguments a and b have acquired the head CenterDot.

(This does not always happen. Here are a few examples where only some or none of the arguments acquire the CenterDot head):

CenterDot[x, 3] /. CenterDot[a_, 3] :> {a, 3}
CenterDot[x, 3] /. CenterDot[a_, b_Integer] :> {a, b}
CenterDot[x, f[3]] /. CenterDot[a_, f[b_]] :> {a, b}
CenterDot[x, f[3]] /. CenterDot[a_, b_f] :> {a, First @ b}

{CenterDot[x], 3}

{x, 3}

{CenterDot[x], 3}

{x, 3}

Your rule is similar to the 3rd example above:

CenterDot[a, f[b, c]] /. CenterDot[a_, f[b_, c_]] :> {a, b, c}

{CenterDot[a], b, c}

Now, compare this to a version where CenterDot has both the Flat and OneIdentity attributes:

ClearAll[CenterDot]
SetAttributes[CenterDot, {Flat, OneIdentity}]

CenterDot[x, y] /. CenterDot[a_, b_] :> {a,b}

{x, y}

Note that the arguments have not acquired the CenterDot head. Now, your rule behaves the way you want:

CenterDot[a, f[b, c]] /. CenterDot[a_, f[b_, c_]] :> {a, b, c}

{a, b, c}