Library Coq.Numbers.Cyclic.Int63.Int63
Require Import Utf8.
Require Export DoubleType.
Require Import Lia.
Require Import Zpow_facts.
Require Import Zgcd_alt.
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
Access to the nth digits
Definition get_digit x p := (0 < (x land (1 << p))).
Definition set_digit x p (b:bool) :=
if if 0 <= p then p < digits else false then
if b then x lor (1 << p)
else x land (max_int lxor (1 << p))
else x.
Definition set_digit x p (b:bool) :=
if if 0 <= p then p < digits else false then
if b then x lor (1 << p)
else x land (max_int lxor (1 << p))
else x.
Equality to 0
Parity
Bit
Extra modulo operations
Definition opp (i:int) := 0 - i.
Notation "- x" := (opp x) : int63_scope.
Definition oppcarry i := max_int - i.
Definition succ i := i + 1.
Definition pred i := i - 1.
Definition addcarry i j := i + j + 1.
Definition subcarry i j := i - j - 1.
Notation "- x" := (opp x) : int63_scope.
Definition oppcarry i := max_int - i.
Definition succ i := i + 1.
Definition pred i := i - 1.
Definition addcarry i j := i + j + 1.
Definition subcarry i j := i - j - 1.
Exact arithmetic operations
Definition addc_def x y :=
let r := x + y in
if r < x then C1 r else C0 r.
Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope.
Definition addcarryc_def x y :=
let r := addcarry x y in
if r <= x then C1 r else C0 r.
Definition subc_def x y :=
if y <= x then C0 (x - y) else C1 (x - y).
Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope.
Definition subcarryc_def x y :=
if y < x then C0 (x - y - 1) else C1 (x - y - 1).
Definition diveucl_def x y := (x/y, x\%y).
Definition addmuldiv_def p x y :=
(x << p) lor (y >> (digits - p)).
Definition oppc (i:int) := 0 -c i.
Definition succc i := i +c 1.
Definition predc i := i -c 1.
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.
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
Fixpoint to_Z_rec (n:nat) (i:int) :=
match n with
| O => 0%Z
| S n =>
(if is_even i then Z.double else Zdouble_plus_one) (to_Z_rec n (i >> 1))
end.
Definition to_Z := to_Z_rec size.
Fixpoint of_pos_rec (n:nat) (p:positive) :=
match n, p with
| O, _ => 0
| S n, xH => 1
| S n, xO p => (of_pos_rec n p) << 1
| S n, xI p => (of_pos_rec n p) << 1 lor 1
end.
Definition of_pos := of_pos_rec size.
Definition of_Z z :=
match z with
| Zpos p => of_pos p
| Z0 => 0
| Zneg p => - (of_pos p)
end.
Notation "[| x |]" := (to_Z x) (at level 0, x at level 99) : int63_scope.
Definition wB := (2 ^ (Z.of_nat size))%Z.
Lemma to_Z_rec_bounded size : forall x, (0 <= to_Z_rec size x < 2 ^ Z.of_nat size)%Z.
Corollary to_Z_bounded : forall x, (0 <= [| x |] < wB)%Z.
Local Open Scope Z_scope.
Lemma Z_lt_div2 x y : x < 2 * y -> x / 2 < y.
Theorem Zmod_le_first a b : 0 <= a -> 0 < b -> 0 <= a mod b <= a.
Theorem Zmod_distr: forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
(2 ^a * r + t) mod (2 ^ b) = (2 ^a * r) mod (2 ^ b) + t.
Lemma pow2_pos n : 0 <= n → 2 ^ n > 0.
Lemma pow2_nz n : 0 <= n → 2 ^ n ≠ 0.
Hint Resolve pow2_pos pow2_nz : zarith.
match n with
| O => 0%Z
| S n =>
(if is_even i then Z.double else Zdouble_plus_one) (to_Z_rec n (i >> 1))
end.
Definition to_Z := to_Z_rec size.
Fixpoint of_pos_rec (n:nat) (p:positive) :=
match n, p with
| O, _ => 0
| S n, xH => 1
| S n, xO p => (of_pos_rec n p) << 1
| S n, xI p => (of_pos_rec n p) << 1 lor 1
end.
Definition of_pos := of_pos_rec size.
Definition of_Z z :=
match z with
| Zpos p => of_pos p
| Z0 => 0
| Zneg p => - (of_pos p)
end.
Notation "[| x |]" := (to_Z x) (at level 0, x at level 99) : int63_scope.
Definition wB := (2 ^ (Z.of_nat size))%Z.
Lemma to_Z_rec_bounded size : forall x, (0 <= to_Z_rec size x < 2 ^ Z.of_nat size)%Z.
Corollary to_Z_bounded : forall x, (0 <= [| x |] < wB)%Z.
Local Open Scope Z_scope.
Lemma Z_lt_div2 x y : x < 2 * y -> x / 2 < y.
Theorem Zmod_le_first a b : 0 <= a -> 0 < b -> 0 <= a mod b <= a.
Theorem Zmod_distr: forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
(2 ^a * r + t) mod (2 ^ b) = (2 ^a * r) mod (2 ^ b) + t.
Lemma pow2_pos n : 0 <= n → 2 ^ n > 0.
Lemma pow2_nz n : 0 <= n → 2 ^ n ≠ 0.
Hint Resolve pow2_pos pow2_nz : zarith.
Trivial lemmas without axiom
Lemma wB_diff_0 : wB <> 0.
Lemma wB_pos : 0 < wB.
Lemma to_Z_0 : [|0|] = 0.
Lemma to_Z_1 : [|1|] = 1.
Local Open Scope Z_scope.
Notation "[+| c |]" :=
(interp_carry 1 wB to_Z c) (at level 0, c at level 99) : int63_scope.
Notation "[-| c |]" :=
(interp_carry (-1) wB to_Z c) (at level 0, c at level 99) : int63_scope.
Notation "[|| x ||]" :=
(zn2z_to_Z wB to_Z x) (at level 0, x at level 99) : int63_scope.
Axiom of_to_Z : forall x, of_Z [| x |] = x.
Notation "'φ' x" := [| x |] (at level 0) : int63_scope.
Lemma can_inj {rT aT} {f: aT -> rT} {g: rT -> aT} (K: forall a, g (f a) = a) {a a'} (e: f a = f a') : a = a'.
Lemma to_Z_inj x y : φ x = φ y → x = y.
Specification of logical operations
Local Open Scope Z_scope.
Axiom lsl_spec : forall x p, [| x << p |] = [| x |] * 2 ^ [| p |] mod wB.
Axiom lsr_spec : forall x p, [|x >> p|] = [|x|] / 2 ^ [|p|].
Axiom land_spec: forall x y i , bit (x land y) i = bit x i && bit y i.
Axiom lor_spec: forall x y i, bit (x lor y) i = bit x i || bit y i.
Axiom lxor_spec: forall x y i, bit (x lxor y) i = xorb (bit x i) (bit y i).
Axiom lsl_spec : forall x p, [| x << p |] = [| x |] * 2 ^ [| p |] mod wB.
Axiom lsr_spec : forall x p, [|x >> p|] = [|x|] / 2 ^ [|p|].
Axiom land_spec: forall x y i , bit (x land y) i = bit x i && bit y i.
Axiom lor_spec: forall x y i, bit (x lor y) i = bit x i || bit y i.
Axiom lxor_spec: forall x y i, bit (x lxor y) i = xorb (bit x i) (bit y i).
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
Local Open Scope int63_scope.
Definition sqrt_step (rec: int -> int -> int) (i j: int) :=
let quo := i / j in
if quo < j then rec i ((j + quo) >> 1)
else j.
Definition iter_sqrt :=
Eval lazy beta delta [sqrt_step] in
fix iter_sqrt (n: nat) (rec: int -> int -> int)
(i j: int) {struct n} : int :=
sqrt_step
(fun i j => match n with
O => rec i j
| S n => (iter_sqrt n (iter_sqrt n rec)) i j
end) i j.
Definition sqrt i :=
match compare 1 i with
Gt => 0
| Eq => 1
| Lt => iter_sqrt size (fun i j => j) i (i >> 1)
end.
Definition high_bit := 1 << (digits - 1).
Definition sqrt2_step (rec: int -> int -> int -> int)
(ih il j: int) :=
if ih < j then
let (quo,_) := diveucl_21 ih il j in
if quo < j then
match j +c quo with
| C0 m1 => rec ih il (m1 >> 1)
| C1 m1 => rec ih il ((m1 >> 1) + high_bit)
end
else j
else j.
Definition iter2_sqrt :=
Eval lazy beta delta [sqrt2_step] in
fix iter2_sqrt (n: nat)
(rec: int -> int -> int -> int)
(ih il j: int) {struct n} : int :=
sqrt2_step
(fun ih il j =>
match n with
| O => rec ih il j
| S n => (iter2_sqrt n (iter2_sqrt n rec)) ih il j
end) ih il j.
Definition sqrt2 ih il :=
let s := iter2_sqrt size (fun ih il j => j) ih il max_int in
let (ih1, il1) := mulc s s in
match il -c il1 with
| C0 il2 =>
if ih1 < ih then (s, C1 il2) else (s, C0 il2)
| C1 il2 =>
if ih1 < (ih - 1) then (s, C1 il2) else (s, C0 il2)
end.
Definition sqrt_step (rec: int -> int -> int) (i j: int) :=
let quo := i / j in
if quo < j then rec i ((j + quo) >> 1)
else j.
Definition iter_sqrt :=
Eval lazy beta delta [sqrt_step] in
fix iter_sqrt (n: nat) (rec: int -> int -> int)
(i j: int) {struct n} : int :=
sqrt_step
(fun i j => match n with
O => rec i j
| S n => (iter_sqrt n (iter_sqrt n rec)) i j
end) i j.
Definition sqrt i :=
match compare 1 i with
Gt => 0
| Eq => 1
| Lt => iter_sqrt size (fun i j => j) i (i >> 1)
end.
Definition high_bit := 1 << (digits - 1).
Definition sqrt2_step (rec: int -> int -> int -> int)
(ih il j: int) :=
if ih < j then
let (quo,_) := diveucl_21 ih il j in
if quo < j then
match j +c quo with
| C0 m1 => rec ih il (m1 >> 1)
| C1 m1 => rec ih il ((m1 >> 1) + high_bit)
end
else j
else j.
Definition iter2_sqrt :=
Eval lazy beta delta [sqrt2_step] in
fix iter2_sqrt (n: nat)
(rec: int -> int -> int -> int)
(ih il j: int) {struct n} : int :=
sqrt2_step
(fun ih il j =>
match n with
| O => rec ih il j
| S n => (iter2_sqrt n (iter2_sqrt n rec)) ih il j
end) ih il j.
Definition sqrt2 ih il :=
let s := iter2_sqrt size (fun ih il j => j) ih il max_int in
let (ih1, il1) := mulc s s in
match il -c il1 with
| C0 il2 =>
if ih1 < ih then (s, C1 il2) else (s, C0 il2)
| C1 il2 =>
if ih1 < (ih - 1) then (s, C1 il2) else (s, C0 il2)
end.
Gcd
Fixpoint gcd_rec (guard:nat) (i j:int) {struct guard} :=
match guard with
| O => 1
| S p => if j == 0 then i else gcd_rec p j (i \% j)
end.
Definition gcd := gcd_rec (2*size).
match guard with
| O => 1
| S p => if j == 0 then i else gcd_rec p j (i \% j)
end.
Definition gcd := gcd_rec (2*size).
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.
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
Lemma eqbP x y : reflect ([| x |] = [| y |]) (x == y).
Lemma ltbP x y : reflect ([| x |] < [| y |])%Z (x < y).
Lemma lebP x y : reflect ([| x |] <= [| y |])%Z (x ≤ y).
Lemma compare_spec x y : compare x y = ([|x|] ?= [|y|])%Z.
Lemma is_zero_spec x : is_zero x = true <-> x = 0%int63.
Lemma diveucl_spec x y :
let (q,r) := diveucl x y in
([| q |], [| r |]) = Z.div_eucl [| x |] [| y |].
Local Open Scope Z_scope.
Addition
Lemma addc_spec x y : [+| x +c y |] = [| x |] + [| y |].
Lemma succ_spec x : [| succ x |] = ([| x |] + 1) mod wB.
Lemma succc_spec x : [+| succc x |] = [| x |] + 1.
Lemma addcarry_spec x y : [| addcarry x y |] = ([| x |] + [| y |] + 1) mod wB.
Lemma addcarryc_spec x y : [+| addcarryc x y |] = [| x |] + [| y |] + 1.
Lemma succ_spec x : [| succ x |] = ([| x |] + 1) mod wB.
Lemma succc_spec x : [+| succc x |] = [| x |] + 1.
Lemma addcarry_spec x y : [| addcarry x y |] = ([| x |] + [| y |] + 1) mod wB.
Lemma addcarryc_spec x y : [+| addcarryc x y |] = [| x |] + [| y |] + 1.
Subtraction
Lemma subc_spec x y : [-| x -c y |] = [| x |] - [| y |].
Lemma pred_spec x : [| pred x |] = ([| x |] - 1) mod wB.
Lemma predc_spec x : [-| predc x |] = [| x |] - 1.
Lemma oppc_spec x : [-| oppc x |] = - [| x |].
Lemma opp_spec x : [|- x |] = - [| x |] mod wB.
Lemma oppcarry_spec x : [| oppcarry x |] = wB - [| x |] - 1.
Lemma subcarry_spec x y : [| subcarry x y |] = ([| x |] - [| y |] - 1) mod wB.
Lemma subcarryc_spec x y : [-| subcarryc x y |] = [| x |] - [| y |] - 1.
Lemma pred_spec x : [| pred x |] = ([| x |] - 1) mod wB.
Lemma predc_spec x : [-| predc x |] = [| x |] - 1.
Lemma oppc_spec x : [-| oppc x |] = - [| x |].
Lemma opp_spec x : [|- x |] = - [| x |] mod wB.
Lemma oppcarry_spec x : [| oppcarry x |] = wB - [| x |] - 1.
Lemma subcarry_spec x y : [| subcarry x y |] = ([| x |] - [| y |] - 1) mod wB.
Lemma subcarryc_spec x y : [-| subcarryc x y |] = [| x |] - [| y |] - 1.
GCD
Lemma to_Z_gcd : forall i j, [| gcd i j |] = Zgcdn (2 * size) [| j |] [| i |].
Lemma gcd_spec a b : Zis_gcd [| a |] [| b |] [| gcd a b |].
Lemma gcd_spec a b : Zis_gcd [| a |] [| b |] [| gcd a b |].
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 80) : 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.
Lemma tail00_spec x : [| x |] = 0 -> [|tail0 x|] = [|digits|].
Infix "≡" := (eqm wB) (at level 80) : 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.