diff options
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/Logic/ExistsEqAnd.v | 25 |
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. |