読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

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