Library Stdlib.Reals.Raxioms
Lifts of basic operations for classical reals
Require Export BinInt.
Require Import Znat.
Require Import ClassicalDedekindReals.
Require Import ConstructiveCauchyReals.
Require Import ConstructiveCauchyRealsMult.
Require Import ConstructiveRcomplete.
Require Import ConstructiveLUB.
Require Export Rdefinitions.
Local Open Scope R_scope.
Open Scope CReal_scope.
Lemma Rrepr_0 : Rrepr 0 == 0.
Lemma Rrepr_1 : Rrepr 1 == 1.
Lemma Rrepr_plus : forall x y:R, Rrepr (x + y) == Rrepr x + Rrepr y.
Lemma Rrepr_opp : forall x:R, Rrepr (- x) == - Rrepr x.
Lemma Rrepr_minus : forall x y:R, Rrepr (x - y) == Rrepr x - Rrepr y.
Lemma Rrepr_mult : forall x y:R, Rrepr (x * y) == Rrepr x * Rrepr y.
Lemma Rrepr_inv : forall (x:R) (xnz : Rrepr x # 0),
Rrepr (/ x) == (/ Rrepr x) xnz.
Lemma Rrepr_le : forall x y:R, (x <= y)%R <-> Rrepr x <= Rrepr y.
Lemma Rrepr_appart : forall x y:R,
(x <> y)%R -> Rrepr x # Rrepr y.
Lemma Rappart_repr : forall x y:R,
Rrepr x # Rrepr y -> (x <> y)%R.
Close Scope CReal_scope.
Lemma Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1.
#[global]
Hint Resolve Rplus_comm: real.
Lemma Rplus_assoc : forall r1 r2 r3:R, r1 + r2 + r3 = r1 + (r2 + r3).
#[global]
Hint Resolve Rplus_assoc: real.
Lemma Rplus_opp_r : forall r:R, r + - r = 0.
#[global]
Hint Resolve Rplus_opp_r: real.
Lemma Rplus_0_l : forall r:R, 0 + r = r.
#[global]
Hint Resolve Rplus_0_l: real.
Lemma Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.
#[global]
Hint Resolve Rmult_comm: real.
Lemma Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3).
#[global]
Hint Resolve Rmult_assoc: real.
Lemma Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
#[global]
Hint Resolve Rinv_l: real.
Lemma Rmult_1_l : forall r:R, 1 * r = r.
#[global]
Hint Resolve Rmult_1_l: real.
Lemma R1_neq_R0 : 1 <> 0.
#[global]
Hint Resolve R1_neq_R0: real.
#[global]
Hint Resolve Rmult_comm: real.
Lemma Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3).
#[global]
Hint Resolve Rmult_assoc: real.
Lemma Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
#[global]
Hint Resolve Rinv_l: real.
Lemma Rmult_1_l : forall r:R, 1 * r = r.
#[global]
Hint Resolve Rmult_1_l: real.
Lemma R1_neq_R0 : 1 <> 0.
#[global]
Hint Resolve R1_neq_R0: real.
Lemma
Rmult_plus_distr_l : forall r1 r2 r3:R, r1 * (r2 + r3) = r1 * r2 + r1 * r3.
#[global]
Hint Resolve Rmult_plus_distr_l: real.
Rmult_plus_distr_l : forall r1 r2 r3:R, r1 * (r2 + r3) = r1 * r2 + r1 * r3.
#[global]
Hint Resolve Rmult_plus_distr_l: real.
Lemma Rlt_asym : forall r1 r2:R, r1 < r2 -> ~ r2 < r1.
Lemma Rlt_trans : forall r1 r2 r3:R, r1 < r2 -> r2 < r3 -> r1 < r3.
Lemma Rplus_lt_compat_l : forall r r1 r2:R, r1 < r2 -> r + r1 < r + r2.
Lemma Rmult_lt_compat_l : forall r r1 r2:R, 0 < r -> r1 < r2 -> r * r1 < r * r2.
#[global]
Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.
Lemma Rlt_trans : forall r1 r2 r3:R, r1 < r2 -> r2 < r3 -> r1 < r3.
Lemma Rplus_lt_compat_l : forall r r1 r2:R, r1 < r2 -> r + r1 < r + r2.
Lemma Rmult_lt_compat_l : forall r r1 r2:R, 0 < r -> r1 < r2 -> r * r1 < r * r2.
#[global]
Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.
Fixpoint INR (n:nat) : R :=
match n with
| O => 0
| S O => 1
| S n => INR n + 1
end.
Arguments INR n%_nat.
match n with
| O => 0
| S O => 1
| S n => INR n + 1
end.
Arguments INR n%_nat.
Lemma Rrepr_INR : forall n : nat,
CRealEq (Rrepr (INR n)) (inject_Z (Z.of_nat n)).
Lemma Rrepr_IPR2 : forall n : positive,
CRealEq (Rrepr (IPR_2 n)) (inject_Z (Z.pos (n~0))).
Lemma Rrepr_IPR : forall n : positive,
CRealEq (Rrepr (IPR n)) (inject_Z (Z.pos n)).
Lemma Rrepr_IZR : forall n : Z,
CRealEq (Rrepr (IZR n)) (inject_Z n).
Lemma archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1.
Definition is_upper_bound (E:R -> Prop) (m:R) := forall x:R, E x -> x <= m.
Definition bound (E:R -> Prop) := exists m : R, is_upper_bound E m.
Definition is_lub (E:R -> Prop) (m:R) :=
is_upper_bound E m /\ (forall b:R, is_upper_bound E b -> m <= b).
Lemma completeness :
forall E:R -> Prop,
bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.
Definition bound (E:R -> Prop) := exists m : R, is_upper_bound E m.
Definition is_lub (E:R -> Prop) (m:R) :=
is_upper_bound E m /\ (forall b:R, is_upper_bound E b -> m <= b).
Lemma completeness :
forall E:R -> Prop,
bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.