reintroduce a type for angle (wip)

extra_trigo.v

@@ -238,6 +238,294 @@ case: (cos (a / 2%:R) =P 0) => [->|/eqP saD0]; first by rewrite invr0 mulr0 !mul
 by rewrite expr2 -mulf_div divff // mul1r.
 Qed.
 
+End Extra.
+
+From mathcomp Require Import ssrint complex sequences exp.
+Local Open Scope complex_scope.
+
+Section Rmod.
+Local Open Scope real_scope.
+Variable R : realType.
+Implicit Types x y : R.
+
+Definition Rmod x y := x - y * Rfloor (x / y).
+
+Local Notation "m %% d" := (Rmod m d).
+Local Notation "m = n %[mod d ]" := (m %% d = n %% d).
+
+Lemma Rmodx0 x : x %% 0 = x.
+Proof. by rewrite /Rmod mul0r subr0. Qed.
+
+End Rmod.
+Notation "m %% d" := (Rmod m d) : real_scope.
+Notation "m = n %[mod d ]" := (m %% d = n %% d) : real_scope.
+
+Section backport_complex.
+Variable R : realType.
+
+Lemma eq0c (x : R) : (x%:C == 0) = (x == 0).
+Proof. by rewrite eq_complex eqxx/= andbT. Qed.
+
+Lemma real_complexN (r : R) : (- r)%:C = - r%:C.
+Proof. by apply/eqP; rewrite eq_complex/= oppr0 !eqxx. Qed.
+
+Lemma real_complexM (r s : R) : (r * s)%:C = r%:C * s%:C.
+Proof. by apply/eqP; rewrite eq_complex/= 2!mulr0 mul0r subr0 addr0 !eqxx. Qed.
+
+Lemma scalec r s : (r * s)*i = r%:C * s*i :> R[i].
+Proof. by apply/eqP; rewrite eq_complex/= mulr0 !mul0r subr0 addr0 !eqxx. Qed.
+
+End backport_complex.
+
+Section backport_trigo.
+Variable R : realType.
+
+Lemma sin_nat_pi (n : nat) : sin (n%:R * pi) = 0 :> R.
+Proof.
+elim: n => [|n ih]; first by rewrite mul0r sin0.
+by rewrite -addn1 natrD mulrDl mul1r sinD ih sinpi mul0r mulr0 add0r.
+Qed.
+
+Lemma sin_int_pi (k : int) : sin (k%:~R * pi) = 0 :> R.
+Proof.
+wlog k0 : k / 0 <= k.
+  move=> h; have [k0|k0] := leP 0 k; first by rewrite h.
+  by rewrite -(opprK (_ * _)) sinN -mulNr -mulrNz h ?oppr0// ler_oppr oppr0 ltW.
+by rewrite -[in LHS](gez0_abs k0) sin_nat_pi.
+Qed.
+
+Lemma sin_eq0 (r : R) : sin r = 0 <-> exists k, r = k%:~R * pi.
+Proof.
+split; last by move=> [k ->]; rewrite sin_int_pi.
+wlog rpi : r / - pi < r <= pi.
+  move=> h1 sr0; wlog r0 : r sr0 / 0 <= r.
+    move=> h2; have [|r0] := leP 0 r; first exact: h2.
+    have := h2 (- r); rewrite sinN sr0 oppr0 => /(_ erefl); rewrite ler_oppr.
+    rewrite oppr0 => /(_ (ltW r0))[k rkpi]; exists (- k); rewrite mulrNz mulNr.
+    by rewrite -rkpi opprK.
+  have [rpi|pir] := leP r pi.
+    by apply: h1 => //; rewrite rpi (lt_le_trans _ r0)// ltr_oppl oppr0 pi_gt0.
+  have /h1 : - pi < r - (floor (r / pi))%:~R * pi <= pi.
+    apply/andP; split.
+      rewrite ltr_subr_addr addrC -[X in _ - X]mul1r -mulrBl.
+      rewrite -ltr_pdivl_mulr ?pi_gt0// ltr_subl_addr -RfloorE.
+      by rewrite (le_lt_trans (Rfloor_le _))// ltr_addl ltr01.
+    rewrite ler_subl_addr -[X in X + _]mul1r -mulrDl.
+    by rewrite -ler_pdivr_mulr ?pi_gt0// addrC -RfloorE ltW // lt_succ_Rfloor.
+  rewrite sinB sin_int_pi mulr0 subr0 sr0 mul0r => /(_ erefl)[k /eqP].
+  by rewrite subr_eq -mulrDl -intrD => /eqP rkpi; eexists; exact: rkpi.
+by move=> /eqP; rewrite sin_eq0_Npipi// => /orP[|] /eqP ->;
+  [exists 0; rewrite mul0r|exists 1; rewrite mul1r].
+Qed.
+
+Lemma cos_pi_mulrn n : cos (pi *+ n) = (- 1) ^+ odd n :> R.
+Proof.
+elim: n => [|n ih]; first by rewrite mulr0n/= cos0 expr0.
+by rewrite mulrS cosD cospi sinpi mul0r subr0 {}ih/= signrN mulN1r.
+Qed.
+
+Lemma cos_pi_mulrz (k : int)  : cos (pi *~ k) = (- 1) ^+ odd `|k|%N :> R.
+Proof.
+have [|k0] := leP 0 k.
+  by case: k => // k _; rewrite -pmulrn cos_pi_mulrn.
+by rewrite -cosN -mulrNz -ltz0_abs // -pmulrn cos_pi_mulrn.
+Qed.
+
+Lemma expR_eq0 (x : R) : expR x = 1 -> x = 0.
+Proof.
+move/eqP; rewrite eq_le => /andP[eone onee]; apply/eqP; rewrite eq_le.
+apply/andP; split.
+  by move: eone; rewrite -ler_ln ?posrE ?ltr01 ?expR_gt0// ln1 expK.
+by move: onee; rewrite -ler_ln ?posrE ?ltr01 ?expR_gt0// ln1 expK.
+Qed.
+
+End backport_trigo.
+
+Section exp.
+Variable R : realType.
+
+Definition exp (z : R[i]) := (expR (Re z))%:C * (cos (Im z) +i* sin (Im z)).
+
+Lemma exp_neq0 (z : R[i]) : exp z != 0.
+Proof.
+apply: mulf_neq0; first by rewrite eq0c gt_eqF// expR_gt0.
+rewrite eq_complex/= -norm_sin_eq1; apply/negP => /andP[]/[swap]/eqP ->.
+by rewrite normr0 eq_sym oner_eq0.
+Qed.
+
+Lemma exp_pi : exp (pi *i) = - 1.
+Proof.
+by rewrite /exp/= expR0 sinpi cospi/= mul1r complexr0 real_complexN.
+Qed.
+
+Lemma exp0 : exp 0 = 1.
+Proof. by rewrite /exp/= cos0 sin0 expR0 mul1r. Qed.
+
+Lemma exp_pihalf : exp ((pi / 2%:R) *i) = 'i.
+Proof. by rewrite /exp/= sin_pihalf cos_pihalf expR0 mul1r. Qed.
+
+Lemma expD (z w : R[i]) : exp (z + w) = exp z * exp w.
+Proof.
+move: z w => [x1 y1] [x2 y2]; rewrite /exp /=.
+rewrite mulrCA !mulrA -real_complexM -expRD (addrC x2) -mulrA; congr (_ * _).
+by rewrite cosD sinD/=; apply/eqP; rewrite eq_complex/= eqxx/= addrC.
+Qed.
+
+Lemma norm_exp (z : R[i]) : `| exp z | = (expR (Re z))%:C.
+Proof.
+move: z => [x y]/=; rewrite normc_def/= 2!mul0r subr0 addr0.
+do 2 (rewrite exprMn_comm//; last exact: mulrC).
+by rewrite -mulrDr cos2Dsin2 mulr1 sqrtr_sqr gtr0_norm// expR_gt0.
+Qed.
+
+Lemma exp_eq1 (z : R[i]) : exp z = 1 <-> exists k, z = 2%:R * k%:~R * pi *i.
+Proof.
+split.
+  move: z => [x y] /eqP; rewrite eq_complex/= 2!mul0r addr0 subr0 => /andP[].
+  move=> /[swap]; rewrite mulf_eq0 gt_eqF/= ?expR_gt0// => /eqP/sin_eq0[k yk] h.
+  have cs0 : 0 < cos y.
+    by move: (@ltr01 R); rewrite -(eqP h); rewrite pmulr_rgt0 // expR_gt0.
+  have ok : ~~ odd `|k|%N.
+    apply/negP => ok; move: cs0.
+    by rewrite yk mulrzl cos_pi_mulrz ok/= expr1 ltr0N1.
+  move: h; rewrite yk mulrzl cos_pi_mulrz (negbTE ok) expr0 mulr1 => /eqP.
+  move/expR_eq0 => ->{x}.
+  rewrite (intEsg k); exists (sgz k * `|k|./2%N).
+  rewrite (_ : _ * _%:~R = k%:~R); last first.
+    rewrite intrM mulrCA -natrM mul2n.
+    move: (odd_double_half `|k|); rewrite (negbTE ok) add0n => ->.
+    by rewrite [in RHS](intEsg k) intrM.
+  rewrite -mulrzl -intEsg.
+  (* NB: should be easy *)
+  admit.
+move=> [k ->].
+rewrite /exp/=.
+(* NB: should be easy *)
+Admitted.
+
+End exp.
+
+Module Angle.
+Section angle.
+Record t (R : realType) := mk {
+  a : R ;
+  _ : - pi < a <= pi }.
+End angle.
+Module Exports.
+Section exports.
+Variable R : realType.
+Local Notation angle := (@t R).
+Canonical angle_subType := [subType for @a R].
+Coercion a : angle >-> Real.sort.
+End exports.
+End Exports.
+End Angle.
+Export Angle.Exports.
+
+Notation angle := Angle.t.
+
+Section angle_canonicals.
+Local Open Scope real_scope.
+Variable R : realType.
+
+Lemma angle0_subproof : - pi < (0 : R) <= pi.
+Proof. by rewrite pi_ge0 andbT oppr_lt0 pi_gt0. Qed.
+
+Definition angle0 := Angle.mk angle0_subproof.
+
+Lemma angleNpi (a : angle R) : - pi < (a : R).
+Proof. by case: a => ? /= /andP[]. Qed.
+
+Lemma angle_pi (a : angle R) : (a : R) <= pi.
+Proof. by case: a => ? /= /andP[]. Qed.
+
+Let add (a b : angle R) : R :=
+  let c := (a : R) + (b : R) in
+  if pi < c then c - 2%:R * pi else
+  if c <= - pi then c + 2%:R * pi else c.
+
+Let two_mone (x : R) : 2%:R * x - x = x.
+Proof.
+rewrite -{2}(mul1r x) -mulrBl.
+by rewrite {2}(_ : 1 = 1%:R)// -natrB// mul1r.
+Qed.
+
+Let add_pi (a b : angle R) : - pi < add a b <= pi.
+Proof.
+apply/andP; split; rewrite /add.
+  case: ifPn => [piab|].
+    by rewrite ltr_subr_addl two_mone.
+  rewrite -leNgt => abpi; case: ifPn => [abNpi|]; last by rewrite -ltNge.
+  rewrite -ltr_subl_addr (@lt_trans _ _ (- pi - pi))//.
+    by rewrite ler_lt_sub// ltr_pmull// ?ltr1n// pi_gt0.
+  by rewrite ltr_add// ?(angleNpi _).
+case: ifPn => [piab|].
+  rewrite ler_subl_addl (@le_trans _ _ (pi + pi))// ler_add// ?(angle_pi _)//.
+  by rewrite ler_pmull ?pi_gt0// ler1n.
+rewrite -leNgt => abpi; case: ifPn => [abNpi|//].
+rewrite -ler_subr_addr (le_trans abNpi)// ler_subr_addl.
+by rewrite two_mone.
+Qed.
+
+Definition add_angle (a b : angle R) : angle R := Angle.mk (add_pi a b).
+
+Let opp (a : angle R) : R := if a == pi :> R then pi else - (a : R).
+
+Let opp_pi (a : angle R) : - pi < opp a <= pi.
+Proof.
+apply/andP; split; rewrite /opp.
+  case: ifPn => [_|api].
+    by rewrite (@lt_trans _ _ 0) ?pi_gt0// ltr_oppl oppr0 pi_gt0.
+  by rewrite ltr_oppl opprK lt_neqAle api (angle_pi a).
+case: ifPn => // api.
+by rewrite ler_oppl (le_trans (ltW (angleNpi a))).
+Qed.
+
+Definition opp_angle (a : angle R) : angle R := Angle.mk (opp_pi a).
+
+Lemma add_angleC : commutative add_angle.
+Proof.
+by move=> a b; apply/val_inj => /=; rewrite /add addrC.
+Qed.
+
+Lemma add_0angle x : add_angle angle0 x = x.
+Proof.
+apply/val_inj => /=; rewrite /add/= add0r.
+case: ifPn => [pix|_].
+  by have := angle_pi x; rewrite leNgt pix.
+case: ifPn => // xpi.
+by have := angleNpi x; rewrite ltNge xpi.
+Qed.
+
+Lemma add_Nangle x : add_angle (opp_angle x) x = angle0.
+Proof.
+apply/val_inj => /=; rewrite /add/= /opp/=.
+have [->|xpi] := eqVneq (x : R) pi.
+  by rewrite ltr_addl pi_gt0 -mulr2n mulr_natl subrr.
+by rewrite addrC subrr ltNge pi_ge0/= ler_oppr oppr0 leNgt pi_gt0//.
+Qed.
+
+Lemma add_angleA : associative add_angle.
+Proof.
+move=> a b c; apply/val_inj => /=; rewrite /add/= /add/=.
+Admitted.
+
+Definition angle_eqMixin := [eqMixin of angle R by <:].
+Canonical angle_eqType := EqType (angle R) angle_eqMixin.
+Definition angle_choiceMixin := [choiceMixin of angle R by <:].
+Canonical angle_choiceType := ChoiceType (angle R) angle_choiceMixin.
+Definition angle_ZmodMixin := ZmodMixin add_angleA add_angleC add_0angle
+ add_Nangle.
+Canonical angle_ZmodType := ZmodType (angle R) angle_ZmodMixin.
+
+End angle_canonicals.
+
+Section Extra2.
+
+Variable R : realType.
+
+Implicit Types a : R.
+
 Definition norm_angle a :=
   if sin a < 0 then - acos (cos a) else acos (cos a).
 
@@ -614,4 +902,4 @@ Definition sec a := (cos a)^-1.
 Lemma secpi : sec pi = -1.
 Proof. by rewrite /sec cospi invrN invr1. Qed.
 
-End Extra.
+End Extra2.

rot.v

@@ -85,7 +85,7 @@ Local Open Scope ring_scope.
 Section two_dimensional_rotation.
 
 Variable T : realType.
-Implicit Types (a b : T) (M : 'M[T]_2).
+Implicit Types (a b : angle T) (M : 'M[T]_2).
 
 Definition RO a := col_mx2 (row2 (cos a) (sin a)) (row2 (- sin a) (cos a)).