Library Stdlib.Numbers.Cyclic.Int63.Uint63
From Stdlib Require Import Utf8.
From Stdlib Require Export DoubleType.
From Stdlib Require Import Lia.
From Stdlib Require Import Zpow_facts.
From Stdlib Require Import Zgcd_alt.
From Stdlib Require ZArith.
Import Znumtheory.
From Stdlib Require Export PrimInt63 Uint63Axioms.
Notation int :=
int (
only parsing).
Notation lsl :=
lsl (
only parsing).
Notation lsr :=
lsr (
only parsing).
Notation land :=
land (
only parsing).
Notation lor :=
lor (
only parsing).
Notation lxor :=
lxor (
only parsing).
Notation add :=
add (
only parsing).
Notation sub :=
sub (
only parsing).
Notation mul :=
mul (
only parsing).
Notation mulc :=
mulc (
only parsing).
Notation div :=
div (
only parsing).
Notation mod :=
mod (
only parsing).
Notation eqb :=
eqb (
only parsing).
Notation ltb :=
ltb (
only parsing).
Notation leb :=
leb (
only parsing).
Notation size :=
Uint63Axioms.size (
only parsing).
Notation digits :=
Uint63Axioms.digits (
only parsing).
Notation max_int :=
Uint63Axioms.max_int (
only parsing).
Notation get_digit :=
Uint63Axioms.get_digit (
only parsing).
Notation set_digit :=
Uint63Axioms.set_digit (
only parsing).
Notation is_zero :=
Uint63Axioms.is_zero (
only parsing).
Notation is_even :=
Uint63Axioms.is_even (
only parsing).
Notation bit :=
Uint63Axioms.bit (
only parsing).
Notation addcarry :=
Uint63Axioms.addcarry (
only parsing).
Notation to_Z :=
Uint63Axioms.to_Z (
only parsing).
Notation of_pos :=
Uint63Axioms.of_pos (
only parsing).
Notation of_Z :=
Uint63Axioms.of_Z (
only parsing).
Notation wB :=
Uint63Axioms.wB (
only parsing).
Notation of_to_Z :=
Uint63Axioms.of_to_Z (
only parsing).
Notation lsl_spec :=
Uint63Axioms.lsl_spec (
only parsing).
Notation lsr_spec :=
Uint63Axioms.lsr_spec (
only parsing).
Notation land_spec :=
Uint63Axioms.land_spec (
only parsing).
Notation lor_spec :=
Uint63Axioms.lor_spec (
only parsing).
Notation lxor_spec :=
Uint63Axioms.lxor_spec (
only parsing).
Notation add_spec :=
Uint63Axioms.add_spec (
only parsing).
Notation sub_spec :=
Uint63Axioms.sub_spec (
only parsing).
Notation mul_spec :=
Uint63Axioms.mul_spec (
only parsing).
Notation mulc_spec :=
Uint63Axioms.mulc_spec (
only parsing).
Notation div_spec :=
Uint63Axioms.div_spec (
only parsing).
Notation mod_spec :=
Uint63Axioms.mod_spec (
only parsing).
Notation eqb_correct :=
Uint63Axioms.eqb_correct (
only parsing).
Notation eqb_refl :=
Uint63Axioms.eqb_refl (
only parsing).
Notation ltb_spec :=
Uint63Axioms.ltb_spec (
only parsing).
Notation leb_spec :=
Uint63Axioms.leb_spec (
only parsing).
Notation compare_def_spec :=
Uint63Axioms.compare_def_spec (
only parsing).
Notation head0_spec :=
Uint63Axioms.head0_spec (
only parsing).
Notation tail0_spec :=
Uint63Axioms.tail0_spec (
only parsing).
Notation addc_def_spec :=
Uint63Axioms.addc_def_spec (
only parsing).
Notation addcarryc_def_spec :=
Uint63Axioms.addcarryc_def_spec (
only parsing).
Notation subc_def_spec :=
Uint63Axioms.subc_def_spec (
only parsing).
Notation subcarryc_def_spec :=
Uint63Axioms.subcarryc_def_spec (
only parsing).
Notation diveucl_def_spec :=
Uint63Axioms.diveucl_def_spec (
only parsing).
Notation diveucl_21_spec :=
Uint63Axioms.diveucl_21_spec (
only parsing).
Notation addmuldiv_def_spec :=
Uint63Axioms.addmuldiv_def_spec (
only parsing).
Local Open Scope uint63_scope.
Module Import Uint63NotationsInternalB.
Infix "<<" :=
lsl (
at level 30,
no associativity) :
uint63_scope.
Infix ">>" :=
lsr (
at level 30,
no associativity) :
uint63_scope.
Infix "land" :=
land (
at level 40,
left associativity) :
uint63_scope.
Infix "lor" :=
lor (
at level 40,
left associativity) :
uint63_scope.
Infix "lxor" :=
lxor (
at level 40,
left associativity) :
uint63_scope.
Infix "+" :=
add :
uint63_scope.
Infix "-" :=
sub :
uint63_scope.
Infix "*" :=
mul :
uint63_scope.
Infix "/" :=
div :
uint63_scope.
Infix "mod" :=
mod (
at level 40,
no associativity) :
uint63_scope.
Infix "=?" :=
eqb (
at level 70,
no associativity) :
uint63_scope.
Infix "<?" :=
ltb (
at level 70,
no associativity) :
uint63_scope.
Infix "<=?" :=
leb (
at level 70,
no associativity) :
uint63_scope.
Infix "≤?" :=
leb (
at level 70,
no associativity) :
uint63_scope.
End Uint63NotationsInternalB.
Register Inline max_int.
Register Inline is_zero.
Register Inline is_even.
Extra modulo operations
Definition opp (
i:
int) := 0
- i.
Register Inline opp.
Definition oppcarry i :=
max_int - i.
Register Inline oppcarry.
Definition succ i :=
i + 1.
Register Inline succ.
Definition pred i :=
i - 1.
Register Inline pred.
Register Inline addcarry.
Definition subcarry i j :=
i - j - 1.
Register Inline subcarry.
Exact arithmetic operations
Trivial lemmas without axiom
I should add the definition (like for compare)
Notation head0 :=
head0 (
only parsing).
Notation tail0 :=
tail0 (
only parsing).
Square root functions using newton iteration
Gcd
equality
Lemma eqb_complete :
forall x y,
x = y -> (x =? y) = true.
Lemma eqb_spec :
forall x y,
(x =? y) = true <-> x = y.
Lemma eqb_false_spec :
forall x y,
(x =? y) = false <-> x <> y.
Lemma eqb_false_complete :
forall x y,
x <> y -> (x =? y) = false.
Lemma eqb_false_correct :
forall x y,
(x =? y) = false -> x <> y.
Definition eqs (
i j :
int) :
{i = j} + { i <> j } :=
(
if i =? j as b return (
(b = true -> i = j) -> (b = false -> i <> j) -> {i=j} + {i <> j} )
then fun (
Heq :
true = true -> i = j)
_ =>
left _ (
Heq (
eq_refl true))
else fun _ (
Hdiff :
false = false -> i <> j) =>
right _ (
Hdiff (
eq_refl false)))
(
eqb_correct i j)
(
eqb_false_correct i j).
Lemma eq_dec :
forall i j:
int,
i = j \/ i <> j.
Definition cast i j :=
(
if i =? j as b return (
(b = true -> i = j) -> option (
forall P :
int -> Type,
P i -> P j))
then fun Heq :
true = true -> i = j =>
Some
(
fun (
P :
int -> Type) (
Hi :
P i) =>
match Heq (
eq_refl true)
in (
_ = y)
return (
P y)
with
|
eq_refl =>
Hi
end)
else fun _ :
false = true -> i = j =>
None) (
eqb_correct i j).
Lemma cast_refl :
forall i,
cast i i = Some (
fun P H =>
H).
Lemma cast_diff :
forall i j,
i =? j = false -> cast i j = None.
Definition eqo i j :=
(
if i =? j as b return (
(b = true -> i = j) -> option (
i=j))
then fun Heq :
true = true -> i = j =>
Some (
Heq (
eq_refl true))
else fun _ :
false = true -> i = j =>
None) (
eqb_correct i j).
Lemma eqo_refl :
forall i,
eqo i i = Some (
eq_refl i).
Lemma eqo_diff :
forall i j,
i =? j = false -> eqo i j = None.
Comparison
Addition
Subtraction
GCD
Head0, Tail0
Lemma head00_spec x :
φ x = 0
-> φ (head0 x) = φ digits .
Lemma tail00_spec x :
φ x = 0
-> φ (tail0 x) = φ digits.
Infix "≡" := (
eqm wB) (
at level 70,
no associativity) :
uint63_scope.
Lemma eqm_mod x y :
x mod wB ≡ y mod wB → x ≡ y.
Lemma eqm_sub x y :
x ≡ y → x - y ≡ 0.
Lemma eqmE x y :
x ≡ y → ∃ k, x - y = k * wB.
Lemma eqm_subE x y :
x ≡ y ↔ x - y ≡ 0.
Lemma int_eqm x y :
x = y → φ x ≡ φ y.
Lemma eqmI x y :
φ x ≡ φ y → x = y.
Lemma add_assoc x y z: (
x + (y + z) = (x + y) + z)%
uint63.
Lemma add_comm x y: (
x + y = y + x)%
uint63.
Lemma add_le_r m n:
if (
n <=? m + n)%
uint63 then (
φ m + φ n < wB)%
Z else (
wB <= φ m + φ n)%
Z.
Lemma add_cancel_l x y z : (
x + y = x + z)%
uint63 -> y = z.
Lemma add_cancel_r x y z : (
y + x = z + x)%
uint63 -> y = z.
Coercion b2i (
b:
bool) :
int :=
if b then 1%
uint63 else 0%
uint63.
Lemma lsr0 i : 0
>> i = 0%
uint63.
Lemma lsr_0_r i:
i >> 0
= i.
Lemma lsr_1 n : 1
>> n = (
n =? 0)%
uint63.
Lemma lsr_add i m n: (
(i >> m) >> n = if n <=? m + n then i >> (m + n) else 0)%
uint63.
Lemma lsl0 i: 0
<< i = 0%
uint63.
Lemma lsl0_r i :
i << 0
= i.
Lemma lsl_add_distr x y n:
(x + y) << n = (
(x << n) + (y << n))%
uint63.
Lemma lsr_M_r x i (
H: (
digits <=? i = true)%
uint63) :
x >> i = 0%
uint63.
Lemma bit_0_spec i:
φ (bit i 0
) = φ i mod 2.
Lemma bit_split i : (
i = (i >> 1
) << 1
+ bit i 0)%
uint63.
Lemma bit_lsr x i j :
(
bit (
x >> i)
j = if j <=? i + j then bit x (
i + j)
else false)%
uint63.
Lemma bit_b2i (
b:
bool)
i :
bit b i = (
i =? 0)%
uint63 && b.
Lemma bit_1 n :
bit 1
n = (
n =? 0)%
uint63.
Local Hint Resolve Z.lt_gt Z.div_pos :
zarith.
Lemma to_Z_split x :
φ x = φ (x >> 1
) * 2
+ φ (bit x 0
).
Lemma bit_M i n (
H: (
digits <=? n = true)%
uint63):
bit i n = false.
Lemma bit_half i n (
H: (
n <? digits = true)%
uint63) :
bit (
i>>1)
n = bit i (
n+1).
Lemma bit_ext i j :
(forall n,
bit i n = bit j n) -> i = j.
Lemma bit_lsl x i j :
bit (
x << i)
j =
(
if (j <? i) || (digits <=? j) then false else bit x (
j - i))%
uint63.
Lemma lor_lsr i1 i2 i:
(i1 lor i2) >> i = (i1 >> i) lor (i2 >> i).
Lemma lor_le x y : (
y <=? x lor y)%
uint63 = true.
Lemma bit_0 n :
bit 0
n = false.
Lemma bit_add_or x y:
(forall n,
bit x n = true -> bit y n = true -> False) <-> (
x + y)%
uint63= x lor y.
Lemma addmuldiv_spec x y p :
φ p <= φ digits ->
φ (addmuldiv p x y) = (φ x * (2
^ φ p) + φ y / (2
^ (φ digits - φ p))) mod wB.
Lemma is_even_bit i :
is_even i = negb (
bit i 0).
Lemma is_even_spec x :
if is_even x then φ x mod 2
= 0
else φ x mod 2
= 1.
Lemma is_even_0 :
is_even 0
= true.
Lemma is_even_lsl_1 i :
is_even (
i << 1)
= true.
Ltac elim_div :=
unfold Z.div,
Z.modulo;
match goal with
|
H :
context[
Z.div_eucl ?
X ?
Y ] |-
_ =>
generalize dependent H;
generalize (
Z_div_mod_full X Y) ;
case (
Z.div_eucl X Y)
| |-
context[
Z.div_eucl ?
X ?
Y ] =>
generalize (
Z_div_mod_full X Y) ;
case (
Z.div_eucl X Y)
end;
unfold Remainder.
Lemma quotient_by_2 a:
a - 1
<= (a/2
) + (a/2
).
Lemma sqrt_main_trick j k: 0
<= j -> 0
<= k ->
(j * k) + j <= ((j + k)/2
+ 1
) ^ 2.
Lemma sqrt_main i j: 0
<= i -> 0
< j -> i < ((j + (i/j))/2
+ 1
) ^ 2.
Lemma sqrt_test_false i j: 0
<= i -> 0
< j -> i/j < j -> (j + (i/j))/2
< j.
Lemma sqrt_test_true i j: 0
<= i -> 0
< j -> i/j >= j -> j ^ 2
<= i.
Lemma sqrt_step_correct rec i j:
0
< φ i -> 0
< φ j -> φ i < (φ j + 1
) ^ 2
->
2
* φ j < wB ->
(forall j1 :
int,
0
< φ j1 < φ j -> φ i < (φ j1 + 1
) ^ 2
->
φ (rec i j1) ^ 2
<= φ i < (φ (rec i j1) + 1
) ^ 2
) ->
φ (sqrt_step rec i j) ^ 2
<= φ i < (φ (sqrt_step rec i j) + 1
) ^ 2.
Lemma iter_sqrt_correct n rec i j: 0
< φ i -> 0
< φ j ->
φ i < (φ j + 1
) ^ 2
-> 2
* φ j < wB ->
(forall j1, 0
< φ j1 -> 2
^(Z_of_nat n) + φ j1 <= φ j ->
φ i < (φ j1 + 1
) ^ 2
-> 2
* φ j1 < wB ->
φ (rec i j1) ^ 2
<= φ i < (φ (rec i j1) + 1
) ^ 2
) ->
φ (iter_sqrt n rec i j) ^ 2
<= φ i < (φ (iter_sqrt n rec i j) + 1
) ^ 2.
Lemma sqrt_init i: 1
< i -> i < (i/2
+ 1
) ^ 2.
Lemma sqrt_spec :
forall x,
φ (sqrt x) ^ 2
<= φ x < (φ (sqrt x) + 1
) ^ 2.
Lemma sqrt2_step_def rec ih il j:
sqrt2_step rec ih il j =
if (
ih <? j)%
uint63 then
let quo :=
fst (
diveucl_21 ih il j)
in
if (
quo <? j)%
uint63 then
let m :=
match j +c quo with
|
C0 m1 =>
m1 >> 1
|
C1 m1 => (
m1 >> 1
+ 1
<< (digits -1
))%
uint63
end in
rec ih il m
else j
else j.
Lemma sqrt2_lower_bound ih il j:
Φ (WW ih il) < (φ j + 1
) ^ 2
-> φ ih <= φ j.
Lemma diveucl_21_spec_aux :
forall a1 a2 b,
wB/2
<= φ b ->
φ a1 < φ b ->
let (
q,
r) :=
diveucl_21 a1 a2 b in
φ a1 *wB+ φ a2 = φ q * φ b + φ r /\
0
<= φ r < φ b.
Lemma div2_phi ih il j: (2
^62
<= φ j -> φ ih < φ j ->
φ (fst (
diveucl_21 ih il j)
) = Φ (WW ih il) / φ j)%
Z.
Lemma sqrt2_step_correct rec ih il j:
2
^ (Z_of_nat (
size - 2)
) <= φ ih ->
0
< φ j -> Φ (WW ih il) < (φ j + 1
) ^ 2
->
(forall j1, 0
< φ j1 < φ j -> Φ (WW ih il) < (φ j1 + 1
) ^ 2
->
φ (rec ih il j1) ^ 2
<= Φ (WW ih il) < (φ (rec ih il j1) + 1
) ^ 2
) ->
φ (sqrt2_step rec ih il j) ^ 2
<= Φ (WW ih il)
< (φ (sqrt2_step rec ih il j) + 1
) ^ 2.
Lemma iter2_sqrt_correct n rec ih il j:
2
^(Z_of_nat (
size - 2)
) <= φ ih -> 0
< φ j -> Φ (WW ih il) < (φ j + 1
) ^ 2
->
(forall j1, 0
< φ j1 -> 2
^(Z_of_nat n) + φ j1 <= φ j ->
Φ (WW ih il) < (φ j1 + 1
) ^ 2
->
φ (rec ih il j1) ^ 2
<= Φ (WW ih il) < (φ (rec ih il j1) + 1
) ^ 2
) ->
φ (iter2_sqrt n rec ih il j) ^ 2
<= Φ (WW ih il)
< (φ (iter2_sqrt n rec ih il j) + 1
) ^ 2.
Lemma sqrt2_spec :
forall x y,
wB/ 4
<= φ x ->
let (
s,
r) :=
sqrt2 x y in
Φ (WW x y) = φ s ^ 2
+ [+|r|] /\
[+|r|] <= 2
* φ s.
Lemma of_pos_rec_spec (
k:
nat) :
(
k <= size)%
nat →
∀ p, φ(of_pos_rec k p) = Zpos p mod 2
^ Z.of_nat k.
Lemma is_int n :
0
<= n < 2
^ φ digits →
n = φ (of_Z n).
Lemma of_Z_spec n :
φ (of_Z n) = n mod wB.
Lemma Z_oddE a :
Z.odd a = (
a mod 2
=? 1)%
Z.
Lemma Z_evenE a :
Z.even a = (
a mod 2
=? 0)%
Z.
Lemma is_zeroE n :
is_zero n = Z.eqb (
φ n) 0.
Lemma bitE i j :
bit i j = Z.testbit φ(i) φ(j).
Lemma lt_pow_lt_log d k n :
0
< d <= n →
0
<= k < 2
^ d →
Z.log2 k < n.
Lemma land_spec' x y :
φ (x land y) = Z.land φ(x) φ(y).
Lemma lor_spec' x y :
φ (x lor y) = Z.lor φ(x) φ(y).
Lemma lxor_spec' x y :
φ (x lxor y) = Z.lxor φ(x) φ(y).
Lemma landC i j :
i land j = j land i.
Lemma landA i j k :
i land (j land k) = i land j land k.
Lemma land0 i : 0
land i = 0%
uint63.
Lemma land0_r i :
i land 0
= 0%
uint63.
Lemma lorC i j :
i lor j = j lor i.
Lemma lorA i j k :
i lor (j lor k) = i lor j lor k.
Lemma lor0 i : 0
lor i = i.
Lemma lor0_r i :
i lor 0
= i.
Lemma lxorC i j :
i lxor j = j lxor i.
Lemma lxorA i j k :
i lxor (j lxor k) = i lxor j lxor k.
Lemma lxor0 i : 0
lxor i = i.
Lemma lxor0_r i :
i lxor 0
= i.
Lemma opp_to_Z_opp (
x :
int) :
φ x mod wB <> 0
->
(- φ (- x)) mod wB = (φ x) mod wB.
Minimum / maximum