bossLib.Induct

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)