The goal of this chapter is to formalize more informal proofs, this time about discrete mathematics (property of summations).
In the .v file about formalizing summations, prove a small handful of lemmas as well as the last property (about_Sigma1).
In the resource file about formalizing summations, Sigma is defined recursively. Define a tail-recursive version of it that uses an accumulator and prove the equivalence of these two implementations.
Bong-sun: This one seems unproblematic. I mean look at the recursive definition:
Fixpoint Sigma0 (n : nat) (f : nat -> nat) : nat :=
match n with
| O =>
f 0
| S n' =>
Sigma0 n' f + f n
end.
Anton: Right. We define a main function whose job is to call an auxiliary function with its arguments, plus the initial value of the accumulator, which would be, what, the neutral element of addition, i.e., 0:
Definition Sigma0_alt (n : nat) (f : nat -> nat) : nat :=
Sigma0_acc n f 0.
Pablito: And then the auxiliary function:
Fixpoint Sigma0_acc (n : nat) (f : nat -> nat) (a : nat) : nat :=
match n with
| O =>
...
| S n' =>
Sigma0_acc n' f (a + f n)
end.
Anton: That looks right. The delimited context of the recursive call to Sigma0, i.e., [[] + f n] has been relocated to the third argument of the tail call to Sigma0_acc, giving a + f n.
Pablito: But what should Sigma0_acc return in the base case? I wrote ....
Anton (authoritative): It should return the accumulator.
Pablito: But what about f 0?
Anton: What about f 0?
Pablito: That’s what Sigma0 returns in the base case.
Anton: Ah, right, we should not forget that. Just add it to the accumulator, the way we do when we state a lemma about resetting the accumulator.
Pablito: So you mean:
Fixpoint Sigma0_acc (n : nat) (f : nat -> nat) (a : nat) : nat :=
match n with
| O =>
a + f 0
| S n' =>
Sigma0_acc n' f (a + f n)
end.
Anton: Yes.
Pablito <clickety clickety click>: OK, it passes the unit tests.
Anton: So you were right, Bong-sun. Completely unproblematic.
Bong-sun (after a pause): I don’t know.
Anton: You don’t know?
Bong-sun: It doesn’t look right.
Anton: What doesn’t look right?
Bong-sun: Well, this function is not the first accumulator-based auxiliary function we write, right?
Anton: Right.
Bong-sun: But then it would be the first one where the accumulator is not returned in the base case.
Pablito: Let me check, let me check. Huh, you are right. All the accumulator-based auxiliary functions we wrote return the accumulator in the base case.
Bong-sun: That’s what didn’t look right.
Dana: I think the problem is in the definition of Sigma0_alt, look:
Definition Sigma0_alt (n : nat) (f : nat -> nat) : nat :=
Sigma0_acc n f 0.
Bong-sun: Ah, right. The accumulator should be initialized with what Sigma0 returns in the base case.
Pablito: You mean that the accumulator should be initialized with f 0? Like this:
Definition Sigma0_alt (n : nat) (f : nat -> nat) : nat :=
Sigma0_acc n f (f 0).
Dana: Yes.
Anton: OK, OK. And then the auxiliary function would return the accumulator in the base case:
Fixpoint Sigma0_acc (n : nat) (f : nat -> nat) (a : nat) : nat :=
match n with
| O =>
a
| S n' =>
Sigma0_acc n' f (a + f n)
end.
Bong-sun: Yes. This definition looks right in that its form is aligned with the form of all the other accumulator-based functions we implemented so far.
Anton: And that matters why?
Dana: Remember list_fold_right and list_fold_left in the term project?
Anton (with a sigh): Yes...
Dana: The accumulator-based functions all returned the accumulator in the nil case.
Anton: Yes, they did.
Dana: And so we could express them directly using list_fold_left.
Anton: Indeed we could.
Dana: And then we could relate them with their recursive counterpart, via list_fold_right.
Pablito: Yes we could.
Dana: Well, chances are there is a counterpart of these fold functions for nats.
Mimer (floating by): Yes.
Bong-sun: You mean something like – let me guess – nat_fold_right and nat_fold_left?
Mimer: Yes.
Anton (hastily): Which would be the topic for another chapter.
Mimer (regretfully): Yes.
Loki (ironically): Or for an oral exam?
Mimer (reasonably): No.
Created by splitting a previous chapter about informal proofs [05 June 2025]