定理証明の会で実演した中間値の定理の証明

は

にあります。試すにはcoqを適当にインストールしてcoqideを起動して、このファイルを開く。
あとはツールバーから適当に下に進むボタンを押してれば証明の様子が分かります。Ctrl+Alt+↓でもおけ。

ほとんど実数の公理から直接証明しています。ポイントは

$A := \{ t \in R : t \le y \wedge f(t) \le 0 \}$

という集合 $A$ を使うと、求める点は $z = \sup A$ となるので、あとは

$f(z) = 0$

を証明するだけになります。これを示すために実数が全順序であることから

$f(z) < 0 \vee f(z) = 0 \vee f(z) > 0$

であることがいえるので、

$z = \sup A \to f(z) < 0 \to f(z) = 0$
$z = \sup A \to f(z) = 0 \to f(z) = 0$
$z = \sup A \to f(z) > 0 \to f(z) = 0$

をそれぞれ証明すれば終わりです。まず真ん中は自明。残りの二つはそれぞれの二つの前提が矛盾しているので、矛盾からは何でも証明できることによって $f(z) = 0$ が示せます。