Is there a tactic that would allow one to automatically rewrite/reduce equations with linear functions?

```
From mathcomp Require Import all_ssreflect all_algebra.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GRing.Theory.
Open Scope ring_scope.
Section finVS.
Variables (P : fieldType) (U V : vectType P).
Implicit Types f : 'Hom(U, V).
Lemma foobar f a b : linear f -> f (a *+ 2 + b) = f a *+ 2 + f b.
Proof. by rewrite linearD linearMn. Qed.
End finVS.
```

In general it appears math-comp doesn't have many additional tactics for rewriting over various algebraic theories

Would a repeat rewrite with a multi-rule be sufficient?

```
Definition linear_rule := (linearD, linear0, linearB, linearMNn, linearMn,linearZ).
```

then

```
rewrite !linear_rule.
```

--- I have not tried it.

The appropriate name would be `linearE`

and I do think we should add it. (as well as `rmorphE`

and `raddfE`

)

Thanks @Yves Bertot, that worked.

I am adding PR on math-comp for this.

Last updated: Oct 13 2024 at 01:02 UTC