\[\begin{split}\newcommand{\as}{\kw{as}}
\newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)}
\newcommand{\case}{\kw{case}}
\newcommand{\cons}{\textsf{cons}}
\newcommand{\consf}{\textsf{consf}}
\newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)}
\newcommand{\emptyf}{\textsf{emptyf}}
\newcommand{\End}{\kw{End}}
\newcommand{\kwend}{\kw{end}}
\newcommand{\even}{\textsf{even}}
\newcommand{\evenO}{\textsf{even}_\textsf{O}}
\newcommand{\evenS}{\textsf{even}_\textsf{S}}
\newcommand{\Fix}{\kw{Fix}}
\newcommand{\fix}{\kw{fix}}
\newcommand{\for}{\textsf{for}}
\newcommand{\forest}{\textsf{forest}}
\newcommand{\Functor}{\kw{Functor}}
\newcommand{\In}{\kw{in}}
\newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)}
\newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)}
\newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)}
\newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}}
\newcommand{\injective}{\kw{injective}}
\newcommand{\kw}[1]{\textsf{#1}}
\newcommand{\length}{\textsf{length}}
\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
\newcommand{\List}{\textsf{list}}
\newcommand{\lra}{\longrightarrow}
\newcommand{\Match}{\kw{match}}
\newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})}
\newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})}
\newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})}
\newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})}
\newcommand{\mto}{.\;}
\newcommand{\nat}{\textsf{nat}}
\newcommand{\Nil}{\textsf{nil}}
\newcommand{\nilhl}{\textsf{nil\_hl}}
\newcommand{\nO}{\textsf{O}}
\newcommand{\node}{\textsf{node}}
\newcommand{\nS}{\textsf{S}}
\newcommand{\odd}{\textsf{odd}}
\newcommand{\oddS}{\textsf{odd}_\textsf{S}}
\newcommand{\ovl}[1]{\overline{#1}}
\newcommand{\Pair}{\textsf{pair}}
\newcommand{\plus}{\mathsf{plus}}
\newcommand{\SProp}{\textsf{SProp}}
\newcommand{\Prop}{\textsf{Prop}}
\newcommand{\return}{\kw{return}}
\newcommand{\Set}{\textsf{Set}}
\newcommand{\Sort}{\mathcal{S}}
\newcommand{\Str}{\textsf{Stream}}
\newcommand{\Struct}{\kw{Struct}}
\newcommand{\subst}[3]{#1\{#2/#3\}}
\newcommand{\tl}{\textsf{tl}}
\newcommand{\tree}{\textsf{tree}}
\newcommand{\trii}{\triangleright_\iota}
\newcommand{\Type}{\textsf{Type}}
\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}}
\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}}
\newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]}
\newcommand{\WFE}[1]{\WF{E}{#1}}
\newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)}
\newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}
\newcommand{\with}{\kw{with}}
\newcommand{\WS}[3]{#1[] \vdash #2 <: #3}
\newcommand{\WSE}[2]{\WS{E}{#1}{#2}}
\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4}
\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}
\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}}
\newcommand{\zeroone}[1]{[{#1}]}
\end{split}\]
Writing proofs
Coq is an interactive theorem prover, or proof assistant, which means
that proofs can be constructed interactively through a dialog between
the user and the assistant. The building blocks for this dialog are
tactics which the user will use to represent steps in the proof of a
theorem.
Incomplete proofs have one or more open (unproven) sub-goals. Each
goal has its own context (a set of assumptions that can be used to
prove the goal). Tactics can transform goals and contexts.
Internally, the incomplete proof is represented as a partial proof
term, with holes for the unproven sub-goals.
When a proof is complete, the user leaves the proof mode and defers
the verification of the resulting proof term to the kernel.
This chapter is divided in several parts, describing the basic ideas
of the proof mode (during which tactics can be used), and several
flavors of tactics, including the SSReflect proof language.