Require Import Rdefinitions Raxioms RIneq Rbasic_fun.
Require Import  ssreflect ssrbool eqtype ssrnat choice seq ssrfun ssralg.
Require Import IndefiniteDescription.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Open Scope R_scope.


Lemma Req_EM_T : forall r1 r2:R, {r1 = r2} + {r1 <> r2}.
Proof.
  intros; elim (total_order_T r1 r2); intros;
    [ elim a; intro;
      [ right; red in |- *; intro; rewrite H in a0; elim (Rlt_irrefl r2 a0)
        | left; assumption ]
      | right; red in |- *; intro; rewrite H in b; elim (Rlt_irrefl r2 b) ].
Qed.


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.
Proof.
move=> r1 r2; apply: (iffP idP) => [|<-];
[rewrite /eqr; case (Req_EM_T r1 r2) =>//=|
rewrite /eqr; case (Req_EM_T r1 r1) =>//=].
Qed.


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'.
Proof. exact: eq_irrelevance. Qed.

Definition real_xchoose : forall P : R -> bool , (exists x, P x) -> R.
intros P HP.
destruct (constructive_indefinite_description P HP) as [x HPx].
exact x.
Defined.


Definition real_choose P x0 :=
  if insub x0 : {? x | P x} is Some (exist x Px) then
    real_xchoose (ex_intro [eta P] x Px)
  else x0.


Lemma real_xchooseP : Choice.correct real_xchoose.
Proof. 
move=> P xP.
rewrite /real_xchoose.
by case (constructive_indefinite_description (fun x : R => P x) xP) => x HPx.
Qed.

Lemma real_chooseP : forall (P:R->bool) x0, P x0 -> P (real_choose P x0).
Proof.
intros P x0 HPx0.
by rewrite /real_choose (insubT P HPx0) real_xchooseP.
Qed.



Lemma eq_real_xchoose : Choice.extensional real_xchoose.
Admitted.

(*move=> P Q xP xQ eqPQ.
rewrite /real_xchoose.
case (constructive_indefinite_description (fun x : R => P x) xP) => x HPx.
case (constructive_indefinite_description (fun x : R => Q x) xQ)  => y HQy.
*)

Definition sreal_xchoose : forall P : (seq (seq R)) ->
   bool , (exists x, P x) -> (seq (seq R)).
intros P HP.
destruct (constructive_indefinite_description P HP) as [x HPx].
exact x.
Defined.


Lemma sreal_xchooseP : Choice.correct sreal_xchoose.
Proof. 
move=> P xP.
rewrite /sreal_xchoose.
by case (constructive_indefinite_description 
  (fun x : (seq (seq R)) => P x) xP) => x HPx.
Qed.


Lemma eq_sreal_xchoose : Choice.extensional sreal_xchoose.
Admitted.



Definition real_choiceMixin := ChoiceMixin  sreal_xchooseP  eq_sreal_xchoose.
Canonical Structure real_choiceType := Eval hnf in ChoiceType R real_choiceMixin.

(*we define a commutative ring structure for the real numbers, 
so that we may use the matrices in ssreflect*)

Lemma RplusA : associative (Rplus).
by move=> *; ring_simplify. Qed.

Lemma RplusC : commutative (Rplus).
by move=> *; ring_simplify.
Qed.
Lemma RplusR0 : left_id R0 Rplus.
by move=> *; ring_simplify.
Qed.
Lemma R0Rplus : right_id R0 Rplus.
by move=> *; ring_simplify.
Qed.
Lemma RplusN : left_inverse R0 Ropp Rplus.
by move=> *; ring_simplify.
Qed.


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

Lemma RmultA : associative (Rmult).
by move=> *; ring_simplify.
Qed.
Lemma left_idRmult: left_id R1 Rmult.
by move=> *; ring_simplify.
Qed.
Lemma right_idRmult : right_id R1 Rmult.
by move=> *; ring_simplify.
Qed.
Lemma left_distr_Rmult_Rplus : left_distributive Rmult Rplus.
by move=> *; ring_simplify.
Qed.
Lemma right_distr_Rmult_Rplus : right_distributive Rmult Rplus.
by move=> *; ring_simplify.
Qed.
Lemma R1_neq_0 : R1 != R0.
apply/eqP.
by exact: R1_neq_R0.
Qed.


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.
by move=> *; ring_simplify.
Qed.

(*Definition real_comringMixin := ComRingMixin RmultC.

RmultA RmultC left_idRmult 
   left_distr_Rmult_Rplus  R1_neq_0 .*)
Canonical Structure real_comringType := Eval hnf in ComRingType R RmultC.


(*why do i need all the lemmas in the mixin for the com ring?; it should be infered 
from the can struct of ring for R *)

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

Definition unit_R : pred R := fun r => r != 0.

(*Definition invmx A := if unit_mx A then (\det A)^-1 *m: \adj A else A.*)

Lemma RmultRinvx : {in unit_R, left_inverse 1 Rinvx Rmult}.
move=> r; rewrite -topredE /= => n0r.
rewrite /Rinvx /=.
rewrite /unit_R in n0r.
case C: (r != 0).
by rewrite <-Rinv_l_sym; [| apply/eqP].
move/eqP : C => C.
move/eqP : n0r => n0r.
elim (n0r C).
Qed.


Lemma RinvxRmult : {in unit_R, right_inverse 1 Rinvx Rmult}.
move=> r.
 rewrite -topredE /= => n0r.
rewrite /Rinvx /=.
rewrite /unit_R in n0r.
case C: (r != 0).
by rewrite <-Rinv_r_sym; [| apply/eqP].
move/eqP : C => C.
move/eqP : n0r => n0r.
elim (n0r C).
Qed.

Import GRing.Theory.

Lemma intro_unit_R : forall a b : R , b * a = 1 /\ a * b = 1 -> unit_R a.
move=> a b [Hab Hba].
rewrite /unit_R.
apply/eqP.
move=> Hc.
rewrite Hc in Hab.
ring_simplify in Hab.
have Hc2:= R1_neq_R0.
by apply Hc2; rewrite Hab.
Qed.

Lemma Rinvx_out : {in predC unit_R, Rinvx =1 id}.
Proof.
by move=> A; rewrite inE /=/Rinvx   -if_neg => ->.
Qed.

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)).
Proof.
 by move=> b1 b2;  case b1; case b2; constructor; auto; case; auto. Qed.

Lemma real_idomainMixin : forall p q, p * q = 0 -> (p == 0) || (q == 0).
Proof.
move=> p q Hpq.
apply/neq_norP.
move => [Hc1 Hc2].
move/eqP: Hc1 => Hc1.
move/eqP: Hc2 => Hc2.
have Hc3: p*q <>0.
by apply Rmult_integral_contrapositive_currified.
by elim Hc3.
Qed.

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

Lemma unit_n0 : forall x, x != 0 -> GRing.unit x.
Proof.
by move=> x Hx; rewrite /GRing.unit /= /unit_R.
Qed.

Lemma Rinvx0: Rinvx 0 = 0.
Proof.
rewrite /Rinvx.
by case C: (0!=0); move/eqP: C => C; elim C.
Qed.


Lemma real_fieldMixin : 
 GRing.Field.mixin_of [unitRingType of R].
Proof.
 move=> x nzx.
 rewrite /GRing.unit /= /unit_R.
apply: nzx.
Qed.

Definition real_fieldIdomainMixin := FieldIdomainMixin real_fieldMixin.

Canonical Structure real_field := @FieldType (IdomainType R real_fieldIdomainMixin) 
  real_fieldMixin.

(* reflect the order on the reals to bool *)

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 RleP: forall r1 r2, reflect (r1 <= r2) (Rleb r1 r2).
Proof.
move=> r1 r2; rewrite /Rleb; apply: (iffP idP);
by elim (Rle_dec r1 r2) => H.
Qed.

Lemma RltP: forall r1 r2, reflect (r1 < r2) (Rltb r1 r2).
Proof.
move=> r1 r2; rewrite /Rltb /Rleb; apply: (iffP idP).
elim (Rle_dec r1 r2) => H; move/andP=> [tf Hdif].
by move/eqP : Hdif => Hdif; elim (Rle_lt_or_eq_dec r1 r2 H) => H1.
done.
elim (Rle_dec r1 r2) => H => Hineq.
by rewrite /=; apply/eqP; apply Rlt_not_eq.
by elim H; left.
Qed.

Lemma RgeP: forall r1 r2, reflect (r1 >= r2) (Rgeb r1 r2).
Proof.
move=> r1 r2; rewrite /Rleb; apply: (iffP idP) => H.
by apply Rle_ge;  apply/RleP.
by apply/RleP; apply Rge_le.
Qed.

Lemma RgtP: forall r1 r2, reflect (r1 > r2) (Rgtb r1 r2).
Proof.
move=> r1 r2; rewrite /Rleb; apply: (iffP idP) => H.
by apply Rlt_gt;  apply/RltP.
by apply/RltP; apply Rgt_lt.
Qed.

Ltac toR := rewrite /GRing.add /GRing.opp /GRing.zero /GRing.mul /GRing.inv
  /GRing.one //=.