Add eta_expand to Prod.v

1 files changed, 17 insertions, 0 deletions

diff --git a/src/Util/Prod.v b/src/Util/Prod.v
index 39e32865f..b83aea68f 100644
--- a/src/Util/Prod.v
+++ b/src/Util/Prod.v
@@ -91,3 +91,20 @@ Ltac inversion_prod_step :=
     => induction_path_prod H
   end.
 Ltac inversion_prod := repeat inversion_prod_step.
+
+(** This turns a goal like [x = let v := p in let '(x, y) := f v in x
+    + y)] into a goal like [x = fst (f p) + snd (f p)].  Note that it
+    inlines [let ... in ...] as well as destructuring lets. *)
+Ltac only_eta_expand_and_contract :=
+  repeat match goal with
+         | [ |- context[let '(x, y) := ?e in _] ]
+           => rewrite (surjective_pairing e)
+         | _ => rewrite <- !surjective_pairing
+         end.
+Ltac eta_expand :=
+  repeat match goal with
+         | _ => progress cbv beta iota zeta
+         | [ |- context[let '(x, y) := ?e in _] ]
+           => rewrite (surjective_pairing e)
+         | _ => rewrite <- !surjective_pairing
+         end.