V. Coq proof assistant

3. Induction principle

A recursive datatype (e.g. int, lists or trees) involves an "induction" principle. For instance, prooving a property on natural number (or a list) requires to:

1. prove the property for an initial case 0 (or the empty list), and
2. admit the property for n (or a list l) and prove the property for (n+1) (or x::l).

As a simple example, Natural numbers and the addition are defined below with some proofs of properties of the addition.

source

Nb. t3 corresponds to the "commutativity" of the addition.
But how to prove "associativity", ie. n+(m+p)=(n+m)+p ?

Formally, induction principle on natural numbers can be expressed as follow:

induction: forall P, P(0) /\ (forall n, P(n)=>P(n+1)) => forall n, P(n).

4 - 7