lean-tactics.tex

\documentclass[a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}

%\usepackage[urw-garamond,expert,uppercase=upright,greeklowercase=upright]{mathdesign}
%\usepackage[osf,swashQ]{garamondx}
%
%\usepackage{microtype}

\usepackage[textwidth=17cm, textheight=27cm]{geometry}
\usepackage{booktabs, xspace}
\usepackage{amsmath,amsfonts,amssymb}

\newcommand{\lean}[1]{{\tt #1}}
\newcommand{\nv}{\textit{new\_name}\xspace}
\newcommand{\nom}{\textit{name}\xspace}
\newcommand{\expr}{\textit{expr}\xspace}
\newcommand{\proposition}{\textit{proposition}\xspace}
\newcommand{\hyp}{\textit{hyp}\xspace}
\setlength\parindent{0pt}

% Original authors (Lean 3 version): Patrick Massot and Johan Commelin
% https://github.com/leanprover-community/lftcm2020/blob/master/lean-tactics.tex

\usepackage{makecell}
\usepackage{xcolor}

\begin{document}
\pagestyle{empty}
\begin{center}
 \large\textsc{Lean 4 Cheatsheet}
\end{center}

% In the following table,
% \nom always refers to a name already known to Lean
% while \nv refers to a new name provided by the user;
% \expr designates any expression.\\
% When one of these words appears twice in the same line,
% the appearances do not designate the same name or
% the same expression.

\begin{center}
If a tactic is not recognized, write \lean{import Mathlib.Tactic} at the top of your file.\smallskip
\setlength\tabcolsep{5mm}
\def\arraystretch{1.3}
\begin{tabular}{@{}lll@{}}
  \toprule
  Logical symbol & Appears in goal & Appears in hypothesis \\
  \midrule
  $\forall$ (for all) & \lean{intro x} & \lean{apply h} or \lean{specialize h x}  \\
  $\to$ (implies) & \lean{intro h} & \lean{apply h} or \lean{specialize h1 h2} \\
  $\neg$ (not) & \lean{intro h} & \lean{apply h} or \lean{contradiction}  \\
  $\leftrightarrow$ (if and only if)\qquad & \lean{constructor}  & \lean{rw [h]} or \lean{rw [← h]} or \lean{apply h.1} or \lean{apply h.2}\\
  $\wedge$ (and) & \lean{constructor} & \lean{obtain ⟨h1, h2⟩ := h} \\
  $\exists$ (there exists) & \lean{use x} & \lean{obtain ⟨x, hx⟩ := h} \\
  $\vee$ (or) & \lean{left} or \lean{right} & \lean{obtain h1|h2 := h} \\
  $ a = b$ (equality) & \lean{rfl} or \lean{ext} & \lean{rw [h]} or \lean{rw [← h]} or \lean{subst h} (if $b$ is a variable) \\
\bottomrule
\end{tabular}
\end{center}

\begin{center}
\setlength\tabcolsep{5mm}
\def\arraystretch{1.3}
\begin{tabular}{@{}lp{113mm}@{}}
  \toprule
  Tactic & Effect \\
  \midrule
  \lean{exact} \expr & prove the current goal exactly by \expr. \\
  \lean{apply} \expr & prove the current goal by applying \expr to some arguments. \\
  \lean{refine} \expr & like \lean{exact}, but \expr can contain sub-expressions \lean{?\_} that will be turned into new goals. \\
  \lean{convert} \expr & prove the goal by showing that it is equal to the type of \expr. \\
  \lean{have h :} \proposition\ \lean{:=} \expr & add a new hypothesis \lean{h} of type \proposition. \\
  \lean{have h :} \proposition & $\ldots$ also creates \proposition as a new goal.  \\
  \lean{by\_cases h :} \proposition & create two goals, one where \lean{h} is the hypothesis that \proposition is true and one where \lean{h} is the hypothesis where it is false. \\
  \makecell[lt]{\lean{exfalso}} & replace the current goal by \lean{False}. \\
  \makecell[lt]{\lean{by\_contra h}} & proof by contradiction; adds the negation of the goal as hypothesis \lean{h}. \\
  \makecell[lt]{\lean{push\_neg} or \lean{push\_neg at h}} & push negations into quantifiers and connectives in the goal (or in \lean{h}).
  %; e.g.~change $\neg\;\forall$ \lean{x, P x} to $\exists$ \lean{x,} $\neg\;$\lean{P x}.
  \\
  \lean{symm} & swap a symmetric relation. \\
  \lean{trans} \expr & split a transitive relation into two parts with \expr in the middle. \\
  \lean{congr} & prove an equality using congruence rules. \\
  \lean{gcongr} & prove an inequality using congruence rules. \\
  % \lean{ext} & prove an equality between elements of a specific type. \\
  \lean{rw [}\expr\lean{]} & in the goal, replace (all occurrences of) the left-hand side
  of \expr by its right-hand side. \expr must be an equality or if and only if statement.\\
  \lean{rw [←}\expr\lean{]} & $\ldots$ rewrites using \expr from right-to-left. \\
  \lean{rw [}\expr\lean{] at h} & $\ldots$ rewrite in hypothesis \lean{h}. \\
  \lean{simp} & simplify the goal using all lemmas tagged \lean{@[simp]} and basic reductions. \\
  \lean{simp at h} & $\ldots$ simplify in hypothesis \lean{h}. \\
  \lean{simp [*, }\expr\lean{]} & $\ldots$ also simplify with all hypotheses and \expr. \\
  \lean{simp only [}\expr\lean{]}& $\ldots$ only simplify with \expr and basic reductions (not with simp-lemmas). \\
  \lean{simp?}& $\ldots$ generate a \lean{simp only [...]} tactic that applies the same simplifications. \\
  \lean{simp\_rw [}\textit{expr1}\lean{, }\textit{expr2}\lean{]} & like \lean{rw}, but uses \lean{simp only} at each step. \\
  \makecell[lt]{\lean{exact?}} & search for a single lemma that closes the goal using the current hypotheses. \\
  \makecell[lt]{\lean{apply?}} & gives a list of lemmas that can apply to the current goal. \\
  \makecell[lt]{\lean{rw?}} & gives a list of lemmas that can be used to rewrite the current goal. \\
  \makecell[lt]{\lean{linarith}} & prove linear (in)equalities from the hypotheses. \\
  \makecell[lt]{\lean{ring} / \lean{noncomm\_ring}\\ \lean{field\_simp} / \lean{abel} / \lean{group}} & prove the goal by using the axioms of a commutative ring / ring / field / abelian group / group. \\
  \makecell[lt]{\lean{aesop}} & simplify the goal, and use various techniques to prove the goal. \\
  \makecell[lt]{\lean{tauto}} & prove logical tautologies. \\
  \bottomrule
\end{tabular}
\mbox{}\\
other useful tactics: \lean{induction}, \lean{ext}, \lean{positivity}, \lean{split\_ifs}, \lean{calc}, \lean{conv}, \lean{polyrith}, \lean{norm\_cast}, \lean{push\_cast}%, $\ldots$
% honourable mentions: \lean{zify}, qify, lift
\end{center}

\end{document}