-
Notifications
You must be signed in to change notification settings - Fork 11
/
Copy pathrealalg.v
1537 lines (1283 loc) · 57.4 KB
/
realalg.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
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
From mathcomp
Require Import bigop ssralg ssrnum ssrint rat poly polydiv polyorder.
From mathcomp
Require Import perm matrix mxpoly polyXY binomial generic_quotient.
From mathcomp
Require Import cauchyreals separable zmodp bigenough.
(*************************************************************************)
(* This files constructs the real closure of an archimedian field in the *)
(* way described in Cyril Cohen. Construction of real algebraic numbers *)
(* in Coq. In Lennart Beringer and Amy Felty, editors, ITP - 3rd *)
(* International Conference on Interactive Theorem Proving - 2012, *)
(* Princeton, United States, August 2012. Springer *)
(* *)
(* The only definition one may want to use in this file is the operator *)
(* {realclosure R} which constructs the real closure of the archimedian *)
(* field R (for which rat is a prefect candidate) *)
(*************************************************************************)
Import GRing.Theory Num.Theory BigEnough.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Reserved Notation "{ 'realclosure' T }"
(at level 0, format "{ 'realclosure' T }").
Reserved Notation "{ 'alg' T }" (at level 0, format "{ 'alg' T }").
Section extras.
Local Open Scope ring_scope.
Local Notation "p ^ f" := (map_poly f p) : ring_scope.
Lemma map_comp_poly (aR : fieldType) (rR : idomainType)
(f : {rmorphism aR -> rR})
(p q : {poly aR}) : (p \Po q) ^ f = (p ^ f) \Po (q ^ f).
Proof.
rewrite !comp_polyE size_map_poly; apply: (big_ind2 (fun x y => x ^ f = y)).
+ by rewrite rmorph0.
+ by move=> u u' v v' /=; rewrite rmorphD /= => -> ->.
move=> /= i _; rewrite -mul_polyC rmorphM /= map_polyC mul_polyC.
by rewrite coef_map rmorphX.
Qed.
End extras.
Module RealAlg.
Local Open Scope ring_scope.
Local Notation eval := horner_eval.
Section RealAlg.
Variable F : archiFieldType.
Local Notation m0 := (fun _ => 0%N).
(*********************************************************************)
(* Construction of algebraic Cauchy reals : Cauchy real + polynomial *)
(*********************************************************************)
CoInductive algcreal := AlgCReal {
creal_of_alg :> creal F;
annul_creal : {poly F};
_ : annul_creal \is monic;
_ : (annul_creal.[creal_of_alg] == 0)%CR
}.
Lemma monic_annul_creal x : annul_creal x \is monic.
Proof. by case: x. Qed.
Hint Resolve monic_annul_creal.
Lemma annul_creal_eq0 x : (annul_creal x == 0) = false.
Proof. by rewrite (negPf (monic_neq0 _)). Qed.
Lemma root_annul_creal x : ((annul_creal x).[x] == 0)%CR.
Proof. by case: x. Qed.
Hint Resolve root_annul_creal.
Definition cst_algcreal (x : F) :=
AlgCReal (monicXsubC _) (@root_cst_creal _ x).
Local Notation zero_algcreal := (cst_algcreal 0).
Local Notation one_algcreal := (cst_algcreal 1).
Lemma size_annul_creal_gt1 (x : algcreal) :
(1 < size (annul_creal x))%N.
Proof.
apply: (@has_root_creal_size_gt1 _ x).
by rewrite monic_neq0 // monic_annul_creal.
exact: root_annul_creal.
Qed.
Lemma is_root_annul_creal (x : algcreal) (y : creal F) :
(x == y)%CR -> ((annul_creal x).[y] == 0)%CR.
Proof. by move <-. Qed.
Definition AlgCRealOf (p : {poly F}) (x : creal F)
(p_neq0 : p != 0) (px_eq0 : (p.[x] == 0)%CR) :=
AlgCReal (monic_monic_from_neq0 p_neq0) (root_monic_from_neq0 px_eq0).
Lemma sub_annihilant_algcreal_neq0 (x y : algcreal) :
sub_annihilant (annul_creal x) (annul_creal y) != 0.
Proof. by rewrite sub_annihilant_neq0 ?monic_neq0. Qed.
Lemma root_sub_algcreal (x y : algcreal) :
((sub_annihilant (annul_creal x) (annul_creal y)).[x - y] == 0)%CR.
Proof. by rewrite root_sub_annihilant_creal ?root_annul_creal ?monic_neq0. Qed.
Definition sub_algcreal (x y : algcreal) : algcreal :=
AlgCRealOf (sub_annihilant_algcreal_neq0 x y) (@root_sub_algcreal x y).
Lemma root_opp_algcreal (x : algcreal) :
((annul_creal (sub_algcreal (cst_algcreal 0) x)).[- x] == 0)%CR.
Proof. by apply: is_root_annul_creal; rewrite /= add_0creal. Qed.
Definition opp_algcreal (x : algcreal) : algcreal :=
AlgCReal (@monic_annul_creal _) (@root_opp_algcreal x).
Lemma root_add_algcreal (x y : algcreal) :
((annul_creal (sub_algcreal x (opp_algcreal y))).[x + y] == 0)%CR.
Proof.
apply: is_root_annul_creal; apply: eq_crealP.
by exists m0=> * /=; rewrite opprK subrr normr0.
Qed.
Definition add_algcreal (x y : algcreal) : algcreal :=
AlgCReal (@monic_annul_creal _) (@root_add_algcreal x y).
Lemma div_annihilant_algcreal_neq0 (x y : algcreal) :
(annul_creal y).[0] != 0 ->
div_annihilant (annul_creal x) (annul_creal y) != 0.
Proof. by move=> ?; rewrite div_annihilant_neq0 ?monic_neq0. Qed.
Hint Resolve eq_creal_refl.
Hint Resolve le_creal_refl.
Lemma simplify_algcreal (x : algcreal) (x_neq0 : (x != 0)%CR) :
{y | ((annul_creal y).[0] != 0) & ((y != 0)%CR * (x == y)%CR)%type}.
Proof.
elim: size {-3}x x_neq0 (leqnn (size (annul_creal x))) =>
{x} [|n ihn] x x_neq0 hx.
by move: hx; rewrite leqn0 size_poly_eq0 annul_creal_eq0.
have [dvdX|ndvdX] := boolP ('X %| annul_creal x); last first.
by exists x=> //; rewrite -rootE -dvdp_XsubCl subr0.
have monic_p: @annul_creal x %/ 'X \is monic.
by rewrite -(monicMr _ (@monicX _)) divpK //.
have root_p: ((@annul_creal x %/ 'X).[x] == 0)%CR.
have := @eq_creal_refl _ ((annul_creal x).[x])%CR.
rewrite -{1}(divpK dvdX) horner_crealM // root_annul_creal.
by case/poly_mul_creal_eq0=> //; rewrite horner_crealX.
have [//|/=|y *] := ihn (AlgCReal monic_p root_p); last by exists y.
by rewrite size_divp ?size_polyX ?polyX_eq0 ?leq_subLR ?add1n.
Qed.
(* Decidability of equality to 0 *)
Lemma algcreal_eq0_dec (x : algcreal) : {(x == 0)%CR} + {(x != 0)%CR}.
Proof.
pose p := annul_creal x; move: {2}(size _)%N (leqnn (size p))=> n.
elim: n x @p => [x p|n ihn x p le_sp_Sn].
by rewrite leqn0 size_poly_eq0 /p annul_creal_eq0.
move: le_sp_Sn; rewrite leq_eqVlt; have [|//|eq_sp_Sn _] := ltngtP.
by rewrite ltnS=> /ihn ihnp _; apply: ihnp.
have px0 : (p.[x] == 0)%CR by apply: root_annul_creal.
have [cpX|ncpX] := boolP (coprimep p 'X).
by right; move: (cpX)=> /coprimep_root /(_ px0); rewrite horner_crealX.
have [eq_pX|] := altP (p =P 'X).
by left; move: px0; rewrite eq_pX horner_crealX.
rewrite -eqp_monic /p ?monicX // negb_and orbC.
have:= ncpX; rewrite coprimepX -dvdp_XsubCl subr0 => /negPf-> /= ndiv_pX.
have [r] := smaller_factor (monic_annul_creal _) px0 ndiv_pX ncpX.
rewrite eq_sp_Sn ltnS => /andP[le_r_n monic_r] rx_eq0.
exact: (ihn (AlgCReal monic_r rx_eq0)).
Qed.
Lemma eq_algcreal_dec (x y : algcreal) : {(x == y)%CR} + {(x != y)%CR}.
Proof.
have /= [d_eq0|d_neq0] := algcreal_eq0_dec (sub_algcreal x y); [left|right].
apply: eq_crealP; exists_big_modulus m F.
by move=> e i e_gt0 hi; rewrite (@eq0_modP _ _ d_eq0).
by close.
pose_big_enough i.
apply: (@neq_crealP _ (lbound d_neq0) i i); do ?by rewrite ?lbound_gt0.
by rewrite (@lbound0P _ _ d_neq0).
by close.
Qed.
Definition eq_algcreal : rel algcreal := eq_algcreal_dec.
Lemma eq_algcrealP (x y : algcreal) : reflect (x == y)%CR (eq_algcreal x y).
Proof. by rewrite /eq_algcreal; case: eq_algcreal_dec=> /=; constructor. Qed.
Arguments eq_algcrealP [x y].
Lemma neq_algcrealP (x y : algcreal) : reflect (x != y)%CR (~~ eq_algcreal x y).
Proof. by rewrite /eq_algcreal; case: eq_algcreal_dec=> /=; constructor. Qed.
Arguments neq_algcrealP [x y].
Prenex Implicits eq_algcrealP neq_algcrealP.
Fact eq_algcreal_is_equiv : equiv_class_of eq_algcreal.
Proof.
split=> [x|x y|y x z]; first by apply/eq_algcrealP.
by apply/eq_algcrealP/eq_algcrealP; symmetry.
by move=> /eq_algcrealP /eq_creal_trans h /eq_algcrealP /h /eq_algcrealP.
Qed.
Canonical eq_algcreal_rel := EquivRelPack eq_algcreal_is_equiv.
Lemma root_div_algcreal (x y : algcreal) (y_neq0 : (y != 0)%CR) :
(annul_creal y).[0] != 0 ->
((div_annihilant (annul_creal x) (annul_creal y)).[x / y_neq0] == 0)%CR.
Proof. by move=> hx; rewrite root_div_annihilant_creal ?monic_neq0. Qed.
Definition div_algcreal (x y : algcreal) :=
match eq_algcreal_dec y (cst_algcreal 0) with
| left y_eq0 => cst_algcreal 0
| right y_neq0 =>
let: exist2 y' py'0_neq0 (y'_neq0, _) := simplify_algcreal y_neq0 in
AlgCRealOf (div_annihilant_algcreal_neq0 x py'0_neq0)
(@root_div_algcreal x y' y'_neq0 py'0_neq0)
end.
Lemma root_inv_algcreal (x : algcreal) (x_neq0 : (x != 0)%CR) :
((annul_creal (div_algcreal (cst_algcreal 1) x)).[x_neq0^-1] == 0)%CR.
Proof.
rewrite /div_algcreal; case: eq_algcreal_dec=> [/(_ x_neq0)|x_neq0'] //=.
case: simplify_algcreal=> x' px'0_neq0 [x'_neq0 eq_xx'].
apply: is_root_annul_creal; rewrite /= -(@eq_creal_inv _ _ _ x_neq0) //.
by apply: eq_crealP; exists m0=> * /=; rewrite div1r subrr normr0.
Qed.
Definition inv_algcreal (x : algcreal) :=
match eq_algcreal_dec x (cst_algcreal 0) with
| left x_eq0 => cst_algcreal 0
| right x_neq0 =>
AlgCReal (@monic_annul_creal _) (@root_inv_algcreal _ x_neq0)
end.
Lemma div_creal_creal (y : creal F) (y_neq0 : (y != 0)%CR) :
(y / y_neq0 == 1%:CR)%CR.
Proof.
apply: eq_crealP; exists_big_modulus m F.
move=> e i e_gt0 hi; rewrite /= divff ?subrr ?normr0 //.
by rewrite (@creal_neq_always _ _ 0%CR).
by close.
Qed.
Lemma root_mul_algcreal (x y : algcreal) :
((annul_creal (div_algcreal x (inv_algcreal y))).[x * y] == 0)%CR.
Proof.
rewrite /div_algcreal /inv_algcreal.
case: (eq_algcreal_dec y)=> [->|y_neq0]; apply: is_root_annul_creal.
rewrite mul_creal0; case: eq_algcreal_dec=> // neq_00.
by move: (eq_creal_refl neq_00).
case: eq_algcreal_dec=> /= [yV_eq0|yV_neq0].
have: (y * y_neq0^-1 == 0)%CR by rewrite yV_eq0 mul_creal0.
by rewrite div_creal_creal=> /eq_creal_cst; rewrite oner_eq0.
case: simplify_algcreal=> y' py'0_neq0 [y'_neq0 /= eq_yy'].
rewrite -(@eq_creal_inv _ _ _ yV_neq0) //.
by apply: eq_crealP; exists m0=> * /=; rewrite invrK subrr normr0.
Qed.
Definition mul_algcreal (x y : algcreal) :=
AlgCReal (@monic_annul_creal _) (@root_mul_algcreal x y).
Lemma le_creal_neqVlt (x y : algcreal) : (x <= y)%CR -> {(x == y)%CR} + {(x < y)%CR}.
Proof.
case: (eq_algcreal_dec x y); first by left.
by move=> /neq_creal_ltVgt [|h /(_ h) //]; right.
Qed.
Lemma ltVge_algcreal_dec (x y : algcreal) : {(x < y)%CR} + {(y <= x)%CR}.
Proof.
have [eq_xy|/neq_creal_ltVgt [lt_xy|lt_yx]] := eq_algcreal_dec x y;
by [right; rewrite eq_xy | left | right; apply: lt_crealW].
Qed.
Definition lt_algcreal : rel algcreal := ltVge_algcreal_dec.
Definition le_algcreal : rel algcreal := fun x y => ~~ ltVge_algcreal_dec y x.
Lemma lt_algcrealP (x y : algcreal) : reflect (x < y)%CR (lt_algcreal x y).
Proof. by rewrite /lt_algcreal; case: ltVge_algcreal_dec; constructor. Qed.
Arguments lt_algcrealP [x y].
Lemma le_algcrealP (x y : algcreal) : reflect (x <= y)%CR (le_algcreal x y).
Proof. by rewrite /le_algcreal; case: ltVge_algcreal_dec; constructor. Qed.
Arguments le_algcrealP [x y].
Prenex Implicits lt_algcrealP le_algcrealP.
Definition exp_algcreal x n := iterop n mul_algcreal x one_algcreal.
Lemma exp_algcrealE x n : (exp_algcreal x n == x ^+ n)%CR.
Proof.
case: n=> // n; rewrite /exp_algcreal /exp_creal !iteropS.
by elim: n=> //= n ->.
Qed.
Definition horner_algcreal (p : {poly F}) x : algcreal :=
\big[add_algcreal/zero_algcreal]_(i < size p)
mul_algcreal (cst_algcreal p`_i) (exp_algcreal x i).
Lemma horner_algcrealE p x : (horner_algcreal p x == p.[x])%CR.
Proof.
rewrite horner_coef_creal.
apply: (big_ind2 (fun (u : algcreal) v => u == v)%CR)=> //.
by move=> u u' v v' /= -> ->.
by move=> i _ /=; rewrite exp_algcrealE.
Qed.
Definition norm_algcreal (x : algcreal) :=
if le_algcreal zero_algcreal x then x else opp_algcreal x.
Lemma norm_algcrealE (x : algcreal) : (norm_algcreal x == `| x |)%CR.
Proof.
rewrite /norm_algcreal /le_algcreal; case: ltVge_algcreal_dec => /=.
move=> x_lt0; apply: eq_crealP; exists_big_modulus m F.
move=> e i e_gt0 hi /=; rewrite [`|x i|]ler0_norm ?subrr ?normr0 //.
by rewrite ltrW // [_ < 0%CR i]creal_lt_always.
by close.
move=> /(@le_creal_neqVlt zero_algcreal) /= [].
by move<-; apply: eq_crealP; exists m0=> * /=; rewrite !(normr0, subrr).
move=> x_gt0; apply: eq_crealP; exists_big_modulus m F.
move=> e i e_gt0 hi /=; rewrite [`|x i|]ger0_norm ?subrr ?normr0 //.
by rewrite ltrW // creal_gt0_always.
by close.
Qed.
(**********************************************************************)
(* Theory of the "domain" of algebraic numbers: polynomial + interval *)
(**********************************************************************)
CoInductive algdom := AlgDom {
annul_algdom : {poly F};
center_alg : F;
radius_alg : F;
_ : annul_algdom \is monic;
_ : radius_alg >= 0;
_ : annul_algdom.[center_alg - radius_alg]
* annul_algdom.[center_alg + radius_alg] <= 0
}.
Lemma radius_alg_ge0 x : 0 <= radius_alg x. Proof. by case: x. Qed.
Lemma monic_annul_algdom x : annul_algdom x \is monic. Proof. by case: x. Qed.
Hint Resolve monic_annul_algdom.
Lemma annul_algdom_eq0 x : (annul_algdom x == 0) = false.
Proof. by rewrite (negPf (monic_neq0 _)). Qed.
Lemma algdomP x : (annul_algdom x).[center_alg x - radius_alg x]
* (annul_algdom x).[center_alg x + radius_alg x] <= 0.
Proof. by case: x. Qed.
Definition algdom' := seq F.
Definition encode_algdom (x : algdom) : algdom' :=
[:: center_alg x, radius_alg x & (annul_algdom x)].
Definition decode_algdom (x : algdom') : option algdom :=
if x is [::c, r & p']
then let p := Poly p' in
if ((p \is monic) =P true, (r >= 0) =P true,
(p.[c - r] * p.[c + r] <= 0) =P true)
is (ReflectT monic_p, ReflectT r_gt0, ReflectT hp)
then Some (AlgDom monic_p r_gt0 hp)
else None
else None.
Lemma encode_algdomK : pcancel encode_algdom decode_algdom.
Proof.
case=> p c r monic_p r_ge0 hp /=; rewrite polyseqK.
do 3?[case: eqP; rewrite ?monic_p ?r_ge0 ?monic_p //] => monic_p' r_ge0' hp'.
by congr (Some (AlgDom _ _ _)); apply: bool_irrelevance.
Qed.
Definition algdom_EqMixin := PcanEqMixin encode_algdomK.
Canonical algdom_eqType := EqType algdom algdom_EqMixin.
Definition algdom_ChoiceMixin := PcanChoiceMixin encode_algdomK.
Canonical algdom_choiceType := ChoiceType algdom algdom_ChoiceMixin.
Fixpoint to_algcreal_of (p : {poly F}) (c r : F) (i : nat) : F :=
match i with
| 0 => c
| i.+1 =>
let c' := to_algcreal_of p c r i in
if p.[c' - r / 2%:R ^+ i] * p.[c'] <= 0
then c' - r / 2%:R ^+ i.+1
else c' + r / 2%:R ^+ i.+1
end.
Lemma to_algcreal_of_recP p c r i : 0 <= r ->
`|to_algcreal_of p c r i.+1 - to_algcreal_of p c r i| <= r * 2%:R ^- i.+1.
Proof.
move=> r_ge0 /=; case: ifP=> _; rewrite addrAC subrr add0r ?normrN ger0_norm //;
by rewrite mulr_ge0 ?invr_ge0 ?exprn_ge0 ?ler0n.
Qed.
Lemma to_algcreal_ofP p c r i j : 0 <= r -> (i <= j)%N ->
`|to_algcreal_of p c r j - to_algcreal_of p c r i| <= r * 2%:R ^- i.
Proof.
move=> r_ge0 leij; pose r' := r * 2%:R ^- j * (2%:R ^+ (j - i) - 1).
rewrite (@ler_trans _ r') //; last first.
rewrite /r' -mulrA ler_wpmul2l // ler_pdivr_mull ?exprn_gt0 ?ltr0n //.
rewrite -{2}(subnK leij) exprD mulfK ?gtr_eqF ?exprn_gt0 ?ltr0n //.
by rewrite ger_addl lerN10.
rewrite /r' subrX1 addrK mul1r -{1 2}(subnK leij); set f := _ c r.
elim: (_ - _)%N=> [|k ihk]; first by rewrite subrr normr0 big_ord0 mulr0 lerr.
rewrite addSn big_ord_recl /= mulrDr.
rewrite (ler_trans (ler_dist_add (f (k + i)%N) _ _)) //.
rewrite ler_add ?expr0 ?mulr1 ?to_algcreal_of_recP // (ler_trans ihk) //.
rewrite exprSr invfM -!mulrA !ler_wpmul2l ?invr_ge0 ?exprn_ge0 ?ler0n //.
by rewrite mulr_sumr ler_sum // => l _ /=; rewrite exprS mulKf ?pnatr_eq0.
Qed.
Lemma alg_to_crealP (x : algdom) :
creal_axiom (to_algcreal_of (annul_algdom x) (center_alg x) (radius_alg x)).
Proof.
pose_big_modulus m F.
exists m=> e i j e_gt0 hi hj.
wlog leij : i j {hi} hj / (j <= i)%N.
move=> hwlog; case/orP: (leq_total i j)=> /hwlog; last exact.
by rewrite distrC; apply.
rewrite (ler_lt_trans (to_algcreal_ofP _ _ _ _)) ?radius_alg_ge0 //.
rewrite ltr_pdivr_mulr ?gtr0E // -ltr_pdivr_mull //.
by rewrite upper_nthrootP.
by close.
Qed.
Definition alg_to_creal x := CReal (alg_to_crealP x).
Lemma exp2k_crealP : @creal_axiom F (fun i => 2%:R ^- i).
Proof.
pose_big_modulus m F.
exists m=> e i j e_gt0 hi hj.
wlog leij : i j {hj} hi / (i <= j)%N.
move=> hwlog; case/orP: (leq_total i j)=> /hwlog; first exact.
by rewrite distrC; apply.
rewrite ger0_norm ?subr_ge0; last first.
by rewrite ?lef_pinv -?topredE /= ?gtr0E // ler_eexpn2l ?ltr1n.
rewrite -(@ltr_pmul2l _ (2%:R ^+ i )) ?gtr0E //.
rewrite mulrBr mulfV ?gtr_eqF ?gtr0E //.
rewrite (@ler_lt_trans _ 1) // ?ger_addl ?oppr_le0 ?mulr_ge0 ?ger0E //.
by rewrite -ltr_pdivr_mulr // mul1r upper_nthrootP.
by close.
Qed.
Definition exp2k_creal := CReal exp2k_crealP.
Lemma exp2k_creal_eq0 : (exp2k_creal == 0)%CR.
Proof.
apply: eq_crealP; exists_big_modulus m F.
move=> e i e_gt0 hi /=.
rewrite subr0 gtr0_norm ?gtr0E // -ltf_pinv -?topredE /= ?gtr0E //.
by rewrite invrK upper_nthrootP.
by close.
Qed.
Notation lbound0_of p := (@lbound0P _ _ p _ _ _).
Lemma to_algcrealP (x : algdom) : ((annul_algdom x).[alg_to_creal x] == 0)%CR.
Proof.
set u := alg_to_creal _; set p := annul_algdom _.
pose r := radius_alg x; pose cr := cst_creal r.
have: ((p).[u - cr * exp2k_creal] * (p).[u + cr * exp2k_creal] <= 0)%CR.
apply: (@le_crealP _ 0%N)=> i _ /=.
rewrite -/p -/r; set c := center_alg _.
elim: i=> /= [|i].
by rewrite !expr0 divr1 algdomP.
set c' := to_algcreal_of _ _ _=> ihi.
have [] := lerP (_ * p.[c' i]).
rewrite addrNK -addrA -opprD -mulr2n -[_ / _ *+ _]mulr_natr.
by rewrite -mulrA exprSr invfM mulfVK ?pnatr_eq0.
rewrite addrK -addrA -mulr2n -[_ / _ *+ _]mulr_natr.
rewrite -mulrA exprSr invfM mulfVK ?pnatr_eq0 // => /ler_pmul2l<-.
rewrite mulr0 mulrCA !mulrA [X in X * _]mulrAC -mulrA.
by rewrite mulr_ge0_le0 // -expr2 exprn_even_ge0.
rewrite exp2k_creal_eq0 mul_creal0 opp_creal0 add_creal0.
move=> hu pu0; apply: hu; pose e := (lbound pu0).
pose_big_enough i.
apply: (@lt_crealP _ (e * e) i i) => //.
by rewrite !pmulr_rgt0 ?invr_gt0 ?ltr0n ?lbound_gt0.
rewrite add0r [u]lock /= -!expr2.
rewrite -[_.[_] ^+ _]ger0_norm ?exprn_even_ge0 // normrX.
rewrite ler_pexpn2r -?topredE /= ?lbound_ge0 ?normr_ge0 //.
by rewrite -lock (ler_trans _ (lbound0_of pu0)).
by close.
Qed.
Definition to_algcreal_rec (x : algdom) :=
AlgCReal (monic_annul_algdom x) (@to_algcrealP x).
(* "Encoding" function from algdom to algcreal *)
Definition to_algcreal := locked to_algcreal_rec.
(* "Decoding" function, constructed interactively *)
Lemma to_algdom_exists (x : algcreal) :
{ y : algdom | (to_algcreal y == x)%CR }.
Proof.
pose p := annul_creal x.
move: {2}(size p) (leqnn (size p))=> n.
elim: n x @p=> [x p|n ihn x p le_sp_Sn].
by rewrite leqn0 size_poly_eq0 /p annul_creal_eq0.
move: le_sp_Sn; rewrite leq_eqVlt.
have [|//|eq_sp_Sn _] := ltngtP.
by rewrite ltnS=> /ihn ihnp _; apply: ihnp.
have px0 := @root_annul_creal x; rewrite -/p -/root in px0.
have [|ncop] := boolP (coprimep p p^`()).
move/coprimep_root => /(_ _ px0) /deriv_neq0_mono [r r_gt0 [i ir sm]].
have p_chg_sign : p.[x i - r] * p.[x i + r] <= 0.
have [/accr_pos_incr hp|/accr_neg_decr hp] := sm.
have hpxj : forall j, (i <= j)%N ->
(p.[x i - r] <= p.[x j]) * (p.[x j] <= p.[x i + r]).
move=> j hj.
suff: p.[x i - r] <= p.[x j] <= p.[x i + r] by case/andP=> -> ->.
rewrite !hp 1?addrAC ?subrr ?add0r ?normrN;
rewrite ?(gtr0_norm r_gt0) //;
do ?by rewrite ltrW ?cauchymodP ?(leq_trans _ hj).
by rewrite -ler_distl ltrW ?cauchymodP ?(leq_trans _ hj).
rewrite mulr_le0_ge0 //; apply/le_creal_cst; rewrite -px0;
by apply: (@le_crealP _ i)=> h hj /=; rewrite hpxj.
have hpxj : forall j, (i <= j)%N ->
(p.[x i + r] <= p.[x j]) * (p.[x j] <= p.[x i - r]).
move=> j hj.
suff: p.[x i + r] <= p.[x j] <= p.[x i - r] by case/andP=> -> ->.
rewrite !hp 1?addrAC ?subrr ?add0r ?normrN;
rewrite ?(gtr0_norm r_gt0) //;
do ?by rewrite ltrW ?cauchymodP ?(leq_trans _ hj).
by rewrite andbC -ler_distl ltrW ?cauchymodP ?(leq_trans _ hj).
rewrite mulr_ge0_le0 //; apply/le_creal_cst; rewrite -px0;
by apply: (@le_crealP _ i)=> h hj /=; rewrite hpxj.
pose y := (AlgDom (monic_annul_creal x) (ltrW r_gt0) p_chg_sign).
have eq_py_px: (p.[to_algcreal y] == p.[x])%CR.
rewrite /to_algcreal -lock.
by have := @to_algcrealP y; rewrite /= -/p=> ->; apply: eq_creal_sym.
exists y.
move: sm=> /strong_mono_bound [k k_gt0 hk].
rewrite -/p; apply: eq_crealP.
exists_big_modulus m F.
move=> e j e_gt0 hj; rewrite (ler_lt_trans (hk _ _ _ _)) //.
+ rewrite /to_algcreal -lock.
rewrite (ler_trans (to_algcreal_ofP _ _ _ (leq0n _))) ?(ltrW r_gt0) //.
by rewrite expr0 divr1.
+ by rewrite ltrW // cauchymodP.
rewrite -ltr_pdivl_mull //.
by rewrite (@eq_modP _ _ _ eq_py_px) // ?pmulr_rgt0 ?invr_gt0.
by close.
case: (@smaller_factor _ p p^`() x); rewrite ?monic_annul_creal //.
rewrite gtNdvdp // -?size_poly_eq0 size_deriv eq_sp_Sn //=.
apply: contra ncop=> /eqP n_eq0; move: eq_sp_Sn; rewrite n_eq0.
by move=> /eqP /size_poly1P [c c_neq0 ->]; rewrite derivC coprimep0 polyC_eqp1.
move=> r /andP [hsr monic_r rx_eq0].
apply: (ihn (AlgCReal monic_r rx_eq0))=> /=.
by rewrite -ltnS -eq_sp_Sn.
Qed.
Definition to_algdom x := projT1 (to_algdom_exists x).
Lemma to_algdomK x : (to_algcreal (to_algdom x) == x)%CR.
Proof. by rewrite /to_algdom; case: to_algdom_exists. Qed.
Lemma eq_algcreal_to_algdom x : eq_algcreal (to_algcreal (to_algdom x)) x.
Proof. by apply/eq_algcrealP; apply: to_algdomK. Qed.
(* Explicit encoding to a choice type *)
Canonical eq_algcreal_encModRel := EncModRel eq_algcreal eq_algcreal_to_algdom.
Local Open Scope quotient_scope.
(***************************************************************************)
(* Algebraic numbers are the quotient of algcreal by their setoid equality *)
(***************************************************************************)
Definition alg := {eq_quot eq_algcreal}.
Definition alg_of of (phant F) := alg.
Identity Coercion type_alg_of : alg_of >-> alg.
Notation "{ 'alg' F }" := (alg_of (Phant F)).
(* A lot of structure is inherited *)
Canonical alg_eqType := [eqType of alg].
Canonical alg_choiceType := [choiceType of alg].
Canonical alg_quotType := [quotType of alg].
Canonical alg_eqQuotType := [eqQuotType eq_algcreal of alg].
Canonical alg_of_eqType := [eqType of {alg F}].
Canonical alg_of_choiceType := [choiceType of {alg F}].
Canonical alg_of_quotType := [quotType of {alg F}].
Canonical alg_of_eqQuotType := [eqQuotType eq_algcreal of {alg F}].
Definition to_alg_def (phF : phant F) : F -> {alg F} :=
lift_embed {alg F} cst_algcreal.
Notation to_alg := (@to_alg_def (Phant F)).
Notation "x %:RA" := (to_alg x)
(at level 2, left associativity, format "x %:RA").
Local Notation "p ^ f" := (map_poly f p) : ring_scope.
Canonical to_alg_pi_morph := PiEmbed to_alg.
Local Notation zero_alg := 0%:RA.
Local Notation one_alg := 1%:RA.
Lemma equiv_alg (x y : algcreal) : (x == y)%CR <-> (x = y %[mod {alg F}]).
Proof.
split; first by move=> /eq_algcrealP /eqquotP ->.
by move=> /eqquotP /eq_algcrealP.
Qed.
Lemma nequiv_alg (x y : algcreal) : reflect (x != y)%CR (x != y %[mod {alg F}]).
Proof. by rewrite eqquotE; apply: neq_algcrealP. Qed.
Arguments nequiv_alg [x y].
Prenex Implicits nequiv_alg.
Lemma pi_algK (x : algcreal) : (repr (\pi_{alg F} x) == x)%CR.
Proof. by apply/equiv_alg; rewrite reprK. Qed.
Definition add_alg := lift_op2 {alg F} add_algcreal.
Lemma pi_add : {morph \pi_{alg F} : x y / add_algcreal x y >-> add_alg x y}.
Proof. by unlock add_alg=> x y; rewrite -equiv_alg /= !pi_algK. Qed.
Canonical add_pi_morph := PiMorph2 pi_add.
Definition opp_alg := lift_op1 {alg F} opp_algcreal.
Lemma pi_opp : {morph \pi_{alg F} : x / opp_algcreal x >-> opp_alg x}.
Proof. by unlock opp_alg=> x; rewrite -equiv_alg /= !pi_algK. Qed.
Canonical opp_pi_morph := PiMorph1 pi_opp.
Definition mul_alg := lift_op2 {alg F} mul_algcreal.
Lemma pi_mul : {morph \pi_{alg F} : x y / mul_algcreal x y >-> mul_alg x y}.
Proof. by unlock mul_alg=> x y; rewrite -equiv_alg /= !pi_algK. Qed.
Canonical mul_pi_morph := PiMorph2 pi_mul.
Definition inv_alg := lift_op1 {alg F} inv_algcreal.
Lemma pi_inv : {morph \pi_{alg F} : x / inv_algcreal x >-> inv_alg x}.
Proof.
unlock inv_alg=> x; symmetry; rewrite -equiv_alg /= /inv_algcreal.
case: eq_algcreal_dec=> /= [|x'_neq0].
by rewrite pi_algK; case: eq_algcreal_dec.
move: x'_neq0 (x'_neq0); rewrite {1}pi_algK.
case: eq_algcreal_dec=> // x'_neq0' x_neq0 x'_neq0 /=.
by apply: eq_creal_inv; rewrite pi_algK.
Qed.
Canonical inv_pi_morph := PiMorph1 pi_inv.
Lemma add_algA : associative add_alg.
Proof.
elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; rewrite !piE -equiv_alg.
by apply: eq_crealP; exists m0=> * /=; rewrite addrA subrr normr0.
Qed.
Lemma add_algC : commutative add_alg.
Proof.
elim/quotW=> x; elim/quotW=> y; rewrite !piE -equiv_alg /=.
by apply: eq_crealP; exists m0=> * /=; rewrite [X in _ - X]addrC subrr normr0.
Qed.
Lemma add_0alg : left_id zero_alg add_alg.
Proof. by elim/quotW=> x; rewrite !piE -equiv_alg /= add_0creal. Qed.
Lemma add_Nalg : left_inverse zero_alg opp_alg add_alg.
Proof.
elim/quotW=> x; rewrite !piE -equiv_alg /=.
by apply: eq_crealP; exists m0=> *; rewrite /= addNr subr0 normr0.
Qed.
Definition alg_zmodMixin := ZmodMixin add_algA add_algC add_0alg add_Nalg.
Canonical alg_zmodType := Eval hnf in ZmodType alg alg_zmodMixin.
Canonical alg_of_zmodType := Eval hnf in ZmodType {alg F} alg_zmodMixin.
Lemma add_pi x y : \pi_{alg F} x + \pi_{alg F} y
= \pi_{alg F} (add_algcreal x y).
Proof. by rewrite [_ + _]piE. Qed.
Lemma opp_pi x : - \pi_{alg F} x = \pi_{alg F} (opp_algcreal x).
Proof. by rewrite [- _]piE. Qed.
Lemma zeroE : 0 = \pi_{alg F} zero_algcreal.
Proof. by rewrite [0]piE. Qed.
Lemma sub_pi x y : \pi_{alg F} x - \pi_{alg F} y
= \pi_{alg F} (add_algcreal x (opp_algcreal y)).
Proof. by rewrite [_ - _]piE. Qed.
Lemma mul_algC : commutative mul_alg.
Proof.
elim/quotW=> x; elim/quotW=> y; rewrite !piE -equiv_alg /=.
by apply: eq_crealP; exists m0=> * /=; rewrite mulrC subrr normr0.
Qed.
Lemma mul_algA : associative mul_alg.
Proof.
elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; rewrite !piE -equiv_alg /=.
by apply: eq_crealP; exists m0=> * /=; rewrite mulrA subrr normr0.
Qed.
Lemma mul_1alg : left_id one_alg mul_alg.
Proof. by elim/quotW=> x; rewrite piE -equiv_alg /= mul_1creal. Qed.
Lemma mul_alg_addl : left_distributive mul_alg add_alg.
Proof.
elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; rewrite !piE -equiv_alg /=.
by apply: eq_crealP; exists m0=> * /=; rewrite mulrDl subrr normr0.
Qed.
Arguments neq_creal_cst [F x y].
Prenex Implicits neq_creal_cst.
Lemma nonzero1_alg : one_alg != zero_alg.
Proof. by rewrite piE -(rwP neq_algcrealP) (rwP neq_creal_cst) oner_eq0. Qed.
Definition alg_comRingMixin :=
ComRingMixin mul_algA mul_algC mul_1alg mul_alg_addl nonzero1_alg.
Canonical alg_Ring := Eval hnf in RingType alg alg_comRingMixin.
Canonical alg_comRing := Eval hnf in ComRingType alg mul_algC.
Canonical alg_of_Ring := Eval hnf in RingType {alg F} alg_comRingMixin.
Canonical alg_of_comRing := Eval hnf in ComRingType {alg F} mul_algC.
Lemma mul_pi x y : \pi_{alg F} x * \pi_{alg F} y
= \pi_{alg F} (mul_algcreal x y).
Proof. by rewrite [_ * _]piE. Qed.
Lemma oneE : 1 = \pi_{alg F} one_algcreal.
Proof. by rewrite [1]piE. Qed.
Lemma mul_Valg (x : alg) : x != zero_alg -> mul_alg (inv_alg x) x = one_alg.
Proof.
elim/quotW: x=> x; rewrite piE -(rwP neq_algcrealP) /= => x_neq0.
apply/eqP; rewrite piE; apply/eq_algcrealP; rewrite /= /inv_algcreal.
case: eq_algcreal_dec=> [/(_ x_neq0) //|/= x_neq0'].
apply: eq_crealP; exists_big_modulus m F.
by move=> * /=; rewrite mulVf ?subrr ?normr0 ?creal_neq0_always.
by close.
Qed.
Lemma inv_alg0 : inv_alg zero_alg = zero_alg.
Proof.
rewrite !piE -equiv_alg /= /inv_algcreal.
by case: eq_algcreal_dec=> //= zero_neq0; move: (eq_creal_refl zero_neq0).
Qed.
Lemma to_alg_additive : additive to_alg.
Proof.
move=> x y /=; rewrite !piE sub_pi -equiv_alg /=.
by apply: eq_crealP; exists m0=> * /=; rewrite subrr normr0.
Qed.
Canonical to_alg_is_additive := Additive to_alg_additive.
Lemma to_alg_multiplicative : multiplicative to_alg.
Proof.
split=> [x y |] //; rewrite !piE mul_pi -equiv_alg.
by apply: eq_crealP; exists m0=> * /=; rewrite subrr normr0.
Qed.
Canonical to_alg_is_rmorphism := AddRMorphism to_alg_multiplicative.
Lemma expn_pi (x : algcreal) (n : nat) :
(\pi_{alg F} x) ^+ n = \pi (exp_algcreal x n).
Proof.
rewrite /exp_algcreal; case: n=> [|n]; first by rewrite expr0 oneE.
rewrite exprS iteropS; elim: n=> /= [|n ihn]; rewrite ?expr0 ?mulr1 //.
by rewrite exprS ihn mul_pi.
Qed.
Lemma horner_pi (p : {poly F}) (x : algcreal) :
(p ^ to_alg).[\pi_alg x] = \pi (horner_algcreal p x).
Proof.
rewrite horner_coef /horner_algcreal size_map_poly.
apply: (big_ind2 (fun x y => x = \pi_alg y)).
+ by rewrite zeroE.
+ by move=> u u' v v' -> ->; rewrite [_ + _]piE.
by move=> i /= _; rewrite expn_pi coef_map /= [_ * _]piE.
Qed.
(* Defining annihilating polynomials for algebraics *)
Definition annul_alg : {alg F} -> {poly F} := locked (annul_creal \o repr).
Lemma root_annul_algcreal (x : algcreal) : ((annul_alg (\pi x)).[x] == 0)%CR.
Proof. by unlock annul_alg; rewrite /= -pi_algK root_annul_creal. Qed.
Lemma root_annul_alg (x : {alg F}) : root ((annul_alg x) ^ to_alg) x.
Proof.
apply/rootP; rewrite -[x]reprK horner_pi /= zeroE -equiv_alg.
by rewrite horner_algcrealE root_annul_algcreal.
Qed.
Lemma monic_annul_alg (x : {alg F}) : annul_alg x \is monic.
Proof. by unlock annul_alg; rewrite monic_annul_creal. Qed.
Lemma annul_alg_neq0 (x : {alg F}) : annul_alg x != 0.
Proof. by rewrite monic_neq0 ?monic_annul_alg. Qed.
Definition AlgFieldUnitMixin := FieldUnitMixin mul_Valg inv_alg0.
Canonical alg_unitRing :=
Eval hnf in UnitRingType alg AlgFieldUnitMixin.
Canonical alg_comUnitRing := Eval hnf in [comUnitRingType of alg].
Canonical alg_of_unitRing :=
Eval hnf in UnitRingType {alg F} AlgFieldUnitMixin.
Canonical alg_of_comUnitRing := Eval hnf in [comUnitRingType of {alg F}].
Lemma field_axiom : GRing.Field.mixin_of alg_unitRing. Proof. exact. Qed.
Definition AlgFieldIdomainMixin := (FieldIdomainMixin field_axiom).
Canonical alg_iDomain :=
Eval hnf in IdomainType alg (FieldIdomainMixin field_axiom).
Canonical alg_fieldType := FieldType alg field_axiom.
Canonical alg_of_iDomain :=
Eval hnf in IdomainType {alg F} (FieldIdomainMixin field_axiom).
Canonical alg_of_fieldType := FieldType {alg F} field_axiom.
Lemma inv_pi x : (\pi_{alg F} x)^-1 = \pi_{alg F} (inv_algcreal x).
Proof. by rewrite [_^-1]piE. Qed.
Lemma div_pi x y : \pi_{alg F} x / \pi_{alg F} y
= \pi_{alg F} (mul_algcreal x (inv_algcreal y)).
Proof. by rewrite [_ / _]piE. Qed.
Definition lt_alg := lift_fun2 {alg F} lt_algcreal.
Definition le_alg := lift_fun2 {alg F} le_algcreal.
Lemma lt_alg_pi : {mono \pi_{alg F} : x y / lt_algcreal x y >-> lt_alg x y}.
Proof.
move=> x y; unlock lt_alg; rewrite /lt_algcreal.
by do 2!case: ltVge_algcreal_dec=> //=; rewrite !pi_algK.
Qed.
Canonical lt_alg_pi_mono := PiMono2 lt_alg_pi.
Lemma le_alg_pi : {mono \pi_{alg F} : x y / le_algcreal x y >-> le_alg x y}.
Proof.
move=> x y; unlock le_alg; rewrite /le_algcreal.
by do 2!case: ltVge_algcreal_dec=> //=; rewrite !pi_algK.
Qed.
Canonical le_alg_pi_mono := PiMono2 le_alg_pi.
Definition norm_alg := lift_op1 {alg F} norm_algcreal.
Lemma norm_alg_pi : {morph \pi_{alg F} : x / norm_algcreal x >-> norm_alg x}.
Proof.
move=> x; unlock norm_alg; rewrite /norm_algcreal /le_algcreal.
by do 2!case: ltVge_algcreal_dec=> //=; rewrite !(pi_opp, pi_algK, reprK).
Qed.
Canonical norm_alg_pi_morph := PiMorph1 norm_alg_pi.
(* begin hide *)
(* Lemma norm_pi (x : algcreal) : `|\pi_{alg F} x| = \pi (norm_algcreal x). *)
(* Proof. by rewrite /norm_algcreal -lt_pi -zeroE -lerNgt fun_if -opp_pi. Qed. *)
(* end hide *)
Lemma add_alg_gt0 x y : lt_alg zero_alg x -> lt_alg zero_alg y ->
lt_alg zero_alg (x + y).
Proof.
rewrite -[x]reprK -[y]reprK !piE -!(rwP lt_algcrealP).
move=> x_gt0 y_gt0; pose_big_enough i.
apply: (@lt_crealP _ (diff x_gt0 + diff y_gt0) i i) => //.
by rewrite addr_gt0 ?diff_gt0.
by rewrite /= add0r ler_add // ?diff0P.
by close.
Qed.
Lemma mul_alg_gt0 x y : lt_alg zero_alg x -> lt_alg zero_alg y ->
lt_alg zero_alg (x * y).
Proof.
rewrite -[x]reprK -[y]reprK !piE -!(rwP lt_algcrealP).
move=> x_gt0 y_gt0; pose_big_enough i.
apply: (@lt_crealP _ (diff x_gt0 * diff y_gt0) i i) => //.
by rewrite pmulr_rgt0 ?diff_gt0.
rewrite /= add0r (@ler_trans _ (diff x_gt0 * (repr y) i)) //.
by rewrite ler_wpmul2l ?(ltrW (diff_gt0 _)) // diff0P.
by rewrite ler_wpmul2r ?diff0P ?ltrW ?creal_gt0_always.
by close.
Qed.
Lemma gt0_alg_nlt0 x : lt_alg zero_alg x -> ~~ lt_alg x zero_alg.
Proof.
rewrite -[x]reprK !piE -!(rwP lt_algcrealP, rwP le_algcrealP).
move=> hx; pose_big_enough i.
apply: (@le_crealP _ i)=> j /= hj.
by rewrite ltrW // creal_gt0_always.
by close.
Qed.
Lemma sub_alg_gt0 x y : lt_alg zero_alg (y - x) = lt_alg x y.
Proof.
rewrite -[x]reprK -[y]reprK !piE; apply/lt_algcrealP/lt_algcrealP=> /= hxy.
pose_big_enough i.
apply: (@lt_crealP _ (diff hxy) i i); rewrite ?diff_gt0 //.
by rewrite (monoLR (addNKr _) (ler_add2l _)) addrC diff0P.
by close.
pose_big_enough i.
apply: (@lt_crealP _ (diff hxy) i i); rewrite ?diff_gt0 //.
by rewrite (monoRL (addrK _) (ler_add2r _)) add0r addrC diffP.
by close.
Qed.
Lemma lt0_alg_total (x : alg) : x != zero_alg ->
lt_alg zero_alg x || lt_alg x zero_alg.
Proof.
rewrite -[x]reprK !piE => /neq_algcrealP /= x_neq0.
apply/orP; rewrite -!(rwP lt_algcrealP).
case/neq_creal_ltVgt: x_neq0=> /= [lt_x0|lt_0x]; [right|by left].
pose_big_enough i.
by apply: (@lt_crealP _ (diff lt_x0) i i); rewrite ?diff_gt0 ?diffP.
by close.
Qed.
Lemma norm_algN x : norm_alg (- x) = norm_alg x.
Proof.
rewrite -[x]reprK !piE /= -equiv_alg !norm_algcrealE; apply: eq_crealP.
exists_big_modulus m F=> [e i e_gt0 hi /=|].
by rewrite normrN subrr normr0.
by close.
Qed.
Lemma ge0_norm_alg x : le_alg 0 x -> norm_alg x = x.
Proof. by rewrite -[x]reprK !piE /= /norm_algcreal => ->. Qed.
Lemma lt_alg0N (x : alg) : lt_alg 0 (- x) = lt_alg x 0.
Proof. by rewrite -sub0r sub_alg_gt0. Qed.
Lemma lt_alg00 : lt_alg zero_alg zero_alg = false.
Proof. by have /implyP := @gt0_alg_nlt0 0; case: lt_alg. Qed.
Lemma le_alg_def x y : le_alg x y = (y == x) || lt_alg x y.
Proof.
rewrite -[x]reprK -[y]reprK eq_sym piE [lt_alg _ _]piE; apply/le_algcrealP/orP.
move=> /le_creal_neqVlt [/eq_algcrealP/eqquotP/eqP-> //|lt_xy]; first by left.
by right; apply/lt_algcrealP.
by move=> [/eqP/eqquotP/eq_algcrealP-> //| /lt_algcrealP /lt_crealW].
Qed.
Definition AlgNumFieldMixin := RealLtMixin add_alg_gt0 mul_alg_gt0
gt0_alg_nlt0 sub_alg_gt0 lt0_alg_total norm_algN ge0_norm_alg le_alg_def.
Canonical alg_numDomainType := NumDomainType alg AlgNumFieldMixin.
Canonical alg_numFieldType := [numFieldType of alg].
Canonical alg_of_numDomainType := [numDomainType of {alg F}].
Canonical alg_of_numFieldType := [numFieldType of {alg F}].
Definition AlgRealFieldMixin := RealLeAxiom alg.
Canonical alg_realDomainType := RealDomainType alg AlgRealFieldMixin.
Canonical alg_realFieldType := [realFieldType of alg].
Canonical alg_of_realDomainType := [realDomainType of {alg F}].
Canonical alg_of_realFieldType := [realFieldType of {alg F}].
Lemma lt_pi x y : \pi_{alg F} x < \pi y = lt_algcreal x y.
Proof. by rewrite [_ < _]lt_alg_pi. Qed.
Lemma le_pi x y : \pi_{alg F} x <= \pi y = le_algcreal x y.
Proof. by rewrite [_ <= _]le_alg_pi. Qed.
Lemma norm_pi (x : algcreal) : `|\pi_{alg F} x| = \pi (norm_algcreal x).
Proof. by rewrite [`|_|]piE. Qed.
Lemma lt_algP (x y : algcreal) : reflect (x < y)%CR (\pi_{alg F} x < \pi y).
Proof. by rewrite lt_pi; apply: lt_algcrealP. Qed.
Arguments lt_algP [x y].
Lemma le_algP (x y : algcreal) : reflect (x <= y)%CR (\pi_{alg F} x <= \pi y).
Proof. by rewrite le_pi; apply: le_algcrealP. Qed.
Arguments le_algP [x y].
Prenex Implicits lt_algP le_algP.
Lemma ler_to_alg : {mono to_alg : x y / x <= y}.
Proof.
apply: homo_mono=> x y lt_xy; rewrite !piE -(rwP lt_algP).
by apply/lt_creal_cst; rewrite lt_xy.
Qed.
Lemma ltr_to_alg : {mono to_alg : x y / x < y}.
Proof. by apply: lerW_mono; apply: ler_to_alg. Qed.
Lemma normr_to_alg : { morph to_alg : x / `|x| }.
Proof.
move=> x /=; have [] := ger0P; have [] := ger0P x%:RA;
rewrite ?rmorph0 ?rmorphN ?oppr0 //=.
by rewrite ltr_to_alg lerNgt => ->.
by rewrite ler_to_alg ltrNge => ->.
Qed.
Lemma inf_alg_proof x : {d | 0 < d & 0 < x -> (d%:RA < x)}.
Proof.
have [|] := lerP; first by exists 1.
elim/quotW: x=> x; rewrite zeroE=> /lt_algP /= x_gt0.
exists (diff x_gt0 / 2%:R); first by rewrite pmulr_rgt0 ?gtr0E ?diff_gt0.
rewrite piE -(rwP lt_algP) /= => _; pose_big_enough i.
apply: (@lt_crealP _ (diff x_gt0 / 2%:R) i i) => //.
by rewrite pmulr_rgt0 ?gtr0E ?diff_gt0.
by rewrite -[_ + _](splitf 2) diff0P.
by close.