Library Coq.Reals.Rdefinitions



Require Export ZArith_base.
Require Import QArith_base.
Require Import ConstructiveRIneq.

Parameter R : Set.


Delimit Scope R_scope with R.


Local Open Scope R_scope.

Axiom sig_forall_dec
  : forall (P : nat -> Prop),
    (forall n, {P n} + {~P n})
    -> {n | ~P n} + {forall n, P n}.

Axiom sig_not_dec : forall P : Prop, { ~~P } + { ~P }.

Axiom Rabst : ConstructiveRIneq.R -> R.
Axiom Rrepr : R -> ConstructiveRIneq.R.
Axiom Rquot1 : forall x y:R, Req (Rrepr x) (Rrepr y) -> x = y.
Axiom Rquot2 : forall x:ConstructiveRIneq.R, Req (Rrepr (Rabst x)) x.

Module Type RbaseSymbolsSig.
  Parameter R0 : R.
  Parameter R1 : R.
  Parameter Rplus : R -> R -> R.
  Parameter Rmult : R -> R -> R.
  Parameter Ropp : R -> R.
  Parameter Rlt : R -> R -> Prop.

  Parameter R0_def : R0 = Rabst (CRzero CR).
  Parameter R1_def : R1 = Rabst (CRone CR).
  Parameter Rplus_def : forall x y : R,
      Rplus x y = Rabst (ConstructiveRIneq.Rplus (Rrepr x) (Rrepr y)).
  Parameter Rmult_def : forall x y : R,
      Rmult x y = Rabst (ConstructiveRIneq.Rmult (Rrepr x) (Rrepr y)).
  Parameter Ropp_def : forall x : R,
      Ropp x = Rabst (ConstructiveRIneq.Ropp (Rrepr x)).
  Parameter Rlt_def : forall x y : R,
      Rlt x y = ConstructiveRIneq.RltProp (Rrepr x) (Rrepr y).
End RbaseSymbolsSig.

Module RbaseSymbolsImpl : RbaseSymbolsSig.
  Definition R0 : R := Rabst (CRzero CR).
  Definition R1 : R := Rabst (CRone CR).
  Definition Rplus : R -> R -> R
    := fun x y : R => Rabst (ConstructiveRIneq.Rplus (Rrepr x) (Rrepr y)).
  Definition Rmult : R -> R -> R
    := fun x y : R => Rabst (ConstructiveRIneq.Rmult (Rrepr x) (Rrepr y)).
  Definition Ropp : R -> R
    := fun x : R => Rabst (ConstructiveRIneq.Ropp (Rrepr x)).
  Definition Rlt : R -> R -> Prop
    := fun x y : R => ConstructiveRIneq.RltProp (Rrepr x) (Rrepr y).

  Definition R0_def := eq_refl R0.
  Definition R1_def := eq_refl R1.
  Definition Rplus_def := fun x y => eq_refl (Rplus x y).
  Definition Rmult_def := fun x y => eq_refl (Rmult x y).
  Definition Ropp_def := fun x => eq_refl (Ropp x).
  Definition Rlt_def := fun x y => eq_refl (Rlt x y).
End RbaseSymbolsImpl.
Export RbaseSymbolsImpl.

Notation R0 := RbaseSymbolsImpl.R0 (only parsing).
Notation R1 := RbaseSymbolsImpl.R1 (only parsing).
Notation Rplus := RbaseSymbolsImpl.Rplus (only parsing).
Notation Rmult := RbaseSymbolsImpl.Rmult (only parsing).
Notation Ropp := RbaseSymbolsImpl.Ropp (only parsing).
Notation Rlt := RbaseSymbolsImpl.Rlt (only parsing).

Infix "+" := Rplus : R_scope.
Infix "*" := Rmult : R_scope.
Notation "- x" := (Ropp x) : R_scope.

Infix "<" := Rlt : R_scope.


Definition Rgt (r1 r2:R) : Prop := r2 < r1.

Definition Rle (r1 r2:R) : Prop := r1 < r2 \/ r1 = r2.

Definition Rge (r1 r2:R) : Prop := Rgt r1 r2 \/ r1 = r2.

Definition Rminus (r1 r2:R) : R := r1 + - r2.


Infix "-" := Rminus : R_scope.

Infix "<=" := Rle : R_scope.
Infix ">=" := Rge : R_scope.
Infix ">" := Rgt : R_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : R_scope.
Notation "x < y < z" := (x < y /\ y < z) : R_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : R_scope.

Injection from Z to R


Fixpoint IPR_2 (p:positive) : R :=
  match p with
  | xH => R1 + R1
  | xO p => (R1 + R1) * IPR_2 p
  | xI p => (R1 + R1) * (R1 + IPR_2 p)
  end.

Definition IPR (p:positive) : R :=
  match p with
  | xH => R1
  | xO p => IPR_2 p
  | xI p => R1 + IPR_2 p
  end.

Definition IZR (z:Z) : R :=
  match z with
  | Z0 => R0
  | Zpos n => IPR n
  | Zneg n => - IPR n
  end.

Lemma total_order_T : forall r1 r2:R, {Rlt r1 r2} + {r1 = r2} + {Rlt r2 r1}.

Lemma Req_appart_dec : forall x y : R,
    { x = y } + { x < y \/ y < x }.

Lemma Rrepr_appart_0 : forall x:R,
    (x < R0 \/ R0 < x) -> Rappart (Rrepr x) (CRzero CR).

Module Type RinvSig.
  Parameter Rinv : R -> R.
  Parameter Rinv_def : forall x : R,
      Rinv x = match Req_appart_dec x R0 with
               | left _ => R0
               | right r => Rabst ((ConstructiveRIneq.Rinv (Rrepr x) (Rrepr_appart_0 x r)))
               end.
End RinvSig.

Module RinvImpl : RinvSig.
  Definition Rinv : R -> R
    := fun x => match Req_appart_dec x R0 with
             | left _ => R0
             | right r => Rabst ((ConstructiveRIneq.Rinv (Rrepr x) (Rrepr_appart_0 x r)))
             end.
  Definition Rinv_def := fun x => eq_refl (Rinv x).
End RinvImpl.
Notation Rinv := RinvImpl.Rinv (only parsing).

Notation "/ x" := (Rinv x) : R_scope.

Definition Rdiv (r1 r2:R) : R := r1 * / r2.
Infix "/" := Rdiv : R_scope.

Definition up (x : R) : Z.