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 //=.