Simply select a premise of an inductive type from the goal, and Induction does the rest. The usage is thus one of
|
do induction on premise {name:type} |
|
do induction on numberth unnamed premise (type)-> |
|
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:
?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.