Library Rstruct

Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
Require Import Ranalysis1 Rsqrt_def.
Require Import IndefiniteDescription.
Require Import ssreflect ssrbool eqtype ssrnat choice seq ssrfun ssralg.
Require Import fintype bigop rat ssrnum poly.

Set Implicit Arguments.
Import Prenex Implicits.

Import GRing.Theory.

Section Rstruct.

Open Scope R_scope.

Lemma Req_EM_T : forall r1 r2:R, {r1 = r2} + {r1 <> r2}.

Definition eqr (r1 r2 : R) : bool :=
let H:=(Req_EM_T r1 r2) in
match H with
|left _ => true
| right _ => false
end.

Lemma eqrP : Equality.axiom eqr.

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

Lemma R_irrelevance : forall (x y : R) (E E' : x = y), E = E'.

Parameter find_real : pred R -> nat -> option R.

Axiom correct_real : forall P n x, find_real P n = Some x -> P x.
Axiom complete_real: forall (P : pred R), (exists x, P x) ->
  exists n, find_real P n.
Axiom ext_real : forall P Q, P =1 Q -> find_real P =1 find_real Q.

Definition real_choiceMixin := Choice.Mixin correct_real complete_real ext_real.
Canonical Structure real_choiceType :=
  Eval hnf in ChoiceType R real_choiceMixin.

Lemma RplusA : associative (Rplus).

Lemma RplusC : commutative (Rplus).
Lemma RplusR0 : left_id R0 Rplus.
Lemma R0Rplus : right_id R0 Rplus.
Lemma RplusN : left_inverse R0 Ropp Rplus.

Definition real_zmodMixin := ZmodMixin RplusA RplusC RplusR0 RplusN.
Canonical Structure real_zmodType := Eval hnf in ZmodType R real_zmodMixin.

Lemma RmultA : associative (Rmult).
Lemma left_idRmult: left_id R1 Rmult.
Lemma right_idRmult : right_id R1 Rmult.
Lemma left_distr_Rmult_Rplus : left_distributive Rmult Rplus.
Lemma right_distr_Rmult_Rplus : right_distributive Rmult Rplus.
Lemma R1_neq_0 : R1 != R0.

Definition real_ringMixin := RingMixin RmultA left_idRmult
  right_idRmult left_distr_Rmult_Rplus right_distr_Rmult_Rplus R1_neq_0.
Canonical Structure real_ringType := Eval hnf in RingType R real_ringMixin.

Lemma RmultC: commutative Rmult.

Canonical Structure real_comringType := Eval hnf in ComRingType R RmultC.

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

Definition unit_R : pred R := fun 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 : forall a b : R , b * a = 1 /\ a * b = 1 -> unit_R a.

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 neq_norP (b1 b2: bool): reflect (~ (~~ b1 /\ ~~ b2)) ((b1 || b2)).

Lemma real_idomainMixin : forall p q, p * q = 0 -> (p == 0) || (q == 0).

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

Lemma unit_n0 : forall x, x != 0 -> x \is a GRing.unit.

Lemma Rinvx0: Rinvx 0 = 0.

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

Definition real_fieldIdomainMixin := FieldIdomainMixin real_fieldMixin.
Canonical Structure real_field := Eval hnf in FieldType R real_fieldMixin.

Definition Rleb r1 r2 :=
 match (Rle_dec r1 r2) with
  |left _ => true
  |right _ => false
end.

Definition Rltb r1 r2 := Rleb r1 r2 && (r1 != r2).
Definition Rgeb r1 r2 := Rleb r2 r1.
Definition Rgtb r1 r2 := Rltb r2 r1.

Lemma RlebP: forall r1 r2, reflect (r1 <= r2) (Rleb r1 r2).

Lemma RltbP: forall r1 r2, reflect (r1 < r2) (Rltb r1 r2).

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

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

End Rstruct.

Section ssreal_struct.

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.

Local Open Scope R_scope.

Lemma Rleb_norm_add x y : Rleb (Rabs (x + y)) (Rabs x + Rabs y).

Lemma addr_Rgtb0 x y : Rltb 0 x -> Rltb 0 y -> Rltb 0 (x + y).

Lemma Rnorm0_eq0 x : Rabs x = 0 -> x = 0.

Lemma Rleb_leVge x y : Rleb 0 x -> Rleb 0 y -> (Rleb x y) || (Rleb y x).

Lemma RnormM : {morph Rabs : x y / x * y}.

Lemma Rleb_def x y : (Rleb x y) = (Rabs (y - x) == y - x).

Lemma Rltb_def x y : (Rltb x y) = (y != x) && (Rleb x y).

Definition realNumMixin := NumMixin Rleb_norm_add addr_Rgtb0 Rnorm0_eq0
  Rleb_leVge RnormM Rleb_def Rltb_def.
Canonical Structure realNumDomainType := NumDomainType R realNumMixin.

Lemma RleP : forall x y, reflect (Rle x y) (Num.le x y).

Lemma RltP : forall x y, reflect (Rlt x y) (Num.lt x y).

Canonical Structure realNumFieldType := [numFieldType of R].

Lemma Rreal_axiom (x : R) : (Rleb 0 x) || (Rleb x 0).

Canonical Structure realRealDomainType := RealDomainType R Rreal_axiom.

Canonical Structure realRealFieldType := [realFieldType of R].

Lemma Rarchimedean_axiom : Num.archimedean_axiom realRealFieldType.

Canonical Structure realArchiFieldType := ArchiFieldType R Rarchimedean_axiom.

Lemma continuity_eq f g : f =1 g -> continuity f -> continuity g.

Lemma continuity_sum (I : finType) F (P : pred I):
(forall i, P i -> continuity (F i)) ->
  continuity (fun x => (\sum_(i | P i) ((F i) x)))%R.

Lemma continuity_exp f n: continuity f -> continuity (fun x => (f x)^+ n)%R.

Lemma Rreal_closed_axiom : Num.real_closed_axiom realArchiFieldType.

Canonical Structure realRcfType := RcfType R Rreal_closed_axiom.

End ssreal_struct.