I am currently going through Philip Walder's "Proposition as Types" and a passage of the introduction has struck me:
for each way to simplify a proof there is a corresponding way to evaluate a program
What does simplify a proof means here? I have searched in my logic textbook and on the Internet but surprisingly enough I could not find any direct, informal explanation.
There are two inference rule of propositional logic involving implication (which I write using $\to$ instead of $\Rightarrow$):
The introduction rule says that we can prove $A \to B$ if we derive $B$ from the assumption $A$ (there are brackets around $[A]$ because $A$ here is a "temporary" assumption which is "discharged" by $A \to B$): $$\frac{\begin{matrix}[A]\\ \vdots \\ B\\\end{matrix}}{A \to B}$$
The elimination rule says that from $A \to B$ and $A$ we may derive $B$: $$\frac{A \to B\qquad A}{B}$$
Now consider what happens if we prove $A \to B$ in the elimination rule using the introduction rule. We get a derivation that looks like this: $$\frac{\displaystyle \frac{\begin{matrix}[A]\\ \vdots \\ B\\\end{matrix}}{A \to B} \qquad \frac{\begin{matrix} \\ \\ \vdots \\\end{matrix}}{A} }{B}$$ In words this proof would go as follows:
We can transform the proof into a simpler one: step one already contains the proof of $B$, except that it relies on the assumption $A$. But we can get rid of the assumption by replacing it with the proof of $A$ whenever it gets used. So our new proof will look like this: $$ \begin{matrix}\vdots \\ A\\ \vdots \\ B\\\end{matrix} $$ This is what is meant by proof simpliication. It is a transformation of a proof in which an introduction rule is immediately followed by an elimination rule. Another example is this: $$\frac{\displaystyle \frac{A \qquad B}{A \land B} } {A} $$ There is no point in first proving $A \land B$ and then forgetting about the proof of $B$ – we can just directly go for the upper-left part, which is a proof of $A$.
These proof transformations correspond precisely to computation steps in a functional programming language. The first example is the $\beta$-rule $$(\lambda x : A \,.\, e_1) \, e_2 \leadsto e_1[e_2/x]$$ which reads: "a function mapping $x$ of type $A$ to an expression $e_1$ of type $B$ applied to an expression $e_2$ of type $A$ equals the expression $e_1$ with $x$ replaced by $e_2$". By the Curry-Howard correspondence $x$ is the assumption $A$, $e_1$ is the proof that $B$ follows from $A$, $\lambda x : A \,.\, e_1$ is the proof of the implication $A \to B$, $e_2$ is the proof of $A$, and $e_1[e_2/x]$ is the "simplified" (logicians say "reduced" or "normalized") proof of $B$ in which the assumption $x$ was replaced by $e_2$.
The second example corresponds to the rule for computng the first component of a pair: $$\pi_1 \langle e_1, e_2 \rangle \leadsto e_1.$$
Andrej's answer gives the technical explanation, but it might be useful to note, in addition, that "proof simplification" is a technical term that roughly corresponds to "lemma elimination", and is analogous to cut-elimination in the sequent calculus.
Informally, this operation is the opposite of a "proof simplification"! The things humans usually do to simplify proofs, e.g. introduce new notations, prove intermediate lemmas, generalize conclusions are the things that are eliminated by the operation you are referring to.
