Library CoqApprox.Rstruct

This file is part of the CoqApprox formalization of rigorous polynomial approximation in Coq:
Copyright (c) 2010-2013, ENS de Lyon and Inria.
This library is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the library under the terms of the CeCILL-C license as circulated by CEA, CNRS and Inria at the following URL:
As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the library's author, the holder of the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details.

Require Import Rdefinitions Raxioms RIneq Rbasic_fun.
Require Import Epsilon FunctionalExtensionality.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice bigop ssralg.

Set Implicit Arguments.

Local Open Scope R_scope.

Lemma Req_EM_T (r1 r2 : R) : {r1 = r2} + {r1 <> r2}.

Definition eqr (r1 r2 : R) : bool :=
  if Req_EM_T r1 r2 is left _ then true else false.

Lemma eqrP : Equality.axiom eqr.

Canonical Structure real_eqMixin := EqMixin eqrP.
Canonical Structure real_eqType := Eval hnf in EqType R real_eqMixin.

Fact inhR : inhabited R.

Definition pickR (P : pred R) (n : nat) :=
  let x := epsilon inhR P in if P x then Some x else None.

Fact pickR_some P n x : pickR P n = Some x -> P x.

Fact pickR_ex (P : pred R) :
  (exists x : R, P x) -> exists n, pickR P n.

Fact pickR_ext (P Q : pred R) : P =1 Q -> pickR P =1 pickR Q.

Definition R_choiceMixin : choiceMixin R :=
  Choice.Mixin pickR_some pickR_ex pickR_ext.

Canonical R_choiceType := Eval hnf in ChoiceType R R_choiceMixin.

Fact RplusA : associative (Rplus).

Definition real_zmodMixin := ZmodMixin RplusA Rplus_comm Rplus_0_l Rplus_opp_l.

Canonical Structure real_zmodType := Eval hnf in ZmodType R real_zmodMixin.

Fact RmultA : associative (Rmult).

Fact R1_neq_0 : R1 != R0.

Definition real_ringMixin := RingMixin RmultA Rmult_1_l Rmult_1_r
  Rmult_plus_distr_r Rmult_plus_distr_l R1_neq_0.

Canonical Structure real_ringType := Eval hnf in RingType R real_ringMixin.
Canonical Structure real_comringType := Eval hnf in ComRingType R Rmult_comm.

Import Monoid.

Canonical Radd_monoid := Law RplusA Rplus_0_l Rplus_0_r.
Canonical Radd_comoid := ComLaw Rplus_comm.

Canonical Rmul_monoid := Law RmultA Rmult_1_l Rmult_1_r.
Canonical Rmul_comoid := ComLaw Rmult_comm.

Canonical Rmul_mul_law := MulLaw Rmult_0_l Rmult_0_r.
Canonical Radd_add_law := AddLaw Rmult_plus_distr_r Rmult_plus_distr_l.

Definition Rinvx r := if (r != 0) then / r else r.

Definition unit_R r := r != 0.

Lemma RmultRinvx : {in unit_R, left_inverse 1 Rinvx Rmult}.

Lemma RinvxRmult : {in unit_R, right_inverse 1 Rinvx Rmult}.

Lemma intro_unit_R x y : y * x = 1 /\ x * y = 1 -> unit_R x.

Lemma Rinvx_out : {in predC unit_R, Rinvx =1 id}.

Definition real_unitRingMixin :=
  UnitRingMixin RmultRinvx RinvxRmult intro_unit_R Rinvx_out.

Canonical Structure real_unitRing :=
  Eval hnf in UnitRingType R real_unitRingMixin.

Canonical Structure real_comUnitRingType :=
  Eval hnf in [comUnitRingType of R].

Lemma real_idomainMixin x y : x * y = 0 -> (x == 0) || (y == 0).

Canonical Structure real_idomainType :=
   Eval hnf in IdomainType R real_idomainMixin.

Lemma real_fieldMixin : GRing.Field.mixin_of [unitRingType of R].

Definition real_fieldIdomainMixin := FieldIdomainMixin real_fieldMixin.

Canonical Structure real_field := FieldType R real_fieldMixin.

Reflect the order on the reals to bool

Definition Rleb r1 r2 := if Rle_dec r1 r2 is left _ then true else false.
Definition Rltb r1 r2 := Rleb r1 r2 && (r1 != r2).
Definition Rgeb r1 r2 := Rleb r2 r1.
Definition Rgtb r1 r2 := Rltb r2 r1.

Lemma RleP r1 r2 : reflect (r1 <= r2) (Rleb r1 r2).

Lemma RltP r1 r2 : reflect (r1 < r2) (Rltb r1 r2).

Lemma RgeP r1 r2 : reflect (r1 >= r2) (Rgeb r1 r2).

Lemma RgtP r1 r2 : reflect (r1 > r2) (Rgtb r1 r2).