attribute
前回書いた通り、例えば variable {V : Type*} [SetStructure V] [hV_Nonempty: Nonempty V] [hV_ZFC : V ⊧ₘ* 𝗭𝗙𝗖]とかしてやると、VはZFCのモデルとして振る舞うことになる。それはとても良いのだけれども、Z.leanはV ⊧ₘ* 𝗭という仮定のもとに書かれていて、このV ⊧ₘ* 𝗭𝗙𝗖という仮定だと自動的には適用されない。みたい。例えば、これは[V ⊧ₘ* 𝗭]を消すと通らない。それどころか、∅がこの場合なにかわからないと言い出す。
example [V ⊧ₘ* 𝗭] : IsEmpty (∅ : V) := by exact IsEmpty.empty
いちいちそういうの書くの嫌だなぁと思っていたら、こうすれば大丈夫らしい。
lemma hV_ZF : V ⊧ₘ* 𝗭𝗙 := by unfold ZermeloFraenkelChoice at hV_ZFC exact ModelsTheory.of_add_left V 𝗭𝗙 𝗔𝗖 lemma hV_Z : V ⊧ₘ* 𝗭 := by apply ModelsTheory.of_ss hV_ZF z_subset_zf -- By doing this, hV_Z and hV_ZF can be used without explicitly passing them. attribute [local instance] hV_Z attribute [local instance] hV_ZF -- Now, it works without [V ⊧ₘ* 𝗭]. example : IsEmpty (∅ : V) := by exact IsEmpty.empty
つまり、V ⊧ₘ* 𝗭𝗙𝗖という仮定から、V ⊧ₘ* 𝗭もV ⊧ₘ* 𝗭𝗙も証明できるのでやっておいて、それをattributeというコマンドを使って登録しておくと、自動的に見つけて仮定として使ってくれるらしい。これはほぼ常にZFで作業をする私にとってはとても便利である。なお、localと断っているので、sectionが終わったらそこで効力は終わる。
ext tactic
Finsetのときも外延性の公理を用いて集合が等しいことを示すextというtacticを使ったが、これはZのモデルでも使えるようにZ.leanで設定されている。というわけで、定番の空集合はユニークっていうのはこう書ける。
example : ∀ x : V, (∀ y : V, y ∉ x) ↔ x = (∅ : V):= by
intro x
constructor
case mp =>
intro h
ext z
constructor
case a.mp =>
intro hz
absurd hz
apply h
case a.mpr =>
intro hz
simp only [not_mem_empty] at hz
case mpr =>
intro hx
rw [hx]
simp only [not_mem_empty, not_false_eq_true, implies_true]
実はすでにZ.leanでisEmpty_iff_eq_emptyという定理として示されているんだけど。まあ、車輪の再発明上等である。
2つの集合の和集合
2つの集合xとyの和集合を表すx ∪ yも定義されているので、トリプルトンもそうやって定義することができる。まあ、結局はsUnionを使った場合とあまり変わらないのだが。
-- Rewrite by using union of two sets.
example : ∀ a b c : V, ∃ x : V, ∀ y : V, y ∈ x ↔ y = a ∨ y = b ∨ y = c := by
intro a b c
use (doubleton a b) ∪ (singleton c)
intro y
constructor
case h.mp =>
intro h
simp only [mem_union_iff, mem_doubleton_iff] at h
obtain (ha | hb) | hc := h
case inl.inl =>
left; exact ha
case inl.inr =>
right; left; exact hb
case inr =>
apply mem_singleton_iff.mp at hc
right; right; exact hc
case h.mpr =>
intro h
simp only [mem_union_iff, mem_doubleton_iff]
obtain ha | hb | hc := h
case inl =>
left; left; exact ha
case inr.inl =>
left; right; exact hb
case inr.inr =>
right
apply mem_singleton_iff.mpr hc
有限集合の定義
いや、まあ、こんなことをやらなくてもトリプルトンは{a, b, c}とかで書けてしまうんだけど。
example : ∀ a b c : V, ∃ x : V, ∀ y : V, y ∈ x ↔ y = a ∨ y = b ∨ y = c := by
intro a b c
use {a, b, c}
intro y
simp only [mem_insert, mem_singleton_iff]
こういうのを実装するのにどうしたらいいのかは皆目見当がつかないので、よくわかっている人が整備してくれるのは本当に助かる。
順序対
xとyの順序対、{{x}, {x, y}}はKuratowski Pairということでkpair x yで記述できる。記号では⟨x, y⟩ₖ。この小さいkを出すには"_k"ね。
それ以上のタプルにも対応しているようで、例えば⟨x, y, z⟩ₖは⟨x, ⟨y, z⟩ₖ⟩ₖとして実装されているようだ。というわけで、example (x1 y1 z1 x2 y2 z2 : V) : x1 = x2 ∧ y1 = y2 ∧ z1 = z2 ↔ ⟨x1, y1, z1⟩ₖ =⟨x2, y2, z2⟩ₖとかも証明できる。
べき集合
xのべき集合はpower xで書ける。練習にlemma power_singleton_empty : power ({∅} : V) = {∅, {∅}}とか証明したりしてみる。
無限の公理
ωはωで書けるようになっている。なので、(∅ : V) ∈ (ω : V)とか∀ x : V, (x ∈ (ω : V) → x ∪ {x} ∈ (ω : V))とか証明できるというかすでにできてる。いや、後者はいくつか定義をほどかないといけないので少しやることはある。もちろんこれらだけではユニークにならないので、そういうののなかで最小のものと書いてある。
次回予告
さて、次はいよいよ分出公理ということになる。これはこれまでと違って、図式になっているだけじゃなくて、「V上で定義可能」という概念を扱わないといけないことになる。論理式で書いちゃえばそれでおしまいといえばそうなのだけれども、思想として極力モデルで解釈して書きたいと思っているわけで、そこの架け橋がどう実装されてそれをどう運用するかというのは重要な問題である。ってわけで、ぼちぼちやっていきます。
