diff options
author | Jason Gross <jgross@mit.edu> | 2018-10-29 16:51:24 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-10-29 16:51:24 -0400 |
commit | ad54fb6c73c305cdd997a313fefc6e2a4dcc2d5d (patch) | |
tree | a5f1764df4e1c578771f9f62967586a045f2c6ca /src/Util/Logic/ExistsEqAnd.v | |
parent | 063c874f4bd87911cff3466542d599b579f2ff2d (diff) |
Add ex_eq_and tactic
Diffstat (limited to 'src/Util/Logic/ExistsEqAnd.v')
-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. |