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 forall x:nat, O <> S x.
Proof.
  intros x H.
  inversion H.
Qed.

Goal forall 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 forall x:nat, x = O \/ exists y:nat , x = S y.
Proof.
  intro x. destruct x.
  + left. reflexivity.
  + right. exists 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 : forall 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 forall x y : nat, S x + y = S (x +y).
Proof.
  intros. reflexivity.
Qed.

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

Lemma plus_O : forall x:nat, x + O = x.
Proof.
  admit.
Qed.

Lemma commutativity : forall x y : nat, x + y = y + x.
Proof.
  admit.
Qed.

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 forall 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 : forall x:nat, O <= x.
Proof.
  admit.
Qed.

Theorem le_S_S : forall x:nat, forall y:nat,
  S x <= S y -> x <= y.
Proof.
  admit.
Qed.

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

Print lt.

Theorem le_lt : forall x:nat, forall y:nat, x < S y -> x <= y.
Proof.
  admit.
Qed.

Theorem lt_S_case : forall x:nat, forall y:nat,
  x < S y -> x = y \/ x < y.
Proof.
  admit.
Qed.

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 :
  forall (P:nat->Prop),
  (forall x:nat,
     (forall y:nat, y <x -> P y) -> P x) ->
  (forall x:nat, P x).
Proof.
  admit.
Qed.

Reasoning about multiples

One last exercise for this tutorial!

Inductive multiple : nat -> nat -> Prop :=
  | multiple_O : forall n:nat, multiple n O
  | multiple_step :
      forall n:nat, forall m:nat, multiple n m -> multiple n (n +m).

Goal forall x:nat,
  multiple 2 x -> multiple 3 x -> multiple 6 x.
Proof.
  admit.
Qed.