ROSCOQ.CartIR

Require Export CartCR.
Require Export MCInstances.

Open Scope mc_scope.
Instance Pi_Instance_IR: RealNumberPi :=
 Pi.

Lemma PiBy2NoMC :
   ('½) × π = Pi [/]TwoNZ.
Proof.
  apply (injective IRasCR).
  rewrite <- CRPiBy2Correct.
  unfold mult, Mult_instance_IR.
  autorewrite with IRtoCR.
  unfold cast, Cart_CR_IR.
  rewrite CRasIRasCR_id.
  pose proof (@rings.mult_comm CR _ _ _ _ _ _ ) as Hc.
  unfold Commutative in Hc.
  unfold mult in Hc.
  rewrite Hc. reflexivity.
Qed.

Lemma cgminus_Qminus : (a b : Q),
  (a-b) a[-]b.
  reflexivity.
Qed.

Require Import Psatz.

Lemma QabsQpos : (qp: Qpos),
   ((Qabs.Qabs qp) == qp)%Q.
  intros.
  destruct qp; simpl.
  rewrite Qabs.Qabs_pos; lra.
Qed.

Hint Rewrite QabsQpos : CoRN.

Lemma QAbsMultSign: (a : Q) (b : Qpos),
  ((Qabs.Qabs a) × / b × ((QSign a 1) × b) == a)%Q.
Proof.
  intros ? ?.
  unfold QSign. destruct b as [b bp].
  simpl.
  destruct (decide (a < 0)) as [Hd | Hd]; revert Hd; unfoldMC; intro Hd.
- ring_simplify. rewrite Qabs.Qabs_neg;[|lra]. field. lra.
- ring_simplify. rewrite Qabs.Qabs_pos;[|lra]. field. lra.
Qed.

Lemma approximateAbsSmallIR: (r:CR) (eps : Qpos),
    AbsSmall eps (CRasIR r [-] (approximate r eps)).
  intros ? ?.
  pose proof (ball_approx_r r eps ) as Hball.
  apply CRAbsSmall_ball in Hball.
  fold (inject_Q_CR) in Hball.
  apply CR_AbsSmall_as_IR in Hball.
  rewrite CR_minus_asIR2 in Hball.
  rewrite <- IR_inj_Q_as_CR in Hball.
  rewrite <- IR_inj_Q_as_CR in Hball.
  rewrite IRasCRasIR_id in Hball.
  rewrite IRasCRasIR_id in Hball.
  exact Hball.
Qed.

Lemma multRAbsSmallIR:
   (y x e : IR),
  AbsSmall e x AbsSmall (e[*]AbsIR y) (x[*]y).
Proof.
  intros.
  apply mult_AbsSmall;[assumption|].
  apply AbsIR_imp_AbsSmall.
  apply leEq_reflexive.
Qed.

Require Export Coq.QArith.Qabs.

Lemma QMinusShiftRLe:
   a b c,
  ((a - b) c
  → a c +b)%Q.
Proof.
  intros.
  lra.
Qed.
Lemma QposDivLe0 : (qp : Qpos),
0[<=](/ qp)%Q.
Proof.
  intros.
  destruct qp.
  simpl. apply Qinv_le_0_compat.
  lra.
Qed.

Lemma QposDivLe0IR : (qp : Qpos),
[0][<=]Q2R (/ qp)%Q.
Proof.
  intros.
  apply injQ_nonneg.
  apply QposDivLe0.
Qed.

Lemma QDivQopp : (a b: Q),
  (-(a /b )== ((-a )/ b))%Q.
Proof.
  intros.
  destruct (decide (b=0)) as [Hd|Hd].
- rewrite Hd. destruct a.
  unfoldMC. unfold Qdiv, Qinv. simpl.
  ring.
- field. assumption.
Qed.

Lemma AbsIRQpos : (qp : Qpos),
  AbsIR qp [=] qp.
Proof.
  intros.
  rewrite AbsIR_eq_x;[reflexivity|].
  rewrite <- inj_Q_Zero.
  apply inj_Q_leEq.
  simpl.
  destruct qp. simpl.
  lra.
Qed.

Hint Unfold Zero_instance_IR : IRMC.
Lemma Sin_nonpos
     : θ : , -π θ 0 → Sin θ 0.
Proof.
  intros ? Hd.
  apply inv_cancel_leEq.
  autounfold with IRMC.
  autorewrite with CoRN.
  rewrite <- Sin_inv.
  repnd.
  apply inv_resp_leEq in Hdr.
  apply inv_resp_leEq in Hdl.
  autounfold with IRMC in Hdl, Hdr.
  autorewrite with CoRN in Hdr, Hdl.
  apply Sin_nonneg; assumption.
Qed.

This proof can be generalized for even functions. Similarly, AbsIRSin can be generalized for odd functions
Lemma CosEven2 : θ,
  AbsIR θ Pi [/]TwoNZ
  → Cos θ = Cos (AbsIR θ).
Proof.
  intros ? H.
  pose proof (leEq_or_leEq _ θ [0]) as Hd.
  apply not_ap_imp_eq.
  intro Hc.
  apply Hd.
  clear Hd. intro Hd.
  apply ap_tight in Hc;[contradiction|].
  repnd.
  destruct Hd as [c|].
- rewrite AbsIR_eq_inv_x;[|assumption].
  rewrite Cos_inv. reflexivity.
- rewrite AbsIR_eq_x; [|assumption].
  reflexivity.
Qed.

Lemma AbsIRCos : θ,
  AbsIR θ Pi [/]TwoNZ
  → AbsIR (Cos θ) = Cos (AbsIR θ).
Proof.
  intros ? Hb.
  rewrite <- CosEven2 by assumption.
  apply AbsIR_imp_AbsSmall in Hb.
  unfold AbsSmall in Hb.
  repnd.
  eapply Cos_nonneg in Hbl; eauto.
  rewrite AbsIR_eq_x;[| assumption].
  reflexivity.
Qed.

Lemma Cos_nonnegAbs
  : θ : , AbsIR θ [<=] Pi [/]TwoNZ [0] [<=]Cos θ.
Proof.
  intros ? H.
  apply AbsIR_imp_AbsSmall in H.
  destruct H.
  apply Cos_nonneg; assumption.
Qed.

Lemma TimeRangeShortenL :
   (a b t : Q) (qt : QTime),
    a + qt t b
    → a t b.
Proof.
  unfoldMC.
  intros ? ? ? ? Hb.
  destruct qt as [? p].
  simpl. pose proof p as pb.
  apply QTimeD in pb.
  repnd. simpl in Hbl. split; lra.
Qed.

Lemma AbsIRSine : θ,
  -π θ π
  → AbsIR (Sin θ) = Sin (AbsIR θ).
Proof.
  intros ? Hb.
  pose proof (leEq_or_leEq _ θ [0]) as Hd.
  apply not_ap_imp_eq.
  intro Hc.
  apply Hd.
  clear Hd. intro Hd.
  apply ap_tight in Hc;[contradiction|].
  repnd.
  destruct Hd as [c|].
- unfold CanonicalNotations.norm, NormSpace_instance_IR.
  symmetry. rewrite AbsIR_eq_inv_x; [|assumption].
  rewrite Sin_inv.
  rewrite AbsIR_eq_inv_x; [reflexivity|].
  apply Sin_nonpos; split; try assumption.
- unfold CanonicalNotations.norm, NormSpace_instance_IR.
  symmetry. rewrite AbsIR_eq_x; [|assumption].
  rewrite AbsIR_eq_x; [reflexivity|].
  apply Sin_nonneg; assumption.
Qed.

Definition normIR (pt : Cart2D IR) : IR.
  apply sqrt with (x:=normSqr pt).
  unfold normSqr.
  unfoldMC. unfold Plus_instance_IR, Mult_instance_IR.
  rewrite <- nexp_two.
  rewrite <- nexp_two.
  apply cc_abs_aid.
Defined.

Lemma normIRSpec : (pt : Cart2D IR),
  (normIR pt) × (normIR pt) = (normSqr pt).
Proof.
  intros. unfoldMC. unfold Plus_instance_IR, Mult_instance_IR.
  rewrite <- nexp_two.
  apply sqrt_sqr.
Qed.

Definition normIRInv (pt : Cart2D IR) (nz : 0 [<] normIR pt) : IR.
  apply f_rcpcl with (x:= normIR pt).
  simpl. apply ap_symmetric.
  apply less_imp_ap.
  exact nz.
Defined.

Lemma normIRInvSpec : (pt : Cart2D IR) (nz : 0 [<] normIR pt),
   (normIR pt) × (normIRInv pt nz) = 1.
  intros. unfold normIRInv.
  unfoldMC. unfold Plus_instance_IR, Mult_instance_IR, Zero_instance_IR,
    Negate_instance_IR.
  rewrite field_mult_inv.
  reflexivity.
Qed.

Lemma normIRInvSpecInvLeft : (pt : Cart2D IR) (nz : 0 [<] normIR pt),
    (normIRInv pt nz) × (normIR pt) = 1.

  intros. rewrite mult_comm.
  apply normIRInvSpec.
Qed.

Lemma MultIRSqrMix:
a b : IR,
 (a × a × b × b = (a × b) × (a × b)).
  intros.
   unfoldMC. unfold Plus_instance_IR, Mult_instance_IR, Zero_instance_IR,
    Negate_instance_IR.
  ring.
Qed.

Lemma normIRInv2 : (pt : Cart2D IR) (nz : 0 [<] normIR pt),
   (normSqr pt) × (normIRInv pt nz) × (normIRInv pt nz) = 1.
  intros. rewrite <- normIRSpec.
  rewrite MultIRSqrMix.
  rewrite normIRInvSpec.

  unfoldMC. unfold Plus_instance_IR, Mult_instance_IR, Zero_instance_IR,
    Negate_instance_IR, One_instance_IR.
    ring.
Qed.

rotate the axis so that the X axis points towards xAxisDir
Definition rotateOriginTowards
  (XTowards : Cart2D IR)
  (nz : 0 [<] normIR XTowards)
  (pt : Cart2D IR) : Cart2D IR :=
  let normInv := normIRInv XTowards nz in
{|X:= ((X pt)*(X XTowards) + (Y pt)*(Y XTowards)) × (normInv);
  Y:= ((Y pt)*(X XTowards) - (X pt)*(Y XTowards)) × (normInv) |}.

Require Import Ring.
Require Import CoRN.tactics.CornTac.
Require Import CoRN.algebra.CRing_as_Ring.

Add Ring RisaRing: (CRing_Ring IR).
Lemma rotateOriginTowardsTowards : (XTowards : Cart2D IR)
  (nz : 0 [<] normIR XTowards),
  rotateOriginTowards XTowards nz XTowards
  = {|X:= normIR XTowards; Y:=0|}.
Proof.
  intros. unfold rotateOriginTowards.
  unfold equiv, EquivCart.
  simpl.
  fold (normSqr XTowards).
  rewrite <- normIRSpec.
  unfoldMC. unfold Plus_instance_IR, Mult_instance_IR, Zero_instance_IR,
    Negate_instance_IR.
  split; [| ring].
  rewrite <- CRings.mult_assoc.
  unfold normIRInv. rewrite field_mult_inv.
  ring.
Qed.

Lemma rotateOriginTowardsNormSqrPreserved
    : (XTowards : Cart2D IR)
  (nz : 0 [<] normIR XTowards) pt,
  normSqr (rotateOriginTowards XTowards nz pt)
  = normSqr pt.
Proof.
  intros. unfold rotateOriginTowards.
  unfold normSqr. simpl.
  unfoldMC. unfold Plus_instance_IR, Mult_instance_IR, Zero_instance_IR,
    Negate_instance_IR.
  match goal with
  [ |-_ [=] ?r] ⇒ assert (r [=] r [*] [1]) as Heq by ring
  end.
  ring_simplify.
  rewrite <- normIRInv2 with (nz:=nz) in Heq.
  unfold normSqr in Heq.
  rewrite Heq.
  unfoldMC. unfold Plus_instance_IR, Mult_instance_IR, Zero_instance_IR,
    Negate_instance_IR.
  ring.
Qed.

Definition ConstTContR :=
  (ContConstFun (closel [0]) I).

Global Instance Proper_instance_ConstTContR :
  Proper (@st_eq IR ==> @st_eq TContR) ConstTContR.
Proof.
  intros ? ? Heq ?.
  simpl. assumption.
Qed.

Definition rotateOriginTowardsF
  (XTowards : Cart2D IR)
  (nz : 0 [<] normIR XTowards)
  (pt : Cart2D TContR) : Cart2D TContR :=
  let normInv := (normIRInv XTowards nz) in
  let Xf := ConstTContR (normInv × X XTowards) in
  let Yf := ConstTContR (normInv × Y XTowards) in
{|X:= (Xf × X pt + Yf × Y pt);
  Y:= (Xf × Y pt - Yf × X pt)|}.

Definition CartFunEta (ptf : Cart2D TContR) (t:Time) : Cart2D IR :=
{|X:= {X ptf} t ; Y:= {Y ptf} t|}.

Definition XYAbs (pt : Cart2D IR) : Cart2D IR :=
{| X:= AbsIR (X pt) ; Y:= AbsIR (Y pt)|}.

Lemma Cart2D_instance_le_IRtransitive :
  (a b c : Cart2D IR),
  a b
   b c
   a c.
Proof.
  intros ? ? ? H1 H2.
  destruct H1, H2.
  split; eapply leEq_transitive; eauto.
Qed.

Local Opaque AbsIR.
Global Instance :
  Proper (equiv ==> equiv ) XYAbs.
  intros a b Heq.
  split; simpl; rewrite Heq; auto.
Qed.

Global Instance ProperLeCartIR : Proper
 (equiv ==> equiv ==> iff)
(@le (Cart2D IR) _).
Proof.
  intros ? ? ? ? ? ?.
  unfold le, Cart2D_instance_le.
  rewrite H, H0.
  tauto.
Qed.

Lemma XYAbsLeAdd :
   a b c d,
    XYAbs a c
    → XYAbs b d
    → XYAbs (a+b) (c+d).
Proof.
  intros ? ? ? ? H1 H2.
  destruct H1 as [H1x H1y].
  destruct H2 as [H2x H2y].
  simpl in H1x, H1y, H2x, H2y.
  split; simpl;
  apply AbsIR_plus; assumption.
Qed.

Lemma sameXYAdd : (a b: IR),
  sameXY a + sameXY b = sameXY (a + b).
Proof.
  intros.
  split; simpl; reflexivity.
Qed.

Lemma QPQTQplusnNeg: sp qt,
   (0<=(Qplus (QposAsQ sp) (QT2Q qt)))%Q.
Proof.
  intros.
  destruct sp.
  destruct qt as [? y].
  simpl.
  apply QTimeD in y.
  lra.
Qed.

Lemma rotateOriginTowardsFAp :
  (XTowards : Cart2D IR)
  (nz : 0 [<] normIR XTowards)
  (pt : Cart2D TContR) (t : Time),
CartFunEta (rotateOriginTowardsF XTowards nz pt) t
= rotateOriginTowards XTowards nz (CartFunEta pt t).
Proof.
  intros ? ? ? ?.
  unfold CartFunEta, rotateOriginTowardsF.
  simpl. autorewrite with IContRApDown.
  unfold rotateOriginTowards.
  simpl. unfold equiv, EquivCart. simpl.
  unfoldMC. autounfold with IRMC.
  simpl. unfold getF. simpl.
  split; ring.
Qed.

Lemma DerivativerotateOriginTowards :
   (XTowards : Cart2D IR)
  (nz : 0 [<] normIR XTowards)
  (pt : Cart2D TContR) (Dx Dy : TContR),
  let normInv := (normIRInv XTowards nz) in
  let Xf := ConstTContR (normInv × X XTowards) in
  let Yf := ConstTContR (normInv × Y XTowards) in
  let ptR := rotateOriginTowardsF XTowards nz pt in
  isDerivativeOf Dx (X pt)
   isDerivativeOf Dy (Y pt)
   (isDerivativeOf (Xf×Dx + Yf×Dy) (X ptR)
      × isDerivativeOf (Xf×Dy - Yf×Dx) (Y ptR)).
Proof.
  intros ? ? ? ? ?.
  simpl. intros H1d H2d.
  split.
- apply TContRDerivativePlus;
    apply TContRDerivativeMultConstL; assumption.
- apply TContRDerivativePlus;[|apply TContRDerivativeOpp];
    apply TContRDerivativeMultConstL; assumption.
Qed.

Local Opaque Sin Cos.
Lemma CartToPolarToXIR : (q : Cart2D Q),
  let θq : IR := '(polarTheta q) in
  ' q = {| X := ('|q|) × Cos θq ; Y := ('|q|) × Sin θq |}.
Proof.
  intros ?.
  simpl.
  pose proof (Cart2Polar2CartID q) as Hid.
  unfold cast, castCart, Cast_instace_Q_IR, Cart_CR_IR.
  unfold cast, castCart, Cast_instace_Q_IR in Hid.
  unfold Polar2Cart, Cart2Polar in Hid.
  simpl in Hid.
  unfold equiv, EquivCart in Hid.
  unfold equiv, EquivCart.
  simpl in Hid. simpl.
  unfold cast.
  repnd.
  apply CRasIR_wd in Hidr.
  apply CRasIR_wd in Hidl.
  rewrite CR_mult_asIR in Hidl, Hidr.
  rewrite sin_correct_CR in Hidr.
  rewrite cos_correct_CR in Hidl.
  rewrite <- Hidl, <- Hidr.
  rewrite <- IR_inj_Q_as_CR, <- IR_inj_Q_as_CR.
  rewrite IRasCRasIR_id, IRasCRasIR_id.
  split; reflexivity.
Qed.

Lemma QNormSqrIR : (q : Cart2D Q),
  normIR ('q) = '|q|.
Proof.
  intros.
  unfold CanonicalNotations.norm, NormSpace_instance_Cart2D, sqrtFun,
    rational_sqrt_SqrtFun_instance.
  rewrite rational_sqrt_correct.
  unfold cast.
  rewrite IRasCRasIR_id.
  apply sqrt_wd.
  unfold castCart, normSqr.
Local Opaque inj_Q.
  simpl.
  unfoldMC.
  unfold Mult_instance_IR,Mult_instance_IR.
  autorewrite with InjQDown.
  reflexivity.
Grab Existential Variables.
  pose proof (cc_abs_aid _ (X q) (Y q)) as HH.
  simpl in HH.
  rewrite <- inj_Q_Zero.
  apply inj_Q_leEq.
  unfoldMC.
  simpl. simpl in HH.
  lra.
Qed.

Lemma RingLeftMult : `{Ring R} (c a b : R),
  a = b
  → c × a = c × b.
Proof.
  intros ? ? ? ? ? ? ? ? ? ? ? H.
  rewrite H.
  reflexivity.
Qed.

Lemma CartToPolarToXIR2 : (XTowards : Cart2D Q)
    (nz : 0 [<] normIR ('XTowards)),
  let normInv := (normIRInv ('XTowards) nz) in
  let Xf :IR := (normInv × '(X XTowards)) in
  let Yf :IR := (normInv × ' (Y XTowards)) in
  let θq : IR := '(polarTheta XTowards) in
  {|X:= Xf ; Y:=Yf|}
    = {| X := Cos θq ; Y := Sin θq |}.
Proof.
  intros q ?.
  simpl.
  pose proof (CartToPolarToXIR q) as Hid.
  unfold equiv, EquivCart. simpl.
  unfold equiv, EquivCart in Hid.
  simpl in Hid.
  rewrite <- QNormSqrIR in Hid.
  repnd.
  apply (RingLeftMult (normIRInv (' q) nz)) in Hidr.
  apply (RingLeftMult (normIRInv (' q) nz)) in Hidl.
  rewrite sr_mult_associative in Hidr.
  rewrite sr_mult_associative in Hidl.
  rewrite normIRInvSpecInvLeft in Hidl.
  rewrite normIRInvSpecInvLeft in Hidr.
  rewrite mult_1_l in Hidl.
  rewrite mult_1_l in Hidr.
  rewrite <- Hidl, <- Hidr.
  split; reflexivity.
Qed.

Add Ring TContRisaRing: (CRing_Ring TContR).

Lemma DerivativerotateOriginTowards2 :
   (XTowards : Cart2D Q)
  (nz : 0 [<] normIR (' XTowards))
  (pt : Cart2D TContR) (V θ : TContR),
  let θt : TContR := ConstTContR ('(polarTheta XTowards)) in
  let ptR := rotateOriginTowardsF (' XTowards) nz pt in
  isDerivativeOf (V × (CFCos θ)) (X pt)
   isDerivativeOf (V × (CFSine θ)) (Y pt)
   (isDerivativeOf (V × (CFCos (θ - θt))) (X ptR)
      × isDerivativeOf (V × (CFSine (θ - θt))) (Y ptR)).
Proof.
  intros ? ? ? ? ?.
  simpl. intros H1d H2d.
  pose proof (DerivativerotateOriginTowards _ nz pt _ _ H1d H2d) as Hd.
  clear H1d H2d.
  pose proof (CartToPolarToXIR2 _ nz) as Hn.
  simpl in Hn.
  unfold equiv, EquivCart in Hn.
  simpl in Hn.
  repnd. destruct Hd as [Hdl Hdr].
  eapply isIDerivativeOfWdl in Hdr;
  [| rewrite Hnl; rewrite Hnr;reflexivity].
  eapply isIDerivativeOfWdl in Hdl;
  [| rewrite Hnl; rewrite Hnr;reflexivity].
  unfold rotateOriginTowardsF in Hdl, Hdr.
  simpl in Hdl, Hdr.
  unfold isDerivativeOf. unfoldMC.
  unfold Mult_instance_TContR, Plus_instance_TContR, Negate_instance_TContR,
    Negate_instance_TContR,Negate_instance_TContR, Mult_instance_IR.
  split.
- eapply isIDerivativeOfWdl;[| apply Hdl].
  pose proof CFCos_minus as Hc.
  unfold cg_minus in Hc.
  rewrite Hc.

Local Opaque Sine Cos Cosine.
  rewrite CFCosConst, CFCosSine.
  fold ConstTContR.
  unfoldMC. unfold Plus_instance_TContR, Mult_instance_TContR.
  unfold cast.
  fold TContR.
  ring.

- clear Hdl. eapply isIDerivativeOfWdl;[| apply Hdr].
  pose proof CFSine_minus as Hc.
  unfold cg_minus in Hc.
  rewrite Hc. clear Hc.
  rewrite CFCosConst, CFCosSine.
  fold ConstTContR.
  unfoldMC. unfold Plus_instance_TContR, Mult_instance_TContR,
    Negate_instance_TContR.
  unfold cast.
  fold TContR.
  ring.
Qed.

Definition Cart2DIRRing :=
  (rings.stdlib_ring_theory (Cart2D IR)).