ゴールに存在量化子が入っている場合、存在量化子がついた変数に値を入ることでゴールの論理式を証明することができます。useタクティクを使うと、「この値を使え」ということができます。例えばこんな感じです。
example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
use 5 / 2 -- ⊢ 2 < 5 / 2 ∧ 5 / 2 < 3
norm_num -- No goals
ゴールの論理式の意味は「2より大きくて3より小さい実数xが存在する」です。まあ当たり前ですがどうやって証明するかです。この場合xが$\frac{5}{2}$であればこの不等式は確かに成立するので、xが存在することがわかり証明が終わります。
use 5/2とするとゴールの論理式が次のように変化します。
⊢ ∃ x, 2 < x ∧ x < 3
が以下に変化する
⊢ 2 < 5 / 2 ∧ 5 / 2 < 3
式が具体的な数値だけからなる場合、式が正しいかどうかは計算をすることでわかる場合があります。変化後の不等式も正しいことは数値の比較でわかります。その計算確認を正確に行なってくれるのがnorm_numタクティクです。
とはいえ、大抵の証明ではゴールの論理式に存在量化子∃ がある場合に具体的な数値を代入して証明ができることは少ない、というかほとんどないと思います。よくあるパターンは、ゴールの論理式の前提条件にも存在量化子があり、その変数の値が１つ分かったとするとそこからゴールの方の存在量化子がついた変数の値を計算できることはあります。
つまりゴールの前提条件の中の存在量化子を外して値が分かったことにします。それを利用してゴールの方の変数の値を計算しuseタクティクで代入すると証明が大きく進むわけです。
前提条件の中の存在量化子をはずすタクティクは２つあります。rintroタクティクとrcasesタクティクです。これらを使うことで存在量化子のついた変数の１つの値とその条件がラベル付きで導入されます。
簡単な例を見てみましょう。「零点を持つ関数fと任意の関数gを掛けて作った関数f * gには零点がある」という命題を証明していきます。この例はMILに掲載のものではなく自分で考えたものです。小さいものですがMy first lean4 証明です！
関数fは零点を持つ、をFnHasZeroP fとして形式化する。f x=0となるxがあれば良いので以下のように定義できる。
def FnHasZeroP (f : ℝ → ℝ) : Prop := ∃ x, f x = 0
ごく簡単な例として一次関数$2\,x-1$には零点があることを証明する。$x=\frac{1}{2}$が零点なのでuseタクティクを使えば良い。
example : FnHasZeroP fun x ↦ 2 * x - 1 := by
use 1/2 -- ⊢ (fun x => 2 * x - 1) (1 / 2) = 0
simp -- No goalsこれで証明終了。
いよいよ目的の命題「零点を持つ関数fと任意の関数gを掛けて作った関数f * gには零点がある」を形式化して証明する。h1はfに零点があるという前提、ゴールは「fun x ↦ f x * g xに零点がある」。
example (h1: FnHasZeroP f) (g : ℝ→ ℝ ) : FnHasZeroP fun x ↦ f x * g x := by
rcases h1 with ⟨a, ha⟩ -- a: ℝ, ha: f a = 0, ⊢ FnHasZeroP fun x => f x * g x
use a -- ⊢ (fun x => f x * g x) a = 0
dsimp -- ⊢ f a * g a = 0
rw [ha, zero_mul] -- No goalsこれで証明終了。
前提のh1がFnHasZeroP fでこの中に存在量化子がある。これをrcasesタクティクでバラす。f a=0という前提にhaというラベルをつける。
fの零点aがf * gの零点にもなるので、useタクティクを使い、ゴールの中の存在量化子の変数にaを代入する。あとはdsimp, rwのタクティクで式変形を行えば証明が終了する。
存在証明をどうやるのかの一例として他の存在から導く方法はこれでいけそうです。一方、それ以外のパターン、例えば鳩の巣論法による存在証明はどう形式化できるのか、今後調べていきたいと思いました。
