中間値の定理(The Intermediate Value Theorem)
中間値の定理もCoqの標準ライブラリに存在する。Rsqrt_def.vの中にIVTという名前で見つけることができる。
Lemma IVT : forall (f:R -> R) (x y:R), continuity f -> x < y -> f x < 0 -> 0 < f y -> { z:R | x <= z <= y /\ f z = 0 }.
ただ、中間値が f x と f y の間の任意の値というわけではなく、0固定だったので、そこを任意の値が取れるように改良した。
Require Import Reals. Require Import FunctionalExtensionality. Open Scope R_scope. Proposition p05 : forall (f:R -> R) a b y, continuity f -> a < b -> f a < y -> y < f b -> (exists c, a <= c <= b /\ f c = y). Proof. intros. elim (IVT (fun x => f x - y) a b). intros c H3; elim H3; intros; exists c. split. apply H4. apply (Rplus_eq_reg_l (- y)). rewrite Rplus_opp_l in |- *. rewrite Rplus_comm in |- *. apply H5. rewrite (functional_extensionality (fun x : R => f x - y) (f - (fun _ => y))%F) in |- *. apply continuity_minus. apply H. apply continuity_const. intros p q; reflexivity. intro x; reflexivity. apply H0. apply (Rlt_minus (f a) y H1). apply (Rlt_Rminus y (f b) H2). Qed.