Add [etransitivity y], [etransitivity_rev] tactics

2 files changed, 15 insertions, 0 deletions

diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index d98ac1bd4..eac17b0d9 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -5,6 +5,7 @@ Require Export Crypto.Util.Tactics.Head.
 Require Export Crypto.Util.Tactics.DestructHyps.
 Require Export Crypto.Util.Tactics.DestructHead.
 Require Export Crypto.Util.Tactics.DoWithHyp.
+Require Export Crypto.Util.Tactics.ETransitivity.
 Require Export Crypto.Util.Tactics.RewriteHyp.
 Require Export Crypto.Util.Tactics.SpecializeBy.
 Require Export Crypto.Util.Tactics.SplitInContext.
diff --git a/src/Util/Tactics/ETransitivity.v b/src/Util/Tactics/ETransitivity.v
new file mode 100644
index 000000000..c6fe59318
--- /dev/null
+++ b/src/Util/Tactics/ETransitivity.v
@@ -0,0 +1,14 @@
+Require Import Coq.Classes.RelationClasses.
+
+Tactic Notation "etransitivity" open_constr(y) :=
+  let R := match goal with |- ?R ?x ?z => constr:(R) end in
+  let x := match goal with |- ?R ?x ?z => constr:(x) end in
+  let z := match goal with |- ?R ?x ?z => constr:(z) end in
+  let pre_proof_term_head := constr:(@transitivity _ R _) in
+  let proof_term_head := (eval cbn in pre_proof_term_head) in
+  refine (proof_term_head x y z _ _); [ change (R x y) | change (R y z) ].
+Tactic Notation "etransitivity" := etransitivity _.
+Tactic Notation "etransitivity_rev" uconstr(y) := [ > etransitivity y; cycle 1.. ].
+Tactic Notation "etransitivity_rev" := etransitivity_rev _.
+
+Ltac transitivity_rev y := [ > transitivity y; cycle 1.. ].