RingTactics

Pierre Letouzey edited this page Oct 27, 2017 · 15 revisions
Require Export Ring.

ringsimpl

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.

ringreplace

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.

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.