Library nats

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.

Addition

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.
Admitted.

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

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

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.
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.

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:nat →Prop),
  (∀ x:nat, (∀ y:nat, y < x → P y ) → P x ) →
  (∀ x:nat, P x ).
Proof.
Admitted.

Reasoning about multiples

One last exercise for this tutorial!

Inductive multiple : nat → nat → Prop :=
  | multiple_O : ∀ n:nat, multiple n O
  | multiple_step :
      ∀ n:nat, ∀ m:nat, multiple n m → multiple n (n +m).

Goal ∀ x :nat ,
  multiple 2 x → multiple 3 x → multiple 6 x.
Proof.
Admitted.