Create lean-tactics.tex

lean-tactics.tex

@@ -0,0 +1,116 @@
+\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,longtable}
+
+\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{\type}{\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{longtable}{@{}lp{113mm}@{}}
+  \toprule
+  Tactic & Effect \\
+  \midrule
+  &\textbf{Applying Lemmas}\\
+  \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. \\
+  &\textbf{Adding hypotheses/data}\\
+  \lean{have h :} \proposition\ \lean{:=} \expr & add a new hypothesis \lean{h} of type \proposition. \textbf{Do not use for data!} \\
+  \lean{have h :} \proposition & $\ldots$ also creates \proposition as a new goal. \\
+  \lean{set x :} \type\ \lean{:=} \expr & add an abbreviation \lean{x} with value \expr. \\
+  \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{longtable}
+\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
+% MISSING: let!, norm_num
+\end{center}
+
+\end{document}