INDUCT_TAC
numLib.INDUCT_TAC : tactic
Performs tactical proof by mathematical induction on the natural numbers.
INDUCT_TAC reduces a goal !n.P[n], where n has type num, to two
subgoals corresponding to the base and step cases in a proof by
mathematical induction on n. The induction hypothesis appears among
the assumptions of the subgoal for the step case. The specification of
INDUCT_TAC is:
A ?- !n. P
======================================== INDUCT_TAC
A ?- P[0/n] A u {P} ?- P[SUC n'/n]
where n' is a primed variant of n that does not appear free in the
assumptions A (usually, n' just equals n). When INDUCT_TAC is
applied to a goal of the form !n.P, where n does not appear free in
P, the subgoals are just A ?- P and A u {P} ?- P.
Failure
INDUCT_TAC g fails unless the conclusion of the goal g has the form
!n.t, where the variable n has type num.