----------------------------------------------------------------------
Induct                                                       (bossLib)
----------------------------------------------------------------------
Induct : tactic

SYNOPSIS
Performs structural induction over the type of the goal’s
outermost universally quantified variable.

KEYWORDS
tactic, induction

LIBRARY
BasicProvers

DESCRIBE
Given a universally quantified goal, {Induct} attempts to perform an
induction based on the type of the leading universally quantified
variable.  The induction theorem to be used is looked up in the
{TypeBase} database, which holds useful facts about the system’s defined
types. {Induct} may also be used to reason about mutually recursive types.

FAILURE
{Induct} fails if the goal is not universally quantified, or if the
type of the variable universally quantified does not have an induction
theorem in the {TypeBase} database.

EXAMPLE
If attempting to prove

   !list. LENGTH (REVERSE list) = LENGTH list

one can apply {Induct} to begin a proof by induction on {list}.

   - e Induct;

This results in the base and step cases of the induction as new goals.

   ?- LENGTH (REVERSE []) = LENGTH []

   LENGTH (REVERSE list) = LENGTH list
   ?- !h. LENGTH (REVERSE (h::list)) = LENGTH (h::list)

The same tactic can be used for induction over numbers. For example
expanding the goal

   ?- !n. n > 2 ==> !x y z. ~(x EXP n + y EXP n = z EXP n)

with {Induct} yields the two goals

   ?- 0 > 2 ==> !x y z. ~(x EXP 0 + y EXP 0 = z EXP 0)

   n > 2 ==> !x y z. ~(x EXP n + y EXP n = z EXP n)
   ?- SUC n > 2 ==> !x y z. ~(x EXP SUC n + y EXP SUC n = z EXP SUC n)

{Induct} can also be used to perform induction on mutually recursive types.
For example, given the datatype

   Hol_datatype
       `exp = VAR of string                (* variables *)
            | IF  of bexp => exp => exp    (* conditional *)
            | APP of string => exp list    (* function application *)
         ;
       bexp = EQ  of exp => exp            (* boolean expressions *)
            | LEQ of exp => exp
            | AND of bexp => bexp
            | OR  of bexp => bexp
            | NOT of bexp`

one can use {Induct} to prove that all objects of type {exp} and {bexp}
are of a non-zero size. (Recall that size definitions are automatically
defined for datatypes.) Typically, mutually recursive types lead to
mutually recursive induction schemes having multiple predicates. The
scheme for the above definition has 3 predicates: {P0}, {P1}, and {P2},
which respectively range over expressions, boolean expressions, and
lists of expressions.

   |- !P0 P1 P2.
        (!a. P0 (VAR a)) /\
        (!b e e0. P1 b /\ P0 e /\ P0 e0 ==> P0 (IF b e e0)) /\
        (!l. P2 l ==> !b. P0 (APP b l)) /\
        (!e e0. P0 e /\ P0 e0 ==> P1 (EQ e e0)) /\
        (!e e0. P0 e /\ P0 e0 ==> P1 (LEQ e e0)) /\
        (!b b0. P1 b /\ P1 b0 ==> P1 (AND b b0)) /\
        (!b b0. P1 b /\ P1 b0 ==> P1 (OR b b0)) /\
        (!b. P1 b ==> P1 (NOT b)) /\
        P2 [] /\
        (!e l. P0 e /\ P2 l ==> P2 (e::l))
          ==>
        (!e. P0 e) /\ (!b. P1 b) /\ !l. P2 l

Invoking {Induct} on a goal such as

   !e. 0 < exp_size e

yields the three subgoals

   ?- !s. 0 < exp_size (APP s l)


   [ 0 < exp_size e, 0 < exp_size e' ] ?- 0 < exp_size (IF b e e')

   ?- !s. 0 < exp_size (VAR s)

In this case, {P1} and {P2} have been vacuously instantiated in the
application of {Induct}, since it detects that only {P0} is
needed. However, it is also possible to use {Induct} to start the proofs
of

    (!e. 0 < exp_size e) /\ (!b. 0 < bexp_size b)

and

    (!e. 0 < exp_size e) /\
    (!b. 0 < bexp_size b) /\
    (!list. 0 < exp1_size list)


SEEALSO
bossLib.Induct_on, bossLib.completeInduct_on,
bossLib.measureInduct_on, Prim_rec.INDUCT_THEN, bossLib.Cases,
bossLib.Hol_datatype, proofManagerLib.g, proofManagerLib.e.

----------------------------------------------------------------------