verifying-crypto-with-lean/chapters/ch03-propositions-as-types.tex

\chapter{Propositions as Types: The Idea That Makes It All Work}
\label{ch:pat}

\section{A suspicious similarity}

Here are two things that look unrelated. First, a function that converts a
pair into something else:

\begin{lstlisting}[language=Lean]
def swap (pair : A x B) : B x A := (pair.2, pair.1)
\end{lstlisting}

Second, a fact of logic: \emph{if $A$ and $B$ both hold, then $B$ and $A$ both
hold.} To prove it, you would say: ``suppose I have evidence for $A$ and
evidence for $B$; then I can produce evidence for $B$ and evidence for $A$ ---
just present the same two pieces in the other order.''

That prose proof and that program are the \emph{same object}. The function
takes a pair of values and reorders it; the proof takes a pair of pieces of
evidence and reorders it. This is not an analogy or a teaching trick. It is a
theorem about logic and computation, discovered independently by logicians
(Curry, Howard) and now the load-bearing wall of Lean:

\begin{bigidea}
\textbf{The Curry--Howard correspondence.} A proposition can be read as a
type --- the type of its proofs. A proof is then simply a \emph{program} of
that type. Checking a proof is type-checking a program. There is no separate
``proof checker'' bolted onto Lean: the type checker you met in
Chapter~\ref{ch:lean} \emph{is} the proof checker.
\begin{center}
\begin{tabular}{@{}lll@{}}
\toprule
\textbf{Logic} & \textbf{Programming} & \textbf{In Lean} \\
\midrule
proposition $P$        & type            & \lean{P : Prop} \\
proof of $P$           & value/program of that type & \lean{h : P} \\
$P \to Q$ (implication)& function type   & \lean{P -> Q} \\
$P \land Q$ (and)      & pair type       & \lean{P /\ Q} \\
$P \lor Q$ (or)        & tagged union    & \lean{P \/ Q} \\
$\lnot P$ (not)        & \lean{P -> False} & \lean{Not P} \\
``true''               & type with one trivial value & \lean{True} \\
``false''              & \emph{empty} type & \lean{False} \\
\bottomrule
\end{tabular}
\end{center}
\end{bigidea}

Take a minute with the last row: \lean{False} is a type with \emph{no
constructors} --- no way to build a value. To prove a false statement you
would have to produce an inhabitant of an empty type. That is why the system
is sound: lies have no evidence, so lies do not type-check.

\section{Proofs are programs: first proofs}

Let us write actual proofs as actual programs. Implication is a function
type, so proving ``$P$ implies $P$'' means writing the identity function:

\begin{lstlisting}[language=Lean]
theorem p_implies_p (P : Prop) : P -> P :=
  fun h => h
\end{lstlisting}

Read \lean{fun h => h} aloud as a proof: ``assume $P$ holds --- call the
evidence $h$; then $P$ holds, by $h$.'' Every classical proof-writing phrase
has a program shape:

\begin{center}
\begin{tabular}{@{}ll@{}}
\toprule
\textbf{You say in prose} & \textbf{You write in Lean} \\
\midrule
``Assume $P$; call it $h$''       & \lean{fun h => ...} \\
``By hypothesis $h$''             & \lean{h} \\
``Apply lemma $f$ to fact $h$''   & \lean{f h} \\
``Both parts hold: ... and ...''  & \lean{And.intro pf1 pf2} \\
``From $h : P \land Q$, the first part'' & \lean{h.1} \\
\bottomrule
\end{tabular}
\end{center}

The pair-swapping example, now as an official theorem:

\begin{lstlisting}[language=Lean]
theorem and_swap (P Q : Prop) : P /\ Q -> Q /\ P :=
  fun h => And.intro h.2 h.1
\end{lstlisting}

And transitivity of implication is exactly function composition:

\begin{lstlisting}[language=Lean]
theorem imp_trans (P Q R : Prop) : (P -> Q) -> (Q -> R) -> (P -> R) :=
  fun pq qr => fun p => qr (pq p)
\end{lstlisting}

\begin{worked}{type-checking a proof by hand --- being the kernel once}
When Lean accepts \lean{and_swap}, what does it actually \emph{do}? It
type-checks the term --- and you can replay that check on paper, which is
the single best way to make Curry--Howard stop feeling like a slogan. The
term is \lean{fun h => And.intro h.2 h.1}; the claimed type is
\lean{P ∧ Q → Q ∧ P}. A type-checker works by walking the term and
maintaining a \emph{context} of what each variable is assumed to be ---
write the context on the left of a $\vdash$, the judgment on the right:
\[
\begin{array}{ll}
\text{1.} & \text{Goal: } \vdash \mathtt{fun\ h} \Rightarrow \dots \;:\; P \wedge Q \to Q \wedge P\\[2pt]
\text{2.} & \text{A \lean{fun} against an arrow type: put the argument in
             the context.}\\
          & h : P \wedge Q \;\vdash\; \mathtt{And.intro}\ h.2\ h.1 \;:\; Q \wedge P\\[2pt]
\text{3.} & \text{\lean{And.intro} needs a proof of } Q \text{ and a proof of } P
            \text{ (in that order, to build } Q \wedge P\text{).}\\[2pt]
\text{4.} & h : P \wedge Q \;\vdash\; h.2 : Q \qquad\text{✓ (second component
            of a conjunction)}\\
\text{5.} & h : P \wedge Q \;\vdash\; h.1 : P \qquad\text{✓ (first component)}\\[2pt]
\text{6.} & \text{All leaves check; the term has the claimed type. QED.}
\end{array}
\]
Every step is a bookkeeping rule --- ``\lean{fun} eats an arrow,''
``application must match the function's argument type,'' ``\lean{.1}
projects a pair.'' No inspiration occurred anywhere, which is the entire
point: \emph{checking} a proof is mechanical (a few thousand lines of
kernel), while \emph{finding} it is the creative act. Now deliberately
break it: try to check \lean{fun h => And.intro h.1 h.2} against the same
type. Step 4 demands $h.1 : Q$, but the context gives $h.1 : P$ ---
mismatch, rejected. A wrong proof does not check; you have just watched
soundness happen at the level where it lives.
\end{worked}

\begin{aha}
If you have ever composed two functions, you have already done everything
this proof does. The intimidating part of formal logic --- ``natural
deduction,'' ``inference rules'' --- turns out to be the part you knew from
programming all along. What logicians call \emph{modus ponens}, you call
\emph{calling a function}.
\end{aha}

\section{Equality and the proof that \texorpdfstring{$1+1=2$}{1+1=2}}

The proposition $a = b$ is also a type. Its only constructor is reflexivity
--- \lean{rfl} --- which proves \lean{a = a}. How can that ever prove
anything interesting? Because Lean \emph{computes} before comparing:

\begin{lstlisting}[language=Lean]
theorem one_plus_one : 1 + 1 = 2 := rfl
\end{lstlisting}

Lean unfolds \lean{1 + 1} using the two-line definition of addition from
Chapter~\ref{ch:lean}, arrives at \lean{2}, and sees that both sides are
\emph{literally the same value}. The equation holds by computation. This
mechanism --- \emph{definitional equality} --- is the engine that lets proofs
lean on programs, and later lets us prove facts about extracted Rust code by,
in part, just running it symbolically.

\begin{worked}{watching \lean{rfl} compute --- and watching it get stuck}
Both halves of the \lean{rfl} story fit on one sheet of paper, using the
\lean{add} equations from Chapter~\ref{ch:lean} (recursion on the second
argument; $s$ for successor). First, the success. To check
\lean{1 + 1 = 2}, the kernel normalizes both sides:
\[
1 + 1 \;=\; \mathtt{add}\ s(z)\ s(z)
\;=\; s(\mathtt{add}\ s(z)\ z)
\;=\; s(s(z))
\;=\; 2 .
\]
Two rewrite steps, both forced by the definition, and the two sides become
\emph{the same term} --- \lean{rfl} applies. Nothing about this argument
used the smallness of $1$: for \lean{2\textasciicircum{}255 - 19} the same normalization
runs on the efficient binary representation and succeeds just as surely
(only your patience is finite, not the principle).

Now the failure, on the same sheet. To check \lean{0 + n = n} for a
\emph{variable} $n$, the kernel again tries to normalize the left side:
\[
\mathtt{add}\ z\ n \;=\; ?
\]
Which defining equation applies? The first needs the second argument to be
$z$; the second needs it to be $s(\cdot)$. But $n$ is \emph{opaque} --- an
arbitrary variable exhibits neither constructor. No equation fires, the
term is stuck, the two sides stay different terms, \lean{rfl} fails. Note
precisely what failed: not the \emph{truth} of the statement (it is true
for every concrete $n$, and each instance --- \lean{0 + 5 = 5}, say ---
normalizes fine), but computation's ability to see it \emph{uniformly}.
Whenever a variable blocks the recursion pattern, computation ends and
\emph{induction} must take over --- now you can predict, before trying,
which equalities are \lean{rfl}s. Test yourself: \lean{n + 0 = n}?
(Second argument is the concrete $z$ --- first equation fires ---
\lean{rfl}.) \lean{n * 1 = n}? Depends on which argument \lean{mul}
recurses on; go read your Chapter~\ref{ch:lean} solution and decide.
\end{worked}

\begin{pitfall}
\lean{rfl} proves $2^{255} - 19$-sized computations happily, but it can only
prove what computation alone can see. \lean{n + 0 = n} is \lean{rfl} (the
definition's first equation matches), yet \lean{0 + n = n} is \emph{not} ---
recursion is on the \emph{second} argument, and \lean{n} is an opaque
variable, so nothing unfolds. The statement is still true; it just needs a
real proof (induction --- next chapter). The asymmetry feels unfair for about
a day. Then it becomes your sharpest mental model of what a computer can and
cannot know for free.
\end{pitfall}

\section{Universals, existentials, and dependent types}

Cryptographic specifications are universal statements: ``\emph{for all}
inputs, the output is correct.'' In Lean, $\forall$ is a function type whose
\emph{result type mentions the argument}:

\begin{lstlisting}[language=Lean]
theorem add_self_even : forall n : Nat, isEven (n + n) = true := ...
\end{lstlisting}

A proof of \lean{forall n, P n} is a function that eats any \lean{n} and
returns a proof of \lean{P n} --- one uniform recipe covering all the
infinitely many cases at once. This is precisely the thing testing could not
give us in Chapter~\ref{ch:why}: testing produces finitely many
\lean{P 3, P 17, P 42}; a proof produces the function.

\begin{worked}{a universal statement as one uniform recipe}
Feel the difference between testing and proving on the smallest
interesting universal: \emph{every number of the form $n + n$ is even},
where $\mathrm{even}(m) := \exists k,\, m = 2k$. The testing mind
samples: $3 + 3 = 6 = 2\cdot 3$ ✓, $7 + 7 = 14 = 2 \cdot 7$ ✓, and after
a while believes. The proving mind writes \emph{one function}:
\[
\text{given any } n, \text{ return the witness } k := n
\text{ together with the fact } n + n = 2n .
\]
That is the entire proof --- a recipe that, \emph{handed any} $n$,
produces the evidence for \emph{that} $n$: for $n = 3$ it yields witness
$3$ and the equation $6 = 6$; for $n = 2^{254}$ it yields witness
$2^{254}$ just as cheaply, because the recipe never looks at the digits.
In Lean:
\begin{lstlisting}[language=Lean]
theorem add_self_even : ∀ n : Nat, ∃ k, n + n = 2 * k :=
  fun n => ⟨n, (Nat.two_mul n).symm⟩
\end{lstlisting}
Read the term against the table: \lean{fun n =>} consumes the $\forall$
(a function, as promised); \lean{⟨n, ...⟩} produces the $\exists$ (a
witness paired with evidence). Now the punchline for this book: every
correctness certificate in the companion repositories has exactly this
shape --- \lean{∀ a b, Bnd a → Bnd b → ∃ c, ...} --- a function that
eats \emph{arbitrary} 255-bit inputs and manufactures the evidence for
them. When Chapter~\ref{ch:why} said proofs cover $10^{153}$ input pairs
at once, this recipe-not-samples mechanism is \emph{how}. No induction
was even needed here; when the recipe does need to consult the
structure of $n$, induction (Chapter~\ref{ch:tactics}) is how a recipe
consults structure.
\end{worked}

Dually, \lean{exists n, P n} is proved by handing over a concrete witness
together with evidence: \lean{Exists.intro 4 pf}. And remember the
\lean{Rational} exercise from last chapter --- the denominator you could not
keep nonzero? Dependent types fix it by letting data carry proofs:

\begin{lstlisting}[language=Lean]
structure Rational where
  num   : Int
  den   : Nat
  den_ne_zero : den ≠ 0    -- a PROOF, stored inside the value
\end{lstlisting}

No value of this type with a zero denominator can ever be constructed,
anywhere, by anyone. In the real Ed25519 development this exact pattern
appears as a \emph{bounds invariant}: a field element travels together with
the proof that its five limbs are small enough not to overflow the next
multiplication. The data structure makes the unsafe states unrepresentable.

\section{What about proof by contradiction?}

One more resident of the logical zoo. Lean's core logic is
\emph{constructive}: a proof of existence builds a witness. Classical
reasoning --- ``it's either true or false, and not false, hence true'' --- is
available the moment you want it (Mathlib imports it as \lean{Classical.choice},
and we will meet it again on the trust ledger in Chapter~\ref{ch:honesty}),
but it is an \emph{ingredient you can see}, not smuggled seasoning. When a
verification result says ``this proof uses only \lean{propext},
\lean{Classical.choice}, \lean{Quot.sound},'' that is a complete list of the
logical beliefs you are being asked to hold. Three. You can audit them over
coffee.

\begin{tryit}
Open \code{exercises/Ch03.lean} and prove, as programs (no tactics yet!):
\lean{P -> Q -> P}; \ \lean{(P /\ Q) -> (P \/ Q)}; \ and modus ponens
\lean{P -> (P -> Q) -> Q}. Each is a one-liner. Feel free to be delighted
when the pieces click together like typed Lego.
\end{tryit}

\section*{Exercises}

\exercise{Prove \lean{and_assoc : (P /\ Q) /\ R -> P /\ (Q /\ R)} as a
term-mode program using \lean{h.1}, \lean{h.2}, and \lean{And.intro}.}

\exercise{Prove \lean{or_swap : P \/ Q -> Q \/ P}. You will need case
analysis on which side holds: \lean{match h with | Or.inl p => ... | Or.inr q => ...}}

\exercise{\lean{Not P} is \emph{defined} as \lean{P -> False}. Using only
that, prove \lean{P -> Not (Not P)}. Write down in one sentence what program
you just wrote.}

\exercise{(Thought) Explain to a skeptical friend why a type with no
constructors is the right representation of falsehood --- and what would go
wrong with the whole edifice if someone added a constructor to it.}

\section*{Solutions and pathways}
\solutionsintro

\solhead{3.1}
\pathway Draw the shapes before writing the term. You \emph{have} a
nested pair $((p,q),r)$; you \emph{owe} $(p,(q,r))$. The projections
\lean{.1}/\lean{.2} take pairs apart; \lean{And.intro} puts them together;
the whole proof is re-parenthesizing a package. Chase each component: where
does $p$ live inside the input? At \lean{h.1.1}.
\answer
\begin{lstlisting}[language=Lean]
theorem and_assoc' : (P ∧ Q) ∧ R → P ∧ (Q ∧ R) :=
  fun h => And.intro h.1.1 (And.intro h.1.2 h.2)
\end{lstlisting}
Read it back as prose: ``from $((p,q),r)$, produce $(p,(q,r))$.'' If your
version has the components in a different arrangement, type-check it by
hand as in the worked example --- exactly one arrangement survives step 4.

\solhead{3.2}
\pathway A disjunction is a \emph{tagged} value --- you cannot project both
sides out of it (only one exists!), so the projection style of 3.1 is
unavailable. The only way to consume \lean{P ∨ Q} is case analysis: handle
each tag. In term mode that is a \lean{match} with two arms; each arm
holds evidence for one side and must rebuild the output disjunction with
the \emph{other} tag.
\answer
\begin{lstlisting}[language=Lean]
theorem or_swap : P ∨ Q → Q ∨ P :=
  fun h => match h with
    | Or.inl p => Or.inr p
    | Or.inr q => Or.inl q
\end{lstlisting}
Note the tag flip: evidence that arrived tagged ``left'' leaves tagged
``right'' and vice versa. The compiler checks \emph{exhaustiveness} ---
delete an arm and the proof is rejected, because a case of reality would
be unhandled. Compare with \lean{and_swap}: same theorem shape, entirely
different evidence plumbing. The connective dictates the program.

\solhead{3.3}
\pathway Unfold the abbreviation twice.
$\lnot P = P \to \mathtt{False}$, so
$\lnot\lnot P = (P \to \mathtt{False}) \to \mathtt{False}$. The goal
$P \to \lnot\lnot P$ is therefore
$P \to (P \to \mathtt{False}) \to \mathtt{False}$: two arguments --- a
proof and a refuter --- and you must produce \lean{False}. There is exactly
one way to get a \lean{False}: apply the refuter.
\answer
\begin{lstlisting}[language=Lean]
theorem not_not_intro : P → ¬¬P :=
  fun p f => f p
\end{lstlisting}
The one-sentence description: \emph{``given evidence $p$ and any would-be
refutation $f$ of $P$, feed $p$ to $f$ --- the refutation defeats
itself.''} It is modus ponens wearing a philosophy costume. (The converse,
$\lnot\lnot P \to P$, is \emph{not} writable in this plain style --- you
would have to conjure a $p$ out of a function that only consumes them.
That is the constructive/classical boundary of the last section, met in
the wild.)

\solhead{3.4}
\pathway Recall what a proof of \lean{False} would be --- a value of the
empty type --- and follow the consequences of the type not being empty
anymore.
\answer (Model answer.) ``Falsehood must be the proposition with \emph{no
evidence}: if you could construct a proof of \lean{False}, `proof' would
stop meaning anything. In this system that is not a moral claim but a
structural one --- \lean{False} is an inductive type with zero
constructors, so no closed term of that type exists. Every other
proposition's strength derives from this emptiness: $\lnot P$ means
$P \to \mathtt{False}$, and the principle `from \lean{False}, anything'
is safe precisely because its premise is unreachable. Add one constructor
\lean{oops : False} and watch the edifice fall: \lean{False.elim oops}
now proves \emph{every} proposition --- $1 = 2$, `this code is correct,'
everything --- and every certificate ever checked becomes worthless
simultaneously. The kernel's whole job is to be the thing that never lets
\lean{oops} in.'' Connect this forward: Chapter~\ref{ch:honesty}'s
\lean{\#print axioms} audit is, at bottom, checking that nobody smuggled
in an \lean{oops} dressed as an axiom.

\begin{checkpoint}
You should now be able to: translate each logical connective into its type
($\to$, $\land$, $\lor$, $\lnot$, $\forall$, $\exists$); write small proofs
as terms; explain why \lean{rfl} proves \lean{1 + 1 = 2} but not
\lean{0 + n = n}; and articulate the Curry--Howard slogan --- \emph{proofs
are programs, propositions are types, checking is type-checking} --- with a
straight face and genuine conviction.
\end{checkpoint}