1 files changed, 35 insertions, 0 deletions
diff --git a/src/Util/Tactics/SetoidSubst.v b/src/Util/Tactics/SetoidSubst.v
new file mode 100644
index 000000000..4ccf910ed
--- /dev/null
+++ b/src/Util/Tactics/SetoidSubst.v
@@ -0,0 +1,35 @@
+Require Import Crypto.Util.Tactics.Contains.
+
+Ltac setoid_subst'' R x :=
+  is_var x;
+  match goal with
+  | [ H : R x ?y |- _ ]
+    => free_in x y; rewrite ?H in *; clear x H
+  | [ H : R ?y x |- _ ]
+    => free_in x y; rewrite <- ?H in *; clear x H
+  end.
+
+Ltac setoid_subst' x :=
+  is_var x;
+  match goal with
+  | [ H : ?R x _ |- _ ] => setoid_subst'' R x
+  | [ H : ?R _ x |- _ ] => setoid_subst'' R x
+  end.
+
+Ltac setoid_subst_rel' R :=
+  idtac;
+  match goal with
+  | [ H : R ?x _ |- _ ] => setoid_subst'' R x
+  | [ H : R _ ?x |- _ ] => setoid_subst'' R x
+  end.
+
+Ltac setoid_subst_rel R := repeat setoid_subst_rel' R.
+
+Ltac setoid_subst_all :=
+  repeat match goal with
+         | [ H : ?R ?x ?y |- _ ] => is_var x; setoid_subst'' R x
+         | [ H : ?R ?x ?y |- _ ] => is_var y; setoid_subst'' R y
+         end.
+
+Tactic Notation "setoid_subst" ident(x) := setoid_subst' x.
+Tactic Notation "setoid_subst" := setoid_subst_all.