The addition function over natural numbers is total, in that it is defined for all its arguments.
The subtraction function over natural numbers is partial, in that it is only defined when its first argument is not smaller than its second.
Gallina only features pure and total functions, and so the implementation of the subtraction function is also total. It satisfies the following specification:
Definition specification_of_subtraction (monus : nat -> nat -> nat) :=
forall n1 n2 : nat,
(n1 < n2 -> monus n1 n2 = 0)
/\
(n1 >= n2 -> monus n1 n2 = n1 - n2).
In words,
(The name “monus” originates in Church’s encoding of natural numbers as lambda terms, when the world was young.)
The problem with monus is that algebraic identities involving subtractions hold for integers but they do not hold for natural numbers in general. As a consequence, the library lemmas about subtractions are conditional:
Nat.sub_add : forall n m : nat, n <= m -> m - n + n = m
Nat.add_sub_assoc : forall n m p : nat, n <= m -> p + (m - n) = p + m - n
The goal of this chapter is to illustrate the problem with substracting natural numbers with the discrete counterpart of the fundamental theorem of calculus, which – as it happens – only holds for non-decreasing nat-valued functions.
The following definition is inherited from the chapter about formalizing summations:
Fixpoint Sigma0 (n : nat) (f : nat -> nat) : nat :=
match n with
| O =>
f 0
| S n' =>
Sigma0 n' f + f (S n')
end.
This implementation satisfies the following sketchy characterization:
Proposition sketchy_characterization_of_Sigma0 :
forall f : nat -> nat,
(Sigma0 0 f = f 0)
/\
(Sigma0 1 f = f 0 + f 1)
/\
(Sigma0 2 f = f 0 + f 1 + f 2)
/\
(Sigma0 3 f = f 0 + f 1 + f 2 + f 3).
If a nat-valued function is non-decreasing, applying it to 0 yields its smallest result:
Lemma about_the_least_result_of_a_non_decreasing_nat_valued_function_ :
forall f : nat -> nat,
(forall m : nat,
f m <= f (S m)) ->
forall n : nat,
f 0 <= f n.
The proof is by induction on n. (See the accompanying file.)
The fundamental theorem of calculus only holds for non-decreasing nat-valued functions:
Theorem fundamental_for_nat_valued_functions :
forall f : nat -> nat,
(forall m : nat,
f m <= f (S m)) ->
forall n : nat,
Sigma0 n (fun i => (f (S i) - f i)) = f (S n) - f 0.
The proof is by induction on n, using Nat.add_sub_assoc and Nat.sub_add in the induction step. (See the accompanying file.)
The fundamental theorem of calculus does not hold in general for nat-valued functions:
Theorem not_fundamental_for_nat_valued_functions :
exists f : nat -> nat,
(exists n : nat,
not (f n <= f (S n)))
/\
(exists n : nat,
not (Sigma0 n (fun i => (f (S i) - f i)) = f (S n) - f 0)).
For a counter-example, we can pick fun n => match n with 0 => 0 | S n' => 2 - n end, which is sketchily characterized as follows:
Proposition sketchy_characterization_of_the_counter_example :
forall f : nat -> nat,
f = (fun n => match n with 0 => 0 | S n' => 2 - n end) ->
f 0 = 0 /\ f 1 = 1 /\ f 2 = 0 /\ f 3 = 0 /\ f 4 = 0.
This sketchy characterization shows that this function is not non-decreasing since applying it to 1 yields a larger number than applying it to 2. So 1 is the witness for the first conjunct in the theorem.
For the second conjunct, any positive number can serve as witness.
The proof is detailed in the accompanying file.
Prove that the summation by parts for two nat-valued functions holds when these functions are non-decreasing:
Theorem summation_by_parts_for_nat_valued_functions : (* Abel's lemma *)
forall f : nat -> nat,
(forall m : nat,
f m <= f (S m)) ->
forall g : nat -> nat,
(forall m : nat,
g m <= g (S m)) ->
forall n : nat,
Sigma0 n (fun i => f i * (g (S i) - g i)) + f 0 * g 0 + Sigma0 n (fun i => (f (S i) - f i) * g (S i))
=
f (S n) * g (S n).
Prove that the summation by parts for two nat-valued functions does not hold in general:
Theorem not_summation_by_parts_for_nat_valued_functions :
exists f g : nat -> nat,
(exists n : nat,
not (f n <= f (S n)))
/\
(exists n : nat,
not (g n <= g (S n)))
/\
(exists n : nat,
not (Sigma0 n (fun i => f i * (g (S i) - g i)) + f 0 * g 0 + Sigma0 n (fun i => (f (S i) - f i) * g (S i))
=
f (S n) * g (S n))).
The proof for Exercise 04.a is by induction on n.
The counter-example for Exercise 04.b is the same as the one for Theorem not_fundamental_for_nat_valued_functions.
Pablito: I get it now.
Bong-sun: What do you get now, Pablito?
Pablito: Why you all go into conniptions at the sight of any subtraction.
Bong-sun (amused): Good.
Pablito: By the way, do you remember the property we proved in Week 07, the one about all powers of 4 being post-ternary?
Bong-sun (honest): Not really.
Pablito: The property looked like this:
Property all_powers_of_4_are_post_ternary :
forall n : nat,
exists q : nat,
power 4 n = S (3 * q).
Bong-sun: I see you coming, Pablito.
Prove that all powers of 4 are post-ternary:
Property all_powers_of_4_are_post_ternary :
forall n : nat,
exists q : nat,
power 4 n - 1 = 3 * q.
Pablito: Phew...
Bong-sun: Yes, Pablito?
Pablito: The proof was a lot more complicated than the one in Week 07.
Bong-sun: Was it, now.
Pablito (mopping his brow with a surprisingly large handkerchief; a bandanna, maybe?): It even forced me to deal with an inequality...
Bong-sun: So, conniption?
Pablito: Conniption.
Thanks to Sanjay Adhith for mentioning Abel’s theorem in passing.
Created [05 Jun 2025]