Integers¶

To work with integers in tCPA, one needs to use the arithmetic library for them:

Require Import ZArith.

Resources¶

A .v file about integers (latest version: 27 Jun 2025).

Prelude¶

Dana: Good news!

Bong-sun: Yes?

Dana: The ring tactic works for integers!

Bong-sun: Good news indeed. Thanks.

Pablito (making sure): You mean it works even with subtractions?

Dana: Yup.

Bong-sun: Let me check:

Theorem binomial_expansion_at_rank_2 :
  forall x y : Z,
    ((x - y) * (x - y) = x * x - 2 * x * y + y * y)%Z.
Proof.
  intros x y.
  ring.
Qed.

Bong-sun: OK.

Halcyon: This is so cool!

Summations over integers¶

To make integers coexist with natural numbers in the same syntactic unit, one needs to declare the type of subexpressions explicitly:

Fixpoint Sigma0 (n : nat) (f : nat -> Z) : Z :=
  match n with
  | O =>
    f 0
  | S n' =>
    Sigma0 n' f + f (S n')
  end.

Lemma fold_unfold_Sigma0_O :
  forall (f : nat -> Z),
    Sigma0 0 f =
    f 0.

Lemma fold_unfold_Sigma0_S :
  forall (n' : nat)
         (f : nat -> Z),
    Sigma0 (S n') f =
    (Sigma0 n' f + f (S n'))%Z.

The fundamental theorem of calculus for int-valued functions¶

Unlike for nat-valued functions, the fundamental theorem of calculus holds for int-valued functions:

Theorem fundamental_for_int_valued_functions :
  forall (f : nat -> Z)
         (n : nat),
    Sigma0 n (fun i => (f (S i) - f i)%Z) = (f (S n) - f 0%nat)%Z.

The proof is by routine induction on n, using the ring tactic in the induction step. (See the accompanying file.)

Abel’s lemma for int-valued functions¶

Unlike for nat-valued functions, the summation by parts holds unconditionally for int-valued functions:

Theorem summation_by_parts_for_int_valued_functions : (* Abel's lemma *)
  forall (f g : nat -> Z)
         (n : nat),
    (Sigma0 n (fun i => f i * (g (S i) - g i)) + f 0%nat * g 0%nat + Sigma0 n (fun i => g (S i) * (f (S i) - f i)))%Z
    =
    (f (S n) * g (S n))%Z.

The proof is by routine induction on n, using the ring tactic in the induction step. (See the accompanying file.)

Absolute values¶

Here is a simple implementation of the absolute-value function:

Definition abs (n : Z) : Z :=
  if (n <? 0)%Z
  then 0 - n
  else n.

Two identities about absolute values¶

In one of his trip reports, Dijkstra mentions the following two identities about absolute values:

Theorem Dijkstra_s_abs :
  forall a b : Z,
    (abs a < b <-> a < b /\ 0 - a < b)%Z
    /\
    (a < abs b <-> a < b \/ a < 0 - b)%Z.

Their proof is by cases:

first conjunct:
- a is either negative or zero or positive (trichotomy)
 - case a < 0: abs a = 0 - a
 
 to show: 0 - a a a 0:
 
 since a is negative, a < 0 - a
 
 since a < 0 - a and 0 - a < b, then a 0 - a 0 0: abs a = a
 
 to show: a a a 0:
 
 since a is positive, 0 - a < a
 
 since 0 - a < a and a < b, then 0 - a a < b
 
 immediate since the first conjunct in the assumption is what we need to prove
second conjunct:
- b is either negative or zero or positive (trichotomy)
 - case b < 0: abs b = 0 - b
 
 to show: a < 0 - b <-> a a a < 0 - b
 
 or equivalently: (a a < 0 - b) /(a < 0 - b -> a < 0 - b)
 - proof of the first conjunct: a a < 0 - b
 
 since b is negative, 0 - b is positive and therefore b < 0 - b
 
 so we have a a < 0 - b
 
 immediate
 - case b = 0: abs b = 0
 
 to show: a < 0 <-> a < 0 / a < 0
 
 immediate
 - case b > 0: abs b = b
 
 to show: a a a a a < b) /(a < 0 - b -> a < b)
 - proof of the first conjunct: a a a < b
 
 since b is positive, 0 - b is negative and therefore 0 - b < b
 
 so we have a < 0 - b and 0 - b < b
 
 and therefore, by transitivity, a < b

This informal proof is formalized in the accompanying file, as an illustration that the skills acquired so far with natural numbers apply to integers.

Divisibility of polynomials¶

The rest of this chapter is dedicated to proving divisibility properties of polynomials, using the following exponentation function:

Fixpoint zpower (x : Z) (n : nat) : Z :=
  match n with
    O =>
    1%Z
  | S n' =>
    x * zpower x n'
  end.

Exercise 07¶

As a warmup, prove the following properties of exponentation over integers.

Exponentiating one yields one:

Property about_exponentiating_one :
  forall n : nat,
    (zpower 1 n = 1)%Z.

Exponentiating a product yields the product of the exponentiations:

Property about_exponentiating_a_product :
  forall (x y : Z)
         (n : nat),
    (zpower (x * y) n = zpower x n * zpower y n)%Z.

Exponentiating with a sum yields the product of the exponentiations:

Property about_exponentiating_with_a_sum :
  forall (x : Z)
         (i j : nat),
    (zpower x (i + j) = zpower x i * zpower x j)%Z.

Exponentiating with a product yields a tower of exponentiations:

Property about_exponentiating_with_a_product :
  forall (x : Z)
         (y z : nat),
    zpower x (y * z) = zpower (zpower x y) z.

Exercise 08¶

The following properties are about the result of exponentiating an integer x with an odd natural number, plus or minus one: The result is divisible by x + 1 or by x - 1, respectively.

Prove the following property:

Property about_exponentiating_an_integer_with_an_odd_natural_number_and_then_adding_one :
  forall (x : Z)
         (n : nat),
    exists q : Z,
      (zpower x (2 * n + 1) + 1 = q * (x + 1))%Z.

Prove the following property:

Property about_exponentiating_an_integer_with_an_odd_natural_number_and_then_subtracting_one :
  forall (x : Z)
         (n : nat),
    exists q : Z,
      (zpower x (2 * n + 1) - 1 = q * (x - 1))%Z.

Solution for Exercise 08a¶

Dana: Let’s consider the case where n is 0. This base case reads:

forall x : Z, exists q : Z, x^1 + 1 = q * (x + 1)

Bong-sun: Peace of cake, then, since:

x^1 = 1

Dana: OK, so q is 1.

Alfrothul: May I?

Dana: By all means.

Alfrothul: Let’s consider the case where n is 1. This case reads:

forall x : Z, exists q : Z, x^3 + 1 = q * (x + 1)

Bong-sun: q must be a polynomial.

Dana: Of degree 2, since multiplying by x + 1 – which is a polynomial of degree 1 – yields x^3 + 1 – which is a polynomial of degree 3.

Bong-sun: Right. And its coefficient for x^2 must be 1, since the coefficient of x^3 is 1.

Alfrothul: Likewise, its coefficient for x^0 must be 1.

Dana: So let’s posit:

q = x^2 + b * x^1 + 1

Halcyon: OK.

Dana: Now we must find what b stands for to satisfy:

x^3 + 1 = (x^2 + b * x^1 + 1) * (x + 1)

Bong-sun: Let’s calculate:

x^3 + 1 = (x^2 + b * x^1 + 1) * (x + 1)
        = (x^2 + b * x^1 + 1) * (x^1 + 1)
        = (x^3 + b * x^2 + 1 * x^1) + (x^2 + b * x^1 + 1)
        = x^3 + (b + 1) * x^2 + (1 + b) * x^1 + 1

Alfrothul: For this equality to hold, the coefficients of x^2 and of x^1 must be 0, so:

b + 1 = 0

1 + b = 0

Bong-sun: So:

b = -1

Dana: Right. So:

q = x^2 - x^1 + 1

Alfrothul: How about we consider the case where n is 2? This case reads:

forall x : Z, exists q : Z, x^5 + 1 = q * (x + 1)

Bong-sun: Again, q must be a polynomial.

Dana: Of degree 4, since multiplying by x + 1 yields x^5 + 1.

Bong-sun: Right. And its coefficient for x^5 must be 1.

Alfrothul: Likewise, its coefficient for x^0 must be 1.

Dana: All true. But let’s be pedandic and posit:

q = a * x^4 + b * x^3 + c * x^2 + d * x^1 + e * x^0

Halcyon (thoughtfully): There is nothing wrong with being pedantic.

Dana: So now we must find what a, b, c, d, and e stand for to satisfy:

x^5 + 1 = (a * x^4 + b * x^3 + c * x^2 + d * x^1 + e * x^0) * (x + 1)

Bong-sun: Again, let’s calculate:

x^5 + 1 = (a * x^4 + b * x^3 + c * x^2 + d * x^1 + e * x^0) * (x + 1)
        = (a * x^4 + b * x^3 + c * x^2 + d * x^1 + e * x^0) * (x^1 + 1)
        = (a * x^5 + b * x^4 + c * x^3 + d * x^2 + e * x^1) + (a * x^4 + b * x^3 + c * x^2 + d * x^1 + e * x^0)
        = (a * x^5 + b * x^4 + c * x^3 + d * x^2 + e * x^1)
          +         (a * x^4 + b * x^3 + c * x^2 + d * x^1 + e * x^0)
        = a * x^5 + (b + a) * x^4 + (c + b) * x^3 + (d + c) * x^2 + (e + d) * x^1 + e * x^0

Alfrothul: For this equality to hold, the coefficient of x^5 must be 1, the coefficients of x^4, x^3, x^2, and x^1 must be 0, and the coefficient of x^0 must be 1, so:

a = 1

b + a = 0

c + b = 0

d + c = 0

e + d = 0

e = 1

Bong-sun: So:

a = 1

b = 0 - a = 0 - 1 = -1

c = 0 - b = 0 - -1 = 1

d = 0 - c = 0 - 1 = -1

e = 0 - d = 0 - -1 = 1

e = 1

Dana: Right. So:

q = x^4 - x^3 + x^2 - x^1 + 1

Alfrothul: Guys, there is a pattern here:

q = x^4 - x^3 + (x^2 - x^1 + (1))

Bong-sun: Indeed there is one, and we are going to exploit it. In the case where n is n' + 1, the induction hypothesis reads:

exists q' : Z, x^(2 * n' + 1) + 1 = q' * (x + 1)

Alfrothul: Right. And we need to prove:

exists q : Z, x^(2 * (n' + 1) + 1) + 1 = q * (x + 1)

Bong-sun: Based on our calculations, here is our witness:

q = x^(n' + 2) - x^(n' + 1) + q'

Dana: Rock’n’roll:

Property about_exponentiating_an_integer_with_an_odd_natural_number_and_then_adding_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (2 * n + 1) + 1 = q * (x + 1))%Z.
Proof.
  intros x n.

Pablito (helpful): The *goals* window reads:

x : Z
n : nat
============================
exists q : Z, (zpower x (2 * n + 1) + 1)%Z = (q * (x + 1))%Z

Dana: Thanks, Pablito. First, let’s get more comfortable:

rewrite -> Nat.add_1_r.