This repository has been archived by the owner. It is now read-only.
Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
240 lines (209 sloc) 5.59 KB
\documentclass[11pt]{article}
\parindent=0pt
\begin{document}
\pagestyle{empty}
\begin{center}
{\LARGE \textbf{Coq cheat sheet}}
\end{center}
\bigskip
\bigskip
\bigskip
\bigskip
\begin{center}
{\Large \textbf{Notation}}
\bigskip
\bigskip
\begin{tabular}{{|c|c|}}
\hline
{\textbf{Propositions}} & \textbf{Coq} \\ \hline
$\top, \bot$ & \texttt{True}, \texttt{False} \\ \hline
$p \land q$ & \texttt{p /{\char92} q} \\ \hline
$p \Rightarrow q$ & \texttt{p -> q} \\ \hline
$p \lor q$ & \texttt{p {\char92}/ q} \\ \hline
$\lnot p$ & \texttt{{\char126} p} \\ \hline
$\forall x \in A \,.\, p(x)$ & \texttt{forall x:A, p x} \\ \hline
$\forall x, y \in A \,.\,\forall u, v \in B \,.\, q$ &
\texttt{forall (x y:A) (u v:B), q} \\ \hline
$\exists x \in A \,.\, p(x)$ & \texttt{exists x:A, p x} \\ \hline
\end{tabular}
\bigskip
\begin{tabular}{{|c|c|}}
\hline
\textbf{Sets} & \textbf{Coq} \\ \hline
$1$ & \texttt{unit} \\ \hline
$A \times B$ & \texttt{prod A B} or \texttt{A * B} \\ \hline
$A + B$ & \texttt{sum A B} or \texttt{A + B} \\ \hline
$B^A$ or $A \to B$ & \texttt{A -> B} \\ \hline
$\{x \in A \mid p(x)\}$ & \texttt{\{x:A | p x\}} \\ \hline
$\sum_{x \in A} B(x)$ & \texttt{\{x:A \& B x\}} or \texttt{sig A B} \\ \hline
$\prod_{x \in A} B(x)$ & \texttt{forall x:A, B x} \\ \hline
\end{tabular}
\bigskip
\begin{tabular}{{|c|c|}}
\hline
\textbf{Elements} & \textbf{Coq} \\ \hline
$\star \in 1$ & \texttt{tt : unit} \\ \hline
$x \mapsto f(x)$ or $\lambda x \in A \,.\, f(x)$
& \texttt{fun (x : A) => f x} \\ \hline
$\lambda x, y \in A \,.\, \lambda u, v \in B \,.\, f(x)$
& \texttt{fun (x y : A) (u v : B) => f x} \\ \hline
$(a,b) \in A \times B$ & \texttt{(a,b) : A * B} \\ \hline
$\pi_1(t)$ where $t \in A \times B$ & \texttt{fst t} \\ \hline
$\pi_2(t)$ where $t \in A \times B$ & \texttt{snd t} \\ \hline
$\pi_1(t)$ where $t \in \sum_{x \in A} B(x)$ & \texttt{projT1 t} \\ \hline
$\pi_2(t)$ where $t \in \sum_{x \in A} B(x)$ & \texttt{projT2 t} \\ \hline
$\iota_1(t) \in A + B$ where $t \in A$ & \texttt{inl t} \\ \hline
$\iota_2(t) \in A + B$ where $t \in B$ & \texttt{inr t} \\ \hline
$t \in \{ x \in A \mid p(x) \}$ because $\rho$ & \texttt{exist t $\rho$} \\ \hline
$\iota(t)$ where $\iota : \{x \in A \mid p(x) \} \hookrightarrow A$ & \texttt{projT1 t} \\ \hline
\end{tabular}
\end{center}
\newpage
\begin{center}
{\Large \textbf{Basic tactics}}
\bigskip
\bigskip
\begin{tabular}{|c|c|}
\hline
\textbf{When the goal is \dots} & \textbf{\dots use tactic}
\\ \hline
very simple
&
\texttt{auto},
\texttt{tauto} or
\texttt{firstorder}
\\ \hline
\texttt{p /{\char92} q}
&
\texttt{split}
\\ \hline
\texttt{p {\char92}/ q}
&
\texttt{left} or \texttt{right}
\\ \hline
\texttt{p -> q}
&
\texttt{intro}
\\ \hline
\texttt{{\char126}p}
&
\texttt{intro}
\\ \hline
\texttt{p <-> q}
&
\texttt{split}
\\ \hline
an assumption
&
\texttt{assumption}
\\ \hline
\texttt{forall x, p}
&
\texttt{intro}
\\ \hline
\texttt{exists x, p}
&
\texttt{exists $t$}
\\ \hline
\end{tabular}
\bigskip
\begin{tabular}{|c|c|}
\hline
\textbf{To use hypothesis $H$ \dots} & \textbf{\dots use tactic}
\\ \hline
\texttt{p {\char92}/ q}
&
\texttt{destruct $H$ as [$H_1$|$H_2$]}
\\ \hline
\texttt{p /{\char92} q}
&
\texttt{destruct $H$ as [$H_1$ $H_2$]}
\\ \hline
\texttt{p -> q}
&
\texttt{apply $H$}
\\ \hline
\texttt{p <-> q}
&
\texttt{apply $H$}
\\ \hline
\texttt{{\char126}p}
&
\texttt{apply $H$} or \texttt{elim $H$}
\\ \hline
\texttt{False}
&
\texttt{contradiction}
\\ \hline
\texttt{forall x, p}
&
\texttt{apply $H$}
\\ \hline
\texttt{exists x, p}
&
\texttt{destruct $H$ as [$x$ $G$]}
\\ \hline
\texttt{a = b}
&
\texttt{rewrite $H$} or \texttt{rewrite <- $H$}
\\ \hline
\end{tabular}
\bigskip
\begin{tabular}{|c|c|}
\hline
\textbf{If you want to \dots} & \textbf{\dots then use}
\\ \hline
prove by contradiction $p \land \lnot p$ & \texttt{absurd $p$}
\\ \hline
simplify expressions & \texttt{simpl}
\\ \hline
prove via intermediate goal $p$ & \texttt{cut $p$}
\\ \hline
prove by induction on $t$ & \texttt{induction t}
\\ \hline
pretend you are done & \texttt{admit}
\\ \hline
import package $P$ & \texttt{Require Import $P$}
\\ \hline
compute $t$ & \texttt{Eval compute in $t$}
\\ \hline
print definition of $p$ & \texttt{Print $p$}
\\ \hline
check the type of $t$ & \texttt{Check $t$}
\\ \hline
search theorems about $p$ & \texttt{SearchAbout $p$}
\\ \hline
\end{tabular}
\end{center}
\newpage
\begin{center}
{\Large \textbf{Inductive definitions}}
\end{center}
\bigskip
\bigskip
\paragraph{Inductive definition of $X$}
\label{sec:induct-defin-x}
\begin{verbatim}
Inductive X args :=
| constructor1 : args1 -> X
| constructor2 : args2 -> X
...
| constructorN : argsN -> X.
\end{verbatim}
%
Coq generates induction and recursion principles \texttt{X\_ind},
\texttt{X\_rec}, \texttt{X\_rect}.
\paragraph{Construction of an object by cases}
\begin{verbatim}
match t with
| case1: result1
| case2: result2
...
| caseN: resultN
end
\end{verbatim}
\paragraph{Recursive definition of $f$}
\begin{verbatim}
Fixpoint f args := ...
\end{verbatim}
\end{document}