lean4 tactic チートシート

lean-tactics-ja.tex

\documentclass[a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{luatexja}
\usepackage{luatexja-fontspec}

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

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

% 原著者（Lean 3 版）: Patrick Massot, Johan Commelin
% https://github.com/leanprover-community/lftcm2020/blob/master/lean-tactics.tex
% Lean 4 版: Martin Dvořák
% https://github.com/madvorak/lean4-cheatsheet
% 日本語翻訳: Claude Code

\usepackage{makecell}
\usepackage{xcolor}

\begin{document}
\pagestyle{empty}
\begin{center}
 \large\textsc{Lean 4 タクティク・チートシート}
\end{center}

以下の表において、
\nom は Lean が既に知っている名前を指し、
\nv はユーザーが新たに付ける名前を指す。
\expr は式を意味し、
例えばコンテキスト中のオブジェクトの名前、
それらの関数としての算術式、
コンテキスト中の仮定、
またはこれらに適用された補題などである。
\proposition は型 \lean{Prop} を持つ式（例: \lean{0 < x}）である。
同じセル内に同じ語が2回現れる場合、
それぞれ異なる名前や式を指す。

\begin{center}
\setlength\tabcolsep{5mm}
\def\arraystretch{1.3}
\begin{tabular}{@{}lll@{}}
  \toprule
  論理記号 & ゴールに現れる場合 & 仮定に現れる場合 \\
  \midrule
 $\exists$（存在） & \makecell[lt]{\lean{use} \expr} & \makecell[lt]{
\lean{obtain} $\langle$\nv, \nv$\!\!\rangle$ \lean{:=} \expr
} \\
 $\forall$（全称） & \lean{intro} \nv & \lean{apply} \expr または \lean{specialize} \nom \expr  \\
 $\lnot$（否定） & \lean{intro} \nv & \lean{apply} \expr または \lean{specialize} \nom \expr  \\
 $\to$（ならば） & \lean{intro} \nv & \lean{apply} \expr または \lean{specialize} \nom \expr \\
 $\leftrightarrow$（同値）~~ & \lean{constructor}  & \lean{rw [}\expr\lean{]} または \lean{rw [←} \expr\lean{]}\\
 $\land$（かつ） & \lean{constructor} & \makecell[lt]{
\lean{obtain} $\langle$\nv, \nv$\!\!\rangle$ \lean{:=} \expr
} \\
 $\lor$（または） & \makecell[lt]{\lean{left} または \lean{right}} & \makecell[lt]{
\lean{cases} \expr \lean{with} \\
\lean{| inl }\nv \lean{=> ...} \\
\lean{| inr }\nv \lean{=> ...}
} \\
  \bottomrule
\end{tabular}
\end{center}

\medskip
以下の表の左列で、括弧内の部分は省略可能である。
その部分の効果も右列で括弧内に記されている。

\begin{center}
\setlength\tabcolsep{5mm}
\def\arraystretch{1.3}
\begin{tabular}{@{}lp{10cm}@{}}
  \toprule
  タクティク & 効果 \\
  \midrule
  \lean{exact} \expr & ゴールが \expr によって満たされる \\
  \lean{refine} \expr & \lean{exact} と同様だが、\expr の中に任意の数の \lean{?\_} を残して穴（後で埋めるゴール）を作れる \\
  \makecell[lt]{\lean{convert} \expr} & 既存の事実 \expr にゴールを変換して証明し、変換中に自動証明できなかった命題についてゴールを生成する \\
  \makecell[lt]{\lean{convert\_to} \proposition} & ゴールを \proposition に変換し、変換中に自動証明できなかった命題についてゴールを生成する \\
  \makecell[lt]{\lean{have} \nv : \proposition} & \proposition が真であると主張する名前 \nv を導入し、同時に \proposition を証明するゴールを生成してフォーカスする \\
  \lean{unfold} \nom (\lean{at} \hyp) & ゴール（または仮定 \hyp）中の定義 \nom を展開する \\
  \lean{rw [} (\lean{←}) \expr\lean{]} (\lean{at} \hyp) & ゴール（または仮定 \hyp）中で、等式または同値式 \expr の左辺（\lean{←} がある場合は右辺）の出現をすべて反対側に置き換える \\
  \lean{rw [} \expr\lean{,} \expr\lean{,} \expr\lean{]} (\lean{at} \hyp) & 指定された順に複数の書き換えを行う（\lean{←} は任意の位置で使用可能） \\
  \lean{calc} & 計算による証明を開始する（推移律を使用） \\
  \lean{by\_cases} \nv : \proposition & \proposition が真か偽かで証明を2つの場合に分割し、\nv をその仮定の名前として使用する \\
  \makecell[lt]{\lean{exfalso}} & 「偽からは何でも導ける」（爆発律）を適用する（現在のゴールを \lean{False} に置き換える） \\
  \makecell[lt]{\lean{by\_contra} \nv} & 背理法による証明を開始し、\nv をゴールの否定である仮定の名前として使用する \\
  \makecell[lt]{\lean{push\_neg} (\lean{at} \hyp)} & ゴール（または仮定 \hyp）中の否定を内側に押し込む。例: $\neg\;\forall$ x, \proposition を $\exists$ x, $\neg\;$\proposition に変換 \\
  \makecell[lt]{\lean{linarith}} & 仮定の線形結合によりゴールを証明する \\
  \makecell[lt]{\lean{ring}} & （半）環の公理を組み合わせてゴールを証明する \\
  \makecell[lt]{\lean{simp} (\lean{at} \hyp)} & 標準的な等式を使ってゴール（または仮定 \hyp）を簡約する \\
  \makecell[lt]{\lean{exact?}} & ゴールを閉じる既存の補題をローカルな仮定も含めて検索する \\
  \makecell[lt]{\lean{apply?}} & 結論がゴールに一致する補題を検索し、\lean{apply} や \lean{refine} で使えるものを提案する \\
  \makecell[lt]{\lean{aesop}} & 魔法でゴールを解こうとする \\
  \bottomrule
\end{tabular}
\end{center}

\end{document}