LEGO Version 1.3: Induction

Simply select a premise of an inductive type from the goal, and Induction does the rest. The usage is thus one of

Induction name;	do induction on premise {name:type}
Induction number;	do induction on numberth unnamed premise (type)->
Induction term;	abstract term from the goal, then do induction on it

For example,

    ?0 : {m:nat}Eq (plus m zero) m
  Lego> Induction m;
    ?1 : Eq (plus zero zero) zero
    ?2 : {m:nat}(Eq (plus m zero) m)->Eq (plus (suc m) zero) (suc m)

Induction is more than just sugar for `Refine blah_elim'. It will also perform the following rearrangements if necessary:

• The premises will be reordered so that those required for the induction are in the correct sequence and leftmost.
• Any polymorphic parameters (eg a list element type) are fixed in the context.
• In order to do induction on a premise
  (R .. term ..) -> ..
  where term is not a variable, the tactic will introduce a variable and an equality constraint to get
  {x:type}(R .. x ..) -> (Eq x term) -> ..

    ?0: {n|nat}{T|Type}(vect T (suc n))->(vect T n)

into

  T | Type
    ?5: {k:nat}(vect T k)->{n':nat}(Eq k (suc n'))->(vect T n')

before doing induction on the (vect T k) premise.

Note that any equalities introduced by Induction will be as far left in the rewritten goal as their variable dependencies permit, in order to facilitate an attack by Qnify. Type dependencies between parameters are handled using sigma types.

Induction can team up with Invert and Qnify using the Then tactical to produce some very powerful effects:

  Lego> Goal {n:nat}{Sn_le_n:le (suc n) n}absurd;
    ?0 : {n:nat}(le (suc n) n)->absurd
  Lego> Induction n Then intros Then Invert Sn_le_n Then Qnify Then Immed;
    (* machine output *)
  *** QED ***

The Induction tactic uses the equality registered by Configure Equality. Mutual induction is not yet supported.