-
Notifications
You must be signed in to change notification settings - Fork 0
/
UrealAddAssoc.v
6740 lines (6669 loc) · 229 KB
/
UrealAddAssoc.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
(* Reals between 0 and 1; associativity of addition *)
Require Import Utf8 Arith NPeano Psatz PeanoNat.
Require Import Misc Summation Rational Ureal UrealNorm UrealAddAssoc1.
Import Q.Notations.
Import List.ListNotations.
Set Nested Proofs Allowed.
Theorem pred_rad_lt_rad {r : radix} : rad - 1 < rad.
Proof.
specialize radix_ge_2 as H; lia.
Qed.
Definition digit_9 {r : radix} := mkdig _ (rad - 1) pred_rad_lt_rad.
Definition ureal_999 {r : radix} := {| ureal i := digit_9 |}.
Definition ureal_shift {r : radix} k x := {| ureal i := ureal x (k + i) |}.
Arguments ureal_shift _ _ x%F.
Theorem all_9_fA_ge_1_ε {r : radix} : ∀ u i,
(∀ k, u (i + k + 1) = rad - 1)
→ ∀ k, fA_ge_1_ε u i k = true.
Proof.
intros * Hur *.
specialize radix_ge_2 as Hr.
apply A_ge_1_true_iff.
rewrite A_all_9; [ | intros j Hj; apply Hur ].
rewrite Q.frac_small. 2: {
split.
-apply Q.le_add_le_sub_l.
rewrite Q.add_0_l.
replace 1%Q with (1 // 1)%Q by easy.
apply Q.le_pair_mono_l; split; [ pauto | now apply Nat_pow_ge_1 ].
-apply Q.sub_lt, Q.lt_0_pair; pauto.
}
apply Q.sub_le_mono; [ easy | ].
apply Q.le_pair_mono_l; split; [ apply Nat.neq_0_lt_0; pauto | ].
apply Nat.pow_le_mono_r; [ easy | min_n_ge ].
Qed.
Theorem all_fA_ge_1_ε_carry {r : radix} : ∀ u i,
(∀ k, fA_ge_1_ε u i k = true)
→ ∀ k, carry u (i + k) = Q.intg (A (i + k) (min_n (i + k)) u).
Proof.
intros *.
specialize radix_ge_2 as Hr.
intros Haut *.
clear - Haut.
unfold carry, carry_cases.
destruct (LPO_fst (fA_ge_1_ε u (i + k))) as [H1| H1]. {
now rewrite Nat.add_0_r.
}
destruct H1 as (j & Hjj & Hj).
specialize (Haut (k + j)) as H1.
apply A_ge_1_add_r_true_if in H1.
now rewrite Hj in H1.
Qed.
Theorem all_fA_ge_1_ε_carry_carry {r : radix} : ∀ u i,
(∀ k, u (i + k) ≤ 3 * (rad - 1))
→ (∀ k, fA_ge_1_ε u i k = true)
→ ∀ k,
carry u (i + k) =
Q.intg
((u (i + k + 1) + carry u (i + k + 1))%nat // rad +
Q.frac (A (i + k + 1) (min_n (i + k + 1)) u) * 1 // rad)%Q.
Proof.
intros *.
specialize radix_ge_2 as Hr.
intros Hmr Haut *.
rewrite all_fA_ge_1_ε_carry; [ | easy ].
assert (Hmr' : ∀ l, u (i + k + l) ≤ 3 * (rad - 1)). {
intros; rewrite <- Nat.add_assoc; apply Hmr.
}
assert (Haut' : ∀ l, fA_ge_1_ε u (i + k) l = true). {
intros l; apply A_ge_1_add_r_true_if, Haut.
}
specialize (three_lt_rad_pow (i + k)) as H.
replace (i + k) with (i + k + 0) at 2 by easy.
rewrite <- (all_fA_ge_1_ε_NQintg_A 3 (i + k) u H Hmr' Haut' 0 rad).
clear H.
unfold carry, carry_cases.
destruct (LPO_fst (fA_ge_1_ε u (i + k + 1))) as [H1| H1]. 2: {
destruct H1 as (j & Hjj & Hj).
specialize (Haut (k + 1 + j)) as H1.
apply A_ge_1_add_r_true_if in H1.
now rewrite Nat.add_assoc, Hj in H1.
}
clear H1.
rewrite A_split_first; [ | min_n_ge ].
replace (S (i + k)) with (i + k + 1) by flia.
rewrite Q.pair_add_l, <- Q.add_assoc.
rewrite <- (Q.mul_pair_den_num (Q.intg _) 1); [ | easy ].
rewrite <- Q.mul_add_distr_r.
rewrite (min_n_add _ 1), Nat.mul_1_r.
f_equal; f_equal; f_equal.
rewrite Q.intg_frac at 1; [ | easy ].
do 2 rewrite Nat.add_0_r.
f_equal; symmetry.
now rewrite min_n_add, Nat.mul_1_r.
Qed.
Theorem P_999_after_7_ge_17 {r : radix} : ∀ m u i,
m ≤ rad
→ (∀ k, u (i + k) ≤ m * (rad - 1))
→ (∀ k, fA_ge_1_ε u i k = true)
→ ∀ j, 1 ≤ j ≤ m
→ u (i + 1) = j * rad - m
→ u (i + 2) ≥ (m - 1) * rad - m ∧ carry u (i + 1) = m - 1.
Proof.
intros *.
specialize radix_ge_2 as Hr.
intros Hmr Hur Hau * Hj Hu1 *.
destruct (zerop m) as [Hmz| Hmz]. {
rewrite Hmz, Nat.sub_0_r in Hu1.
specialize (Hur 1) as H1.
rewrite Hmz, Nat.mul_0_l, Hu1 in H1.
apply Nat.le_0_r in H1.
apply Nat.eq_mul_0 in H1.
destruct H1 as [H1| H1]; [ flia Hj H1 | flia Hr H1 ].
}
apply Nat.neq_0_lt_0 in Hmz.
specialize (all_fA_ge_1_ε_P_999 u i Hau 0) as H1.
rewrite Nat.add_0_r in H1.
unfold P, d2n, prop_carr, dig in H1.
rewrite Hu1 in H1.
replace j with (j - 1 + 1) in H1 by flia Hj.
rewrite Nat.mul_add_distr_r, Nat.mul_1_l in H1.
rewrite <- Nat.add_sub_assoc in H1; [ | easy ].
rewrite <- Nat.add_assoc in H1.
rewrite Nat.add_comm in H1.
rewrite Nat.mod_add in H1; [ | easy ].
rewrite Nat.add_comm in H1.
specialize (carry_upper_bound_for_adds m u i Hmz) as Hcm.
assert (H : ∀ k, u (i + k + 1) ≤ m * (rad - 1)). {
now intros; rewrite <- Nat.add_assoc.
}
specialize (Hcm H); clear H.
rewrite Nat.mod_small in H1. 2: {
specialize (Hcm 1) as H2.
flia Hmr H2.
}
assert (H2 : carry u (i + 1) = m - 1) by flia H1 Hmz Hmr.
split; [ | easy ].
unfold carry in H2.
apply Q.intg_interv in H2; [ | easy ].
rewrite A_split_first in H2; [ | min_n_ge ].
replace (S (i + 1)) with (i + 2) in H2 by easy.
destruct H2 as (H2, H3).
apply Nat.nlt_ge; intros H4.
apply Q.nlt_ge in H2; apply H2; clear H2.
remember (min_n (i + 1 + carry_cases u (i + 1))) as n eqn:Hn.
eapply Q.lt_le_trans. {
apply (Q.lt_pair_mono_r _ _ rad) in H4.
apply Q.add_lt_le_mono; [ apply H4 | ].
apply Q.mul_le_mono_pos_r; [ apply Q.lt_0_pair; pauto | ].
apply (A_upper_bound_for_adds m).
now intros; do 2 rewrite <- Nat.add_assoc.
}
rewrite <- (Q.mul_pair_den_num _ 1); [ | easy ].
rewrite <- Q.mul_add_distr_r.
apply (Q.mul_le_mono_pos_r (rad // 1)%Q); [ now apply Q.lt_0_pair | ].
rewrite <- Q.mul_assoc.
rewrite Q.mul_inv_pair; [ | easy | easy ].
rewrite Q.mul_1_r.
rewrite <- Q.pair_mul_r.
rewrite Q.mul_sub_distr_l, Q.mul_1_r.
rewrite Q.add_sub_assoc.
eapply Q.le_trans. {
apply Q.le_sub_l.
apply Q.le_0_mul_r; [ easy | ].
apply Q.le_0_pair.
}
rewrite Q.pair_sub_l; [ | flia H4 ].
now rewrite Q.sub_add.
Qed.
Theorem A_mul_inv_rad_interv {r : radix} : ∀ m u i j n,
m ≤ rad
→ (∀ k, u (i + k) ≤ m * (rad - 1))
→ i ≤ j + 1
→ (0 ≤ A j n u * 1 // rad < 1)%Q.
Proof.
intros * Hm Hur Hj.
split; [ now apply Q.le_0_mul_r | ].
apply (Q.mul_lt_mono_pos_r (rad // 1)%Q). {
now apply Q.lt_0_pair.
}
rewrite <- Q.mul_assoc.
rewrite Q.mul_pair_den_num; [ | easy ].
rewrite Q.mul_1_r, Q.mul_1_l.
eapply Q.le_lt_trans. {
apply A_upper_bound_for_adds.
intros p.
replace (j + p + 1) with (i + (j + p + 1 - i)).
apply Hur.
intros; rewrite <- Nat.add_assoc; flia Hj.
}
rewrite Q.mul_sub_distr_l, Q.mul_1_r.
destruct (zerop m) as [Hmz| Hmz]. {
subst m; cbn.
specialize radix_ge_2 as Hr.
now destruct rad.
}
apply (Q.lt_le_trans _ (m // 1)). {
apply Q.sub_lt.
apply Q.mul_pos_cancel_l; [ | easy ].
now apply Q.lt_0_pair.
}
apply Q.le_pair; [ easy | easy | ].
now rewrite Nat.mul_1_r, Nat.mul_1_l.
Qed.
Theorem carry_succ_lemma1 {r : radix} : ∀ u a,
(0 ≤ a)%Q
→ (Q.frac (u // rad) + Q.frac (a * 1 // rad) < 1)%Q
→ u / rad + Q.intg (a * (1 // rad)%Q) = (u + Q.intg a) / rad.
Proof.
intros * Haz H3.
specialize radix_ge_2 as Hr.
rewrite Q.frac_pair in H3.
rewrite <- (Q.mul_pair_den_num _ 1) in H3; [ | easy ].
apply (Q.mul_lt_mono_pos_r (rad // 1)%Q) in H3. 2: {
now apply Q.lt_0_pair.
}
rewrite Q.mul_add_distr_r in H3.
rewrite <- Q.mul_assoc, Q.mul_1_l in H3.
rewrite Q.mul_pair_den_num in H3; [ | easy ].
rewrite Q.mul_1_r in H3.
specialize (Nat.div_mod u rad radix_ne_0) as H5.
symmetry; rewrite H5 at 1.
rewrite Nat.mul_comm, <- Nat.add_assoc, Nat.add_comm.
rewrite Nat.div_add; [ | easy ].
rewrite Nat.add_comm; f_equal.
specialize (Nat.div_mod (u mod rad + Q.intg a) rad radix_ne_0) as H7.
remember ((u mod rad + Q.intg a) / rad) as m eqn:Hm.
symmetry.
apply Q.intg_interv; [ now apply Q.le_0_mul_r | ].
split. {
apply (Q.mul_le_mono_pos_r (rad // 1)); [ now apply Q.lt_0_pair | ].
rewrite <- Q.mul_assoc.
rewrite Q.mul_pair_den_num; [ | easy ].
rewrite Q.mul_1_r, <- Q.pair_mul_r.
apply Q.nlt_ge; intros H10.
rewrite (Q.frac_less_small (m - 1)) in H3. 2: {
split. 2: {
rewrite <- (Q.pair_add_l _ 1).
rewrite Nat.sub_add. 2: {
apply Nat.nlt_ge; intros Hnz.
apply Nat.lt_1_r in Hnz; rewrite Hnz in H10.
cbn in H10.
now apply Q.nle_gt in H10; apply H10.
}
apply (Q.mul_lt_mono_pos_r (rad // 1)); [ now apply Q.lt_0_pair | ].
rewrite <- Q.mul_assoc.
rewrite Q.mul_pair_den_num; [ | easy ].
rewrite Q.mul_1_r.
now rewrite <- Q.pair_mul_l.
}
apply (Q.mul_le_mono_pos_r (rad // 1)); [ now apply Q.lt_0_pair | ].
rewrite <- Q.mul_assoc.
rewrite Q.mul_pair_den_num; [ | easy ].
rewrite Q.mul_1_r.
rewrite <- Q.pair_mul_l.
rewrite Nat.mul_sub_distr_r, Nat.mul_1_l.
rewrite Q.pair_sub_l. 2: {
destruct m; [ | cbn; flia ].
cbn in H10; exfalso.
now apply Q.nle_gt in H10; apply H10.
}
apply Q.le_sub_le_add_r.
rewrite Hm.
rewrite (Q.num_den a) at 2; [ | easy ].
rewrite Q.add_pair; [ | easy | easy ].
do 2 rewrite Nat.mul_1_r.
apply Q.le_pair; [ easy | easy | ].
rewrite Nat.mul_1_l.
remember (u mod rad + Q.intg a) as x eqn:Hx.
apply (le_trans _ (x * Q.den a)). {
apply Nat.mul_le_mono_r.
rewrite Nat.mul_comm.
now apply Nat.mul_div_le.
}
subst x.
rewrite Nat.mul_add_distr_r, Nat.add_comm.
apply Nat.add_le_mono. {
rewrite (Q.num_den a) at 1; [ | easy ].
rewrite Q.intg_pair; [ | easy ].
rewrite Nat.mul_comm.
now apply Nat.mul_div_le.
}
rewrite Nat.mul_comm.
apply Nat.mul_le_mono_l.
now apply Nat.lt_le_incl, Nat.mod_upper_bound.
}
rewrite Q.mul_sub_distr_r in H3.
rewrite <- Q.mul_assoc in H3.
rewrite Q.mul_pair_den_num in H3; [ | easy ].
rewrite Q.mul_1_r in H3.
rewrite <- Q.pair_mul_l in H3.
rewrite Q.add_sub_assoc in H3.
apply Q.lt_sub_lt_add_l in H3.
rewrite <- Q.pair_add_l in H3.
replace rad with (1 * rad) in H3 at 3 by flia.
rewrite <- Nat.mul_add_distr_r in H3.
rewrite Nat.sub_add in H3. 2: {
apply Nat.nlt_ge; intros Hnz.
apply Nat.lt_1_r in Hnz; rewrite Hnz in H10.
cbn in H10.
now apply Q.nle_gt in H10; apply H10.
}
apply Q.nle_gt in H3; apply H3; clear H3.
rewrite Hm.
rewrite (Q.num_den a) at 2; [ | easy ].
rewrite Q.add_pair; [ | easy | easy ].
do 2 rewrite Nat.mul_1_l.
apply Q.le_pair; [ easy | easy | ].
rewrite Nat.mul_1_l.
remember (u mod rad + Q.intg a) as x eqn:Hx.
apply (le_trans _ (x * Q.den a)). {
apply Nat.mul_le_mono_r.
rewrite Nat.mul_comm.
now apply Nat.mul_div_le.
}
subst x.
rewrite Nat.mul_add_distr_r.
apply Nat.add_le_mono_l.
rewrite (Q.num_den a) at 1; [ | easy ].
rewrite Q.intg_pair; [ | easy ].
rewrite Nat.mul_comm.
now apply Nat.mul_div_le.
}
apply (Q.mul_lt_mono_pos_r (rad // 1)); [ now apply Q.lt_0_pair | ].
rewrite <- Q.mul_assoc.
rewrite Q.mul_pair_den_num; [ | easy ].
rewrite Q.mul_1_r.
rewrite <- (Q.pair_add_l _ 1).
rewrite <- Q.pair_mul_r.
specialize (Q.intg_interv (Q.intg a) a) as H10.
specialize (proj2 (H10 Haz) eq_refl) as (H11, H12); clear H10.
eapply Q.lt_le_trans; [ apply H12 | ].
apply Q.le_add_le_sub_l.
rewrite <- (Q.pair_sub_l _ 1). 2: {
rewrite Nat.mul_add_distr_r; flia Hr.
}
apply Q.le_pair_mono_r.
apply Nat.le_add_le_sub_r.
rewrite Hm, Nat.mul_add_distr_r, Nat.mul_1_l.
apply (le_trans _ (Q.intg a / rad * rad + rad)). 2: {
apply Nat.add_le_mono_r.
apply Nat.mul_le_mono_r.
apply Nat.div_le_mono; [ easy | flia ].
}
specialize (Nat.div_mod (Q.intg a) rad radix_ne_0) as H10.
rewrite Nat.mul_comm in H10.
rewrite H10 at 1.
rewrite <- Nat.add_assoc.
apply Nat.add_le_mono_l.
rewrite Nat.add_comm.
now apply Nat.mod_upper_bound.
Qed.
Theorem carry_succ_lemma2 {r : radix} : ∀ u a,
(0 ≤ a)%Q
→ (1 ≤ Q.frac (u // rad) + Q.frac (a * 1 // rad))%Q
→ u / rad + Q.intg (a * (1 // rad)%Q) + 1 = (u + Q.intg a) / rad.
Proof.
intros * Haz H3.
rewrite Q.frac_pair in H3.
rewrite <- (Q.mul_pair_den_num _ 1) in H3; [ | easy ].
apply (Q.mul_le_mono_pos_r (rad // 1)%Q) in H3. 2: {
now apply Q.lt_0_pair.
}
rewrite Q.mul_add_distr_r in H3.
rewrite <- Q.mul_assoc, Q.mul_1_l in H3.
rewrite Q.mul_pair_den_num in H3; [ | easy ].
rewrite Q.mul_1_r in H3.
specialize (Nat.div_mod u rad radix_ne_0) as H5.
symmetry; rewrite H5 at 1.
rewrite Nat.mul_comm, <- Nat.add_assoc, Nat.add_comm.
rewrite Nat.div_add; [ | easy ].
rewrite Nat.add_comm, <- Nat.add_assoc; f_equal.
specialize (Nat.div_mod (u mod rad + Q.intg a) rad radix_ne_0) as H7.
remember ((u mod rad + Q.intg a) / rad) as m eqn:Hm.
destruct m. {
exfalso.
symmetry in Hm.
apply Nat.div_small_iff in Hm; [ | easy ].
clear H7.
rewrite Q.frac_small in H3. 2: {
split; [ now apply Q.le_0_mul_r | ].
apply (Q.mul_lt_mono_pos_r (rad // 1)); [ now apply Q.lt_0_pair | ].
rewrite <- Q.mul_assoc.
rewrite Q.mul_pair_den_num; [ | easy ].
rewrite Q.mul_1_r, Q.mul_1_l.
apply Q.intg_lt_lt; [ easy | flia Hm ].
}
rewrite <- Q.mul_assoc in H3.
rewrite Q.mul_pair_den_num in H3; [ | easy ].
rewrite Q.mul_1_r in H3.
apply Q.nlt_ge in H3; apply H3; clear H3.
apply Q.intg_lt_lt. {
apply Q.le_0_add; [ apply Q.le_0_pair | easy ].
}
rewrite Q.intg_add_cond; [ | apply Q.le_0_pair | easy ].
rewrite Q.intg_pair; [ | easy ].
rewrite Nat.div_1_r, Q.frac_pair, Nat.mod_1_r.
rewrite Q.add_0_l.
destruct (Q.lt_le_dec (Q.frac a) 1) as [H3| H3]. {
now rewrite Nat.add_0_r.
}
exfalso; apply Q.nlt_ge in H3; apply H3.
apply Q.frac_lt_1.
}
rewrite <- Nat.add_1_r in Hm.
rewrite Nat.add_1_r; f_equal; symmetry.
apply Q.intg_interv; [ now apply Q.le_0_mul_r | ].
assert (Hma : (m // 1 ≤ a * 1 // rad)%Q). {
apply (Q.mul_le_mono_pos_r (rad // 1)); [ now apply Q.lt_0_pair | ].
rewrite <- Q.mul_assoc.
rewrite Q.mul_pair_den_num; [ | easy ].
rewrite Q.mul_1_r, <- Q.pair_mul_r.
apply (Q.add_le_mono_r _ _ (rad // 1)).
rewrite Q.add_pair; [ | easy | easy ].
do 2 rewrite Nat.mul_1_r.
rewrite <- Nat.mul_add_distr_r, Hm.
remember (u mod rad + Q.intg a) as x eqn:Hx.
apply (Q.le_trans _ (x // 1)). {
apply Q.le_pair_mono_r; rewrite Nat.mul_comm.
now apply Nat.mul_div_le.
}
rewrite Hx, Nat.add_comm.
rewrite Q.pair_add_l.
apply Q.add_le_mono. {
rewrite Q.intg_to_frac; [ | easy ].
now apply Q.le_sub_l.
}
apply Q.le_pair; [ easy | easy | ].
rewrite Nat.mul_1_r, Nat.mul_1_l.
now apply Nat.lt_le_incl, Nat.mod_upper_bound.
}
split; [ easy | ].
apply (Q.mul_lt_mono_pos_r (rad // 1)); [ now apply Q.lt_0_pair | ].
rewrite <- Q.mul_assoc.
rewrite Q.mul_pair_den_num; [ | easy ].
rewrite Q.mul_1_r.
rewrite <- (Q.pair_add_l _ 1).
rewrite <- Q.pair_mul_r.
apply (Q.mul_le_mono_pos_r (rad // 1)) in Hma; [ | now apply Q.lt_0_pair ].
rewrite <- Q.mul_assoc in Hma.
rewrite Q.mul_pair_den_num in Hma; [ | easy ].
rewrite Q.mul_1_r in Hma.
rewrite <- Q.pair_mul_r in Hma.
clear - Hm Hma H3 Haz.
move H3 at bottom.
assert (H8 : rad ≤ Q.intg a mod rad + u mod rad). {
apply Nat.nlt_ge; intros H8.
apply Nat.lt_add_lt_sub_r in H8.
apply Q.nlt_ge in H3; apply H3; clear H3.
rewrite (Q.num_den a); [ | easy ].
rewrite Q.mul_pair; [ | easy | easy ].
rewrite Nat.mul_1_r, Q.frac_pair, <- Q.pair_mul_l.
rewrite Q.mul_pair_mono_r; [ | easy | easy ].
rewrite Q.add_pair; [ | easy | easy ].
do 2 rewrite Nat.mul_1_l.
apply Q.lt_pair; [ easy | easy | ].
rewrite Nat.mul_1_r.
rewrite Nat.mod_mul_r; [ | easy | easy ].
rewrite (Nat.mul_comm (Q.den a)).
rewrite Nat.add_assoc, Nat.add_shuffle0, <- Nat.mul_add_distr_r.
apply Nat.lt_add_lt_sub_l.
rewrite Nat.mul_comm.
rewrite <- Nat.mul_sub_distr_r.
eapply Nat.lt_le_trans; [ now apply Nat.mod_upper_bound | ].
replace (Q.den a) with (1 * Q.den a) at 1 by flia.
apply Nat.mul_le_mono_r.
unfold Q.intg in H8; flia H8.
}
specialize (proj2 (Q.intg_interv (Q.intg a) a Haz) eq_refl) as H.
eapply Q.lt_le_trans; [ apply H | ].
rewrite <- (Q.pair_add_l _ 1).
apply Q.le_pair; [ easy | easy | ].
rewrite Nat.mul_1_r, Nat.mul_1_l.
eapply Q.le_lt_trans in Hma; [ clear H | apply H ].
remember (Q.intg a) as b eqn:Hb.
rewrite <- (Q.pair_add_l _ 1) in Hma.
apply Q.lt_pair in Hma; [ | easy | easy ].
rewrite Nat.mul_1_r, Nat.mul_1_l in Hma.
clear a Haz Hb H3.
specialize (Nat.mod_upper_bound u rad radix_ne_0) as Hu.
remember (u mod rad) as a eqn:Ha.
rewrite Nat.add_comm in H8.
clear u Ha.
symmetry in Hm.
specialize (Nat.div_mod (a + b) rad radix_ne_0) as H1.
rewrite Hm in H1.
apply (Nat.add_le_mono_l _ _ a).
rewrite Nat.add_assoc.
rewrite H1.
rewrite Nat.mul_comm, <- Nat.add_assoc, (Nat.add_comm).
apply Nat.add_le_mono_r.
rewrite <- Nat.add_mod_idemp_r; [ | easy ].
rewrite (Nat_mod_less_small 1). 2: {
rewrite Nat.mul_1_l; split; [ easy | ].
rewrite Nat.mul_add_distr_r, Nat.mul_1_l.
apply Nat.add_lt_mono; [ easy | ].
now apply Nat.mod_upper_bound.
}
rewrite Nat.mul_1_l.
rewrite <- Nat.add_sub_swap; [ | easy ].
apply Nat.le_sub_le_add_r.
rewrite <- Nat.add_assoc.
apply Nat.add_le_mono_l.
rewrite Nat.add_comm.
now apply Nat.mod_upper_bound.
Qed.
Theorem carry_succ_lemma3 {r : radix} : ∀ u a,
(0 ≤ a)%Q
→ Q.intg ((u // rad)%Q + (a * 1 // rad)%Q) = (u + Q.intg a) / rad.
Proof.
intros * Ha.
rewrite Q.intg_add_cond; [ | apply Q.le_0_pair | now apply Q.le_0_mul_r ].
rewrite Q.intg_pair; [ | easy ].
destruct
(Q.lt_le_dec (Q.frac (u // rad) + Q.frac (a * (1 // rad)%Q)) 1)
as [H3| H3]. {
rewrite Nat.add_0_r.
now apply carry_succ_lemma1.
}
now apply carry_succ_lemma2.
Qed.
Theorem carry_succ {r : radix} : ∀ m u i,
m < rad ^ (rad * (i + 3) - (i + 2))
→ (∀ k, u (i + k) ≤ m * (rad - 1))
→ carry u i = (u (i + 1) + carry u (i + 1)) / rad.
Proof.
intros *.
specialize radix_ge_2 as Hr.
intros Hmrr Hur.
assert (Hmrj : ∀ j, m < rad ^ (rad * (i + j + 3) - i - j - 2)). {
intros j.
eapply lt_le_trans; [ apply Hmrr | ].
apply Nat.pow_le_mono_r; [ easy | ].
rewrite Nat.sub_add_distr.
apply Nat.sub_le_mono_r.
rewrite Nat_sub_sub_swap.
apply Nat.sub_le_mono_r.
rewrite Nat.add_shuffle0.
rewrite (Nat.mul_add_distr_l _ (i + 3)).
rewrite <- Nat.add_sub_assoc; [ flia | ].
destruct rad as [| rr]; [ easy | cbn; flia ].
}
unfold carry, carry_cases.
destruct (LPO_fst (fA_ge_1_ε u i)) as [H1| H1]. {
specialize (all_fA_ge_1_ε_P_999 u i H1 0) as H6.
rewrite Nat.add_0_r in H6.
unfold P, d2n, prop_carr, dig in H6.
unfold carry, carry_cases in H6.
destruct (LPO_fst (fA_ge_1_ε u (i + 1))) as [H2| H2]. {
do 2 rewrite Nat.add_0_r.
rewrite <- (all_fA_ge_1_ε_NQintg_A' m i) with (k := 1); try easy.
rewrite A_split_first; [ | min_n_ge ].
replace (S i) with (i + 1) by flia.
remember (A (i + 1) (min_n (i + 1)) u) as a eqn:Ha.
rewrite <- (Q.mul_pair_den_num _ 1); [ | easy ].
rewrite <- Q.mul_add_distr_r.
remember ((u (i + 1) + Q.intg a) / rad) as n eqn:Hn.
symmetry in Hn.
apply (Q.intg_less_small n).
split. {
rewrite <- Hn.
apply (Q.mul_le_mono_pos_r (rad // 1)); [ now apply Q.lt_0_pair | ].
rewrite <- Q.mul_assoc, Q.mul_pair_den_num; [ | easy ].
rewrite Q.mul_1_r, <- Q.pair_mul_r.
rewrite (Q.num_den a); [ | now rewrite Ha ].
rewrite Q.add_pair; [ | easy | easy ].
do 2 rewrite Nat.mul_1_l.
apply Q.le_pair; [ easy | easy | ].
rewrite Nat.mul_1_l.
rewrite Q.intg_pair; [ | easy ].
eapply le_trans. {
apply Nat.mul_le_mono_r.
rewrite Nat.mul_comm.
now apply Nat.mul_div_le.
}
rewrite Nat.mul_add_distr_r.
apply Nat.add_le_mono_l.
rewrite Nat.mul_comm.
now apply Nat.mul_div_le.
}
specialize (Nat.div_mod (u (i + 1) + Q.intg a) rad radix_ne_0) as H3.
rewrite Nat.add_0_r, <- Ha in H6.
rewrite Hn, H6 in H3.
apply (Q.mul_lt_mono_pos_r (rad // 1)); [ now apply Q.lt_0_pair | ].
rewrite <- Q.mul_assoc, Q.mul_pair_den_num; [ | easy ].
rewrite Q.mul_1_r.
rewrite Q.mul_add_distr_r, Q.mul_1_l.
rewrite <- Q.pair_mul_r, <- Q.pair_add_l.
replace rad with ((rad - 1) + 1) at 2 by flia Hr.
rewrite Nat.mul_comm, Nat.add_assoc, <- H3.
rewrite <- Nat.add_assoc, Q.pair_add_l.
apply Q.add_lt_mono_l.
rewrite Q.pair_add_l.
specialize (Q.intg_interv (Q.intg a) a) as H4.
assert (H : (0 ≤ a)%Q) by now rewrite Ha.
specialize (proj2 (H4 H) eq_refl) as H5; clear H H4.
now destruct H5 as (H4, H5).
}
destruct H2 as (j & Hjj & Hj).
now rewrite A_ge_1_add_r_true_if in Hj.
}
destruct H1 as (j & Hjj & Hj).
assert
(H3 :
∀ k, j ≤ k →
Q.intg (A i (min_n (i + k)) u) = Q.intg (A i (min_n (i + j)) u)). {
intros k Hk.
apply (fA_lt_1_ε_NQintg_A m); try easy.
now unfold min_n.
}
rewrite <- (H3 (j + 1)); [ | flia ].
destruct (LPO_fst (fA_ge_1_ε u (i + 1))) as [H2| H2]. {
specialize (all_fA_ge_1_ε_P_999 u (i + 1) H2 0) as H6.
rewrite Nat.add_0_r in H6.
unfold P, d2n, prop_carr, dig in H6.
unfold carry, carry_cases in H6.
destruct (LPO_fst (fA_ge_1_ε u (i + 1 + 1))) as [H1| H1]. 2: {
destruct H1 as (k & Hjk & Hk).
now rewrite A_ge_1_add_r_true_if in Hk.
}
symmetry.
rewrite Nat.add_0_r.
rewrite <- (all_fA_ge_1_ε_NQintg_A' m) with (k := j); try easy; cycle 1. {
do 2 rewrite Nat.sub_add_distr; apply Hmrj.
} {
now intros; rewrite <- Nat.add_assoc.
}
symmetry.
rewrite A_split_first; [ | min_n_ge ].
replace (S i) with (i + 1) by flia.
rewrite Nat.add_assoc, Nat.add_shuffle0.
now apply carry_succ_lemma3.
}
destruct H2 as (k & Hjk & Hk).
assert
(H4 :
∀ p, k ≤ p →
Q.intg (A (i + 1) (min_n (i + 1 + p)) u) =
Q.intg (A (i + 1) (min_n (i + 1 + k)) u)). {
intros p Hp.
apply (fA_lt_1_ε_NQintg_A m); try easy. {
unfold min_n.
replace (i + 1 + k + 3) with (i + (1 + k) + 3) by flia.
rewrite Nat.sub_add_distr.
now rewrite <- (Nat.sub_add_distr _ 1).
}
now intros q; rewrite <- Nat.add_assoc.
}
rewrite H3; [ | flia ].
rewrite <- (H3 (j + k + 1)); [ | flia ].
rewrite <- (H4 (j + k)); [ | flia ].
rewrite A_split_first; [ | min_n_ge ].
replace (S i) with (i + 1) by flia.
replace (i + (j + k + 1)) with (i + 1 + (j + k)) by flia.
now apply carry_succ_lemma3.
Qed.
Theorem carry_succ_m_le_rad {r : radix} : ∀ m u i,
m ≤ rad
→ (∀ k, u (i + k) ≤ m * (rad - 1))
→ carry u i = (u (i + 1) + carry u (i + 1)) / rad.
Proof.
intros * Hmr Hur.
apply (carry_succ m); [ | easy ].
apply (le_lt_trans _ rad); [ easy | ].
specialize radix_ge_2 as Hr.
replace rad with (rad ^ 1) at 1 by apply Nat.pow_1_r.
apply Nat.pow_lt_mono_r; [ easy | ].
destruct rad as [| rr]; [ easy | ].
destruct rr; [ flia Hr | cbn; flia ].
Qed.
Theorem P_999_after_7_gt {r : radix} : ∀ m u i,
m ≤ rad
→ (∀ k, u (i + k) ≤ m * (rad - 1))
→ (∀ k, fA_ge_1_ε u i k = true)
→ ∀ j, 1 ≤ j ≤ m
→ u (i + 1) = j * rad - m
→ u (i + 2) ≥ (m - 1) * rad.
Proof.
intros *.
specialize radix_ge_2 as Hr.
intros Hmr Hur Hau * Hj Hu1 *.
destruct (zerop m) as [Hmz| Hmz]; [ flia Hmz Hj | ].
move Hmz before Hmr.
specialize (P_999_after_7_ge_17 m u i Hmr Hur Hau _ Hj Hu1) as (Hu2lb, Hc1).
destruct (Nat.eq_dec m 1) as [Hm| Hm]; [ rewrite Hm; cbn; flia | ].
assert (Hmg : m ≥ 2) by flia Hmz Hm.
move Hmg before Hmr; clear Hmz Hm.
destruct (Nat.eq_dec (u (i + 2)) ((m - 1) * rad - m)) as [Hu2| Hu2]. {
exfalso; clear Hu2lb.
specialize (P_999_after_7_ge_17 m u (i + 1) Hmr) as H2.
replace (i + 1 + 1) with (i + 2) in H2 by flia.
replace (i + 1 + 2) with (i + 3) in H2 by flia.
assert (H : ∀ k, u (i + 1 + k) ≤ m * (rad - 1)). {
now intros; rewrite <- Nat.add_assoc.
}
specialize (H2 H); clear H.
assert (H : ∀ k, fA_ge_1_ε u (i + 1) k = true). {
now intros; apply A_ge_1_add_r_true_if.
}
specialize (H2 H (m - 1)); clear H.
assert (H : 1 ≤ m - 1 ≤ m) by flia Hmg.
specialize (H2 H Hu2); clear H.
destruct H2 as (Hu3, Hc2).
specialize (carry_succ_m_le_rad m u (i + 1) Hmr) as H1.
replace (i + 1 + 1) with (i + 2) in H1 by flia.
assert (H : ∀ k, u (i + 1 + k) ≤ m * (rad - 1)). {
now intros; rewrite <- Nat.add_assoc.
}
specialize (H1 H); clear H.
rewrite Hc1, Hc2, Hu2 in H1.
apply (Nat.add_cancel_r _ _ 1) in H1.
rewrite Nat.sub_add in H1; [ | flia Hmg ].
rewrite <- Nat.div_add in H1; [ | easy ].
rewrite Nat.mul_1_l, <- Nat.add_assoc in H1.
rewrite <- Nat.add_sub_swap in H1. 2: {
rewrite Nat.mul_comm.
destruct rad as [| rr]; [ easy | ].
destruct rr; [ flia Hr | cbn; flia Hmg ].
}
rewrite <- Nat.add_sub_assoc in H1; [ | flia Hmr ].
rewrite Nat.add_comm in H1.
rewrite Nat.div_add in H1; [ | easy ].
replace (m - 1 + rad - m) with (rad - 1) in H1 by flia Hmg.
rewrite Nat.div_small in H1; [ flia H1 Hmg | flia Hr ].
}
assert (H : u (i + 2) ≥ (m - 1) * rad - m + 1) by flia Hu2lb Hu2.
move H before Hu2lb; clear Hu2lb Hu2; rename H into Hu2lb.
specialize (carry_succ_m_le_rad m u (i + 1) Hmr) as H1.
assert (H : ∀ k, u (i + 1 + k) ≤ m * (rad - 1)). {
now intros; rewrite <- Nat.add_assoc.
}
specialize (H1 H); clear H.
replace (i + 1 + 1) with (i + 2) in H1 by flia.
specialize (all_fA_ge_1_ε_P_999 u i Hau 1) as H2.
replace (i + 1 + 1) with (i + 2) in H2 by flia.
unfold P, d2n, prop_carr, dig in H2.
specialize (Nat.div_mod (u (i + 2) + carry u (i + 2)) rad) as H3.
specialize (H3 radix_ne_0).
rewrite <- H1, H2, Hc1 in H3; clear H1 H2.
specialize (carry_upper_bound_for_adds m u i) as Hc2.
assert (H : m ≠ 0) by flia Hmg.
specialize (Hc2 H); clear H.
assert (H : ∀ k, u (i + k + 1) ≤ m * (rad - 1)). {
now intros; rewrite <- Nat.add_assoc.
}
specialize (Hc2 H 2); clear H.
clear - Hmr H3 Hc2 Hmg Hu2lb.
flia Hmr H3 Hc2 Hmg Hu2lb.
Qed.
Theorem P_999_once_after_7 {r : radix} : ∀ m u i,
m ≤ rad
→ (∀ k, u (i + k) ≤ m * (rad - 1))
→ (∀ k, fA_ge_1_ε u i k = true)
→ ∀ j, 1 ≤ j ≤ m
→ u (i + 1) = j * rad - m
→ u (i + 2) = m * (rad - 1).
Proof.
intros *.
specialize radix_ge_2 as Hr.
intros Hmr Hur Hau * Hj Hu1 *.
specialize (P_999_after_7_gt m u i Hmr Hur Hau j Hj Hu1) as H1.
specialize (P_999_start u (i + 2) m) as H2.
assert (H : ∀ k, u (i + 2 + k) ≤ m * (rad - 1)). {
now intros; rewrite <- Nat.add_assoc.
}
specialize (H2 H); clear H.
assert (H : ∀ k, P u (i + 2 + k) = rad - 1). {
intros.
replace (i + 2 + k) with (i + (k + 1) + 1) by flia.
now apply all_fA_ge_1_ε_P_999.
}
specialize (H2 H); clear H.
destruct (lt_dec rad m) as [H| H]; [ flia Hmr H | clear H ].
destruct (Nat.eq_dec (u (i + 2)) (m * (rad - 1))) as [Hu| Hu]; [ easy | ].
destruct H2 as (H2 & H3 & H4).
remember (u (i + 2) / rad + 1) as j1 eqn:Hj1.
remember (carry u (i + 2) + 1) as k1 eqn:Hk1.
move k1 before j1; move Hk1 before Hj1.
exfalso.
apply Nat.nlt_ge in H1; apply H1; clear H1.
rewrite H4.
apply (lt_le_trans _ (j1 * rad)). {
apply Nat.sub_lt; [ | flia H3 ].
replace k1 with (1 * k1) by flia.
apply Nat.mul_le_mono; [ easy | flia H3 Hmr ].
}
apply Nat.mul_le_mono_r.
flia H2.
Qed.
Theorem P_999_after_7 {r : radix} : ∀ m u i,
m ≤ rad
→ (∀ k, u (i + k) ≤ m * (rad - 1))
→ (∀ k, fA_ge_1_ε u i k = true)
→ ∀ j, 1 ≤ j ≤ m
→ u (i + 1) = j * rad - m
→ ∀ k, u (i + k + 2) = m * (rad - 1).
Proof.
intros *.
specialize radix_ge_2 as Hr.
intros Hmr Hur Hau * Hj Hu1 *.
induction k. {
rewrite Nat.add_0_r.
now eapply P_999_once_after_7.
}
replace (i + k + 2) with (i + S k + 1) in IHk by flia.
rewrite Nat.mul_sub_distr_l, Nat.mul_1_r in IHk.
apply P_999_once_after_7 with (j0 := m); [ easy | | | flia Hj | easy ]. {
now intros p; rewrite <- Nat.add_assoc.
} {
now intros p; apply A_ge_1_add_r_true_if.
}
Qed.
Theorem rad_2_sum_2_half_A_lt_1 {r : radix} : ∀ i n u,
rad = 2
→ (∀ k, u (i + k) ≤ 2)
→ (A i n u * 1 // 2 < 1)%Q.
Proof.
intros * Hr2 Hu.
specialize (A_mul_inv_rad_interv 2 u i i n radix_ge_2) as H1.
rewrite Hr2 in H1.
specialize (H1 Hu).
assert (H : i ≤ i + 1) by flia.
specialize (H1 H); clear H.
now destruct H1.
Qed.
(* ça serait achement plus cool si au lieu de l'hypothèse
(∀ k, fA_ge_1_ε u i k = true), j'avais
(∀ k, P u (i + k) = rad - 1), mais c'est compliqué
du fait que c'est une somme de 3 *)
Theorem sum_3_all_fA_true_8_not_8 {r : radix} : ∀ u i,
(∀ k, u (i + k) ≤ 3 * (rad - 1))
→ (∀ k, fA_ge_1_ε u i k = true)
→ u (i + 1) = rad - 2
→ u (i + 2) ≠ rad - 2.
Proof.
intros *.
specialize radix_ge_2 as Hr.
intros Hu3 Hau Hu1 Hu2.
specialize (all_fA_ge_1_ε_P_999 _ _ Hau) as Hpu.
assert (Hc3 : ∀ k, carry u (i + k) < 3). {
specialize (carry_upper_bound_for_adds 3 u i) as H6.
assert (H : 3 ≠ 0) by easy.
specialize (H6 H); clear H.
assert (H : ∀ k, u (i + k + 1) ≤ 3 * (rad - 1)). {
intros p; rewrite <- Nat.add_assoc; apply Hu3.
}
now specialize (H6 H).
}
assert (Hci1 : carry u (i + 1) mod rad = 1). {
specialize (Hpu 0) as H1.
rewrite Nat.add_0_r in H1.
unfold P, d2n, prop_carr, dig in H1.
rewrite Hu1 in H1.
rewrite <- Nat.add_mod_idemp_r in H1; [ | easy ].
remember (carry u (i + 1) mod rad) as c eqn:Hc.
symmetry in Hc.
destruct c; [ rewrite Nat.add_0_r, Nat.mod_small in H1; flia Hr H1 | ].
destruct c; [ easy | exfalso ].
replace (rad - 2 + S (S c)) with (rad + c) in H1 by flia Hr.
rewrite Nat_mod_add_same_l in H1; [ | easy ].
destruct c. {
rewrite Nat.mod_0_l in H1; [ flia Hr H1 | easy ].
}
specialize (Hc3 1) as H2.
apply Nat.nle_gt in H2; apply H2; clear H2.
specialize (Nat.div_mod (carry u (i + 1)) rad radix_ne_0) as H2.
rewrite H2, Hc; flia.
}
assert (Hci2 : carry u (i + 2) = 1). {
specialize (Hpu 1) as H1.
unfold P, d2n, prop_carr in H1; cbn in H1.
rewrite <- Nat.add_assoc in H1; replace (1 + 1) with 2 in H1 by easy.
rewrite Hu2 in H1.
destruct (Nat.eq_dec (carry u (i + 2)) 0) as [Hc20| Hc20]. {
rewrite Hc20, Nat.add_0_r in H1.
rewrite Nat.mod_small in H1; [ flia Hr H1 | flia Hr ].
}
destruct (Nat.eq_dec (carry u (i + 2)) 2) as [Hc22| Hc22]. {
rewrite Hc22, Nat.sub_add in H1; [ | easy ].
rewrite Nat.mod_same in H1; [ flia Hr H1 | easy ].
}
specialize (Hc3 2) as H7.
flia Hc20 Hc22 H7.
}
unfold carry, carry_cases in Hci1.
destruct (LPO_fst (fA_ge_1_ε u (i + 1))) as [HA| HA]. 2: {
destruct HA as (p & Hjp & Hp).
specialize (Hau (1 + p)).
now rewrite A_ge_1_add_r_true_if in Hp.
}
clear HA.
unfold carry, carry_cases in Hci2.
destruct (LPO_fst (fA_ge_1_ε u (i + 2))) as [HA| HA]. 2: {
destruct HA as (p & Hjp & Hp).
specialize (Hau (2 + p)).
now rewrite A_ge_1_add_r_true_if in Hp.
}
clear HA.
rewrite <- (all_fA_ge_1_ε_NQintg_A 3) with (l := rad) in Hci1; cycle 1. {
apply three_lt_rad_pow.
} {
intros; rewrite <- Nat.add_assoc; apply Hu3.
} {
now intros; apply A_ge_1_add_r_true_if.
}
replace (i + 2) with (i + 1 + 1) in Hci2 at 2 by flia.
rewrite A_split_first in Hci1; [ | min_n_ge ].
replace (S (i + 1)) with (i + 2) in Hci1 by easy.
rewrite Hu2 in Hci1.
rewrite Q.intg_add_cond in Hci1; [ | apply Q.le_0_pair | ]. 2: {
now apply Q.le_0_mul_r.
}
rewrite Q.intg_small in Hci1. 2: {
split; [ apply Q.le_0_pair | ].
replace 1%Q with (1 // 1)%Q by easy.
apply Q.lt_pair; [ easy | easy | flia Hr ].
}
rewrite Q.frac_small in Hci1. 2: {
split; [ apply Q.le_0_pair | ].
replace 1%Q with (1 // 1)%Q by easy.
apply Q.lt_pair; [ easy | easy | flia Hr ].
}
rewrite Nat.add_0_l in Hci1.
rewrite Q.frac_small in Hci1. 2: {
apply Q.intg_interv in Hci2; [ | easy ].
split; [ now apply Q.le_0_mul_r | ].
apply (Q.mul_lt_mono_pos_r (rad // 1)%Q); [ now apply Q.lt_0_pair | ].
rewrite <- Q.mul_assoc, Q.mul_pair_den_num; [ | easy ].
rewrite Q.mul_1_r, Q.mul_1_l.
rewrite Nat.add_0_r.
rewrite Nat.add_0_r, min_n_add, Nat.mul_1_r in Hci2.
eapply Q.lt_le_trans; [ apply Hci2 | ].
replace 1%Q with (1 // 1)%Q by easy.
rewrite <- Q.pair_add_l.
apply Q.le_pair; [ easy | easy | flia Hr ].
}
remember (A (i + 2) (min_n (i + 1) + rad) u) as a eqn:Ha.
rewrite Nat.add_0_r, min_n_add, Nat.mul_1_r in Hci2.
rewrite Nat.add_0_r, <- Ha in Hci1.
rewrite <- Ha in Hci2.
destruct (Q.lt_le_dec (((rad - 2) // rad)%Q + (a * 1 // rad)%Q) 1)
as [H1| H1]. {
rewrite Nat.add_0_r in Hci1.
rewrite Q.intg_small in Hci1; [ now rewrite Nat.mod_0_l in Hci1 | ].
apply Q.intg_interv in Hci2; [ | now rewrite Ha ].
rewrite Ha.
split; [ now apply Q.le_0_mul_r | ].
rewrite <- Ha.
apply (Q.mul_lt_mono_pos_r (rad // 1)%Q); [ now apply Q.lt_0_pair | ].
rewrite <- Q.mul_assoc, Q.mul_pair_den_num; [ | easy ].
rewrite Q.mul_1_r, Q.mul_1_l.
eapply Q.lt_le_trans; [ apply Hci2 | ].
replace 1%Q with (1 // 1)%Q by easy.
rewrite <- Q.pair_add_l.
apply Q.le_pair; [ easy | easy | flia Hr ].
}
apply Q.intg_interv in Hci2; [ | now rewrite Ha ].
apply Q.nlt_ge in H1; apply H1; clear H1.
apply (Q.lt_le_trans _ ((rad - 2) // rad + 2 // rad)%Q). {
apply Q.add_lt_mono_l.
apply (Q.mul_lt_mono_pos_r (rad // 1)%Q); [ now apply Q.lt_0_pair | ].
rewrite <- Q.mul_assoc, Q.mul_pair_den_num; [ | easy ].
rewrite Q.mul_1_r, Q.mul_pair_den_num; [ now destruct Hci2 | easy ].
}
rewrite <- Q.pair_add_l.
rewrite Nat.sub_add; [ | easy ].
now rewrite Q.pair_diag.
Qed.
(* special case of sum_3_all_fA_true_8_not_8 *)
Theorem rad_2_sum_3_all_1_not_0_0 {r : radix} : ∀ u i,
rad = 2
→ (∀ k, u (i + k) ≤ 3 * (rad - 1))
→ (∀ k, fA_ge_1_ε u i k = true)
→ u (i + 1) = 0
→ u (i + 2) ≠ 0.
Proof.
intros * Hr2 Hu3 Hau Hu1.
replace 0 with (rad - 2) in Hu1 at 2 |-* at 2 by flia Hr2.
now apply sum_3_all_fA_true_8_not_8.
Qed.