Add ring_simplify_subterms

2 files changed, 11 insertions, 0 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index d47fc6acd..5a2ea19a4 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -1299,6 +1299,10 @@ Ltac only_two_square_roots :=
     => repeat only_two_square_roots_step eq opp mul
   end.
 
+(*** Tactics for ring equations *)
+Require Import Coq.setoid_ring.Ring_tac.
+Ltac ring_simplify_subterms := tac_on_subterms ltac:(fun t => ring_simplify t).
+
 Section Example.
   Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
   Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div.
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 83ec603a0..c881478dd 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -300,3 +300,10 @@ Tactic Notation "rewrite_hyp" "<-" "?*" "in" "*" := repeat do_with_hyp' ltac:(fu
 Tactic Notation "rewrite_hyp" "!*" "in" "*" := progress rewrite_hyp ?* in *.
 Tactic Notation "rewrite_hyp" "->" "!*" "in" "*" := progress rewrite_hyp -> ?* in *.
 Tactic Notation "rewrite_hyp" "<-" "!*" "in" "*" := progress rewrite_hyp <- ?* in *.
+
+(** Execute [progress tac] on all subterms of the goal.  Useful for things like [ring_simplify]. *)
+Ltac tac_on_subterms tac :=
+  repeat match goal with
+         | [ |- context[?t] ]
+           => progress tac t
+         end.