-
Notifications
You must be signed in to change notification settings - Fork 2
/
angle.v
1240 lines (1030 loc) · 44.6 KB
/
angle.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(* coq-robot (c) 2017 AIST and INRIA. License: LGPL-2.1-or-later. *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrint.
From mathcomp Require Import ssrnum rat poly closed_field polyrcf matrix.
From mathcomp Require Import mxalgebra tuple mxpoly zmodp binomial realalg.
From mathcomp Require Import complex finset fingroup perm.
Require Import ssr_ext.
(******************************************************************************)
(* Angles *)
(* *)
(* NB(2022-02-15): The development in this directory now uses trigonometric *)
(* from mathcomp-analysis instead of the notation of angle provided by this *)
(* file. *)
(* *)
(* This files provides a theory of angles defined using complex numbers and *)
(* develops the theory of trigonometric functions including trigonometric *)
(* laws such as the cancellation laws between trigonometric functions and *)
(* their inverse, Pythagorean identity, double-angle and half-angle formulas, *)
(* law of cosines and of sines, etc. *)
(* *)
(* angle T == type of angles over the rcfType T, i.e., a complex number *)
(* whose modulus is 1 *)
(* angle0 == 0 angle corresponding to the complex number 1 *)
(* arg x == angle corresponding to the complex number x/|x| *)
(* pi == the angle corresponding to the complete number -1 *)
(* *)
(* Angles form a ZmodType, so that we can do scalar multiplication of angles: *)
(* half_angle a == the angle corresponding to a/2 *)
(* pihalf == pi/2 *)
(* piquarter == pi/4 *)
(* *)
(* Trigonometric functions: *)
(* cos a == the real part of the angle a *)
(* sin a == the imaginary part of angle a *)
(* tan a == tangent a *)
(* acos x == arccosine, the inverse trigonometric function of cosine *)
(* asin x == arcsin x *)
(* atan x == arctan x *)
(* atan2 x y == the 2-argument arctangent, i.e., the angle between the *)
(* positive x axis and the ray to the point (x, y) *)
(* cot a == cotangent a *)
(* *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Section nthroot.
(* TODO: remove? *)
Lemma rootCD (C : numClosedFieldType) (m n : nat) (x : C) :
(m * n).-root (x) = m.-root (n.-root x).
Proof.
have [->|m_gt0] := posnP m; first by rewrite mul0n !root0C.
have [->|n_gt0] := posnP n; first by rewrite muln0 root0C rootC0.
have mn_gt0: (m * n > 0)%N by rewrite ?muln_gt0 ?m_gt0.
wlog x_gt0 : x / x >= 0 => [hwlog_x_ge0|]; last first.
apply: (@pexpIrn _ (m * n)) => //; rewrite ?nnegrE//= ?rootC_ge0 //.
by rewrite rootCK // exprM !rootCK.
wlog nx_eq1 : x / `|x| = 1 => [hwlog_nx_eq1|].
have [->|x_neq0] := eqVneq x 0; first by rewrite !rootC0.
rewrite -[x](@mulfVK _ `|x|) ?normr_eq0 // rootCMr //.
rewrite hwlog_nx_eq1 ?normrM ?normfV ?normr_id ?divff ?normr_eq0 //.
by rewrite hwlog_x_ge0 //; do !rewrite -rootCMr ?rootC_ge0 //.
have [|m_gt1] := leqP m 1%N.
by case: m m_gt0 mn_gt0 hwlog_x_ge0 => [|[|m]] // _ _;
rewrite mul1n root1C.
have [|n_gt1] := leqP n 1%N.
by case: n n_gt0 mn_gt0 hwlog_x_ge0 => [|[|n]] // _ _;
rewrite muln1 root1C.
have mDn_gt1: (m * n > 1)%N.
by rewrite -subn_eq0; move: m n {n_gt0 m_gt0} n_gt1 m_gt1
mn_gt0 hwlog_x_ge0=> [|[|m]] [|[|n]].
apply: eqC_semipolar => //; first 2 last.
- by rewrite mulr_ge0 ?Im_rootC_ge0.
- by rewrite !norm_rootC hwlog_x_ge0.
apply/eqP; rewrite eq_le !rootC_Re_max ?exprM ?rootCK ?Im_rootC_ge0 //.
apply: eqC_semipolar; first 2 last.
- rewrite mulr_ge0 ?Im_rootC_ge0 //. admit.
- by rewrite normrX !norm_rootC hwlog_x_ge0 // rootCK.
apply/eqP; rewrite eq_le rootC_Re_max -?exprM ?rootCK //=; last first.
admit.
admit.
Abort.
End nthroot.
Section angle_def.
Variable T : rcfType.
Record angle := Angle {
expi :> T[i];
_ : `| expi | == 1 }.
Fact angle0_subproof : `| 1 / `| 1 | | == 1 :> T[i].
Proof. by rewrite normr1 divr1 normr1. Qed.
Definition angle0 := Angle angle0_subproof.
HB.instance Definition _ := [isSub for expi].
Lemma normr_expi a : `|expi a| = 1.
Proof. by case: a => x /= /eqP. Qed.
Lemma expi_eq0 a : (expi a == 0) = false.
Proof. case: a => /= a /eqP Ha; apply/negbTE; by rewrite -normr_gt0 Ha. Qed.
Lemma expi_inj : injective expi.
Proof. move=> [a a1] [b b1] /= ab; by apply/val_inj. Qed.
Lemma expi_is_unit a : expi a \is a GRing.unit.
Proof. by rewrite unitfE -normr_eq0 normr_expi oner_eq0. Qed.
Definition arg (x : T[i]) : angle :=
insubd angle0 (x / `| x |).
Lemma argZ x (k : T) : 0 < k -> arg (k %:C%C * x) = arg x.
Proof.
move=> k0; rewrite /arg; congr (insubd _ _).
rewrite normrM gtr0_norm; last by rewrite ltcR.
rewrite -mulf_div divff ?mul1r //.
by rewrite lt0r_neq0 // ltcR.
Qed.
Lemma argZ_neg x (k : T) : k < 0 -> arg (k %:C%C * x) = arg (- x).
Proof.
move=> k0; rewrite /arg; congr (insubd _ _).
rewrite normrM ltr0_norm; last by rewrite ltcR.
rewrite -mulf_div invrN mulrN divff ?mul1r; last by rewrite ltr0_neq0 // ltcR.
by rewrite mulNr mul1r normrN mulNr.
Qed.
Lemma expiK : cancel expi arg.
Proof.
move=> a; apply/val_inj=> /=.
by rewrite insubdK ?normr_expi ?divr1 // -topredE /= normr_expi.
Qed.
Lemma expi_arg x : x != 0 -> expi (arg x) = x / `|x|.
Proof.
move=> Nx_neq0; rewrite insubdK //.
by rewrite -topredE /= normrM normfV normr_id divff // normr_eq0.
Qed.
Lemma expi_conjc (a : T[i]) : a != 0 -> (expi (arg a))^-1 = expi (arg a^*).
Proof.
case: a => a b a0 /=; rewrite expi_arg // expi_arg //; last first.
apply: contra a0 => a0; by rewrite -conjc_eq0.
rewrite invc_norm (_ : `| _ | = 1); last first.
by rewrite normrM normrV ?unitfE ?normr_eq0 // normr_id divrr // unitfE normr_eq0.
rewrite exprnN exp1rz mul1r. simpc. by rewrite /= sqrrN.
Qed.
Lemma mul_norm_arg x : x = `|x| * expi (arg x).
Proof.
have [x0|x_neq0] := boolP (x == 0); first by rewrite (eqP x0) normr0 mul0r.
by rewrite expi_arg // mulrC mulfVK // normr_eq0.
Qed.
Lemma argK x : `|x| = 1 -> expi (arg x) = x.
Proof. by move=> Nx1; rewrite expi_arg ?Nx1 ?divr1 // -normr_gt0 Nx1. Qed.
Lemma arg_Re k : 0 < k -> arg k%:C%C = arg 1.
Proof. by move=> k_gt0; rewrite -[(k%:C)%C]mulr1 argZ. Qed.
Lemma arg_Re_neg k : k < 0 -> arg k%:C%C = arg (- 1).
Proof. by move=> k_gt0; rewrite -[(k%:C)%C]mulr1 argZ_neg. Qed.
Definition add_angle a b := arg (expi a * expi b).
Definition opp_angle a := arg (expi a)^-1.
Lemma add_angleA : associative add_angle.
Proof.
by move=> ???; rewrite /add_angle argK ?mulrA ?argK // ?normrM 2!normr_expi mulr1.
Qed.
Lemma add_angleC : commutative add_angle.
Proof. move=> a b; by rewrite /add_angle mulrC. Qed.
Lemma add_0angle x : add_angle (arg 1) x = x.
Proof. by rewrite /add_angle argK ?normr1 ?mul1r ?expiK. Qed.
Lemma add_Nangle x : add_angle (opp_angle x) x = arg 1.
Proof.
rewrite /add_angle /opp_angle argK; first by rewrite mulVr // expi_is_unit.
by rewrite normrV ?expi_is_unit // normr_expi invr1.
Qed.
HB.instance Definition _ := [Equality of angle by <:].
HB.instance Definition _ := [Choice of angle by <:].
HB.instance Definition _ :=
@GRing.isZmodule.Build angle _ opp_angle add_angle add_angleA add_angleC add_0angle add_Nangle.
Lemma arg1 : arg 1 = 0.
Proof. apply val_inj => /=; by rewrite argK // normr1. Qed.
Lemma expiD a b : expi (a + b) = expi a * expi b.
Proof.
move: a b => [a a1] [b b1] /=.
by rewrite /add_angle /= argK // normrM (eqP a1) (eqP b1) mulr1.
Qed.
Definition pi := arg (-1).
Lemma expipi : expi pi = -1. Proof. by rewrite argK ?normrN1. Qed.
Lemma argN1 : arg (- 1) = pi.
Proof. apply val_inj => /=; by rewrite argK // ?normrN1. Qed.
Lemma expi2pi : expi (pi + pi) = 1.
Proof. by rewrite /pi expiD argK // ?normrN1 // mulrNN mulr1. Qed.
Lemma pi2 : pi *+ 2 = 0.
Proof. apply expi_inj => //; by rewrite expi2pi -arg1 argK // normr1. Qed.
End angle_def.
Arguments expi {T} _.
Arguments angle0 {T}.
Arguments pi {T}.
Section angle_basic_prop.
Variable T : rcfType.
Implicit Types a b : angle T.
Lemma add_angleE a b : a + b = add_angle a b.
Proof. done. Qed.
Lemma opp_angleE a : - a = opp_angle a.
Proof. done. Qed.
Lemma argc (z : T[i]) : z != 0 -> arg z^* = - arg z.
Proof.
case: z => a b z0 /=; by rewrite {2}/arg opp_angleE /opp_angle expi_conjc //= expiK.
Qed.
Definition cos a := complex.Re (expi a).
Lemma cos0 : cos 0 = 1.
Proof. by rewrite /cos -arg1 argK // ger0_norm // ler01. Qed.
Lemma cospi : cos pi = -1.
Proof. by rewrite /cos /pi argK //= normrN normr1. Qed.
Lemma cos_max a : `| cos a | <= 1.
Proof.
rewrite -lecR (le_trans (normc_ge_Re _)) //; by case: a => ? /= /eqP ->.
Qed.
Lemma cosN a : cos (- a) = cos a.
Proof.
case: a => -[a b] ab; rewrite opp_angleE /cos /opp_angle /=.
rewrite invc_norm (eqP ab) expr1n invr1 mul1r expi_arg; last first.
by rewrite conjc_eq0 -normr_eq0 (eqP ab) oner_eq0.
by rewrite normcJ (eqP ab) divr1.
Qed.
Definition sin a := complex.Im (expi a).
Lemma sin0 : sin 0 = 0.
Proof. by rewrite /sin -arg1 argK // normr1. Qed.
Lemma sinpi : sin pi = 0.
Proof. by rewrite /sin /pi argK /= ?oppr0 // normrN normr1. Qed.
Lemma sinN a : sin (- a) = - sin a.
Proof.
case: a => -[a b] ab; rewrite opp_angleE /sin /opp_angle /=.
rewrite invc_norm (eqP ab) expr1n invr1 mul1r expi_arg; last first.
by rewrite conjc_eq0 -normr_eq0 (eqP ab) oner_eq0.
by rewrite normcJ (eqP ab) divr1.
Qed.
Lemma eq_angle a b : (a == b) = ((cos a == cos b) && (sin a == sin b)).
Proof.
case: a b => [[a b] ab] [[c d] cd].
rewrite /cos /= /sin /=.
apply/idP/idP; first by case/eqP => -> ->; rewrite 2!eqxx.
case/andP => /eqP ac /eqP bd.
apply/eqP/val_inj => /=; by rewrite ac bd.
Qed.
Lemma sqrD1_cossin (x y : T) :
x ^+ 2 + y ^+ 2 = 1 -> {a | x = cos a /\ y = sin a}.
Proof.
move=> v1.
have {}v1 : (`| x +i* y | = 1)%C by rewrite normc_def /= v1 sqrtr1.
exists (arg (x +i* y)%C).
rewrite /cos /sin expi_arg //; last by rewrite -normr_eq0 v1 oner_neq0.
by rewrite v1 divr1.
Qed.
(* relation expi<->cos/sin *)
Lemma expi_cos_sin a : expi a = (cos a +i* sin a)%C.
Proof. by case: a => -[a0 a1] Ha; rewrite /cos /sin. Qed.
Lemma expi0 : expi 0 = 1 :> T[i].
Proof. by rewrite expi_cos_sin cos0 sin0. Qed.
Lemma expi_expr k a : expi a ^+ k = expi (a *+ k).
Proof.
elim: k => [|k ih]; by
[rewrite expr0 mulr0n expi0 | rewrite exprS ih mulrS expiD].
Qed.
Lemma moivre n a : ((cos a +i* sin a) ^+n = cos (a *+ n) +i* sin (a *+ n))%C.
Proof.
rewrite -!expi_cos_sin.
elim: n => [|n ih]; by [rewrite expr0 mulr0n expi0 | rewrite expi_expr].
Qed.
Lemma pi_neq0 : pi != 0 :> angle T.
Proof.
apply/eqP => /(congr1 expi).
rewrite argK ?expi0; last by rewrite normrN normr1.
by move/eqP; rewrite eq_sym -subr_eq0 opprK (_ : 1 + 1 = 2%:R) // pnatr_eq0.
Qed.
Lemma expii : expi (arg 'i) = 'i :> T[i].
Proof. by rewrite argK // normc_def /= expr0n expr1n add0r sqrtr1. Qed.
Lemma expiNi : expi (- arg 'i) = -'i :> T[i].
Proof.
rewrite expi_cos_sin sinN cosN /cos /sin expi_arg; last first.
by rewrite -normr_eq0 normci oner_neq0.
rewrite normci divr1 /=; apply/eqP; by rewrite eq_complex /= oppr0 2!eqxx.
Qed.
Lemma expiNpi : expi (- pi) = - 1 :> T[i].
Proof.
rewrite /pi.
rewrite expi_cos_sin cosN sinN cospi sinpi.
by apply/eqP; rewrite eq_complex /= !eqxx.
Qed.
Lemma piNpi : pi = - pi :> angle T.
Proof. by apply expi_inj; rewrite expiNpi expipi. Qed.
Lemma arg0_inv (x : T[i]) y : y != 0 -> `|x| = y -> arg x = 0 -> x = y.
Proof.
move=> y0; case: x => x1 x2 norma H.
rewrite -(mulr1 y) -expi0 -H expi_arg; last by rewrite -normr_eq0 norma.
by rewrite norma mulrCA divrr // mulr1.
Qed.
Lemma argpi_inv (x : T[i]) y : y != 0 -> `|x| = y -> arg x = pi -> x = - y.
Proof.
move=> y0; case: x => x1 x2 norma H.
rewrite -(mulrN1 y) -expipi -H expi_arg; last by rewrite -normr_eq0 norma.
by rewrite norma mulrCA divrr // mulr1.
Qed.
(* standard trigonometric relations *)
Lemma cos2Dsin2 a : (cos a) ^+ 2 + (sin a) ^+ 2 = 1.
Proof.
move: (add_Re2_Im2 (expi a)).
by rewrite normr_expi expr1n => /(congr1 (@complex.Re T)) => /= <-.
Qed.
Lemma sin2cos2 a : sin a ^+ 2 = 1 - cos a ^+ 2.
Proof. move/eqP: (cos2Dsin2 a); by rewrite eq_sym addrC -subr_eq => /eqP. Qed.
Lemma cos2sin2 a : cos a ^+ 2 = 1 - sin a ^+ 2.
Proof. move/eqP: (cos2Dsin2 a); by rewrite eq_sym -subr_eq => /eqP. Qed.
Lemma sinD a b : sin (a + b) = sin a * cos b + cos a * sin b.
Proof. by rewrite {1}/sin expiD 2!expi_cos_sin /= addrC. Qed.
Lemma sinDpi a : sin (a + pi) = - sin a.
Proof. by rewrite sinD ?(cosN, sinN) cospi mulrN1 sinpi ?oppr0 mulr0 addr0. Qed.
Lemma sin_mulr2n a : sin (a *+ 2) = (cos a * sin a) *+ 2.
Proof. by rewrite mulr2n sinD mulrC -mulr2n. Qed.
Lemma cosD a b : cos (a + b) = cos a * cos b - sin a * sin b.
Proof. by rewrite {1}/cos expiD 2!expi_cos_sin /= addrC. Qed.
Lemma cosDpi a : cos (a + pi) = - cos a.
Proof. by rewrite cosD ?(cosN, sinN) cospi mulrN1 sinpi ?oppr0 mulr0 subr0. Qed.
Lemma cosB a b : cos (a - b) = cos a * cos b + sin a * sin b.
Proof. by rewrite cosD cosN sinN mulrN opprK. Qed.
Lemma sinB a b : sin (a - b) = sin a * cos b - cos a * sin b.
Proof. by rewrite sinD cosN sinN mulrN. Qed.
Lemma abs_sin a : `| sin a | = Num.sqrt (1 - cos a ^+ 2).
Proof.
apply/eqP; rewrite -(@eqr_expn2 _ 2) //; last by rewrite sqrtr_ge0.
rewrite -normrX ger0_norm; last by rewrite sqr_ge0.
rewrite sqr_sqrtr; last first.
by rewrite lter_sub_addr add0r -sqr_normr exprn_ilte1 // cos_max.
by rewrite -subr_eq opprK addrC cos2Dsin2.
Qed.
(* valeurs remarquables de cos/sin *)
Lemma norm_cos_eq1 a : (`|cos a| == 1) = (sin a == 0).
Proof.
by rewrite -sqrf_eq0 -sqrp_eq1 // sqr_normr sin2cos2 subr_eq0 eq_sym.
Qed.
Lemma norm_sin_eq1 a : (`|sin a| == 1) = (cos a == 0).
Proof.
by rewrite -sqrf_eq0 -sqrp_eq1 // sqr_normr cos2sin2 subr_eq0 eq_sym.
Qed.
Lemma cos1sin0 a : `|cos a| = 1 -> sin a = 0.
Proof. by move/eqP; rewrite norm_cos_eq1 => /eqP. Qed.
Lemma sin1cos0 a : `|sin a| = 1 -> cos a = 0.
Proof. by move/eqP; rewrite norm_sin_eq1 => /eqP. Qed.
Lemma sin0cos1 a : sin a = 0 -> `|cos a| = 1.
Proof. by move/eqP; rewrite -norm_cos_eq1 => /eqP. Qed.
Lemma cos0sin1 a : cos a = 0 -> `|sin a| = 1.
Proof. by move/eqP; rewrite -norm_sin_eq1 => /eqP. Qed.
Lemma cos_eq1 a : (cos a == 1) = (a == 0).
Proof.
apply/eqP/eqP=> [cosa|->]; last by rewrite cos0.
by rewrite -[a]expiK expi_cos_sin cosa cos1sin0 ?arg1 ?cosa ?normr1.
Qed.
Lemma cos1_angle0 a : cos a = 1 -> a = 0.
Proof. by move/eqP; rewrite cos_eq1 => /eqP. Qed.
Lemma cos_eqN1 a : (cos a == -1) = (a == pi).
Proof.
apply/eqP/eqP=> [cosa|->]; last by rewrite cospi.
rewrite -[a]expiK expi_cos_sin cosa cos1sin0 ?complexr0 ?rmorphN ?argN1 //.
by rewrite cosa normrN1.
Qed.
Lemma cosN1_angle0 a : cos a = -1 -> a = pi.
Proof. by move/eqP; rewrite cos_eqN1 => /eqP. Qed.
Lemma sin_eq0 a : (sin a == 0) = (a == 0) || (a == pi).
Proof. by rewrite -sqrf_eq0 sin2cos2 subr_eq0 eq_sym sqrf_eq1 cos_eq1 cos_eqN1. Qed.
Lemma sin0_inv a : sin a = 0 -> {a = 0} + { a = pi }.
Proof. by move/eqP; rewrite sin_eq0; case: eqP => /= ?/eqP?; [left|right]. Qed.
Definition tan a := sin a / cos a.
Lemma tan0 : tan 0 = 0 :> T.
Proof. by rewrite /tan sin0 cos0 mul0r. Qed.
Lemma tanpi : tan pi = 0.
Proof. by rewrite /tan sinpi mul0r. Qed.
Lemma tanN x : tan (- x) = - tan x :> T.
Proof. by rewrite /tan sinN cosN mulNr. Qed.
Lemma cos2_tan2 x : cos x != 0 -> 1 / (cos x) ^+ 2 = 1 + (tan x) ^+ 2.
Proof.
move=> cosx; rewrite /tan exprMn sin2cos2 mulrBl -exprMn divrr ?unitfE //.
by rewrite expr1n addrCA subrr addr0 div1r mul1r exprVn.
Qed.
Definition pihalf : angle T := arg 'i.
Lemma expi_pihalf : expi pihalf = 'i.
Proof. by rewrite /pihalf argK // normc_def /= expr0n expr1n add0r sqrtr1. Qed.
Lemma expi_Npihalf : expi (- pihalf) = - 'i.
Proof. by rewrite /pihalf expiNi. Qed.
Lemma sin_pihalf : sin pihalf = 1.
Proof.
have i1 : `|'i| = 1 :> T[i] by rewrite normc_def /= expr0n add0r expr1n sqrtr1.
rewrite /sin /pihalf expi_arg //.
by rewrite i1 divr1.
by rewrite -normr_eq0 i1 oner_neq0.
Qed.
Lemma cos_pihalf : cos pihalf = 0.
Proof.
have i1 : `|'i| = 1 :> T[i] by rewrite normc_def /= expr0n add0r expr1n sqrtr1.
rewrite /cos /pihalf expi_arg //.
by rewrite i1 divr1.
by rewrite -normr_eq0 i1 oner_neq0.
Qed.
Lemma tan_pihalf : tan pihalf = 0.
Proof. by rewrite /tan sin_pihalf cos_pihalf invr0 mulr0. Qed.
Lemma cosDpihalf a : cos (a + pihalf) = - sin a.
Proof. by rewrite cosD cos_pihalf mulr0 add0r sin_pihalf mulr1. Qed.
Lemma cosBpihalf a : cos (a - pihalf) = sin a.
Proof. by rewrite cosB cos_pihalf sin_pihalf mulr0 add0r mulr1. Qed.
Lemma sinDpihalf a : sin (a + pihalf) = cos a.
Proof. by rewrite sinD cos_pihalf mulr0 add0r sin_pihalf mulr1. Qed.
Lemma sinBpihalf a : sin (a - pihalf) = - cos a.
Proof. by rewrite sinB cos_pihalf sin_pihalf mulr0 add0r mulr1. Qed.
Lemma cos0_inv a : cos a = 0 -> {a = pihalf} + {a = - pihalf}.
Proof.
case: a => -[a b] ni; rewrite /cos /= => a0.
have [b1|b1] : {b = 1} + {b = - 1}.
move: ni.
rewrite a0 normc_def /= expr0n add0r sqrtr_sqr eq_complex /= eqxx andbT.
case: (lerP 0 b) => b0.
- rewrite ger0_norm // => /eqP ->; by left.
- rewrite ltr0_norm // eqr_oppLR => /eqP ->; by right.
- left; apply val_inj => /=;
by rewrite /pihalf argK // ?a0 ?b1 // normc_def /= expr0n add0r expr1n sqrtr1.
- right; apply val_inj => /=.
by apply/eqP; rewrite /pihalf a0 b1 expiNi eq_complex /= oppr0 2!eqxx.
Qed.
Definition piquarter : angle T := arg (Num.sqrt (2%:R^-1) +i* Num.sqrt (2%:R^-1))%C.
Lemma expi_piquarter :
expi piquarter = (Num.sqrt (2%:R^-1) +i* Num.sqrt (2%:R^-1))%C.
Proof.
rewrite /piquarter argK // normc_def /= sqr_sqrtr ?invr_ge0 ?ler0n //.
by rewrite -div1r -mulr2n -mulrnAl divrr ?unitfE ?pnatr_eq0 // sqrtr1.
Qed.
(*
sin(t) = ( exp(it) - exp(-it) )/2i
cos(t) = ( exp(it) + exp(-it) )/2
*)
Definition acos (x : T) : angle T := arg (x +i* Num.sqrt (1 - x ^+ 2))%C.
Lemma acos1 : acos 1 = 0.
Proof. by rewrite /acos expr1n subrr sqrtr0 complexr0 arg1. Qed.
Lemma acosN1 : acos (- 1) = pi.
Proof.
rewrite /acos sqrrN expr1n subrr sqrtr0 complexr0 (_ : ((_)%:C)%C = -1) //.
apply/eqP; by rewrite eq_complex /= oppr0 eqxx eqxx.
Qed.
Definition asin (x : T) : angle T := arg (Num.sqrt (1 - x ^+ 2) +i* x)%C.
Lemma asinN x : asin (- x) = - asin x.
Proof.
rewrite /asin sqrrN -argc //= eq_complex /= negb_and.
case/boolP : (x == 0) => [/eqP ->|]; last by rewrite orbT.
by rewrite expr0n /= subr0 sqrtr1 oner_neq0.
Qed.
Definition atan (x : T) : angle T :=
if x == 0 then 0 else arg ((x^-1 +i* 1)%C *~ sgz x).
Lemma atan0 : atan 0 = 0.
Proof. by rewrite /atan eqxx. Qed.
Lemma atan1 : atan 1 = piquarter.
Proof.
rewrite /atan oner_eq0 invr1 sgz1 mulr1z.
rewrite -(@argZ _ _ (Num.sqrt 2%:R^-1)) ?sqrtr_gt0 ?invr_gt0 ?ltr0Sn //.
by rewrite -complexZ1 mulr1.
Qed.
Lemma atanN x : atan (- x) = - atan x.
Proof.
rewrite /atan eqr_oppLR oppr0.
case: ifPn => [|x0]; first by rewrite oppr0.
rewrite -argc.
congr arg; apply/eqP.
rewrite sgzN mulrNz /= eq_complex /=.
move: x0; rewrite neq_lt => /orP [] x0.
by rewrite ltr0_sgz // 2!mulrN1z opprK /= invrN opprK 2!eqxx.
by rewrite gtr0_sgz // 2!mulr1z /= invrN opprK 2!eqxx.
move: x0; rewrite neq_lt => /orP [] x0.
rewrite ltr0_sgz // -?oppr_gt0 ?opprK // mulrN1z eq_complex /= negb_and orbC.
by rewrite eqr_oppLR oppr0 oner_neq0.
by rewrite gtr0_sgz ?oppr_gt0 // mulr1z eq_complex /= negb_and oner_neq0 orbC.
Qed.
Definition atan2 x y :=
if y > 0 then atan (x / y) else
if y < 0 then
(if x >= 0 then atan (x / y) + pi else
(* x < 0 *) atan (x / y) - pi) else
(* y == 0 *)
(if x > 0 then pihalf else
if x < 0 then - pihalf else
0) (* undefined *).
Lemma atan200 : atan2 0 0 = 0.
Proof. by rewrite /atan2 ltxx. Qed.
Lemma atan2_11 : atan2 1 1 = piquarter.
Proof. by rewrite /atan2 ltr01 invr1 mulr1 atan1. Qed.
Lemma atan2N (x y : T) : atan2 (- x) y = - atan2 x y.
Proof.
rewrite /atan2; have [y0|y0]:= ltP 0 y; first by rewrite mulNr atanN.
rewrite lt_neqAle y0 andbT; have [y0'|y0'] /= := boolP (y == 0).
by rewrite oppr_gt0 oppr_lt0; case: ltrgt0P => x0; rewrite ?opprK ?oppr0.
by rewrite oppr_ge0; case: ltrgt0P => x0;
rewrite mulNr atanN opprD ?opprK // {1}piNpi.
Qed.
(* cancellation laws *)
(* The following lemmas are true in specific domains only, such as
]-pi/2, pi/2[ = [pred a | cos a > 0]
]0, pi[ = [pred a | sin a > 0]
[-pi/2, pi/2[ = [pred a | cos a > 0]
[0, pi] = [pred a | sin a >= 0]
[0, pi[ = [pred a | sin a >= 0 && a != pi]
*)
Definition Opi_closed := [pred a | 0 <= sin a].
Definition piO_closed := [pred a | sin a < 0].
Lemma angle_in a : a \in Opi_closed \/ a \in piO_closed.
Proof. rewrite 2!inE; case: (lerP 0 (sin a)); by auto. Qed.
(* ]-pi/2, pi/2[ *)
Definition Npi2pi2_open : pred (angle T) := [pred a | cos a > 0].
Definition Npi2pi2_closed : pred (angle T) := [pred a | cos a >= 0].
Lemma Npi2pi2_openP a : (a \in Npi2pi2_open) = (0 < cos a).
Proof. by rewrite inE. Qed.
Lemma acosK (r : T) : -1 <= r <= 1 -> cos (acos r) = r.
Proof.
move=> rdom; rewrite /acos /cos argK // normc_def /= sqr_sqrtr; last first.
by rewrite subr_ge0 -ler_sqrt // ?ltr01 // sqrtr1 sqrtr_sqr ler_norml.
by rewrite addrC subrK sqrtr1.
Qed.
Lemma tanK a : a \in Npi2pi2_open -> atan (tan a) = a.
Proof.
rewrite inE => adoml; rewrite /atan /tan mulf_eq0.
have [|saNZ] /= := boolP (sin a == 0).
rewrite sin_eq0 => /orP[] /eqP aE //.
by rewrite aE cospi // -subr_lt0 opprK add0r (ltr_nat _ 1 0) in adoml.
rewrite invr_eq0.
move: (adoml); rewrite lt0r => /andP[/negPf-> _].
have -> : ((sin a / cos a)^-1 +i* 1 = (sin a)^-1%:C * (cos a +i* sin a))%C.
by rewrite invf_div -complexZ mulVf // mulrC.
rewrite sgzM; case: (sgzP (sin a)) saNZ => //= saP _.
by rewrite mul1r gtr0_sgz ?invr_gt0 // argZ ?invr_gt0 // -expi_cos_sin expiK.
rewrite mulN1r gtr0_sgz ?invr_gt0 // mulrN1z -!mulrN.
by rewrite argZ_neg ?invr_lt0 // opprK -expi_cos_sin expiK.
Qed.
Lemma tanDpi a : tan (a + pi) = tan a.
Proof. by rewrite /tan sinDpi cosDpi mulNr invrN mulrN opprK. Qed.
Lemma tanK_closed a : a \notin Npi2pi2_closed -> atan (tan a) = a + pi.
Proof.
rewrite inE => adoml.
rewrite -{1}[a]addr0 -pi2 mulr2n addrA tanDpi tanK // inE cosDpi.
by rewrite oppr_cp0 ltNge.
Qed.
Lemma cosK a : a \in Opi_closed -> acos (cos a) = a.
Proof.
rewrite inE => adoml; rewrite /acos /cos /= expi_cos_sin /= -sin2cos2.
by rewrite sqrtr_sqr /= ger0_norm // -expi_cos_sin expiK.
Qed.
Lemma cosKN a : a \in piO_closed -> acos (cos a) = - a.
Proof.
rewrite inE => adoml; rewrite /acos /cos /= expi_cos_sin /= -sin2cos2.
rewrite sqrtr_sqr /= ltr0_norm //.
move: (expi_cos_sin (- a)); rewrite cosN sinN => <-; by rewrite expiK.
Qed.
Lemma sinK (x : angle T) : 0 <= cos x (* TODO: define Npi2pi2_closed? *) ->
asin (sin x) = x.
Proof.
case: x => /= -[x y] x1 cosx1; apply/val_inj/eqP => /=.
rewrite eq_complex /asin /sin argK /= ?eqxx ?andbT; last first.
rewrite {cosx1}.
rewrite normc_def /= sqr_sqrtr ?subrK ?sqrtr1 // subr_ge0.
move: x1; rewrite normc_def eq_complex eqxx andbT /=.
move/eqP/(congr1 (fun x => x^+2)); rewrite expr1n.
rewrite sqr_sqrtr ?addr_ge0 // ?sqr_ge0 // => <-.
by rewrite ler_addr // sqr_ge0.
rewrite /cos /= in cosx1.
move : x1; rewrite normc_def /= eq_complex /= eqxx andbT.
move/eqP/(congr1 (fun x => x^+2)); rewrite expr1n.
rewrite sqr_sqrtr // ?addr_ge0 // ?sqr_ge0 // => <-.
by rewrite addrK sqrtr_sqr ger0_norm.
Qed.
Lemma asinK r : -1 <= r <= 1 -> sin (asin r) = r.
Proof.
move=> rdom; rewrite /sin /asin argK // normc_def /= sqr_sqrtr; last first.
by rewrite subr_ge0 -ler_sqrt // ?ltr01 // sqrtr1 sqrtr_sqr ler_norml.
by rewrite subrK sqrtr1.
Qed.
Lemma atan_in x : atan x \in Npi2pi2_open.
Proof.
case/boolP : (x == 0) => [/eqP ->|x0].
by rewrite atan0 inE cos0 ltr01.
rewrite Npi2pi2_openP /atan (negbTE x0) /cos => [:myRe0].
rewrite expi_arg.
rewrite normc_def => [:myltr0].
rewrite Re_scale.
rewrite divr_gt0 //.
abstract: myRe0.
move/lt_total : x0 => /orP [] x0; last by rewrite gtr0_sgz //= invr_gt0.
by rewrite ltr0_sgz //= ltr_oppr oppr0 invr_lt0.
abstract: myltr0.
rewrite -ltcR -normc_def normr_gt0 eq_complex /= negb_and.
move/lt_total : x0 => /orP [] x0; last by rewrite gtr0_sgz //= invr_eq0 gt_eqF.
by rewrite ltr0_sgz //= eqr_oppLR oppr0 invr_eq0 lt_eqF.
by rewrite gt_eqF.
by rewrite eq_complex /= negb_and gt_eqF.
Qed.
Lemma atanKpos x : 0 < x -> tan (atan x) = x.
Proof.
move=> x0; rewrite /atan gt_eqF // gtr0_sgz // mulr1z /tan /sin /cos.
rewrite expi_arg /=; last by rewrite eq_complex /= negb_and oner_neq0 orbT.
rewrite mul0r oppr0 mulr0 add0r mulr0 subr0 expr0n addr0 expr1n.
rewrite sqr_sqrtr; last by rewrite addr_ge0 // ?ler01 // sqr_ge0.
set y := Num.sqrt _ / _; move=> [:yunit].
rewrite mul1r invrM; last 2 first.
by rewrite unitrV unitfE gt_eqF.
abstract: yunit.
rewrite unitfE /y mulf_eq0 negb_or sqrtr_eq0 -ltNge invr_eq0.
move=> [:x2D1]; apply/andP; split.
abstract: x2D1.
by rewrite addr_gt0 // ?ltr01 // exprn_even_gt0 //= invr_eq0 gt_eqF.
by rewrite gt_eqF.
by rewrite mulrA divrr // invrK mul1r.
Qed.
Lemma atanKneg x : x < 0 -> tan (atan x) = x.
Proof.
rewrite -oppr_gt0 => x0; rewrite /atan lt_eqF -?oppr_gt0 //.
move/eqP: (atanKpos x0); rewrite -eqr_oppLR => /eqP H.
by rewrite -{3}H {H} atanN tanN opprK /atan lt_eqF // -oppr_gt0.
Qed.
Lemma atanK x : tan (atan x) = x.
Proof.
case: (lerP 0 x); last by apply atanKneg.
rewrite le_eqVlt => /orP [/eqP <-|]; by [rewrite atan0 tan0 | apply atanKpos].
Qed.
Lemma sqr_sin_atan (x : T) : (sin (atan x)) ^+ 2 = x ^+ 2 / (1 + x ^+ 2).
Proof.
case/boolP : (x == 0) => [/eqP ->|x0].
by rewrite atan0 sin0 expr0n /= mul0r.
rewrite sin2cos2.
apply/eqP; rewrite -eqr_opp opprB subr_eq; apply/eqP.
rewrite -mulNr.
have /divrr H : 1 + x ^+ 2 \in GRing.unit.
by rewrite unitfE gt_eqF // -(addr0 0) ltr_le_add // ?ltr01 // sqr_ge0.
rewrite -{2}H {H} addrC mulNr -mulrBl -invf_div -[LHS]invrK; congr (_ ^-1).
rewrite -exprVn -div1r expr_div_n expr1n cos2_tan2.
by rewrite atanK addrK divr1.
by rewrite gt_eqF // -Npi2pi2_openP atan_in.
Qed.
Lemma sin_atan_ltr0 (x : T) : x < 0 -> sin (atan x) < 0.
Proof.
move=> x0.
rewrite /sin /atan lt_eqF // ltr0_sgz // mulrN1z /= expi_arg //=.
rewrite expr0n addr0 mul0r oppr0 mulr0 add0r.
rewrite sqr_sqrtr; last by rewrite addr_ge0 // sqr_ge0.
rewrite pmulr_llt0; first by rewrite oppr_lt0 ltr01.
rewrite (sqrrN 1) expr1n divr_gt0 //.
rewrite sqrtr_gt0 addr_gt0 // ?ltr01 //.
by rewrite exprn_gt0 // oppr_gt0 invr_lt0.
by rewrite addr_gt0 // ?ltr01 // exprn_gt0 // oppr_gt0 invr_lt0.
by rewrite eq_complex /= negb_and /= orbC eqr_oppLR oppr0 oner_eq0.
Qed.
Lemma sin_atan_gtr0 (x : T) : 0 < x -> 0 < sin (atan x).
Proof.
move=> x0.
by rewrite -(opprK (sin _)) -sinN -atanN -oppr_lt0 opprK sin_atan_ltr0 // oppr_lt0.
Qed.
Lemma sin_atan (x : T) : sin (atan x) = x / Num.sqrt (1 + x ^+ 2).
Proof.
apply/eqP.
case/boolP : (x == 0) => [/eqP ->|].
by rewrite atan0 sin0 mul0r.
move/lt_total => /orP [] x0.
rewrite -eqr_opp -(@eqr_expn2 _ 2) //; last 2 first.
move/sin_atan_ltr0 : x0; by rewrite oppr_ge0 => /ltW.
by rewrite -mulNr divr_ge0 // ?sqrtr_ge0 // oppr_ge0 ltW.
by rewrite 2!sqrrN sqr_sin_atan exprMn exprVn sqr_sqrtr // addr_ge0 // ?ler01 // sqr_ge0.
rewrite -(@eqr_expn2 _ 2) //; last 2 first.
by rewrite ltW // sin_atan_gtr0.
by rewrite mulr_ge0 // ?invr_ge0 ?sqrtr_ge0 // ltW.
by rewrite sqr_sin_atan exprMn exprVn sqr_sqrtr // addr_ge0 // ?ler01 // sqr_ge0.
Qed.
Lemma sin_acos x : `|x| <= 1 -> sin (acos x) = Num.sqrt (1 - x ^+ 2).
Proof.
move=> Nx_le1; rewrite /sin /acos argK //; simpc; rewrite sqr_sqrtr.
by rewrite addrC addrNK sqrtr1.
by rewrite subr_ge0 -[_ ^+ _]real_normK ?num_real // exprn_ile1.
Qed.
Lemma cos_asin (x : T) : `| x | < 1 -> cos (asin x) = Num.sqrt (1 - x ^+ 2).
Proof.
move=> x1.
rewrite /asin /cos argK // normc_def /= sqr_sqrtr ?subr_ge0 ?subrK ?sqrtr1 //.
by rewrite -sqr_normr expr_le1 // ltW.
Qed.
Lemma cos_atan x : cos (atan x) = 1 / Num.sqrt (1 + x ^+ 2).
Proof.
move: (atan_in x); rewrite Npi2pi2_openP lt_neqAle => /andP [H1 H2].
move: (H1); rewrite eq_sym; move/cos2_tan2.
rewrite atanK => <-.
rewrite sqrtrM ?ler01 // sqrtr1 2!mul1r.
rewrite -exprVn sqrtr_sqr ger0_norm; by [rewrite invrK | rewrite invr_ge0].
Qed.
End angle_basic_prop.
Section half_angle.
Variable T : rcfType.
Definition half_anglec (x : T[i]) :=
(if 0 <= complex.Im x then
Num.sqrt ((1 + complex.Re x) / 2%:R) +i* Num.sqrt ((1 - complex.Re x) / 2%:R)
else
- Num.sqrt ((1 + complex.Re x) / 2%:R) +i* Num.sqrt ((1 - complex.Re x) / 2%:R))%C.
Lemma Re_half_anglec (x : T[i]) : `|x| = 1 -> 0 <= 1 + complex.Re x.
Proof.
move=> x1; rewrite -ler_subl_addr add0r.
suff : `| complex.Re x |%:C%C <= `|x|; last by rewrite normc_ge_Re.
rewrite x1 -lecR; apply: le_trans; by rewrite lecR ler_normr lexx orbT.
Qed.
Lemma Im_half_anglec (x : T[i]) : `|x| = 1 -> complex.Re x <= 1.
Proof.
move=> x1; suff : `| complex.Re x |%:C%C <= `|x|; last by rewrite normc_ge_Re.
rewrite x1 -lecR; apply: le_trans; by rewrite lecR ler_normr lexx.
Qed.
Lemma norm_half_anglec (x : T[i]) : `|x| = 1 -> `|half_anglec x| == 1.
Proof.
move=> x1.
rewrite /half_anglec.
case: ifP => a0.
rewrite normc_def /= sqr_sqrtr; last first.
by rewrite divr_ge0 // ?ler0n // Re_half_anglec.
rewrite sqr_sqrtr; last first.
by rewrite divr_ge0 // ?ler0n // subr_ge0 Im_half_anglec.
by rewrite mulrC (mulrC (1 - complex.Re x)) -mulrDr addrCA addrK -mulr2n mulVr ?pnatf_unit // sqrtr1.
rewrite normc_def /= sqr_sqrtr; last first.
by rewrite divr_ge0 // ?ler0n // subr_ge0 Im_half_anglec.
rewrite sqrrN sqr_sqrtr; last first.
by rewrite divr_ge0 // ?ler0n // Re_half_anglec.
by rewrite mulrC (mulrC (1 - complex.Re x)) -mulrDr addrCA addrK -mulr2n mulVr ?pnatf_unit // sqrtr1.
Qed.
Definition half_angle (x : angle T) := Angle (norm_half_anglec (normr_expi x)).
Lemma half_angle0 : half_angle 0 = 0.
Proof.
apply val_inj => /=; rewrite /half_anglec; case: ifPn => /=; rewrite expi0 /=.
2: by rewrite lexx.
move=> _; rewrite subrr mul0r sqrtr0 divrr ?unitfE // ?complexr0 ?sqrtr1 //.
by rewrite (_ : 1 + 1 = 2%:R) // pnatr_eq0.
Qed.
Lemma half_anglepi : half_angle pi = pihalf T.
Proof.
apply val_inj => /=; rewrite /half_anglec; case: ifPn => /=; rewrite expipi /= oppr0.
2: by rewrite lexx.
move=> _; rewrite subrr mul0r sqrtr0 opprK expi_pihalf.
rewrite (_ : 1 + 1 = 2%:R) // ?pnatr_eq0 divrr ?unitfE ?pnatr_eq0 //.
by rewrite sqrtr1.
Qed.
Lemma sin_half_angle_ge0 a : 0 <= sin (half_angle a).
Proof.
case: a => -[a b] /= ab.
rewrite /sin /= /half_anglec /=; case: ifPn => b0 /=; by rewrite sqrtr_ge0.
Qed.
Lemma halfP a : half_angle a + half_angle a = a.
Proof.
apply/eqP.
rewrite eq_angle; apply/andP; split.
rewrite /cos /= add_angleE /add_angle /half_angle /= argK; last first.
by rewrite normrM (eqP (norm_half_anglec (normr_expi _))) mulr1.
rewrite /half_anglec. simpc. rewrite /=.
move=> [:tmp].
case: ifP => a0 /=.
abstract: tmp.
rewrite -2!expr2 sqr_sqrtr; last first.
by rewrite divr_ge0 // ?Re_half_anglec // ?normr_expi // ler0n.
rewrite sqr_sqrtr; last first.
by rewrite divr_ge0 // ?ler0n // subr_ge0 Im_half_anglec // normr_expi.
rewrite mulrC (mulrC (_ - _)) -mulrBr opprB addrC addrA subrK -mulr2n.
by rewrite -(mulr_natl (complex.Re _)) mulrA mulVr ?pnatf_unit // mul1r eqxx.
rewrite mulNr mulrN opprK; exact: tmp.
rewrite /sin /= add_angleE /add_angle /half_angle /= argK; last first.
by rewrite normrM (eqP (norm_half_anglec (normr_expi _))) mulr1.
rewrite /half_anglec. simpc. rewrite /=.
case: ifPn => a0 /=.
rewrite mulrC -mulr2n.
rewrite (@sqrtrM _ (1 - complex.Re a)); last by rewrite subr_ge0 Im_half_anglec // normr_expi.
rewrite (@sqrtrM _ (1 + complex.Re a)); last by rewrite Re_half_anglec // normr_expi.
rewrite mulrCA -mulrA -(sqrtrM 2^-1) ?invr_ge0//.
rewrite -expr2 sqrtr_sqr normfV ger0_norm// -mulr_natr -2!mulrA mulVf ?pnatr_eq0// mulr1.
rewrite mulrC -sqrtrM; last by rewrite subr_ge0 Im_half_anglec // normr_expi.
rewrite -subr_sqr expr1n.
rewrite -(@eqrXn2 _ 2%N) //; last by rewrite sqrtr_ge0.
by rewrite -sin2cos2 sqr_sqrtr // sqr_ge0.
rewrite mulrN mulNr -opprD eqr_oppLR.
rewrite mulrC -mulr2n.
rewrite (@sqrtrM _ (1 - complex.Re a)); last by rewrite subr_ge0 Im_half_anglec // normr_expi.
rewrite (@sqrtrM _ (1 + complex.Re a)); last by rewrite Re_half_anglec // normr_expi.
rewrite mulrAC -2!mulrA -sqrtrM ?invr_ge0//.
rewrite -expr2 sqrtr_sqr normfV ger0_norm// mulrA -[eqbLHS]mulr_natr -!mulrA mulVf ?pnatr_eq0// mulr1.
rewrite -sqrtrM; last by rewrite subr_ge0 Im_half_anglec // normr_expi.
rewrite -subr_sqr expr1n.
rewrite -(@eqrXn2 _ 2%N) //; last 2 first.
by rewrite sqrtr_ge0.
by rewrite ltW // oppr_gt0 ltNge.
by rewrite -sin2cos2 sqrrN sqr_sqrtr // sqr_ge0.
Qed.
Lemma pihalf_is_half : pihalf _ = half_angle pi.
Proof.
rewrite /half_angle; apply val_inj => /=.
rewrite /half_anglec expipi /= oppr0 lexx subrr mul0r sqrtr0 opprK.
by rewrite -(@natrD _ 1 1) divrr ?unitfE ?pnatr_eq0 // sqrtr1 expi_pihalf.
Qed.
Lemma pi_pihalf : pi = pihalf T *+ 2.
Proof. by rewrite -[LHS]halfP pihalf_is_half -mulr2n. Qed.
Lemma piquarter_is_half : piquarter _ = half_angle (pihalf _).
Proof.
rewrite /half_angle; apply val_inj => /=.
by rewrite /half_anglec expi_pihalf /= ler01 addr0 subr0 div1r expi_piquarter.
Qed.
Lemma pi_piquarter : pi = piquarter T *+ 4.
Proof.
rewrite (mulrnA _ 2 2) -[LHS]halfP -mulr2n; congr (_ *+ 2).
by rewrite piquarter_is_half mulr2n halfP pihalf_is_half.
Qed.
Lemma sin_half_angle a : `| sin (half_angle a) | = Num.sqrt ((1 - cos a) / 2%:R).
Proof.
move: (cosD (half_angle a) (half_angle a)).
rewrite halfP -2!expr2 cos2sin2 -addrA -opprD -mulr2n => /eqP.
rewrite eq_sym subr_eq addrC -subr_eq eq_sym => /eqP/(congr1 (fun x => x / 2%:R)).
rewrite -(mulr_natl (sin _ ^+ _)) mulrC mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r.
by move/(congr1 Num.sqrt); rewrite sqrtr_sqr.
Qed.
Lemma cos_half_angle a : `| cos (half_angle a) | = Num.sqrt ((1 + cos a) / 2%:R).
Proof.
move: (cosD (half_angle a) (half_angle a)).
rewrite halfP -2!expr2 sin2cos2 opprB addrA -mulr2n => /eqP.
rewrite eq_sym subr_eq addrC => /eqP/(congr1 (fun x => x / 2%:R)).
rewrite -mulr_natl mulrC mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r.
by move/(congr1 Num.sqrt); rewrite sqrtr_sqr.
Qed.
Lemma tan_half_angle a : tan (half_angle a) = (1 - cos a) / sin a.
Proof.
rewrite /tan.
move: (sin_half_angle a) => H1.
move: (cos_half_angle a) => H2.
have H3 : cos a <= 1 by move: (@ler_norml _ (cos a) 1); rewrite cos_max => /esym/andP[].
have H4 : -1 <= cos a by move: (@ler_norml _ (cos a) 1); rewrite cos_max => /esym/andP[].
move: (sin_half_angle_ge0 a) => sa0.
move: H1; rewrite ger0_norm // => ->.
rewrite sqrtrM; last by rewrite subr_ge0.
case: (lerP 0 (cos (half_angle a))) => ca0.
move: H2; rewrite ger0_norm // => ->.
rewrite sqrtrM; last by rewrite -ler_sub_addl add0r.
rewrite -mulf_div divrr ?unitfE ?sqrtr_eq0 -?ltNge ?invr_gt0 ?ltr0Sn // mulr1.
case/boolP : (cos a == 1) => [/eqP ca1|ca1]; first by rewrite ca1 subrr sqrtr0 2!mul0r.
rewrite -[LHS]mulr1 -{3}(@divrr _ (Num.sqrt (1 - cos a))); last first.
by rewrite unitfE sqrtr_eq0 -ltNge subr_gt0 lt_neqAle ca1.
rewrite mulf_div -sqrtrM; last by rewrite subr_ge0.
rewrite -expr2 -sqrtrM; last by rewrite -ler_sub_addl add0r.