From e7b3d3713e895639c7b9e2c3388d7168d15514ba Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 7 Oct 2016 17:41:31 -0400 Subject: Add eta_expand to Prod.v --- src/Util/Prod.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'src/Util/Prod.v') 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. -- cgit v1.2.3