Stream: math-comp users

Topic: automatic rewriting of linear equations

Ben Siraphob (Jul 12 2021 at 10:04):

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.

Ben Siraphob (Jul 12 2021 at 10:08):

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

Yves Bertot (Jul 21 2021 at 06:54):

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.

Cyril Cohen (Jul 22 2021 at 12:13):

The appropriate name would be linearE and I do think we should add it. (as well as rmorphE and raddfE)

Ben Siraphob (Jul 26 2021 at 12:52):

Thanks @Yves Bertot, that worked.

Yves Bertot (Jul 26 2021 at 13:31):

I am adding PR on math-comp for this.

Last updated: Jan 29 2023 at 18:03 UTC