Add ex_eq_and tactic

1 files changed, 25 insertions, 0 deletions

diff --git a/src/Util/Logic/ExistsEqAnd.v b/src/Util/Logic/ExistsEqAnd.v
index 27f08eb89..108224cb2 100644
--- a/src/Util/Logic/ExistsEqAnd.v
+++ b/src/Util/Logic/ExistsEqAnd.v
@@ -1,3 +1,4 @@
+Require Import Coq.Setoids.Setoid.
 Require Import Crypto.Util.FixCoqMistakes.
 Require Import Crypto.Util.Tactics.DestructHead.
 
@@ -24,3 +25,27 @@ Proof. t. Qed.
 Lemma ex_eq_and_r_iff {A P x}
   : (exists y : A, P y /\ x = y) <-> P x.
 Proof. t. Qed.
+
+Ltac ex_eq_and_step :=
+  let rew lem := (rewrite lem || setoid_rewrite lem) in
+  let rew_in lem H := (rewrite lem in H || setoid_rewrite lem in H) in
+  match goal with
+  | [ |- context[exists y, _ = y /\ _] ]
+    => rew (@ex_and_eq_r_iff)
+  | [ |- context[exists y, y = _ /\ _] ]
+    => rew (@ex_and_eq_l_iff)
+  | [ |- context[exists y, _ /\ _ = y] ]
+    => rew (@ex_eq_and_r_iff)
+  | [ |- context[exists y, _ /\ y = _] ]
+    => rew (@ex_eq_and_l_iff)
+  | [ H : context[exists y, _ = y /\ _] |- _ ]
+    => rew_in (@ex_and_eq_r_iff) H
+  | [ H : context[exists y, y = _ /\ _] |- _ ]
+    => rew_in (@ex_and_eq_l_iff) H
+  | [ H : context[exists y, _ /\ _ = y] |- _ ]
+    => rew_in (@ex_eq_and_r_iff) H
+  | [ H : context[exists y, _ /\ y = _] |- _ ]
+    => rew_in (@ex_eq_and_l_iff) H
+  end.
+
+Ltac ex_eq_and := repeat ex_eq_and_step.