induction

induction is an extension of destruct that allows for case analysis on inductive terms, gaining an inductive hypothesis for each recursive subterm generated by the term destruction. The arguments of induction are patterns.

If the goal still contains named impliciations, induction can be used before introducing them with intros. In this case, if the argument to induction is not the first impliciation in the chain, all implications before it will be introduced to the goal’s assumption space.

induction can act similarly to inversion under specific circumstances. If you induct over an object that already contains subterms, you can remember the subterm(s) and induct on the root object. Then, by an easy inversion on the hypothesis generated by remember, all cases that don’t match the required form generated by the case analysis will be automatically solved by the principle of explosion.

Sometimes, the automatically-generated induction principles for a type are not sufficient to prove some properties about terms with that type. In this case, it is possible to write a custom induction principle for a type and then use it with the induction tactic.

Syntax

(* Simple usage *)
induction n.

(* Induct over a term and introduce a hypothesis E showing its equivalence to the form it took *)
induction n eqn:E.

(* Providing names for newly-introduced terms *)
induction n as [| n' IHn' ].

(* Using a custom induction principle *)
induction z using peano_ind.

Examples

Before

n: nat
=========================
n + 0 = n

induction n as [| n' IHn' ].

After (first goal generated)

=========================
1/2
0 + 0 = 0

After (second goal generated)

n': nat
IHn' : n' + 0 = n'
=========================
1/1
S n' + 0 = S n'

Script

Theorem induction_example1 : forall (n : nat),
    n + 0 = n.
Proof.
    induction n.
    - reflexivity.
    - simpl. rewrite IHn. reflexivity.
Qed.

Script

Require Import ZArith.
Open Scope Z.
Theorem induction_example2 : forall (x y : Z),
    x + y = y + x.
Proof.
    induction x using Z.peano_ind.
    - intros. simpl. rewrite Z.add_0_r. reflexivity.
    - intros. rewrite Z.add_succ_l. rewrite IHx.
      rewrite Z.add_comm. rewrite <- Z.add_succ_l.
      rewrite Z.add_comm. reflexivity.
    - intros. rewrite Z.add_pred_l. rewrite IHx.
      rewrite Z.add_comm. rewrite <- Z.add_pred_l.
      rewrite Z.add_comm. reflexivity.
Qed. 

Resources

Reference Documentation

“Induction Principles” - Logical Foundations

---