# Library nats

# Natural numbers

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.

# Addition

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.

Admitted.

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

Proof.

Admitted.

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

Proof.

Admitted.

# Order

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.

Admitted.

Theorem le_S_S : ∀ x:nat, ∀ y:nat,

S x ≤ S y → x ≤ y.

Proof.

Admitted.

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.

Admitted.

Theorem lt_S_case : ∀ x:nat, ∀ y:nat,

x < S y → x = y ∨ x < y.

Proof.

Admitted.