はじめに
リンク集
第1部: リファレンス
対話的コマンド
❱
#check_failure: 意図的なエラー
#check: 型を調べる
#eval: 式を評価する
#find: ライブラリ検索
#guard_msgs: メッセージのテスト
#guard: Bool 値のテスト
#help: ドキュメントを見る
#html: HTMLをインフォビューに表示
#instances: インスタンスを列挙
#lint: リンタ実行
#print: 中身を見る
#reduce: 式を簡約する
#synth: 型クラスの検査
#time: 実行時間計測
#version: バージョン表示
#whnf: 式を弱頭正規形に
宣言的コマンド
❱
abbrev: 略称を定義する
add_aesop_rules: aesop 改造
attribute: 属性を付与する
axiom: 公理を宣言する
class: 型クラスを定義する
declare_aesop_rule_sets: Aesopでタクティク自作
declare_syntax_cat: 構文カテゴリ
def: 関数などを定義する
deriving: インスタンス自動生成
elab: 構文に意味を与える
example: 名前をつけずに証明
export: 現在の名前空間に追加
inductive: 帰納型を定義する
infix: 中置記法
instance: インスタンスを定義する
local: 有効範囲をセクションで限定
macro_rules: 構文展開の追加
macro: 簡便なマクロ定義
namespace: 名前空間を宣言する
noncomputable: 計算不能にする
notation: 記法を導入する
opaque: 簡約できない名前を宣言
open: 名前空間を開く
partial: 再帰の停止証明をしない
postfix: 後置記法
prefix: 前置記法
private: 定義を不可視にする
proof_wanted: 証明を公募する
protected: フルネームを強制する
scoped: 有効範囲を名前空間で限定
section: スコープを区切る
set_option: オプション設定
structure: 構造体を定義する
syntax: 構文を定義
termination_by: 整礎再帰を使う
theorem: 命題を証明する
variable: 引数を共通化する
属性
❱
app_unexpander: 関数適用の表示
cases_eliminator: 独自場合分け
coe: 型強制 ↑ として表示させる
csimp: 効率的な実装に置換
default_instance: デフォルトの解決法
induction_eliminator: 独自帰納法
inherit_doc: ドキュメントの継承
match_pattern: 独自パタンマッチ
simps: simp 補題の自動生成
オプション
❱
autoImplicit: 自動束縛暗黙引数
hygiene: マクロ衛生
linter.flexible: 脆弱な証明を指摘する
linter.style.multiGoal: フォーカス強制
relaxedAutoImplicit: 更にautoImplicit
型クラス
❱
Coe: 型強制
CoeDep: 依存型強制
CoeFun: 関数型への強制
CoeSort: 型宇宙への強制
Decidable: 決定可能
Functor: ファンクタ
GetElem: n番目の要素を取得
HAdd: + のための記法クラス
HMul: * のための記法クラス
Inhabited: 有項にする
LawfulFunctor: ルール付きファンクタ
OfNat: 数値リテラルを使用
Repr: 表示方法を指定
ToString: 文字列に変換
データ型
❱
Array: 配列
Bool: 真偽値
Char: Unicode 文字
Float: 浮動小数点数
List: 連結リスト
Macro: マクロ
Prop: 命題全体
String: 文字列
Syntax: 具象構文木
Type: 型の型
タクティク
❱
<;> 生成された全ゴールに適用
ac_rfl: 可換性と結合性を使う
aesop: 自明な証明の自動探索
all_goals: 全ゴールに対して適用
apply at: apply を仮定に適用する
apply_assumption: 自動 apply
apply: 含意→を使う
apply?: apply できるか検索
assumption: 仮定を自動で exact
by_cases: 排中律
by_contra: 背理法
by: タクティクモードに入る
calc: 計算モードに入る
cases: 場合分けをする
cases': Lean3版のcases
choose: 選択関数を得る
clear: 命題や定義を削除する
congr: ゴールの関数適用を外す
constructor: 論理積や同値性を示す
contradiction: 矛盾を指摘
contrapose: 対偶をとる
conv: 変換モードに入る
convert: 惜しい補題を使う
decide: 決定可能な命題を示す
done: 証明終了を宣言
dsimp: 定義に展開
exact: 証明を直接構成
exact?: exact できるか検索
exfalso: 矛盾を示すことに帰着
exists: 存在∃を示す
ext: 外延性を使う
field_simp: 分母を払う
fin_cases: 場合分けを簡潔に行う
fun_prop: 関数の諸性質を示す
funext: 関数等式を示す
gcongr: 合同性を用いる
generalize: 一般化する
guard_hyp: 仮定や補題を確認
have: 補題を用意する
hint: 複数のタクティクを同時に試す
induction: 帰納法
induction': inductionの構文違い
intro: 含意→や全称∀を示す
itauto: 直観主義論理の枠内で示す
left: 論理和∨を示す
linarith: 線形(不)等式を示す
native_decide: 実行による証明
nlinarith: 非線形な(不)等式を示す
norm_cast: 型キャストの簡略化
nth_rw: n 番目の項だけ rw
obtain: 分解して取り出す
omega: 自然数の線形計画を解く
positivity: 正値性を示す
push_neg: ドモルガン
qify: 有理数にキャストする
rcases: パターン分解
refine: 穴埋め推論
rel: 不等式を使う
rename_i: 死んだ変数に名前を付ける
repeat: 繰り返し適用
replace: 補題の入れ替え
rfl: 関係の反射性を利用する
right: 論理和∨を示す
ring: 可換環の等式を示す
rw_search: rw で示せるか検索
rw: 同値変形
says: タクティク提案の痕跡を残す
set: 定義の導入
show: 示すべきことを宣言
simp_all: 仮定とゴールを全て単純化
simp: 単純化
plausible: 反例を見つける
sorry: 証明したことにする
split: if/match 式を分解
suffices: 十分条件に帰着
tauto: トートロジーを示す
trans: 推移律を利用する
trivial: 基本的なタクティクを試す
try: 失敗をエラーにしない
unfold: 定義に展開
with_reducible: 透過度指定
wlog: 一般性を失わずに特殊化
第2部: チュートリアル
演習問題
❱
床屋のパラドクス
騎士と悪党のパズル
「ならば」の定義を疑う
全射・単射と左逆・右逆写像
Cantorの定理
Cantorの対関数の全単射性
Heying代数とBool代数
Light
Rust
Coal
Navy
Ayu
Lean by Example
option