REDUCE_TAC
reduceLib.REDUCE_TAC : tactic
Performs arithmetic or boolean reduction on a goal at all levels possible.
REDUCE_TAC attempts to transform a goal by applying REDUCE_CONV. It
will prove any true goal which is constructed from numerals and the
boolean constants T and F.
Failure
Never fails, but may not advance the goal.
Example
The following example takes a couple of minutes' CPU time:
> g ‘((1 EXP 3) + (12 EXP 3) = 1729) /\ ((9 EXP 3) + (10 EXP 3) = 1729)’;
> e reduceLib.REDUCE_TAC;;
OK..
val it =
Initial goal proved
⊢ 1 EXP 3 + 12 EXP 3 = 1729 ∧ 9 EXP 3 + 10 EXP 3 = 1729 : proof
See also
reduceLib.RED_CONV,
reduceLib.REDUCE_CONV,
reduceLib.REDUCE_RULE