🦆

Lean 入門：Scribble (1)

に公開
定理証明支援系
Lean 4
tech

Lean のチュートリアルの Scribble の問題を順に解いていきます。

オンラインチュートリアルで、入力欄に回答を記入すると先に進めます。Scribble は
「Lean 速習コース」とも言うべきもので、これを一通りやると Lean で証明できる様になります。復習にはちょうど良いです。ただ結構な分量があります。
また本当にエッセンスだけ伝える感じなので、これから Lean を初めて学ぶ、と言う人は Lean Game Serverから、"A Lean Intro to Logic" をやって "Natural Number Game" をやった方が良いかもしれません。

命題論理の問題。

  • tauto: 命題論理の恒等式を一発で証明出来ますが、すぐにこの技は封印されてしまう・・・
  • rfl: ゴールが等式で、左辺と右辺が等しい時に使います
  • assumption: ゴールと同じものが仮定の中にある時に使います
  • decide: とりあえずゴールが True の時は使える
  • contradiction: 仮定が矛盾している時に使える
  • constructor:
    • ゴールの A\wedge B を２つのゴール A と B に分解する
    • ゴールの A\leftrightarrow B を A\to B, B\to A に分解する
  • obtain:
    • obtain ⟨hA, hBC⟩ := h で 仮定の h: A\wedge B\wedge C を hA, hBC に分解する
    • obtain h | h := h で仮定の h: A\vee B を h:A と h:B の２つの場合に場合分けする
    • h:A\leftrightarrow Bの場合、obtainを使わなくてもh.mp, h.mpr でアクセスできる
  • left, right: ゴールの A\vee Bの A か B かを選ぶ

Implis

含意を含む命題論理の問題。

  • intro: ゴールのA\to B を intro hA で仮定 hA:A とゴール B に分解
  • revert: ゴールが B で仮定に hA:A があると、revert hAで仮定hAを消してゴールを A\to B に出来る。introの逆。
  • apply: ゴールが B で仮定に hAB:A\to Bがあると、apply hAB でゴールを A にする。apply hAB at h みたいなことも出来る。
  • symm: ゴールの演算子の左右を入れ替える。symm at h なども書ける。
  • rw: rw [h1] とか rw [← h1] とかで書き換える。
  • trans: ゴールが A\leftrightarrow B の時、trans C で A\leftrightarrow C, C\leftrightarrow B と中間にCを挿入できる。
  • by_cases: by_cases h:A で h:A と h:\neg Aの場合分けをする(古典論理)。
  • rw [not_not]: 二重否定除去

Saturn

等式に関する問題。

  • ring: 環に関する等式証明をやってくれる

Quantus

量化子の練習。最後の「酒場のパラドックス」は難しいですね。

  • use: \text{Nonempty }\mathbb{N} を証明するのに、use 0 と実例を１つ挙げる
  • obtain: h:\text{Nonempty }A に対して obtain ⟨a⟩ := h とすると、a:A が手に入る。
  • unfold: 関数とかの定義を展開する
  • choose: 仮定\exists (r:\mathbb{N}): n = r+r を choose s hs using h で hs:n = s + s に変換する。
  • push Not: \neg\exists を \forall\neg に書き換える。

Piazza

集合の包含関係の練習。

  • simp: 計算を進める。
  • ext x: 集合に関する等式 A=B を x\in A\leftrightarrow x\in B に書き換える。
  • univ: Set N: \mathbb{N}の中の最大の集合、なので数学的には\mathbb{N}なんだけど\mathbb{N}は値の型で集合の型では無いので区別して書く、ということなんだと思う。
    • eq_univ_iff_forall: s = \text{Set.univ} \leftrightarrow \forall (x : \alpha), x \in s
  • \emptyset: eq_empty_iff_forall_notMem: s = \emptyset \leftrightarrow \forall (x : \alpha), x \notin s
  • ゴールが x\in Aのとき、h:B\subseteq Aを apply するとゴールが x\in Bに変わる。

包含関係の問題は ext, simp, tauto で割と解ける。

Spinoza

否定に関する命題論理っぽいテーマ。

  • have, suffices: 補題を \text{have } g:\neg B みたいに作れる。
  • by_contra: ゴールが P ならば、by_contra h で仮定 h:\neg P を作り、ゴールが False になる。
  • contrapose: ゴールを対偶で書き換える。
  • revert: 対偶の形を作るのに使える

Luna

不等式に関する証明。

  • omega: 強力な自動証明。整数なら使える。
  • linarith: たまに使える。実数、有理数でOK。
  • lt_trichotomy: obtain h | h | h := lt_trichotomy x y で x < y, x = y, x > y の場合分けが出来る。
  • Icc: Icc a b で \{a, a+1, \ldots, b\} と閉区間を表す。
    • simp で不等式に直す
  • subset_iff: s_1\subseteq s_2 \leftrightarrow \forall x:A, x\in s_1 \to x\in s_2.

Discussion