Library Coquelicot.Rcomplements

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

This file describes basic missing facts about the standard library of reals and a few concerning ssreflect.seq. It also contains a definition of the sign function.

Tactic for changing the last argument of a property to an evar, in order to apply theorems modulo equality.

Ltac evar_last :=
  match goal with
  | |- ?f ?x
    let tx := type of x in
    let tx := eval simpl in tx in
    let tmp := fresh "tmp" in
    evar (tmp : tx) ;
    refine (@eq_ind tx tmp f _ x _) ;
    unfold tmp ; clear tmp
  end.

Require Import Reals Ssreflect.ssreflect.

Module MyNat.

Lemma neq_succ_0 (n : nat) : S n 0.

Lemma sub_succ (n m : nat) : S n - S m = n - m.

Lemma sub_succ_l (n m : nat) : n mS m - n = S (m - n).

Lemma lt_neq (n m : nat) : n < mn m.

Lemma minus_0_le (n m : nat) : n mn - m = 0.

Lemma sub_succ_r (n m : nat) : n - S m = pred (n - m).

Lemma sub_add (n m : nat) : n mm - n + n = m.

Lemma le_pred_le_succ (n m : nat) : pred n m n S m.

End MyNat.

Require Import Even Div2.
Require Import Ssreflect.seq Ssreflect.ssrbool.

Open Scope R_scope.

Integers

Integer part in Z

Lemma floor_ex : x : R, {n : Z | IZR n x < IZR n + 1}.
Definition floor x := proj1_sig (floor_ex x).

Lemma floor1_ex : x : R, {n : Z | IZR n < x IZR n + 1}.
Definition floor1 x := proj1_sig (floor1_ex x).

Interger part in nat

Lemma nfloor_ex : x : R, 0 x{n : nat | INR n x < INR n + 1}.
Definition nfloor x pr := proj1_sig (nfloor_ex x pr).

Lemma nfloor1_ex : x : R, 0 < x{n : nat | INR n < x INR n + 1}.
Definition nfloor1 x pr := proj1_sig (nfloor1_ex x pr).

More theorems about INR

Lemma INRp1_pos : n, 0 < INR n + 1.

Lemma Rlt_nat (x : R) : ( n : nat, x = INR (S n)) → 0 < x.

Lemma Rle_pow_lin (a : R) (n : nat) :
  0 a → 1 + INR n × a (1 + a) ^ n.

Lemma C_n_n: n, C n n = 1.

Lemma C_n_0: n, C n 0 = 1.

Fixpoint pow2 (n : nat) : nat :=
  match n with
    | O ⇒ 1%nat
    | S n ⇒ (2 × pow2 n)%nat
  end.

Lemma pow2_INR (n : nat) : INR (pow2 n) = 2^n.

Lemma pow2_pos (n : nat) : (0 < pow2 n)%nat.

Rinv


Lemma Rinv_le_contravar :
   x y, 0 < xx y/ y / x.

Lemma Rinv_lt_cancel (x y : R) :
  0 < y/ y < / xx < y.

Rdiv

Rewritings

Lemma Rdiv_1 : x : R, x / 1 = x.

Lemma Rdiv_plus : a b c d : R, b 0 → d 0 →
  a / b + c / d = (a × d + c × b) / (b × d).

Lemma Rdiv_minus : a b c d : R, b 0 → d 0 →
  a / b - c / d = (a × d - c × b) / (b × d).

Order

Lemma Rplus_lt_reg_l (x y z : R) : x + y < x + zy < z.

Lemma Rplus_lt_reg_r (x y z : R) : y + x < z + xy < z.

Lemma Rle_div_l : a b c, c > 0 → (a / c b a b × c).

Lemma Rle_div_r : a b c, c > 0 → (a × c b a b / c).

Lemma Rlt_div_l : a b c, c > 0 → (a / c < b a < b×c).

Lemma Rlt_div_r : a b c, c > 0 → (a × c < b a < b / c).

Lemma Rdiv_lt_0_compat : r1 r2 : R, 0 < r1 → 0 < r2 → 0 < r1 / r2.

Lemma Rdiv_le_0_compat : r1 r2 : R, 0 r1 → 0 < r2 → 0 r1 / r2.

Lemma Rdiv_lt_1 : r1 r2, 0 < r2 → (r1 < r2 r1 / r2 < 1).

Lemma Rdiv_le_1 : r1 r2, 0 < r2 → (r1 r2 r1/r2 1).

Rmult


Lemma Rle_mult_Rlt : c a b : R, 0 < bc < 1 → a b×ca < b.

Lemma Rmult_le_0_r : a b, a 0 → 0 ba × b 0.

Lemma Rmult_le_0_l : a b, 0 ab 0 → a × b 0.

Lemma pow2_gt_0 (x : R) : x 0 → 0 < x ^ 2.

Rminus

Rewritings

Lemma Rminus_eq_0 : r : R, r - r = 0.

Lemma Rdiv_minus_distr : a b c, b 0 → a / b - c = (a - b × c) / b.

Lemma Rmult_minus_distr_r: r1 r2 r3 : R, (r1 - r2) × r3 = r1 × r3 - r2 × r3.

Lemma Rminus_eq_compat_l : r r1 r2 : R, r1 = r2 r - r1 = r - r2.

Lemma Ropp_plus_minus_distr : r1 r2 : R, - (r1 + r2) = - r1 - r2.

Order

Lemma Rle_minus_l : a b c,(a - c b a b + c).

Lemma Rlt_minus_r : a b c,(a < b - c a + c < b).

Lemma Rlt_minus_l : a b c,(a - c < b a < b + c).

Lemma Rle_minus_r : a b c,(a b - c a + c b).

Lemma Rminus_le_0 : a b, a b 0 b - a.

Lemma Rminus_lt_0 : a b, a < b 0 < b - a.

Rplus

Sums

Lemma sum_f_rw (a : natR) (n m : nat) :
  (n < m)%natsum_f (S n) m a = sum_f_R0 a m - sum_f_R0 a n.

Lemma sum_f_rw_0 (u : natR) (n : nat) :
  sum_f O n u = sum_f_R0 u n.

Lemma sum_f_n_Sm (u : natR) (n m : nat) :
  (n m)%natsum_f n (S m) u = sum_f n m u + u (S m).
Lemma sum_f_u_Sk (u : natR) (n m : nat) :
  (n m)%natsum_f (S n) (S m) u = sum_f n m (fun ku (S k)).
Lemma sum_f_u_add (u : natR) (p n m : nat) :
  (n m)%natsum_f (n + p)%nat (m + p)%nat u = sum_f n m (fun ku (k + p)%nat).

Lemma sum_f_Sn_m (u : natR) (n m : nat) :
  (n < m)%natsum_f (S n) m u = sum_f n m u - u n.

Lemma sum_f_R0_skip (u : natR) (n : nat) :
  sum_f_R0 (fun ku (n - k)%nat) n = sum_f_R0 u n.

Lemma sum_f_chasles (u : natR) (n m k : nat) :
  (n < m)%nat → (m < k)%nat
  sum_f (S n) k u = sum_f (S n) m u + sum_f (S m) k u.

Rmin and Rmax

Rewritings

Lemma Rplus_max_distr_l :
   a b c, a + Rmax b c = Rmax (a + b) (a + c).

Lemma Rplus_max_distr_r :
   a b c, Rmax b c + a = Rmax (b + a) (c + a).

Lemma Rplus_min_distr_l :
   a b c, a + Rmin b c = Rmin (a + b) (a + c).

Lemma Rplus_min_distr_r :
   a b c, Rmin b c + a = Rmin (b + a) (c + a).

Lemma Rmult_max_distr_l :
   a b c, 0 aa × Rmax b c = Rmax (a × b) (a × c).

Lemma Rmult_max_distr_r :
   a b c, 0 aRmax b c × a = Rmax (b × a) (c × a).

Lemma Rmult_min_distr_l :
   a b c, 0 aa × Rmin b c = Rmin (a × b) (a × c).

Lemma Rmult_min_distr_r :
   a b c, 0 aRmin b c × a = Rmin (b × a) (c × a).

Lemma Rmin_assoc : x y z, Rmin x (Rmin y z) =
  Rmin (Rmin x y) z.

Lemma Rmax_assoc : x y z, Rmax x (Rmax y z) =
  Rmax (Rmax x y) z.

Order

Lemma Rmax_le_compat : a b c d, a bc dRmax a c Rmax b d.

Lemma Rmax_opp_Rmin : a b, Rmax (-a) (-b) = - Rmin a b.
Lemma Rmin_opp_Rmax : a b, Rmin (-a) (-b) = - Rmax a b.

Lemma Rmax_mult : a b c, 0 cRmax a b × c = Rmax (a × c) (b × c).

Lemma Rmax_le_Rplus : a b : R, 0 a → 0 bRmax a b a + b.

Lemma Rplus_le_Rmax : a b : R, a + b 2×Rmax a b.

Lemma Rmin_Rmax_l : a b, Rmin a b a Rmax a b.

Lemma Rmin_Rmax_r : a b, Rmin a b b Rmax a b.

Lemma Rmin_Rmax : a b, Rmin a b Rmax a b.

Rabs

Rewritings

Lemma Rabs_div : a b : R, b 0 → Rabs (a/b) = (Rabs a) / (Rabs b).

Lemma Rabs_eq_0 : x, Rabs x = 0 → x = 0.

Order

Lemma Rabs_le_between : x y, (Rabs x y -y x y).

Lemma Rabs_le_between' : x y z, Rabs (x - y) z y-z x y+z.

Lemma Rabs_lt_between : x y, (Rabs x < y -y < x < y).

Lemma Rabs_lt_between' : x y z, Rabs (x - y) < z y-z < x < y+z.

Lemma Rabs_le_between_min_max : x y z, Rmin x y z Rmax x yRabs (z - y) Rabs (x - y).

Lemma Rabs_le_between_Rmax : x m M,
  m x MRabs x Rmax M (-m).

Lemma Rabs_lt_between_Rmax : x m M,
  m < x < MRabs x < Rmax M (-m).

Lemma Rabs_maj2 : x, -x Rabs x.

Req


Lemma Req_lt_aux : x y, ( eps : posreal, Rabs (x - y) < eps) → x = y.

Lemma Req_le_aux : x y, ( eps : posreal, Rabs (x - y) eps) → x = y.

posreal


Lemma is_pos_div_2 (eps : posreal) : 0 < eps / 2.
Definition pos_div_2 (eps : posreal) := mkposreal _ (is_pos_div_2 eps).

The sign function


Definition sign (x : R) :=
  match Rle_dec 0 x with
    | left Hmatch Rle_lt_or_eq_dec _ _ H with
        | left _ ⇒ 1
        | right _ ⇒ 0
      end
    | right _ ⇒ -1
  end.

Lemma sign_0 : sign 0 = 0.

Lemma sign_opp (x : R) : sign (-x) = - sign x.

Lemma sign_0_lt (x : R) : 0 < x sign x = 1.

Lemma sign_lt_0 (x : R) : x < 0 sign x = -1.

Lemma sign_carac (x y : R) : (x × y > 0 (x = 0 y = 0)) → sign x = sign y.

Lemma sign_mult (x y : R) : sign (x × y) = sign x × sign y.

Lemma sum_INR : n, sum_f_R0 INR n = INR n × (INR n + 1) / 2.

ssreflect.seq

Finite subdivision

Lemma interval_finite_subdiv (a b : R) (eps : posreal) : (a b) →
  {l : seq R | head 0 l = a last 0 l = b
     i, (S i < size l)%natnth 0 l i < nth 0 l (S i) nth 0 l i + eps}.

Lemma interval_finite_subdiv_between (a b : R) (eps : posreal) (Hab : a b) :
  let l := proj1_sig (interval_finite_subdiv a b eps Hab) in
   i, (i < size l)%nata nth 0 l i b.

Notations
Lemma SSR_leq (n m : nat) : is_true (ssrnat.leq n m) (n m)%nat.
Lemma SSR_minus (n m : nat) : ssrnat.subn n m = (n - m)%nat.
rcons
Lemma rcons_ind {T : Type} (P : seq TType) :
  P [::] → ( (s : seq T) (t : T), P sP (rcons s t)) → s, P s.
Lemma rcons_dec {T : Type} (P : seq TType) :
  (P [::]) → ( s t, P (rcons s t)) → s, P s.
Lemma size_rcons_pos {T : Type} (s : seq T) (t : T) : (0 < size (rcons s t))%nat.

Lemma foldr_rcons {T T0 : Type} : (f : T0TT) x0 s t,
  foldr f x0 (rcons s t) = foldr f (f t x0) s.
Lemma foldl_rcons {T T0 : Type} : (f : TT0T) x0 s t,
  foldl f x0 (rcons s t) = f (foldl f x0 s) t.

Lemma head_rcons {T : Type} (x0 : T) (s : seq T) (t : T) : head x0 (rcons s t) = head t s.
Lemma behead_rcons {T : Type} (s : seq T) (t : T) :
  (0 < size s)%natbehead (rcons s t) = rcons (behead s) t.
Definition belast {T : Type} (s : seq T) :=
  match s with
    | [::][::]
    | h :: sbelast h s
  end.
Lemma behead_rev {T : Type} (s : seq T) : behead (rev s) = rev (belast s).

Lemma pairmap_rcons {T T0 : Type} (f : TTT0) (s : seq T) h0 h x0 :
  pairmap f x0 (rcons (rcons s h0) h) = rcons (pairmap f x0 (rcons s h0)) (f h0 h).
Lemma map_pairmap {T T0 T1 : Type} (f : T0T1) (g : TTT0) (s : seq T) (x0 : T) :
  map f (pairmap g x0 s) = pairmap (fun x yf (g x y)) x0 s.
Lemma pairmap_map {T T0 T1 : Type} (f : T0T0T1) (g : TT0) (s : seq T) (x0 : T) :
  pairmap f (g x0) (map g s) = pairmap (fun x yf (g x) (g y)) x0 s.
zip and unzip
Lemma size_unzip1 {T T0 : Type} (s : seq (T × T0)) : size (unzip1 s) = size s.
Lemma size_unzip2 {T T0 : Type} (s : seq (T × T0)) : size (unzip2 s) = size s.
Lemma zip_cons {S T : Type} hs ht (s : seq S) (t : seq T) :
  zip (hs :: s) (ht :: t) = (hs,ht) :: zip s t.
Lemma zip_rcons {S T : Type} (s : seq S) (t : seq T) hs ht : size s = size t
  zip (rcons s hs) (rcons t ht) = rcons (zip s t) (hs,ht).
Lemma unzip1_rcons {S T : Type} (s : seq (S×T)) (h : S×T) :
  unzip1 (rcons s h) = rcons (unzip1 s) (fst h).
Lemma unzip2_rcons {S T : Type} (s : seq (S×T)) (h : S×T) :
  unzip2 (rcons s h) = rcons (unzip2 s) (snd h).
Lemma unzip1_belast {S T : Type} (s : seq (S×T)) :
  unzip1 (belast s) = belast (unzip1 s).
Lemma unzip2_belast {S T : Type} (s : seq (S×T)) :
  unzip2 (belast s) = belast (unzip2 s).
Lemma unzip1_behead {S T : Type} (s : seq (S×T)) :
  unzip1 (behead s) = behead (unzip1 s).
Lemma unzip2_behead {S T : Type} (s : seq (S×T)) :
  unzip2 (behead s) = behead (unzip2 s).
Lemma unzip1_fst {S T : Type} (s : seq (S×T)) :
  unzip1 s = map (@fst S T) s.
Lemma unzip2_snd {S T : Type} (s : seq (S×T)) :
  unzip2 s = map (@snd S T) s.
Lemma size_belast' {T : Type} (s : seq T) :
  size (belast s) = Peano.pred (size s).
Lemma head_map {T1 T2 : Type} (f : T1T2) (s : seq T1) (x : T1) :
  head (f x) (map f s) = f (head x s).

Operations on the Riemann integral


Lemma StepFun_bound {a b : R} (f : StepFun a b) :
   s : R, x, Rmin a b x Rmax a bf x s.

Lemma Riemann_integrable_bound (f : RR) (a b : R) :
  Riemann_integrable f a b s : R, x, Rmin a b x Rmax a bf x s.

Extensionality

Lemma Riemann_integrable_ext : (f g : RR) (a b : R),
  ( x, Rmin a b x Rmax a bf x = g x)
    → Riemann_integrable f a bRiemann_integrable g a b.

Lemma RiemannInt_ext : (f g : RR) (a b : R)
  (pr_f : Riemann_integrable f a b) (pr_g : Riemann_integrable g a b)
  (Heq : x, Rmin a b x Rmax a bf x = g x),
    RiemannInt pr_f = RiemannInt pr_g.

Constant function

Lemma Riemann_integrable_const : (c a b : R),
  Riemann_integrable (fun xc) a b.

Lemma RiemannInt_const : (c a b : R) (pr : Riemann_integrable (fun xc) a b),
  RiemannInt pr = c × (b-a).

Addition

Lemma Riemann_integrable_plus : (f g : RR) (a b : R),
  Riemann_integrable f a bRiemann_integrable g a b
    Riemann_integrable (fun xf x + g x) a b.

Lemma RiemannInt_plus : (f g : RR) (a b : R)
  (pr_f : Riemann_integrable f a b) (pr_g : Riemann_integrable g a b)
  (pr : Riemann_integrable (fun xf x + g x) a b),
  RiemannInt pr = RiemannInt pr_f + RiemannInt pr_g.

Subtraction

Lemma Riemann_integrable_minus : (f g : RR) (a b : R),
  Riemann_integrable f a bRiemann_integrable g a b
    Riemann_integrable (fun xf x - g x) a b.

Lemma RiemannInt_minus : (f g : RR) (a b : R)
  (pr_f : Riemann_integrable f a b) (pr_g : Riemann_integrable g a b)
  (pr : Riemann_integrable (fun xf x - g x) a b),
  RiemannInt pr = RiemannInt pr_f - RiemannInt pr_g.

Opposite

Lemma Riemann_integrable_opp : (f : RR) (a b : R),
  Riemann_integrable f a b
    Riemann_integrable (fun x- f x) a b.

Lemma RiemannInt_opp : (f : RR) (a b : R)
  (pr_f : Riemann_integrable f a b)
  (pr : Riemann_integrable (fun x- f x) a b),
  RiemannInt pr = - RiemannInt pr_f.

Multiplication by a scalar

Lemma Riemann_integrable_scal : (f : RR) (a b c : R),
  Riemann_integrable f a b
    Riemann_integrable (fun xc × f x) a b.

Lemma RiemannInt_scal : (f : RR) (a b c : R)
  (pr_f : Riemann_integrable f a b)
  (pr : Riemann_integrable (fun xc × f x) a b),
  RiemannInt pr = c × RiemannInt pr_f.

Natural logarithm


Lemma ln_pow x n : 0 < xln (x^n) = INR n × ln x.

Lemma ln_le x y : 0 < xx yln x ln y.

Lemma ln_div x y : 0 < x → 0 < yln (x / y) = ln x - ln y.

Other


Lemma derivable_pt_lim_atan :
   x, derivable_pt_lim atan x (/(1 + x^2)).