Mathematics in LeanもC04 Sets and Functionsの最初の章である集合まで辿り着きました。ここでは集合に関する性質の証明方法のLean4での実現の仕方を知ります。
- 集合が等しいこと(A=B)を示す場合、ゴールをA=Bとして方法として、AがBの部分集合であり、かつBがAの部分集合であることを示すこと
- AがBの部分集合であることを示すにはAの任意の要素がBの要素であることを示すこと
- 空集合と全体集合の性質
- 和集合と積集合をメンバーシップの論理和と論理積
- 集合族の積集合と和集合
のようなことがここでは解説されています。ここでは上記の初めの２つについて簡単な命題を示しながら説明してみます。
示すべき命題は：「集合tが集合sの部分集合であることと、集合sとtの積集合がtに等しいこと、は同値である」
example : (t ⊆ s) ↔ (s ∩ t = t) := by
constructor -- 同値を右向きと左向きに分ける
-- まず⊢ t ⊆ s → s ∩ t = tがゴール
· intro h -- h: t ⊆ s, ⊢ s ∩ t = t
rw [subset_def] at h -- h: ∀ x ∈ t, x ∈ s ⊢ s ∩ t = t
ext x --ゴールが集合の等号なので要素の関係に変換-- x ∈ s ∩ t ↔ x ∈ t
constructor -- 同値を右向きと左向きに分ける-- まず⊢ x ∈ s ∩ t → x ∈ tがゴール
· intro h1 -- h1: x ∈ s ∩ t ⊢ x ∈ t
apply h1.2 -- h1の右側を取れば証明終了-- 次は⊢ x ∈ t → x ∈ s ∩ tがゴール
intro h1 -- h1: x ∈ t, ⊢ x ∈ s ∩ t
exact mem_inter (h x h1) h1 -- h x h1でx ∈ s, h1でx ∈ tから証明終了。-- 次は⊢ s ∩ t = t → t ⊆ s がゴール
intro h -- h: s ∩ t = t, ⊢ t ⊆ s
rw [← h] -- ⊢ s ∩ t ⊆ s
exact inter_subset_left s t -- exact?で教えてくれる。
ベン図を思い浮かべてみれば自明な命題ではありますが、きちんと証明できること、それをLean 4できちんと形式化できること（確認できること）も重要です。
ゴールや仮定の中に部分集合の関係がある場合、rw [subset_def]を使って要素の関係に変換することができます。またゴールが集合の等号である場合、extタクティクで要素の関係に変換することができます。
x ∈ sとx ∈ tから、x ∈ s ∩ tを示して部分的な命題の証明が終了しています。exact mem_inter (h x h1) h1という部分です。このようにゴールが仮定からほぼ自明になったらexact? とやるとその自明な命題がすでにライブラリにあれば探してきて適用してくれます。
この証明の最後の部分も直前のゴールがs ∩ t ⊆ sでベン図を考えればほぼ自明です。そこでexact?とやるとexact inter_subset_leftを探してきてそこに引数として s tを与えることで適用してゴールが導かれました。
念の為にmem_interやinter_subset_leftの上にマウスを重ねてその定義を確認すると良いです。
