blob: 2c2dfd8c8d63d15a91de6c929c9177c7365032b9 (
plain)
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
|
Require Import Coq.ZArith.ZArith Coq.QArith.QArith QArith.Qround.
Require Import Coq.micromega.Lia.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
Require Import Crypto.Util.ZUtil.Morphisms.
Local Open Scope Z_scope.
Lemma Qfloor_le_add a b : Qfloor a + Qfloor b <= Qfloor (a + b).
destruct a as [x y], b as [a b]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum].
Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Lemma Qceiling_le_add a b : Qceiling (a + b) <= Qceiling a + Qceiling b.
destruct a as [x y], b as [a b]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum].
Z.div_mod_to_quot_rem_in_goal. nia.
Qed.
Lemma add_floor_l_le_ceiling a b : Qfloor a + Qceiling b <= Qceiling (a + b).
destruct a as [x y], b as [a b]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum].
Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Lemma Zle_floor_ceiling a : Z.le (Qfloor a) (Qceiling a).
pose proof Qle_floor_ceiling.
destruct a as [x y]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum].
Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Section pow_ceil_mul_nat.
Context b f (b_nz:0 <> b) (f_pos:(0 <= f)%Q).
Local Notation wt i := (b^Qceiling (f * inject_Z (Z.of_nat i))) (only parsing).
Lemma zero_le_ceil_mul_nat i :
0 <= Qceiling (f * inject_Z (Z.of_nat i))%Q.
Proof.
rewrite Zle_Qle.
eapply Qle_trans; [|eapply Qle_ceiling].
eapply Qle_trans; [|eapply (Qmult_le_compat_r 0)]; trivial.
cbv; discriminate.
apply (Qle_trans _ (inject_Z 0)); [vm_decide|].
change 0%Q with (inject_Z 0).
rewrite <-Zle_Qle.
eapply Zle_0_nat.
Qed.
Lemma pow_ceil_mul_nat_nonzero
: forall i, wt i <> 0.
Proof.
intros.
eapply Z.pow_nonzero; try omega.
eapply zero_le_ceil_mul_nat.
Qed.
Lemma pow_ceil_mul_nat_nonneg (Hb : 0 <= b)
: forall i, 0 <= wt i.
Proof.
intros.
apply Z.pow_nonneg; assumption.
Qed.
Lemma pow_ceil_mul_S i :
wt (S i) =
(b ^ (Qceiling (f + f * inject_Z (Z.of_nat i)) - Qceiling (f * inject_Z (Z.of_nat i))) * wt i).
Proof.
rewrite Nat2Z.inj_succ.
rewrite <-Z.add_1_l.
rewrite inject_Z_plus.
change (inject_Z 1) with 1%Q.
rewrite Qmult_plus_distr_r, Qmult_1_r.
let g := constr:((f * inject_Z (Z.of_nat i))%Q) in
replace (Qceiling (f+g)) with ((Qceiling (f+g)-Qceiling g)+Qceiling g) at 1 by omega.
rewrite Z.pow_add_r; [reflexivity|eapply Zle_minus_le_0|apply zero_le_ceil_mul_nat].
eapply Qceiling_resp_le.
rewrite <-Qplus_0_l at 1.
eapply Qplus_le_compat;
auto with qarith.
Qed.
Lemma pow_ceil_mul_nat_multiples i :
wt (S i) mod (wt i) = 0.
Proof.
rewrite pow_ceil_mul_S, Z_mod_mult; reflexivity.
Qed.
End pow_ceil_mul_nat.
Section pow_ceil_mul_nat2.
Context b f (b_pos:0 < b) (f_ge_1:(1 <= f)%Q).
Local Notation wt i := (b^Qceiling (f * inject_Z (Z.of_nat i))) (only parsing).
Lemma pow_ceil_mul_nat_pos
: forall i, wt i > 0.
Proof.
intros.
eapply Z.gt_lt_iff.
eapply Z.pow_pos_nonneg; [assumption|].
eapply zero_le_ceil_mul_nat.
eapply (Qle_trans _ 1 _); [vm_decide|assumption].
Qed.
Lemma pow_ceil_mul_nat_divide i :
wt (S i) / (wt i) > 0.
Proof.
rewrite pow_ceil_mul_S.
rewrite Z_div_mult_full; [|apply pow_ceil_mul_nat_nonzero].
rewrite Z.gt_lt_iff.
eapply Z.pow_pos_nonneg; [assumption|].
etransitivity; [|eapply Z.sub_le_ge_Proper].
2:eapply add_floor_l_le_ceiling.
2:eapply Z.ge_le_iff; reflexivity.
assert (1 <= Qfloor f); [|omega].
change 1%Z with (Qfloor 1).
eapply Qfloor_resp_le.
all: trivial; try omega; (eapply (Qle_trans _ 1 _); [vm_decide|assumption]).
Qed.
Lemma pow_ceil_mul_nat_divide_nonzero i :
wt (S i) / (wt i) <> 0.
Proof.
pose proof (pow_ceil_mul_nat_divide i).
lia.
Qed.
Lemma pow_ceil_mul_nat_divide_upperbound i :
wt (S i) / (wt i) <= b^Qceiling f.
Proof.
rewrite pow_ceil_mul_S.
rewrite Z_div_mult_full; [|apply pow_ceil_mul_nat_nonzero].
all:[ > | omega | eapply (Qle_trans _ 1 _); [vm_decide|assumption].. ].
apply Z.pow_le_mono_r; [ assumption | ].
rewrite Z.le_sub_le_add_l, Z.add_comm.
etransitivity; [ | apply Qceiling_le_add ].
reflexivity.
Qed.
End pow_ceil_mul_nat2.
|
