RingTactics
Require Export Ring.
The idea is to put all ring expressions occuring in the goal into normal form. This tactic could use lots of improvement.
Ltac ringsimpl :=
match goal with
| |- (_ ?a ?b) => ring a b
| |- (?a ?b ?c) => try ringsimpl a; try ringsimpl b; try ringsimpl c
end.Instead of this tactic, you can now do replace a with b by ring in Coq. Unfortuately this doesn't work for setoid_replace.See also TacticExts#LHS for using replace with LHS and RHS.
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.