Library Coq.Numbers.Cyclic.Int63.Int63
Require Import Utf8.
Require Export DoubleType.
Require Import Lia.
Require Import Zpow_facts.
Require Import Zgcd_alt.
Require ZArith.
Import Znumtheory.
Definition size := 63%
nat.
Definition id_int :
int -> int :=
fun x =>
x.
Delimit Scope int63_scope with int63.
Infix "<<" :=
lsl (
at level 30,
no associativity) :
int63_scope.
Infix ">>" :=
lsr (
at level 30,
no associativity) :
int63_scope.
Infix "land" :=
land (
at level 40,
left associativity) :
int63_scope.
Infix "lor" :=
lor (
at level 40,
left associativity) :
int63_scope.
Infix "lxor" :=
lxor (
at level 40,
left associativity) :
int63_scope.
Notation "n + m" := (
add n m) :
int63_scope.
Notation "n - m" := (
sub n m) :
int63_scope.
Notation "n * m" := (
mul n m) :
int63_scope.
Notation "n / m" := (
div n m) :
int63_scope.
Notation "n '\%' m" := (
mod n m) (
at level 40,
left associativity) :
int63_scope.
Notation "m '==' n" := (
eqb m n) (
at level 70,
no associativity) :
int63_scope.
Notation "m < n" := (
ltb m n) :
int63_scope.
Notation "m <= n" := (
leb m n) :
int63_scope.
Notation "m ≤ n" := (
leb m n) (
at level 70,
no associativity) :
int63_scope.
Local Open Scope int63_scope.
The number of digits as a int
The bigger int
Definition max_int :=
Eval vm_compute in 0
- 1.
Access to the nth digits
Equality to 0
Parity
Bit
Extra modulo operations
Exact arithmetic operations
Comparison
Definition compare_def x y :=
if x < y then Lt
else if (
x == y)
then Eq else Gt.
Notation "n ?= m" := (
compare n m) (
at level 70,
no associativity) :
int63_scope.
Import Bool ZArith.
Translation to Z
Trivial lemmas without axiom
Specification of logical operations
Specification of basic opetations
Axiom add_spec :
forall x y,
φ (x + y) = (φ x + φ y) mod wB.
Axiom sub_spec :
forall x y,
φ (x - y) = (φ x - φ y) mod wB.
Axiom mul_spec :
forall x y,
φ (x * y) = φ x * φ y mod wB.
Axiom mulc_spec :
forall x y,
φ x * φ y = φ (fst (
mulc x y)
) * wB + φ (snd (
mulc x y)
).
Axiom div_spec :
forall x y,
φ (x / y) = φ x / φ y.
Axiom mod_spec :
forall x y,
φ (x \% y) = φ x mod φ y.
Axiom eqb_correct :
forall i j, (
i == j)%
int63 = true -> i = j.
Axiom eqb_refl :
forall x, (
x == x)%
int63 = true.
Axiom ltb_spec :
forall x y, (
x < y)%
int63 = true <-> φ x < φ y.
Axiom leb_spec :
forall x y, (
x <= y)%
int63 = true <-> φ x <= φ y.
Exotic operations
I should add the definition (like for compare)
Axioms on operations which are just short cut
Axiom compare_def_spec :
forall x y,
compare x y = compare_def x y.
Axiom head0_spec :
forall x, 0
< φ x ->
wB/ 2
<= 2
^ (φ (head0 x)) * φ x < wB.
Axiom tail0_spec :
forall x, 0
< φ x ->
(
exists y, 0
<= y /\ φ x = (2
* y + 1
) * (2
^ φ (tail0 x)))%
Z.
Axiom addc_def_spec :
forall x y, (
x +c y)%
int63 = addc_def x y.
Axiom addcarryc_def_spec :
forall x y,
addcarryc x y = addcarryc_def x y.
Axiom subc_def_spec :
forall x y, (
x -c y)%
int63 = subc_def x y.
Axiom subcarryc_def_spec :
forall x y,
subcarryc x y = subcarryc_def x y.
Axiom diveucl_def_spec :
forall x y,
diveucl x y = diveucl_def x y.
Axiom diveucl_21_spec :
forall a1 a2 b,
let (
q,
r) :=
diveucl_21 a1 a2 b in
let (
q',
r') :=
Z.div_eucl (
φ a1 * wB + φ a2)
φ b in
φ a1 < φ b -> φ q = q' /\ φ r = r'.
Axiom addmuldiv_def_spec :
forall p x y,
addmuldiv p x y = addmuldiv_def p x y.
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) :
int63_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)%
int63.
Lemma add_comm x y: (
x + y = y + x)%
int63.
Lemma add_le_r m n:
if (
n <= m + n)%
int63 then (
φ m + φ n < wB)%
Z else (
wB <= φ m + φ n)%
Z.
Lemma add_cancel_l x y z : (
x + y = x + z)%
int63 -> y = z.
Lemma add_cancel_r x y z : (
y + x = z + x)%
int63 -> y = z.
Coercion b2i (
b:
bool) :
int :=
if b then 1%
int63 else 0%
int63.
Lemma lsr0 i : 0
>> i = 0%
int63.
Lemma lsr_0_r i:
i >> 0
= i.
Lemma lsr_1 n : 1
>> n = (n == 0
).
Lemma lsr_add i m n: (
(i >> m) >> n = if n <= m + n then i >> (m + n) else 0)%
int63.
Lemma lsl0 i: 0
<< i = 0%
int63.
Lemma lsl0_r i :
i << 0
= i.
Lemma lsl_add_distr x y n:
(x + y) << n = (
(x << n) + (y << n))%
int63.
Lemma lsr_M_r x i (
H: (
digits <= i = true)%
int63) :
x >> i = 0%
int63.
Lemma bit_0_spec i:
φ (bit i 0
) = φ i mod 2.
Lemma bit_split i : (
i = (i >> 1
) << 1
+ bit i 0)%
int63.
Lemma bit_lsr x i j :
(
bit (
x >> i)
j = if j <= i + j then bit x (
i + j)
else false)%
int63.
Lemma bit_b2i (
b:
bool)
i :
bit b i = (i == 0
) && b.
Lemma bit_1 n :
bit 1
n = (n == 0
).
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)%
int63):
bit i n = false.
Lemma bit_half i n (
H: (
n < digits = true)%
int63) :
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))%
int63.
Lemma lor_lsr i1 i2 i:
(i1 lor i2) >> i = (i1 >> i) lor (i2 >> i).
Lemma lor_le x y : (
y <= x lor y)%
int63 = 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)%
int63= 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)%
int63 then
let quo :=
fst (
diveucl_21 ih il j)
in
if (
quo < j)%
int63 then
let m :=
match j +c quo with
|
C0 m1 =>
m1 >> 1
|
C1 m1 => (
m1 >> 1
+ 1
<< (digits -1
))%
int63
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 negbE a b :
a = negb b → negb a = b.
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%
int63.
Lemma land0_r i :
i land 0
= 0%
int63.
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.