Next: Infix Notation Up: New features in LEGO Version 1.3 Previous: Elimination Rule for Relations

LEGO Version 1.3: Induction

Fed up typing `Refine blah_elim (* cut and paste the goal and square a few brackets *)'? The new Induction tactic is intended to ease your irritation.

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:

Hence Induction 1; will turn

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


  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.