# Formalize the proof of theorem 2.4 in Harper's PFPL

In Harper's Practical Foundations for Programming Languages, page 19, rule (2.9) defines the $$sum$$ function inductively.

$$\frac{b:nat}{sum(zero;b;b)}\tag{rule 2.9a}$$

$$\frac{sum(a;b;c)}{sum(succ(a);b;succ(c))}\tag{rule 2.9b}$$

Then the author introduced Theorem 2.4 to prove $$sum$$ is indeed a function, that is, $$c:nat$$ is guaranteed to exist and to be unique for any $$a:nat$$ and $$b:nat$$.

The proof of existence does a rule induction on $$a:nat$$. This is essentially a mathematical induction on a single variable. I think I understand the proof and can translate it into a formal one without much difficulty.

But the proof of uniqueness frustrates me a lot.

First, the author decides to do the induction on rule 2.9 (rather than 2.2). My understanding is that here we can have a set-theoretic view of the function $$sum$$. It could be thought of as a relation $$\Sigma$$, a subset of $$\mathbb{N}\times\mathbb{N}\times\mathbb{N}$$. Each element $$r \in \Sigma$$ is a 3-tuple $$\langle a,b,c\rangle$$ where $$a,b,c \in \mathbb{N}$$. The set $$\Sigma$$ is inductively defined by rule 2.9. From this viewpoint, a structural induction on $$\Sigma$$ is perfectly acceptable (as a newbie I spent substantial amount of time to figure this out).

The author states the property to be held as "if $$sum(a;b;c_1)$$, then if $$sum(a;b;c_2)$$, then $$c_1\;is\;c_2$$", which could be straightforwardly translated into

$$sum(a;b;c_1) \rightarrow (sum(a;b;c_2) \rightarrow c_1\;is\;c_2)\tag{a}$$

But I am not sure whether it is a single variable predicate $$\mathcal{P}(sum(a;b;c_1))$$, or a two-variable one $$\mathcal{P}(sum(a;b;c_1),sum(a;b;c_2))$$. Since "an inner induction" is mentioned in both parts (2.9a and 2.9b), it seems the latter is in author's mind, but I have no idea how a two-variable induction works.

In the induction step (rule 2.9b) the author seems to put the induction hypothesis as

$$sum(a^\prime;b;c_1^\prime) \rightarrow (sum(a^\prime;b;c_2^\prime) \rightarrow c_1^\prime\;is\;c_2^\prime)\tag{b}$$

then the goal is to prove something like

$$sum(a;b;c_1) \rightarrow (sum(a;b;c_2) \rightarrow c_1\;is\;c_2)\tag{c}$$

where $$a,c_1,c_2$$ are successors of their primed version respectively.

I understood the statement "We have that $$a\;is\;succ(a^\prime)$$ and $$c_1\;is\;succ(c_1^\prime)$$, where $$sum(a^\prime;b;c_1^\prime)$$." as

$$sum(a^\prime;b;c_1^\prime) \rightarrow sum(a;b;c_1) \tag{d}$$

and "we may show that if $$sum(a;b;c_2)$$, then $$c_2\;is\;succ(c_2^\prime)$$ where $$sum(a^\prime;b;c_2^\prime)$$" as

$$sum(a^\prime;b;c_2^\prime) \rightarrow sum(a;b;c_2) \tag{e}$$

Even each piece looks reasonable, I failed to combine those pieces into a whole picture. I expect from induction hypothesis (b), with rules 2.9, natural deduction rules of first order logic, $$\mathcal{P}(conclusion)$$ (c) should be arrived. But I cannot figure out how. I get stuck here.

The author's proof is intuitively correct. But I do hope to see:

1. a formal proof, or an explanation or clarification from where a formal proof can easily be constructed.
2. confirmations or corrections of the descriptions and predicates above.
3. if this is a two-variable induction, how it works (in the context of rule induction)?
• Can you please add the definition of the sum function and the rule in the question text. It would make the question more comprehensive. Commented Feb 24, 2023 at 18:58
• @Apoorv rule 2.9 added. :) Commented Feb 24, 2023 at 19:49