中間値の定理(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.