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.

The proof is by induction on n:

• Base case:

  q = 0 and r = 0 since 0 = 0 * d + 0.

• Induction step:

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

  Since r < d, either r = d - 1 or r < d - 1:

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

QED.

Exercise 03

Formalize the above proof in tCPA.

Hints:

• it would be a good idea to name each component of the induction hypothesis (reminder: an existential is represented as a pair);
• le_lt_or_eq will come handy to distinguish the two cases where r = d - 1 or r < d - 1;
• lt_le_S will also come handy; and
• since d is strictly positive, r = d - 1 is equivalent to S r = d and likewise for r < d - 1.

Exercise 04

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 05

More precisely, Euclid’s division lemma states that q and r are unique. Formalize and prove this unicity, starting from the following 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 06

Prove the following lemma as a corollary of Euclid’s division lemma:

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

Exercise 07

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 (and so it should be expressible as an instance of nat_fold_right).

Resource

• The .v file for Exercise 05 (latest version: 15 Mar 2024).

Version

Created [15 Mar 2024]