Mathematics in Leanの第4章「集合と関数」の中の２つ目のセクションである「関数」を読みながら練習問題を解いています。その問題の中で集合族の積集合の写像と集合族の写像の積集合に関する問題がありました。全称量化子と存在量化子が絡み、なかなか手強かったので、紹介したいと思います。
練習問題とその証明は下記のとおりです。
example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' ⋂ i, A i := by
01 intro y h1
02 simp at h1
03 simp
04 have : (∃ x, (∀ (j : I), x ∈ A j) ∧ f x = y) → (∃ x, (∀ (i : I), x ∈ A i) ∧ f x = y) := by exact fun a => a
05 apply this
06 rcases (h1 i) with ⟨ xᵢ,_,h3⟩
07 use xᵢ
08 constructor
09 · intro k
10 rcases (h1 k) with ⟨ xₖ,h4,h5⟩
11 rw [← h5] at h3
12 convert h4
13 exact injf h3
14 assumption
いつものゴールをコメントで追記するスタイルだと追いきれないので行番号をつけました。行番号に基づいてポイントを解説します。
まず仮定で使われている命題Injective fは関数fが単射、すなわち任意のx, yについてf x=f yならばx=yを満たす、を意味します。
証明するべき命題は
fが単射かつ集合族$A_i, i\in I$の各集合$A_i$がfの定義域に含まれる時、fによる$A_i$の値域f'' $A_i$の積集合$\bigcap_{i\in I} f'' A_i$は$A_i$の積集合の値域$f'' \bigcap_{i\in I}A_i$に含まれる
となります。
証明の1行目はこの手の命題を証明する際の定番で、これによりゴールの部分集合関係が下記のように要素の関係になります。見やすいようにmathjaxを併用しています。
i: I
injf : Injective f
h1: $y\in \bigcap_{i\in I} f'' A_i$
⊢ $y\in f'' \bigcap_{i\in I}A_i$
h1のyとゴールのyは同じであることに注意してください。
証明の２行目simp at h1と３行目simpで集合族の積集合の部分をさらに展開するとこんなふうになります。
i: I
injf : Injective f
h1: $\forall i\in I, \exists x\in A_i, f x=y$
⊢ $\exists x, (\forall i\in I, x\in A_i)\land f x=y$
４行目のhaveと５行目のapplyを用いて結果として上記ゴールの全称量化子の変数iをjに書き換えています。ゴールがこんな感じになります。
⊢ $\exists x, (\forall j\in I, x\in A_j)\land f x=y$
ここからどう証明を進めるかで分からず結局答えを見てしまいました。ゴールが存在量化子で始まっているので仮定から１つのxを計算してuseする必要があります。ところが使えそうな仮定であるh1は全称量化子で始まっていてその内側の存在量化子に手が届きません。
ポイントは6行目のrcasesの第1引数である(h1 i)です。h1は関数型言語としては関数で、h1の外側で定義されたi: I（つまり任意のi）を引数に与えると、そのiでの内側の$\exists x\in A_i, f x=y$を返します（多分）。rcasesは存在量化子で始まる命題を指定されるとそれをwithの後ろで指定されたパターンに分解できます。この場合はi ごとに$A_i$の中に$x_i$があり$f x_i=y$です。
ゴールの存在量化子に使える$x_i$が計算できたのでそれを7行目でuse しています。その結果仮定とゴールはこんな感じになります。
i: I
infj: Injective f
h1: $\forall i\in I, \exists x\in A_i, f x=y$
h3: f $x_i$=y
⊢ $(\forall j\in I, x_i\in A_j)\land f x_i=y$
ゴールから存在量化子が外れて、２つの命題の論理和になりました。両方とも証明する必要があります。
ゴールの２つの論理和をそれぞれ証明するには8行目constructorを使います。・で始まりインデントされた9行目から13行目で左側、14行目で右側の証明を行います。
まず左側の証明を見てましょう。9行目のintro kで全称量化子を外します。すると、
i: I
infj: Injective f
h1: $\forall i\in I, \exists x\in A_i, f x=y$
h3: f $x_i$=y
k: I
⊢ $x_i\in A_k$
ゴールは簡単になりましたが、どうやって証明するのでしょうか。kは任意なのでちょうど$x_i$が含まれる$A_i$であるならば証明は終了するはずです。ところがゴールの式としてはAの添字はkです。この苦難の状況はどうやって乗り越えるのか、答えを見てびっくりです。
もう一度、今度はこの添字kを使い(h1 k)をrcasesで分解するのです。それが10行目です。この結果仮定とゴールは以下のようになります。
i: I
infj: Injective f
h3: f $x_i$ = y
k: I
$x_k$ : $\alpha$
h4: $x_k \in A_k$
h5: f $x_k$ = y
⊢ $x_i \in A_k$
ここまできてようやく証明の仕組みが分かりました。h3とh5からf $x_i$ = f $x_k$が分かります(11行目)。一方h4と現在のゴールを比較すると$x_i=x_k$が言えればよいです(12行目)。fが単射であることを使えば$x_i$=$x_k$が分かり左側の証明が終了します。
もう一度７行目に戻って、
i: I
infj: Injective f
h1: $\forall i\in I, \exists x\in A_i, f x=y$
h3: f $x_i$=y
⊢ $(\forall j\in I, x_i\in A_j)\land f x_i=y$
でゴールの論理和の右側の証明も必要です。が、よく見るとそれはh3と同じです。ゴールが仮定に含まれている場合はassumptionというタクティクで証明を終了することができます(14行目)。
これで全ての証明が終了しました。
この形式証明を見ると元々は同じように現れるiという添字のスコープが異なるため実際には3つの異なる文字であり、しかし結局$x_i=x_k$であることをfの単射から導いています。仮定h1に異なる出自のi, kを与えて、結果rcasesで$x_i, x_k$を得るところは言葉で証明を書いてもうまく書ききれない気がします。またきちんと思考の中では区別しておかないと形式証明も進まなくなります。
それなりに複雑でデリケートな変数の扱いがきちんとされているおかげで、形式証明が上手くいけばこの辺の細かい処理まで自信を持てることもこのようなシステムの利点だと感じました。
