From c2a9824de5ccc1721d0f41a1d0f770806b67f631 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 26 Oct 2016 15:12:34 -0400 Subject: Add tactics to implement better fraction removal From https://github.com/coq/ceps/blob/master/text/007-nsatz-inequalities.md --- src/Util/Tactics.v | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'src/Util/Tactics.v') diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index d0c785fed..2f9f6c59f 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -263,7 +263,7 @@ Ltac specialize_by' tac := match goal with | [ H : ?A -> ?B |- _ ] => match type of A with - Prop => + Prop => let H' := fresh in assert (H' : A) by tac; transparent_specialize_one H H'; @@ -279,6 +279,12 @@ Ltac specialize_by tac := repeat specialize_by' tac. flaw. *) Tactic Notation "specialize_by" tactic3(tac) := specialize_by tac. +(** A marginally faster version of [specialize_by assumption] *) +Ltac specialize_by_assumption := + repeat match goal with + | [ H : ?T, H' : (?T -> ?U)%type |- _ ] => specialize (H' H) + end. + (** If [tac_in H] operates in [H] and leaves side-conditions before the original goal, then [side_conditions_before_to_side_conditions_after tac_in H] does -- cgit v1.2.3