The Euclidean division

Goal

The goal of this lecture note is to formalize Euclid’s division lemma.

Euclid’s division lemma

For any positive natural number d (the divisor) and for any natural number n (the dividend), there exists a natural number q (the quotient) and a natural number r (the remainder) such that r < d and n = q * d + r hold.

The proof is by induction on n:

• Base case: (n = O)

  q = 0 and r = 0 do the job since 0 < d and 0 = 0 * d + 0 hold.

• Induction step: (n = S n')

  Under the induction hypothesis that for a given n', there exist q' and r' such that r' < d and n' = q' * d + r' hold, we need to show that there exist q and r such that r < d and S n' = q * d + r hold.

  Since r' < d, either r' < d - 1 (r' is way smaller than d) or r' = d - 1 (r' just precedes d):

  • if r' < d - 1 then q = q' and r = S r' do the job;
  • if r' = d - 1 then q = S q' and r = 0 do the job.

QED.

Exercise 06

Formalize the above proof in tCPA.

Hints:

• it would be a good idea to name each component of the induction hypothesis (reminder: in an assumption, an existentially quantified expression such as exists x : a_type, an_expression is deconstructed as the pair [x H_x] where x is the witness and H_x is the assumption about x, i.e., the expression);

• the library lemma forall n m : nat, n < m -> S n <= m (named lt_le_S in the author’s version of tCPA) will also come handy; and

• the library lemma forall n m : nat, n <= m -> n < m \/ n = m (named le_lt_or_eq in the author’s version of tCPA) will come handy to distinguish the two cases r' < d - 1 and r' = d - 1;

• since d is strictly positive, r' < d - 1 is equivalent to S r' < d and likewise, r' = d - 1 is equivalent to S r' = d.

(Concretely, r' < d implies S r' <= d which implies S r' < d \/ S r' = d which gives rise to the proof by cases.)

Exercise 07

Here is an alternative statement of Euclid’s division lemma: for any natural number d and for any natural number n, there exists a natural number q and a natural number r such that r < S d and n = q * S d + r.

1. Prove informally this alternative statement.
2. Formalize this alternative statement in tCPA and prove it formally.
3. Prove formally this alternative statement as a corollary of the original statement.
4. Prove formally the original statement as a corollary of this alternative statement.

Exercise 08

More precisely, Euclid’s division lemma states that q and r are unique. Formalize and prove this unicity, starting from this accompanying resource file that formalizes the uniqueness proof in Wikipedia:

Lemma uniqueness :
  forall n d : nat,
  forall q1 r1 : nat,
    n = q1 * S d + r1 ->
    r1 < S d ->
    forall q2 r2 : nat,
      n = q2 * S d + r2 ->
      r2 < S d ->
      q1 = q2 /\ r1 = r2.

(Apologies for spoiling the fun of stating this lemma, but it is critical to start off simply and correctly.)

Exercise 09

Prove the following lemma as a corollary of (either version of) Euclid’s division lemma:

Lemma even_or_odd :
  forall n : nat,
    exists q : nat,
      n = 2 * q \/ n = S (2 * q).

Exercise 10

Implement at least one function quorem of type nat -> nat -> option (nat * nat) that, given a natural number n (the dividend) and a positive natural number d (the divisor), computes a pair of natural numbers (q, r) where q is the quotient and r is the remainder of dividing n by d. (The option type accounts for division by zero.)

At least one of your implementations should be using structural recursion over n the way the proof above is using structural induction over the dividend.

Resource

• The accompanying .v file for Exercise 08 (latest version: 13 Mar 2025).

Version

Clarified the statement of Exercise 06 [24 Mar 2025]

Created [13 Mar 2025]