# Natural numbers

Natural numbers are pre-defined in Coq, as shown by the next query. Syntactic sugar is also available to write e.g. 2 instead of S (S O).

Print nat.

Goal 2 = S (S O).
Proof.
reflexivity.
Qed.

The inductive definition of nat is outside of the capabilities of first-order logic: it has a number of implicit consequences shown next.
Note here the use of inversion on equalities between constructors of the inductive type nat.

Goal x:nat, O S x.
Proof.
intros x H.
inversion H.
Qed.

Goal x y : nat, S x = S y x = y.
Proof.
intros x y H.
inversion H.
reflexivity.
Qed.

We can use destruct to perform case analysis over a natural number.

Goal x:nat, x = O y:nat, x = S y.
Proof.
intro x. destruct x.
+ left. reflexivity.
+ right. x. reflexivity.
Qed.

An induction principle is also derived from the inductive definition, which is implicitly used through the induction tactic. Note that the induction principle is a higher-order formula, quantifying over Prop.

Check nat_ind.

Lemma Sx_x : x:nat, S x x.
Proof.
intros x H.
induction x.
+ inversion H.
+ inversion H. apply IHx. exact H1.
Qed.

x+y is a notation for plus x y. Unlike in first-order logic, plus is not an abstract function symbol whose interpretation is constrained by axioms.
Rather, it is defined as a recursive function over natural numbers. In Coq, all functions are total: termination is guaranteed and there are no errors.

Print plus.

In the next proof we use simpl to compute 1+1. Note that the proof script works without this explicit simplification step.

Goal 2 = 1+1.
Proof.
simpl.
reflexivity.
Qed.

Goal x y : nat, S x + y = S (x+y).
Proof.
intros. reflexivity.
Qed.

The next proofs are not obvious computations for Coq: induction will be needed instead. In order to use an equality hypothesis, you will need the rewrite tactic.

Goal x y z : nat, x = y x + z = y + z.
Proof.
intros x y z Heq.
rewrite Heq.
reflexivity.
Qed.

Lemma plus_S : x y : nat, x + S y = S (x + y).
Proof.

Lemma plus_O : x:nat, x + O = x.
Proof.

Lemma commutativity : x y : nat, x + y = y + x.
Proof.

# Order

x y is a notation for le x y, where le is inductively defined as shown by the next query.
The constructors le_n and le_S that define le can be used as hypothesis / lemmas e.g. in the apply tactic.

Print le.

Goal le 2 3.
Proof.
apply le_S. apply le_n.
Qed.

If x y holds it must have been obtained through one of the two constructors: the corresponding case analysis rule is given by the inversion tactic.

Goal x y : nat, x y x = y x pred y.
Proof.
intros x y H. inversion H.
+ left. reflexivity.
+ right.
simpl. exact H0.
Qed.

Theorem le_O : x:nat, O x.
Proof.

Theorem le_S_S : x:nat, y:nat,
S x S y x y.
Proof.

x<y is a notation for lt x y which is itself defined in terms of le.

Print lt.

Theorem le_lt : x:nat, y:nat, x < S y x y.
Proof.

Theorem lt_S_case : x:nat, y:nat,
x < S y x = y x < y.
Proof.

# Strong induction

With the above ingredients, you should be able to prove a strong induction principle, expressed using a quantification over natural number predicates.

Theorem strong_induction :
(P:natProp),
( x:nat, ( y:nat, y < x P y) P x)
( x:nat, P x).
Proof.