Lean4を証明支援系として使っていても、型と証明の対応や関数型言語が突然現れることがあります。このことを知っていないと証明が読めないことがありました。
具体的には例えばある定理がこんな形だったとします。
def P (x:ℕ) : Prop := sorry
theorem theoA : ∀ x > 3, P x := sorry
P xを命題としてxが3より大きい場合はP xが成り立つ、というのがtheoAという定理です。
当然P 4は4>3なので成り立つはずです。証明は普通はこんなふうにやると思うのです。
example : P 4 := by
apply theoA -- ⊢ 4 > 3
norm_num -- ⊢ No goals
apply theoAで定理theoAをゴールP 4にマッチさせるとx=4となりゴールが4>3に変化します。4>3は数値同士の関係ですからnorm_numタクティクで成立を確認できて証明が終了します。
ところが同じ証明が以下のように書かれているとちょっと悩むわけです。theoA 4 hは一体何ものなのでしょうか。
example : P 4 := by
have h : 4 > 3 := by norm_num
exact theoA 4 h
theoAの型を調べてみると（VSCodeならマウスを重ねると）
theoA : (x:ℕ) -> (x>3) -> (P x)
であることが分かります。つまり２つの引数を取り(P x)型の命題を返す関数型であることが分かります。これでtheoA 4 hの正体がわかりました。theoA 4 hは関数theoAに２つの引数4及びhを与えたものです。関数の戻り値はP 4です。これはゴールそのものですからexactで証明を終了させることができます。
ちなみに4だけを引数として与えると型がこんなふうになります。
theoA 4 : (4>3) -> (P 4)
さらに引数hを与えてtheoA 4 hと書くと(P 4)が戻ってくるわけですが、ちなみにhの位置に4>3を直接書いてもうまく行きません。theoA 4 (4>3)みたいに書いても4>3はProp:Type型であってProp型ではない、というエラーが生じます。多分ちゃんと証明されたものだけが命題として指定できると理解しています。
おそらく他にも色々あるとは思うのですが、ここは関数型プログラミングの側面がそのまま出ていると思います。定理に全称量化子がついている場合、その定理を関数としてみると引数を与えることで全称量化子を特定することが出来ることが分かりました。
