# ROSCOQ.CartCR

Require Export CoRN.reals.fast.CRtrans.

Require Export Coq.Program.Tactics.
Require Export MathClasses.interfaces.canonical_names.
Require Export MathClasses.misc.decision.
Require Export IRLemmasAsCR.

Definition QSignHalf (q: Q) : Q :=
QSign q ½ .

Require Export Vector.
Local Notation yes := left.
Local Notation no := right.

Definition polarTheta (cart :Cart2D Q) : CR :=
if (decide ((X cart) = 0))
then
CRpi × ' QSignHalf (Y cart)
else
let angle := (rational_arctan (Y cart / (X cart))) in
if decide (X cart < 0) then angle + (QSign (Y cart) π) else angle.

Definition polarθSign (target : Cart2D Q) : Q := QSign (Y target) 1.

Definition Cart2Polar (cart :Cart2D Q) : Polar2D CR :=
; θ := polarTheta cart |}.

Definition Polar2Cart (pol : Polar2D CR) : Cart2D CR :=
{|X := (rad pol) × (cos (θ pol))
; Y := (rad pol) × (sin (θ pol)) |}.

Require Import Coq.QArith.Qfield.
Require Import Coq.QArith.Qring.
Require Import Psatz.

Lemma Cart2Polar2CartID : (c :Cart2D Q),
' c = Polar2Cart (Cart2Polar c).
Proof.
intros c.
unfold Cart2Polar, Polar2Cart.
simpl. destruct c as [cx cy].
unfold polarTheta. simpl.
destruct (decide (cx = 0)) as [Hcx0 | Hcx0];
unfold equiv,EquivCart,CanonicalNotations.norm, NormSpace_instance_Cart2D ; simpl;[|].
- rewrite Hcx0. prepareForCRRing.
unfold stdlib_rationals.Q_mult, stdlib_rationals.Q_plus. QRing_simplify.
simpl. rewrite CRrational_sqrt_ofsqr.
unfold QSignHalf, QSign.
destruct (decide (cy < 0)) as [Hlt | Hlt];
autorewrite with CRSimpl;
prepareForCRRing; try rewrite (morph_opp QCRM);
split; CRRing.
- destruct (decide (cx < 0)) as [HcxNeg | HcxNeg].
+ rewrite CRCos_PlusMinus_Pi, CRSin_PlusMinus_Pi. split;
[apply cos_o_arctan_west| apply sin_o_arctan_west]; assumption.
+ apply orders.full_pseudo_srorder_le_iff_not_lt_flip in HcxNeg.
apply CRle_Qle in HcxNeg.
split; [apply cos_o_arctan_east | apply sin_o_arctan_east];
apply CRle_Qle in HcxNeg; revert Hcx0 HcxNeg;
unfoldMC; intros; lra.
Qed.

Require Export orders.

Lemma CRabsCRpi : CRabs CRpi = CRpi.
rewrite CRabs_pos;[reflexivity|].
apply CRweakenLt.
apply CR_lt_ltT.
apply CRpi_pos.
Qed.

Instance NormSpace_instance_Q : NormSpace Q Q := Qabs.Qabs.

Lemma QAbsQSign :
a c, (|QSign a c|) = |c|.
Proof.
intros.
unfold QSign, CanonicalNotations.norm,
NormSpace_instance_Q.
destruct (decide (a < 0)) as [Hd | Hd]; auto.
apply Qabs.Qabs_opp.
Qed.

Lemma multMiddle: (a b c : CR),
a×b×c = a×c×b.
Proof.
intros.
prepareForCRRing.
ring.
Qed.

Open Scope Q_scope.
Lemma Qle_shift_div_r_neg:
a b, 0 a b < 0 (Qdiv a b 0).
Proof.
intros.
unfold Qle, Qinv.
simpl. ring_simplify.
destruct a, b.
unfold Qlt in H0.
unfold Qle in H.
simpl in H, H0.
simpl.
ring_simplify in H.
ring_simplify in H0.
unfold Qinv. simpl.
destruct Qnum0; simpl; try omega.
nia.
nia.
Qed.

Lemma Qle_shift_div_l_neg:
a b, a 0 b < 0 (0 Qdiv a b).
Proof.
intros.
unfold Qle, Qinv.
simpl. ring_simplify.
destruct a, b.
unfold Qlt in H0.
unfold Qle in H.
simpl in H, H0.
simpl.
ring_simplify in H.
ring_simplify in H0.
unfold Qinv. simpl.
destruct Qnum0; simpl; try omega.
nia.
nia.
Qed.

Close Scope Q_scope.

: c a b : CR, a + c < b + ca < b.
Proof.
intros ? ? ? H.
revert H. prepareForCRRing.
intro H. ring_simplify in H.
assumption.
Qed.

Lemma CRLtTrans : a b c:CR,
a < b
→ b < c
→ a < c.
Proof.
intros ? ? ? ? ? . eapply ( orders.strict_po_trans _ _ _ );
eauto.
Qed.

a +b -b =a.
Proof.
intros.
prepareForCRRing. ring.
Qed.

Hint Rewrite <- CRopp_Qopp : MoveInjQCRIn.
Lemma polarθSignCorr1 : targetPos,
(|polarTheta targetPos|)* '(polarθSign targetPos) =polarTheta targetPos.
Proof.
intros. unfold polarθSign, polarTheta.
destruct (decide (X targetPos = 0)); auto.
- rewrite (mult_comm CRpi).
unfold CanonicalNotations.norm, NormSpace_instance_0.
rewrite CRabs_CRmult_Q.
rewrite CRabsCRpi.
unfold QSignHalf.
rewrite QAbsQSign.
unfold CanonicalNotations.norm, NormSpace_instance_Q.
simpl Qabs.Qabs. rewrite multMiddle.
apply CRmult_wd;[| reflexivity].
rewrite CRmult_Qmult.
apply inject_Q_CR_wd.
unfold QSign.
destruct (decide (Y targetPos < 0)); reflexivity.
- destruct (decide (X targetPos < 0)) as [Hd | Hd].
+ unfold lt, stdlib_rationals.Q_lt, zero,
stdlib_rationals.Q_0 in Hd, n.
unfold QSign, CanonicalNotations.norm,
NormSpace_instance_0.
destruct (decide (Y targetPos < 0)) as [Hdy | Hdy].
× rewrite CRabs_neg;[ prepareForCRRing;
unfold stdlib_rationals.Q_1; ring|].
apply CRweakenLt.
unfold π, CRpi_RealNumberPi_instance.
prepareForCRRing.
ring_simplify.
rewrite <- arctan_Qarctan.
eapply CRLtTrans;[apply CRarctan_range|].
1%nat.
vm_compute. reflexivity.

× rewrite CRabs_pos;[ prepareForCRRing;
unfold stdlib_rationals.Q_1; ring|].
apply CRweakenLt.
unfold π, CRpi_RealNumberPi_instance.
rewrite <- arctan_Qarctan.
eapply CRLtTrans; [|apply (proj1 (CRarctan_range _))].
1%nat.
vm_compute. reflexivity.

+ unfold lt, stdlib_rationals.Q_lt, zero,
stdlib_rationals.Q_0 in Hd, n.
unfold QSign, CanonicalNotations.norm,
NormSpace_instance_0.
destruct (decide (Y targetPos < 0)) as [Hdy | Hdy].
× unfold lt, stdlib_rationals.Q_lt, zero,
stdlib_rationals.Q_0 in Hdy.
unfold cast. autorewrite with MoveInjQCRIn.
rewrite CRabs_neg;[ prepareForCRRing;
unfold stdlib_rationals.Q_1; ring|].
apply rational_arctan_nonpos.
prepareForLra. prepareForCRRing.
unfold equiv, stdlib_rationals.Q_eq in n.
apply Qle_shift_div_r; try lra.

× unfold lt, stdlib_rationals.Q_lt, zero,
stdlib_rationals.Q_0 in Hdy.
rewrite CRabs_pos;[ prepareForCRRing;
unfold stdlib_rationals.Q_1; ring|].
apply rational_arctan_nonneg.
prepareForLra. prepareForCRRing.
unfold equiv, stdlib_rationals.Q_eq in n.
apply Qle_shift_div_l; try lra.
Qed.

Lemma Cart2PolarRadRange : (c :Cart2D Q),
Proof.
intros c.
unfold Cart2Polar. unfold CanonicalNotations.norm, NormSpace_instance_Cart2D.
simpl. rewrite <- CRsqrt_Qsqrt. apply CRsqrt_nonneg.
destruct c.
simpl.
apply CRle_Qle. unfoldMC. apply Q.Qplus_nonneg;apply Qpower.Qsqr_nonneg.
Qed.

Lemma addRangeLe : a t b v : CR,
(a - v) t (b - v) a t + v b.
Proof.
intros ? ? ? ? Hb.
repnd.
split.
- apply shift_leEq_plus. assumption.
- apply shift_plus_leEq. assumption.
Qed.

Lemma Cart2PolarAngleRange : (c :Cart2D Q),
-π θ (Cart2Polar c) π.
Proof.
intro c.
destruct c. simpl.
unfold polarTheta.
simpl. destruct (decide (X = 0)).
- clear. unfold QSignHalf, QSign.
destruct (decide (Y < 0));
[split;[|apply CRweakenLt]|apply CRweakenRange; split];
try( (1%nat); vm_compute; reflexivity).
rewrite <- CRopp_Qopp.
rewrite multNegShiftOut.
rewrite <- CRle_opp.
apply CRweakenLt.
1%nat.
vm_compute.
reflexivity.

- destruct (CRarctan_range ('(Y/X)%Q)) as [Hl Hr].
rewrite arctan_Qarctan in Hl.
rewrite arctan_Qarctan in Hr.
destruct (decide (X < 0)) as [l|l].
autounfold with QMC in l.
unfold QSign, CanonicalNotations.norm,
NormSpace_instance_0.
destruct (decide (Y < 0)) as [Hdy | Hdy];
autounfold with QMC in Hdy.
× split; [
| apply CRweakenLt;
eapply (orders.strict_po_trans); eauto;
1%nat; vm_compute; reflexivity].
prepareForCRRing.
rewrite CRplus_opp.
apply rational_arctan_nonneg.
autounfold with QMC.
apply Qle_shift_div_l_neg; try lra.

× split; [
apply CRweakenLt;
eapply (orders.strict_po_trans); eauto;
1%nat; vm_compute; reflexivity| ].
prepareForCRRing.
rewrite CRplus_opp.
apply rational_arctan_nonpos.
autounfold with QMC.
apply Qle_shift_div_r_neg; try lra.

+ apply CRweakenRange. split;
eapply (orders.strict_po_trans); eauto;
1%nat; vm_compute; reflexivity.
Qed.