3. Inductive Definitions and Structural Induction

Inductive Definitions and Structural Induction

Understanding inductive definitions

An inductive definition is a way of defining a set or a data type by specifying a base case and one or more constructors that generate new elements of the set from existing elements. In Coq, inductive definitions are used to define data structures such as lists, trees, and other recursively defined objects.

Principles of structural induction

Structural induction is a proof technique used to reason about recursively defined objects. It involves proving that a property holds for all elements of a recursively defined set by considering the base case and showing that if the property holds for the constructor(s), it also holds for the generated elements. Structural induction is widely used in mathematics and computer science to prove properties of inductively defined data structures.

Coq lab activities: Writing and proving properties about inductively defined data structures in Coq

In this lab activity, we will use Coq to define inductively defined data structures and prove properties about them using structural induction.

Lab Activities

Definition of Natural Numbers in Coq

We will define the set of natural numbers (Nat) using the Peano axioms in Coq. The Peano axioms state that 0 is a natural number, and every natural number has a successor, which is also a natural number.

Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

Proving Properties of Natural Numbers

Using structural induction, we will prove properties of natural numbers. For example, we can prove the commutativity of addition:

Lemma plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
  induction n as [| n' IHn'].
  - simpl. intros. rewrite <- plus_n_O. reflexivity.
  - simpl. intros. rewrite <- plus_n_Sm. rewrite <- IHn'. reflexivity.
Qed.

This Coq code proves the commutativity of addition for natural numbers. The proof uses structural induction on the first argument (n), considering the base case (n = 0) and the inductive step (n = S n').