This mini-project is a spinoff of Chapter Formalizing summations, Chapter Induction principles: from first-order to higher-order induction, and Chapter Binomial coefficients. Its goal is to generalize summations from starting at zero to starting at zero or above.
Here is a sketchy characterization of a summation function that starts at zero:
Definition sketchy_characterization_of_a_summation_function_that_starts_at_zero (Sigma0 : nat -> (nat -> nat) -> nat) :=
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.
Chapter Formalizing summations introduced such a summation function that starts at zero:
Fixpoint Sigma0 (n : nat) (f : nat -> nat) : nat :=
match n with
| O =>
f 0
| S n' =>
Sigma0 n' f + f (S n')
end.
This summation function satisfies the sketchy characterization:
Proposition sketchy_characterization_of_Sigma0 :
sketchy_characterization_of_a_summation_function_that_starts_at_zero Sigma0.
In words, applying Sigma0 to n and f yields the result of adding f 0, f 1, ..., and f n.
Here is a specification of a summation function that may start above zero:
Definition specification_of_a_summation_function (Sigma : nat -> nat -> (nat -> nat) -> nat) :=
(forall (x : nat)
(f : nat -> nat),
Sigma x x f = f x)
/\
(forall (x y : nat)
(f : nat -> nat),
x <= y ->
Sigma x (S y) f = Sigma x y f + f (S y)).
To crystallize, here is a sketchy characterization of such a summation function:
Property sketchy_characterization_of_a_summation_function :
forall Sigma : nat -> nat -> (nat -> nat) -> nat,
specification_of_a_summation_function Sigma ->
forall (x : nat)
(f : nat -> nat),
Sigma x x f = f x
/\
Sigma x (S x) f = f x + f (S x)
/\
Sigma x (S (S x)) f = f x + f (S x) + f (S (S x))
/\
Sigma x (S (S (S x))) f = f x + f (S x) + f (S (S x)) + f (S (S (S x))).
In words, applying Sigma to x, y, and f yields the result of adding f x, f (x + 1), ..., f (y - 1), and f y if x <= y holds.
The following theorem formalizes an index shift from x to 0 (for the lower bound of the summation) and from y to y - x (for the lower bound):
Theorem simulation_of_Sigma_as_an_instance_of_Sigma0 :
forall Sigma : nat -> nat -> (nat -> nat) -> nat,
specification_of_a_summation_function Sigma ->
forall x y : nat,
x <= y ->
forall f : nat -> nat,
Sigma x y f = Sigma0 (y - x) (fun i => f (i + x)).
Prove this theorem.
Hints:
Chapter Formalizing summations featured the following property:
Property about_Sigma0_with_two_equivalent_functions :
forall (x : nat)
(f g : nat -> nat),
(forall i : nat,
f i = g i) ->
Sigma0 x f = Sigma0 x g.
In words, summing up from zero to the same upper bound with equivalent functions yields the same result.
Prove the following analogous property for summing up above zero:
Property about_Sigma_with_two_equivalent_functions :
forall Sigma : nat -> nat -> (nat -> nat) -> nat,
specification_of_a_summation_function Sigma ->
forall x y : nat,
x <= y ->
forall f g : nat -> nat,
(forall i : nat,
f i = g i) ->
Sigma x y f = Sigma x y g.
Prove that summing from zero explicitly yields the same result as summing from zero implicitly:
Theorem self_simulation_of_Sigma_as_an_instance_of_Sigma0 :
forall Sigma : nat -> nat -> (nat -> nat) -> nat,
specification_of_a_summation_function Sigma ->
forall (y : nat)
(f : nat -> nat),
Sigma 0 y f = Sigma0 y f.
Prove that the lower bound and the upper bound of a summation can be shifted up:
Theorem simulation_of_Sigma_as_an_up_instance_of_Sigma :
forall Sigma : nat -> nat -> (nat -> nat) -> nat,
specification_of_a_summation_function Sigma ->
forall x y : nat,
x <= y ->
forall (f : nat -> nat)
(z : nat),
Sigma x y f = Sigma (x + z) (y + z) (fun i => f (i - z)).
Prove that the lower bound and the upper bound of a summation can be shifted down, within reason:
Theorem simulation_of_Sigma_as_a_down_instance_of_Sigma :
forall Sigma : nat -> nat -> (nat -> nat) -> nat,
specification_of_a_summation_function Sigma ->
forall x y : nat,
x <= y ->
forall (f : nat -> nat)
(z : nat),
z <= x ->
Sigma x y f = Sigma (x - z) (y - z) (fun i => f (i + z)).
The following induction principle may start above zero instead of starting at zero:
Lemma nat_ind_shifted :
forall (m : nat)
(P : nat -> Prop),
P m ->
(forall n' : nat,
m <= n' -> P n' -> P (S n')) ->
forall n : nat,
m <= n -> P n.
Prove this tailored induction principle.
Revisit the theorem from Task 1.a and prove it using nat_ind_shifted.
N.B.: The resident induction tactic balks at using nat_ind_shifted, so just use this induction principle directly, as suggested in the accompanying file.
Chapter Binomial coefficients introduced the following implementation of binomial coefficients:
Fixpoint binomial_coefficient (n k : nat) : nat :=
match n with
O =>
match k with
O =>
1
| S k' =>
0
end
| S n' =>
match k with
O =>
1
| S k' =>
binomial_coefficient n' k' + binomial_coefficient n' (S k')
end
end.
As a warmup, prove the following property:
Property warmup :
forall n : nat,
Sigma0 n (fun i => binomial_coefficient i 0) = S n.
Here is a first shot at a sketchy characterization of the hockey-stick identity:
Lemma sketchy_characterization_of_the_hockey_stick_identity_first_shot :
binomial_coefficient 3 3 =
binomial_coefficient 4 4
/\
binomial_coefficient 2 2 + binomial_coefficient 3 2 =
binomial_coefficient 4 3
/\
binomial_coefficient 1 1 + binomial_coefficient 2 1 + binomial_coefficient 3 1 =
binomial_coefficient 4 2
/\
binomial_coefficient 0 0 + binomial_coefficient 1 0 + binomial_coefficient 2 0 + binomial_coefficient 3 0 =
binomial_coefficient 4 1.
Here is a second shot, using summations that for most, start above zero:
Lemma sketchy_characterization_of_the_hockey_stick_identity_second_shot :
forall Sigma : nat -> nat -> (nat -> nat) -> nat,
specification_of_a_specification Sigma ->
Sigma 3 3 (fun i => binomial_coefficient i 3) = binomial_coefficient 4 4
/\
Sigma 2 3 (fun i => binomial_coefficient i 2) = binomial_coefficient 4 3
/\
Sigma 1 3 (fun i => binomial_coefficient i 1) = binomial_coefficient 4 2
/\
Sigma 0 3 (fun i => binomial_coefficient i 0) = binomial_coefficient 4 1.
The goal of this task is to prove the hockey-stick identity:
Theorem hockey_stick_identity :
forall Sigma : nat -> nat -> (nat -> nat) -> nat,
specification_of_a_ Sigma ->
forall n k : nat,
k <= n ->
Sigma k n (fun i => binomial_coefficient i k) = binomial_coefficient (S n) (S k).
Hint: Prove this theorem as a corollary of the following lemma:
Lemma hockey_stick_identity_shifted :
forall n k : nat,
k <= n ->
Sigma0 (n - k) (fun i => binomial_coefficient (i + k) k) = binomial_coefficient (S n) (S k).
Hint: Prove this lemma either by induction over n or using nat_ind_shifted.
The goal of this task is to prove the following theorem:
Theorem summing_one_up :
forall Sigma : nat -> nat -> (nat -> nat) -> nat,
specification_of_Sigma Sigma ->
forall a b : nat,
S a <= b ->
forall f : nat -> nat,
f a + Sigma (S a) b f = Sigma a b f.
Hint: Prove this theorem as a corollary of the following lemma:
Lemma summing_one_up_shifted :
forall a b : nat,
S a <= b ->
forall f : nat -> nat,
f a + Sigma0 (b - S a) (fun i => f (i + S a)) = Sigma0 (b - a) (fun i => f (i + a)).
Hint: Prove this lemma using nat_ind_shifted.
The goal of this task is to show that adding a sum from x to y to the same sum from y+1 to z is the same as summing from x to z.
To this end, prove the following theorem:
Theorem summing_up_and_up :
forall Sigma : nat -> nat -> (nat -> nat) -> nat,
specification_of_Sigma Sigma ->
forall x y : nat,
x <= y ->
forall z : nat,
S y <= z ->
forall f : nat -> nat,
Sigma x y f + Sigma (S y) z f = Sigma x z f.
The goal of this task is to implement a summation function that starts at one, based on the following sketchy characterization:
Definition sketchy_characterization_of_a_summation_function_that_starts_at_1 (Sigma1 : nat -> (nat -> nat) -> nat) :=
forall f : nat -> nat,
(Sigma1 1 f = f 1)
/\
(Sigma1 2 f = f 1 + f 2)
/\
(Sigma1 3 f = f 1 + f 2 + f 3).
In a mathematically informed way, implement such a summation function using your programming intuition:
Fixpoint Sigma1 (n : nat) (f : nat -> nat) : nat :=
...
Verify that your implementation satisfies the sketchy characterization:
Proposition sketchy_characterization_of_Sigma1 :
sketchy_characterization_of_a_summation_function_that_starts_at_1 Sigma1.
Re-implement this summation function based on Theorem simulation_of_Sigma_as_an_instance_of_Sigma0, and verify that your re-implementation satisfies the sketchy characterization.
Prove the equivalence of your two implementations.
Prove the following properties of Sigma1.
Summing up with two equivalent functions yields the same result:
Property about_Sigma1_with_two_equivalent_functions :
forall (x : nat)
(f g : nat -> nat),
(forall i : nat,
f i = g i) ->
Sigma1 x f = Sigma1 x g.
Summing up with an additive function yields the same as summing up with each of its components:
Property about_Sigma1_with_an_additive_function :
forall (x : nat)
(f g : nat -> nat),
Sigma1 x (fun i => f i + g i) = Sigma1 x f + Sigma1 x g.
Summing up with a constant function yields the same as multiplying the upper bound with the contant:
Property about_Sigma1_with_a_constant_function :
forall x c : nat,
Sigma1 x (fun _ => c) = x * c.
Nesting summations commutes:
Property about_swapping_Sigma1 :
forall (x y : nat)
(f : nat -> nat -> nat),
Sigma1 x (fun i => Sigma1 y (fun j => f i j)) = Sigma1 y (fun j => Sigma1 x (fun i => f i j)).
About summing up with the identity function:
Property about_Sigma1_with_the_identity_function :
forall x : nat,
2 * Sigma1 x (fun i => i) = x * S x.
Using the properties proved in Task 9, prove the following property:
Property to_sum_up_with_Sigma1 :
forall x y : nat,
2 * Sigma1 x (fun i => Sigma1 y (fun j => i + j)) = x * y * (x + y + 2).
State and prove an analogous property to sum up with Sigma0.