mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
abf99d05fc
Restructured from flat .tex/.pdf files into per-paper subdirectories. Added Antje Worring as co-author on all papers. Synced PDFs to pdfs/ for download site.
78 lines
3.0 KiB
TeX
78 lines
3.0 KiB
TeX
\section{Lean~4 Fundamentals}
|
|
|
|
|
|
Lean~4 is simultaneously a programming language and a proof assistant. Programs are
|
|
proofs; types are propositions. This section teaches the minimum Lean~4 needed to write
|
|
blockchain proofs.
|
|
|
|
\subsection{Propositions as Types}
|
|
|
|
In Lean~4, a proposition is a type in \texttt{Prop}. A proof of proposition \texttt{P}
|
|
is a term of type \texttt{P}. If you can construct a term of type \texttt{P}, you have
|
|
proved \texttt{P}.
|
|
|
|
\begin{lstlisting}[language=Lean,caption={Basic propositions in Lean~4}]
|
|
-- A proposition: for all natural numbers n, n + 0 = n
|
|
theorem add_zero (n : Nat) : n + 0 = n := by
|
|
induction n with
|
|
| zero => rfl
|
|
| succ k ih => simp [Nat.add_succ, ih]
|
|
\end{lstlisting}
|
|
|
|
Line by line:
|
|
\begin{itemize}[nosep]
|
|
\item \texttt{theorem} declares a named proof obligation.
|
|
\item \texttt{(n : Nat)} universally quantifies over natural numbers.
|
|
\item \texttt{: n + 0 = n} is the proposition (a type in \texttt{Prop}).
|
|
\item \texttt{:= by} enters tactic mode---an interactive proof language.
|
|
\item \texttt{induction n} performs structural induction on \texttt{n}.
|
|
\item \texttt{rfl} closes a goal where both sides are definitionally equal.
|
|
\item \texttt{simp} applies simplification lemmas from the library.
|
|
\end{itemize}
|
|
|
|
\subsection{Tactic Mode}
|
|
|
|
Tactics are commands that transform proof goals. The most important tactics for blockchain
|
|
proofs:
|
|
|
|
\begin{table}[H]
|
|
\centering
|
|
\small
|
|
\begin{tabular}{@{}ll@{}}
|
|
\toprule
|
|
\textbf{Tactic} & \textbf{What it does} \\
|
|
\midrule
|
|
\texttt{intro h} & Introduce hypothesis \texttt{h} from a $\forall$ or $\to$ goal \\
|
|
\texttt{exact e} & Close goal with exact proof term \texttt{e} \\
|
|
\texttt{apply f} & Reduce goal to subgoals matching \texttt{f}'s premises \\
|
|
\texttt{rfl} & Close goal where both sides are definitionally equal \\
|
|
\texttt{simp} & Simplify using registered lemmas \\
|
|
\texttt{omega} & Decide linear arithmetic over integers/naturals \\
|
|
\texttt{induction x} & Structural induction on \texttt{x} \\
|
|
\texttt{cases h} & Case analysis on hypothesis \texttt{h} \\
|
|
\texttt{have h : P := ...} & Introduce intermediate lemma \\
|
|
\texttt{contradiction} & Close goal from contradictory hypotheses \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\caption{Core tactics for blockchain formal verification.}
|
|
\end{table}
|
|
|
|
\subsection{Dependent Types}
|
|
|
|
Lean~4's type system allows types to depend on values. This is essential for expressing
|
|
properties like ``a list of exactly $n$ elements'' or ``a set of validators where
|
|
$|V| \geq 3f + 1$'':
|
|
|
|
\begin{lstlisting}[language=Lean,caption={Dependent types for validator sets}]
|
|
structure ValidatorSet (n : Nat) where
|
|
validators : Fin n -> PublicKey
|
|
threshold : Nat
|
|
threshold_valid : 3 * threshold + 1 <= n
|
|
\end{lstlisting}
|
|
|
|
The field \texttt{threshold\_valid} is not runtime data---it is a proof that must be
|
|
provided when constructing a \texttt{ValidatorSet}. The compiler enforces this at
|
|
construction time. There is no way to create an invalid validator set.
|
|
|
|
%% ============================================================
|