From ad54fb6c73c305cdd997a313fefc6e2a4dcc2d5d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 29 Oct 2018 16:51:24 -0400 Subject: Add ex_eq_and tactic --- src/Util/Logic/ExistsEqAnd.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'src/Util') 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. -- cgit v1.2.3