Induction, sometimes called mathematical induction, is a tool for reasoning about countably infinite structures. Commonly, we can use something called a "proof by induction" to verify facts which reside in infinity.

Let's review. Pretend you're majoring in computer science at a college and you're in your first year: You are asked to show that a + b = b + a. We both hope that you proceed as follows--

The professor updates the question. "Please show forall (a b : nat), a + b = b + a"

We hope you do not commence with the following list

0 + 1 = 1 + 0
1 + 2 = 2 + 1
0 + 2 = 2 + 0
...

Even if you were aware that a systematic listing procedure exists, you would be foiled by lack of paper, because you're asked to operate on all of an infinite set (or, in short time, a type).

We instead hope you commence the following proof

Fixpoint plus (n m : nat) : mynat :=
  match n with
  | Z => m
  | S n' => S (plus n' m)
  end.
Inductive nat : Type :=
| Z : nat
| S (n : nat) : nat.
Inductive listnat : Type :=
  | empt : listnat
  | cons (h : nat) (t : listnat) : listnat.

Fixpoint append (l1 l2 : listnat) : listnat :=
  match l1 with
  | empt => l2
  | cons h t => cons h (append t l2)
  end.

Fixpoint rev (l : listnat) : listnat :=
  match l with
  | empt => empt
  | cons h t => append (reverse t) (cons h empt)
  end.
Theorem reverse_involutive : forall (l : listnat),
    reverse (reverse l) = l.
Proof.
  intros l.
  induction l as [| head tail IHtail].
  - simpl; reflexivity.
  - simpl.
    rewrite reverse_append_distributive.
    rewrite IHtail.
    simpl.
    reflexivity.
Qed.

In Coq, every inductive data type (that is, a type defined with the Inductive keyword) comes equipped with an induction principle. Let's observe the following definition

Inductive coin :=
  | heads : coin
  | tails : coin.

This is saying that heads is a coin and tails is a coin, and if you observe the Coq system's output when you run this block of code it says

coin is defined
coin_rect is defined
coin_ind is defined
coin_rec is defined

coin_ind is the induction principle for the coin data type. Let's run Check coin_ind to print it out

coin_ind
     : forall P : coin -> Prop, P heads -> P tails -> forall c : coin, P c

This is just a function type. In english, it says "for every predicate over coins, if it holds of heads and of tails, then it holds for all coins."

To see it in action, define a predicate (a function coin -> Prop, where Prop stands for Propositions)

Definition is_heads : coin -> Prop :=
  fun c => c = heads.

and apply coin_ind to is_heads

Check coin_ind is_heads
(* coin_ind is_heads
     : is_heads heads -> is_heads tails -> forall c : coin, is_heads c *)

We have specialized the induction principle which is defined over all predicates to a particular predicate is_heads. To further specialize it, we would need to supply a proof of is_heads heads, and to specialize it all the way to the end we would need a proof of is_heads tails. is_heads tails is not a provable proposition, so the example is silly.

I wanted to show you that function application happens at the type level and that specializing a forall behaves like supplying an argument to a function.

The Professor writes Check listnat on the board, and just beneath it begins to materialize the following type

listnat_ind
     : forall P : listnat -> Prop,
       P empt ->
       (forall (h : nat) (t : listnat), P t -> P (cons h t)) ->
       forall l : listnat, P l
nat_ind
     : forall P : nat -> Prop,
       P Z -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

The english translation for the preceding type is literally the definition of ordinary, vanilla "mathematical induction". The type nat_ind is nothing but an algorithmic description of how to prove stuff about nat, and you'll find the same for any other inductive type (including bool (which we saw by another name, coin), various types of trees, and even whole programming languages).

Inductive tree : Type :=
  | leaf (n : nat) : tree
  | node (l r : tree) : tree.

The board shimmers as it announces: tree is defined. tree_ind is defined.

tree_ind 
     : forall P : tree -> Prop, 
     (forall (n : nat), P (leaf n)) -> 
     (forall (l : tree), P l -> forall (r : tree), P r -> P (node l r)) -> 
     forall (t : tree), P t

To learn more, read Software Foundations.