From 9ac8cc740032bcafa6baa845afc267628b3ad4e6 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 21 Apr 2024 00:29:11 +0200 Subject: [PATCH] Create lean-tactics.tex --- lean-tactics.tex | 116 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 116 insertions(+) create mode 100644 lean-tactics.tex diff --git a/lean-tactics.tex b/lean-tactics.tex new file mode 100644 index 0000000..d8c0188 --- /dev/null +++ b/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}