Library Coq.Numbers.Natural.BigN.NMake
From a cyclic Z/nZ representation to arbitrary precision natural numbers.
Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT !
Require Import BigNumPrelude.
Require Import ZArith.
Require Import CyclicAxioms.
Require Import DoubleType.
Require Import DoubleMul.
Require Import DoubleDivn1.
Require Import DoubleCyclic.
Require Import Nbasic.
Require Import Wf_nat.
Require Import StreamMemo.
Require Import NSig.
Module Make (
Import W0:CyclicType) <:
NType.
Definition w0 :=
W0.w.
Definition w1 :=
zn2z w0.
Definition w2 :=
zn2z w1.
Definition w3 :=
zn2z w2.
Definition w4 :=
zn2z w3.
Definition w5 :=
zn2z w4.
Definition w6 :=
zn2z w5.
Definition w0_op :=
W0.w_op.
Definition w1_op :=
mk_zn2z_op w0_op.
Definition w2_op :=
mk_zn2z_op w1_op.
Definition w3_op :=
mk_zn2z_op w2_op.
Definition w4_op :=
mk_zn2z_op_karatsuba w3_op.
Definition w5_op :=
mk_zn2z_op_karatsuba w4_op.
Definition w6_op :=
mk_zn2z_op_karatsuba w5_op.
Definition w7_op :=
mk_zn2z_op_karatsuba w6_op.
Definition w8_op :=
mk_zn2z_op_karatsuba w7_op.
Definition w9_op :=
mk_zn2z_op_karatsuba w8_op.
Section Make_op.
Variable mk :
forall w',
znz_op w' ->
znz_op (
zn2z w').
Fixpoint make_op_aux (
n:nat) :
znz_op (
word w6 (
S n)):=
match n return znz_op (
word w6 (
S n))
with
|
O =>
w7_op
|
S n1 =>
match n1 return znz_op (
word w6 (
S (
S n1)))
with
|
O =>
w8_op
|
S n2 =>
match n2 return znz_op (
word w6 (
S (
S (
S n2))))
with
|
O =>
w9_op
|
S n3 =>
mk _ (
mk _ (
mk _ (
make_op_aux n3)))
end
end
end.
End Make_op.
Definition omake_op :=
make_op_aux mk_zn2z_op_karatsuba.
Definition make_op_list :=
dmemo_list _ omake_op.
Definition make_op n :=
dmemo_get _ omake_op n make_op_list.
Lemma make_op_omake:
forall n,
make_op n =
omake_op n.
Inductive t_ :=
|
N0 :
w0 ->
t_
|
N1 :
w1 ->
t_
|
N2 :
w2 ->
t_
|
N3 :
w3 ->
t_
|
N4 :
w4 ->
t_
|
N5 :
w5 ->
t_
|
N6 :
w6 ->
t_
|
Nn :
forall n,
word w6 (
S n) ->
t_.
Definition t :=
t_.
Definition w_0 :=
w0_op.(
znz_0).
Definition one0 :=
w0_op.(
znz_1).
Definition one1 :=
w1_op.(
znz_1).
Definition one2 :=
w2_op.(
znz_1).
Definition one3 :=
w3_op.(
znz_1).
Definition one4 :=
w4_op.(
znz_1).
Definition one5 :=
w5_op.(
znz_1).
Definition one6 :=
w6_op.(
znz_1).
Definition zero :=
N0 w_0.
Definition one :=
N0 one0.
Definition to_Z x :=
match x with
|
N0 wx =>
w0_op.(
znz_to_Z)
wx
|
N1 wx =>
w1_op.(
znz_to_Z)
wx
|
N2 wx =>
w2_op.(
znz_to_Z)
wx
|
N3 wx =>
w3_op.(
znz_to_Z)
wx
|
N4 wx =>
w4_op.(
znz_to_Z)
wx
|
N5 wx =>
w5_op.(
znz_to_Z)
wx
|
N6 wx =>
w6_op.(
znz_to_Z)
wx
|
Nn n wx => (
make_op n).(
znz_to_Z)
wx
end.
Open Scope Z_scope.
Notation "[ x ]" := (
to_Z x).
Definition to_N x :=
Zabs_N (
to_Z x).
Definition eq x y := (
to_Z x =
to_Z y).
Fixpoint nmake_op (
ww:Type) (
ww_op:
znz_op ww) (
n:
nat) :
znz_op (
word ww n) :=
match n return znz_op (
word ww n)
with
O =>
ww_op
|
S n1 =>
mk_zn2z_op (
nmake_op ww ww_op n1)
end.
Theorem nmake_op_S:
forall ww (
w_op:
znz_op ww)
x,
nmake_op _ w_op (
S x) =
mk_zn2z_op (
nmake_op _ w_op x).
Let nmake_op0 :=
nmake_op _ w0_op.
Let eval0n n :=
znz_to_Z (
nmake_op0 n).
Let extend0 :=
DoubleBase.extend (
WW w_0).
Let nmake_op1 :=
nmake_op _ w1_op.
Let eval1n n :=
znz_to_Z (
nmake_op1 n).
Let extend1 :=
DoubleBase.extend (
WW (
W0:
w1)).
Let nmake_op2 :=
nmake_op _ w2_op.
Let eval2n n :=
znz_to_Z (
nmake_op2 n).
Let extend2 :=
DoubleBase.extend (
WW (
W0:
w2)).
Let nmake_op3 :=
nmake_op _ w3_op.
Let eval3n n :=
znz_to_Z (
nmake_op3 n).
Let extend3 :=
DoubleBase.extend (
WW (
W0:
w3)).
Let nmake_op4 :=
nmake_op _ w4_op.
Let eval4n n :=
znz_to_Z (
nmake_op4 n).
Let extend4 :=
DoubleBase.extend (
WW (
W0:
w4)).
Let nmake_op5 :=
nmake_op _ w5_op.
Let eval5n n :=
znz_to_Z (
nmake_op5 n).
Let extend5 :=
DoubleBase.extend (
WW (
W0:
w5)).
Let nmake_op6 :=
nmake_op _ w6_op.
Let eval6n n :=
znz_to_Z (
nmake_op6 n).
Let extend6 :=
DoubleBase.extend (
WW (
W0:
w6)).
Theorem digits_doubled:forall
n ww (
w_op:
znz_op ww),
znz_digits (
nmake_op _ w_op n) =
DoubleBase.double_digits (
znz_digits w_op)
n.
Theorem nmake_double:
forall n ww (
w_op:
znz_op ww),
znz_to_Z (
nmake_op _ w_op n) =
@
DoubleBase.double_to_Z _ (
znz_digits w_op) (
znz_to_Z w_op)
n.
Theorem digits_nmake:forall
n ww (
w_op:
znz_op ww),
znz_digits (
nmake_op _ w_op (
S n)) =
xO (
znz_digits (
nmake_op _ w_op n)).
Theorem znz_nmake_op:
forall ww ww_op n xh xl,
znz_to_Z (
nmake_op ww ww_op (
S n)) (
WW xh xl) =
znz_to_Z (
nmake_op ww ww_op n)
xh *
base (
znz_digits (
nmake_op ww ww_op n)) +
znz_to_Z (
nmake_op ww ww_op n)
xl.
Theorem make_op_S:
forall n,
make_op (
S n) =
mk_zn2z_op_karatsuba (
make_op n).
Let znz_to_Z_1:
forall x y,
znz_to_Z w1_op (
WW x y) =
znz_to_Z w0_op x *
base (
znz_digits w0_op) +
znz_to_Z w0_op y.
Let znz_to_Z_2:
forall x y,
znz_to_Z w2_op (
WW x y) =
znz_to_Z w1_op x *
base (
znz_digits w1_op) +
znz_to_Z w1_op y.
Let znz_to_Z_3:
forall x y,
znz_to_Z w3_op (
WW x y) =
znz_to_Z w2_op x *
base (
znz_digits w2_op) +
znz_to_Z w2_op y.
Let znz_to_Z_4:
forall x y,
znz_to_Z w4_op (
WW x y) =
znz_to_Z w3_op x *
base (
znz_digits w3_op) +
znz_to_Z w3_op y.
Let znz_to_Z_5:
forall x y,
znz_to_Z w5_op (
WW x y) =
znz_to_Z w4_op x *
base (
znz_digits w4_op) +
znz_to_Z w4_op y.
Let znz_to_Z_6:
forall x y,
znz_to_Z w6_op (
WW x y) =
znz_to_Z w5_op x *
base (
znz_digits w5_op) +
znz_to_Z w5_op y.
Let znz_to_Z_7:
forall x y,
znz_to_Z w7_op (
WW x y) =
znz_to_Z w6_op x *
base (
znz_digits w6_op) +
znz_to_Z w6_op y.
Let znz_to_Z_8:
forall x y,
znz_to_Z w8_op (
WW x y) =
znz_to_Z w7_op x *
base (
znz_digits w7_op) +
znz_to_Z w7_op y.
Let znz_to_Z_n:
forall n x y,
znz_to_Z (
make_op (
S n)) (
WW x y) =
znz_to_Z (
make_op n)
x *
base (
znz_digits (
make_op n)) +
znz_to_Z (
make_op n)
y.
Let w0_spec:
znz_spec w0_op :=
W0.w_spec.
Let w1_spec:
znz_spec w1_op :=
mk_znz2_spec w0_spec.
Let w2_spec:
znz_spec w2_op :=
mk_znz2_spec w1_spec.
Let w3_spec:
znz_spec w3_op :=
mk_znz2_spec w2_spec.
Let w4_spec :
znz_spec w4_op :=
mk_znz2_karatsuba_spec w3_spec.
Let w5_spec :
znz_spec w5_op :=
mk_znz2_karatsuba_spec w4_spec.
Let w6_spec :
znz_spec w6_op :=
mk_znz2_karatsuba_spec w5_spec.
Let w7_spec :
znz_spec w7_op :=
mk_znz2_karatsuba_spec w6_spec.
Let w8_spec :
znz_spec w8_op :=
mk_znz2_karatsuba_spec w7_spec.
Let w9_spec :
znz_spec w9_op :=
mk_znz2_karatsuba_spec w8_spec.
Let wn_spec:
forall n,
znz_spec (
make_op n).
Qed.
Definition w0_eq0 :=
w0_op.(
znz_eq0).
Let spec_w0_eq0:
forall x,
if w0_eq0 x then [
N0 x] = 0
else True.
Definition w1_eq0 :=
w1_op.(
znz_eq0).
Let spec_w1_eq0:
forall x,
if w1_eq0 x then [
N1 x] = 0
else True.
Definition w2_eq0 :=
w2_op.(
znz_eq0).
Let spec_w2_eq0:
forall x,
if w2_eq0 x then [
N2 x] = 0
else True.
Definition w3_eq0 :=
w3_op.(
znz_eq0).
Let spec_w3_eq0:
forall x,
if w3_eq0 x then [
N3 x] = 0
else True.
Definition w4_eq0 :=
w4_op.(
znz_eq0).
Let spec_w4_eq0:
forall x,
if w4_eq0 x then [
N4 x] = 0
else True.
Definition w5_eq0 :=
w5_op.(
znz_eq0).
Let spec_w5_eq0:
forall x,
if w5_eq0 x then [
N5 x] = 0
else True.
Definition w6_eq0 :=
w6_op.(
znz_eq0).
Let spec_w6_eq0:
forall x,
if w6_eq0 x then [
N6 x] = 0
else True.
Theorem digits_w0:
znz_digits w0_op =
znz_digits (
nmake_op _ w0_op 0).
Let spec_double_eval0n:
forall n,
eval0n n =
DoubleBase.double_to_Z (
znz_digits w0_op) (
znz_to_Z w0_op)
n.
Theorem digits_w1:
znz_digits w1_op =
znz_digits (
nmake_op _ w0_op 1).
Let spec_double_eval1n:
forall n,
eval1n n =
DoubleBase.double_to_Z (
znz_digits w1_op) (
znz_to_Z w1_op)
n.
Theorem digits_w2:
znz_digits w2_op =
znz_digits (
nmake_op _ w0_op 2).
Let spec_double_eval2n:
forall n,
eval2n n =
DoubleBase.double_to_Z (
znz_digits w2_op) (
znz_to_Z w2_op)
n.
Theorem digits_w3:
znz_digits w3_op =
znz_digits (
nmake_op _ w0_op 3).
Let spec_double_eval3n:
forall n,
eval3n n =
DoubleBase.double_to_Z (
znz_digits w3_op) (
znz_to_Z w3_op)
n.
Theorem digits_w4:
znz_digits w4_op =
znz_digits (
nmake_op _ w0_op 4).
Let spec_double_eval4n:
forall n,
eval4n n =
DoubleBase.double_to_Z (
znz_digits w4_op) (
znz_to_Z w4_op)
n.
Theorem digits_w5:
znz_digits w5_op =
znz_digits (
nmake_op _ w0_op 5).
Let spec_double_eval5n:
forall n,
eval5n n =
DoubleBase.double_to_Z (
znz_digits w5_op) (
znz_to_Z w5_op)
n.
Theorem digits_w6:
znz_digits w6_op =
znz_digits (
nmake_op _ w0_op 6).
Let spec_double_eval6n:
forall n,
eval6n n =
DoubleBase.double_to_Z (
znz_digits w6_op) (
znz_to_Z w6_op)
n.
Theorem digits_w0n0:
znz_digits w0_op =
znz_digits (
nmake_op _ w0_op 0).
Let spec_eval0n0:
forall x, [
N0 x] =
eval0n 0
x.
Let spec_extend0n1:
forall x, [
N0 x] = [
N1 (
extend0 0
x)].
Qed.
Theorem digits_w0n1:
znz_digits w1_op =
znz_digits (
nmake_op _ w0_op 1).
Let spec_eval0n1:
forall x, [
N1 x] =
eval0n 1
x.
Let spec_extend0n2:
forall x, [
N0 x] = [
N2 (
extend0 1
x)].
Qed.
Theorem digits_w0n2:
znz_digits w2_op =
znz_digits (
nmake_op _ w0_op 2).
Let spec_eval0n2:
forall x, [
N2 x] =
eval0n 2
x.
Let spec_extend0n3:
forall x, [
N0 x] = [
N3 (
extend0 2
x)].
Qed.
Theorem digits_w0n3:
znz_digits w3_op =
znz_digits (
nmake_op _ w0_op 3).
Let spec_eval0n3:
forall x, [
N3 x] =
eval0n 3
x.
Let spec_extend0n4:
forall x, [
N0 x] = [
N4 (
extend0 3
x)].
Qed.
Theorem digits_w0n4:
znz_digits w4_op =
znz_digits (
nmake_op _ w0_op 4).
Let spec_eval0n4:
forall x, [
N4 x] =
eval0n 4
x.
Let spec_extend0n5:
forall x, [
N0 x] = [
N5 (
extend0 4
x)].
Qed.
Theorem digits_w0n5:
znz_digits w5_op =
znz_digits (
nmake_op _ w0_op 5).
Let spec_eval0n5:
forall x, [
N5 x] =
eval0n 5
x.
Let spec_extend0n6:
forall x, [
N0 x] = [
N6 (
extend0 5
x)].
Qed.
Theorem digits_w0n6:
znz_digits w6_op =
znz_digits (
nmake_op _ w0_op 6).
Let spec_eval0n6:
forall x, [
N6 x] =
eval0n 6
x.
Theorem digits_w0n7:
znz_digits w7_op =
znz_digits (
nmake_op _ w0_op 7).
Let spec_eval0n7:
forall x, [
Nn 0
x] =
eval0n 7
x.
Let spec_eval0n8:
forall x, [
Nn 1
x] =
eval0n 8
x.
Qed.
Theorem digits_w1n0:
znz_digits w1_op =
znz_digits (
nmake_op _ w1_op 0).
Let spec_eval1n0:
forall x, [
N1 x] =
eval1n 0
x.
Let spec_extend1n2:
forall x, [
N1 x] = [
N2 (
extend1 0
x)].
Qed.
Theorem digits_w1n1:
znz_digits w2_op =
znz_digits (
nmake_op _ w1_op 1).
Let spec_eval1n1:
forall x, [
N2 x] =
eval1n 1
x.
Let spec_extend1n3:
forall x, [
N1 x] = [
N3 (
extend1 1
x)].
Qed.
Theorem digits_w1n2:
znz_digits w3_op =
znz_digits (
nmake_op _ w1_op 2).
Let spec_eval1n2:
forall x, [
N3 x] =
eval1n 2
x.
Let spec_extend1n4:
forall x, [
N1 x] = [
N4 (
extend1 2
x)].
Qed.
Theorem digits_w1n3:
znz_digits w4_op =
znz_digits (
nmake_op _ w1_op 3).
Let spec_eval1n3:
forall x, [
N4 x] =
eval1n 3
x.
Let spec_extend1n5:
forall x, [
N1 x] = [
N5 (
extend1 3
x)].
Qed.
Theorem digits_w1n4:
znz_digits w5_op =
znz_digits (
nmake_op _ w1_op 4).
Let spec_eval1n4:
forall x, [
N5 x] =
eval1n 4
x.
Let spec_extend1n6:
forall x, [
N1 x] = [
N6 (
extend1 4
x)].
Qed.
Theorem digits_w1n5:
znz_digits w6_op =
znz_digits (
nmake_op _ w1_op 5).
Let spec_eval1n5:
forall x, [
N6 x] =
eval1n 5
x.
Theorem digits_w1n6:
znz_digits w7_op =
znz_digits (
nmake_op _ w1_op 6).
Let spec_eval1n6:
forall x, [
Nn 0
x] =
eval1n 6
x.
Let spec_eval1n7:
forall x, [
Nn 1
x] =
eval1n 7
x.
Qed.
Theorem digits_w2n0:
znz_digits w2_op =
znz_digits (
nmake_op _ w2_op 0).
Let spec_eval2n0:
forall x, [
N2 x] =
eval2n 0
x.
Let spec_extend2n3:
forall x, [
N2 x] = [
N3 (
extend2 0
x)].
Qed.
Theorem digits_w2n1:
znz_digits w3_op =
znz_digits (
nmake_op _ w2_op 1).
Let spec_eval2n1:
forall x, [
N3 x] =
eval2n 1
x.
Let spec_extend2n4:
forall x, [
N2 x] = [
N4 (
extend2 1
x)].
Qed.
Theorem digits_w2n2:
znz_digits w4_op =
znz_digits (
nmake_op _ w2_op 2).
Let spec_eval2n2:
forall x, [
N4 x] =
eval2n 2
x.
Let spec_extend2n5:
forall x, [
N2 x] = [
N5 (
extend2 2
x)].
Qed.
Theorem digits_w2n3:
znz_digits w5_op =
znz_digits (
nmake_op _ w2_op 3).
Let spec_eval2n3:
forall x, [
N5 x] =
eval2n 3
x.
Let spec_extend2n6:
forall x, [
N2 x] = [
N6 (
extend2 3
x)].
Qed.
Theorem digits_w2n4:
znz_digits w6_op =
znz_digits (
nmake_op _ w2_op 4).
Let spec_eval2n4:
forall x, [
N6 x] =
eval2n 4
x.
Theorem digits_w2n5:
znz_digits w7_op =
znz_digits (
nmake_op _ w2_op 5).
Let spec_eval2n5:
forall x, [
Nn 0
x] =
eval2n 5
x.
Let spec_eval2n6:
forall x, [
Nn 1
x] =
eval2n 6
x.
Qed.
Theorem digits_w3n0:
znz_digits w3_op =
znz_digits (
nmake_op _ w3_op 0).
Let spec_eval3n0:
forall x, [
N3 x] =
eval3n 0
x.
Let spec_extend3n4:
forall x, [
N3 x] = [
N4 (
extend3 0
x)].
Qed.
Theorem digits_w3n1:
znz_digits w4_op =
znz_digits (
nmake_op _ w3_op 1).
Let spec_eval3n1:
forall x, [
N4 x] =
eval3n 1
x.
Let spec_extend3n5:
forall x, [
N3 x] = [
N5 (
extend3 1
x)].
Qed.
Theorem digits_w3n2:
znz_digits w5_op =
znz_digits (
nmake_op _ w3_op 2).
Let spec_eval3n2:
forall x, [
N5 x] =
eval3n 2
x.
Let spec_extend3n6:
forall x, [
N3 x] = [
N6 (
extend3 2
x)].
Qed.
Theorem digits_w3n3:
znz_digits w6_op =
znz_digits (
nmake_op _ w3_op 3).
Let spec_eval3n3:
forall x, [
N6 x] =
eval3n 3
x.
Theorem digits_w3n4:
znz_digits w7_op =
znz_digits (
nmake_op _ w3_op 4).
Let spec_eval3n4:
forall x, [
Nn 0
x] =
eval3n 4
x.
Let spec_eval3n5:
forall x, [
Nn 1
x] =
eval3n 5
x.
Qed.
Theorem digits_w4n0:
znz_digits w4_op =
znz_digits (
nmake_op _ w4_op 0).
Let spec_eval4n0:
forall x, [
N4 x] =
eval4n 0
x.
Let spec_extend4n5:
forall x, [
N4 x] = [
N5 (
extend4 0
x)].
Qed.
Theorem digits_w4n1:
znz_digits w5_op =
znz_digits (
nmake_op _ w4_op 1).
Let spec_eval4n1:
forall x, [
N5 x] =
eval4n 1
x.
Let spec_extend4n6:
forall x, [
N4 x] = [
N6 (
extend4 1
x)].
Qed.
Theorem digits_w4n2:
znz_digits w6_op =
znz_digits (
nmake_op _ w4_op 2).
Let spec_eval4n2:
forall x, [
N6 x] =
eval4n 2
x.
Theorem digits_w4n3:
znz_digits w7_op =
znz_digits (
nmake_op _ w4_op 3).
Let spec_eval4n3:
forall x, [
Nn 0
x] =
eval4n 3
x.
Let spec_eval4n4:
forall x, [
Nn 1
x] =
eval4n 4
x.
Qed.
Theorem digits_w5n0:
znz_digits w5_op =
znz_digits (
nmake_op _ w5_op 0).
Let spec_eval5n0:
forall x, [
N5 x] =
eval5n 0
x.
Let spec_extend5n6:
forall x, [
N5 x] = [
N6 (
extend5 0
x)].
Qed.
Theorem digits_w5n1:
znz_digits w6_op =
znz_digits (
nmake_op _ w5_op 1).
Let spec_eval5n1:
forall x, [
N6 x] =
eval5n 1
x.
Theorem digits_w5n2:
znz_digits w7_op =
znz_digits (
nmake_op _ w5_op 2).
Let spec_eval5n2:
forall x, [
Nn 0
x] =
eval5n 2
x.
Let spec_eval5n3:
forall x, [
Nn 1
x] =
eval5n 3
x.
Qed.
Theorem digits_w6n0:
znz_digits w6_op =
znz_digits (
nmake_op _ w6_op 0).
Let spec_eval6n0:
forall x, [
N6 x] =
eval6n 0
x.
Theorem digits_w6n1:
znz_digits w7_op =
znz_digits (
nmake_op _ w6_op 1).
Let spec_eval6n1:
forall x, [
Nn 0
x] =
eval6n 1
x.
Let spec_eval6n2:
forall x, [
Nn 1
x] =
eval6n 2
x.
Qed.
Let digits_w6n:
forall n,
znz_digits (
make_op n) =
znz_digits (
nmake_op _ w6_op (
S n)).
Qed.
Let spec_eval6n:
forall n x, [
Nn n x] =
eval6n (
S n)
x.
Qed.
Let spec_extend6n:
forall n x, [
N6 x] = [
Nn n (
extend6 n x)].
Qed.
Theorem spec_pos:
forall x, 0 <= [
x].
Let spec_extendn_0:
forall n wx, [
Nn n (
extend n _ wx)] = [
Nn 0
wx].
Qed.
Hint Rewrite spec_extendn_0:
extr.
Let spec_extendn0_0:
forall n wx, [
Nn (
S n) (
WW W0 wx)] = [
Nn n wx].
Hint Rewrite spec_extendn_0:
extr.
Let spec_extend_tr:
forall m n (
w:
word _ (
S n)),
[
Nn (
m +
n) (
extend_tr w m)] = [
Nn n w].
Hint Rewrite spec_extend_tr:
extr.
Let spec_cast_l:
forall n m x1,
[
Nn (
Max.max n m)
(
castm (
diff_r n m) (
extend_tr x1 (
snd (
diff n m))))] =
[
Nn n x1].
Hint Rewrite spec_cast_l:
extr.
Let spec_cast_r:
forall n m x1,
[
Nn (
Max.max n m)
(
castm (
diff_l n m) (
extend_tr x1 (
fst (
diff n m))))] =
[
Nn m x1].
Hint Rewrite spec_cast_r:
extr.
Section LevelAndIter.
Variable res:
Type.
Variable xxx:
res.
Variable P:
Z ->
Z ->
res ->
Prop.
Variable f0:
w0 ->
w0 ->
res.
Variable f0n:
forall n,
w0 ->
word w0 (
S n) ->
res.
Variable fn0:
forall n,
word w0 (
S n) ->
w0 ->
res.
Variable Pf0:
forall x y,
P [
N0 x] [
N0 y] (
f0 x y).
Variable Pf0n:
forall n x y,
Z_of_nat n <= 6 ->
P [
N0 x] (
eval0n (
S n)
y) (
f0n n x y).
Variable Pfn0:
forall n x y,
Z_of_nat n <= 6 ->
P (
eval0n (
S n)
x) [
N0 y] (
fn0 n x y).
Variable f1:
w1 ->
w1 ->
res.
Variable f1n:
forall n,
w1 ->
word w1 (
S n) ->
res.
Variable fn1:
forall n,
word w1 (
S n) ->
w1 ->
res.
Variable Pf1:
forall x y,
P [
N1 x] [
N1 y] (
f1 x y).
Variable Pf1n:
forall n x y,
Z_of_nat n <= 5 ->
P [
N1 x] (
eval1n (
S n)
y) (
f1n n x y).
Variable Pfn1:
forall n x y,
Z_of_nat n <= 5 ->
P (
eval1n (
S n)
x) [
N1 y] (
fn1 n x y).
Variable f2:
w2 ->
w2 ->
res.
Variable f2n:
forall n,
w2 ->
word w2 (
S n) ->
res.
Variable fn2:
forall n,
word w2 (
S n) ->
w2 ->
res.
Variable Pf2:
forall x y,
P [
N2 x] [
N2 y] (
f2 x y).
Variable Pf2n:
forall n x y,
Z_of_nat n <= 4 ->
P [
N2 x] (
eval2n (
S n)
y) (
f2n n x y).
Variable Pfn2:
forall n x y,
Z_of_nat n <= 4 ->
P (
eval2n (
S n)
x) [
N2 y] (
fn2 n x y).
Variable f3:
w3 ->
w3 ->
res.
Variable f3n:
forall n,
w3 ->
word w3 (
S n) ->
res.
Variable fn3:
forall n,
word w3 (
S n) ->
w3 ->
res.
Variable Pf3:
forall x y,
P [
N3 x] [
N3 y] (
f3 x y).
Variable Pf3n:
forall n x y,
Z_of_nat n <= 3 ->
P [
N3 x] (
eval3n (
S n)
y) (
f3n n x y).
Variable Pfn3:
forall n x y,
Z_of_nat n <= 3 ->
P (
eval3n (
S n)
x) [
N3 y] (
fn3 n x y).
Variable f4:
w4 ->
w4 ->
res.
Variable f4n:
forall n,
w4 ->
word w4 (
S n) ->
res.
Variable fn4:
forall n,
word w4 (
S n) ->
w4 ->
res.
Variable Pf4:
forall x y,
P [
N4 x] [
N4 y] (
f4 x y).
Variable Pf4n:
forall n x y,
Z_of_nat n <= 2 ->
P [
N4 x] (
eval4n (
S n)
y) (
f4n n x y).
Variable Pfn4:
forall n x y,
Z_of_nat n <= 2 ->
P (
eval4n (
S n)
x) [
N4 y] (
fn4 n x y).
Variable f5:
w5 ->
w5 ->
res.
Variable f5n:
forall n,
w5 ->
word w5 (
S n) ->
res.
Variable fn5:
forall n,
word w5 (
S n) ->
w5 ->
res.
Variable Pf5:
forall x y,
P [
N5 x] [
N5 y] (
f5 x y).
Variable Pf5n:
forall n x y,
Z_of_nat n <= 1 ->
P [
N5 x] (
eval5n (
S n)
y) (
f5n n x y).
Variable Pfn5:
forall n x y,
Z_of_nat n <= 1 ->
P (
eval5n (
S n)
x) [
N5 y] (
fn5 n x y).
Variable f6:
w6 ->
w6 ->
res.
Variable f6n:
forall n,
w6 ->
word w6 (
S n) ->
res.
Variable fn6:
forall n,
word w6 (
S n) ->
w6 ->
res.
Variable Pf6:
forall x y,
P [
N6 x] [
N6 y] (
f6 x y).
Variable Pf6n:
forall n x y,
P [
N6 x] (
eval6n (
S n)
y) (
f6n n x y).
Variable Pfn6:
forall n x y,
P (
eval6n (
S n)
x) [
N6 y] (
fn6 n x y).
Variable fnn:
forall n,
word w6 (
S n) ->
word w6 (
S n) ->
res.
Variable Pfnn:
forall n x y,
P [
Nn n x] [
Nn n y] (
fnn n x y).
Variable fnm:
forall n m,
word w6 (
S n) ->
word w6 (
S m) ->
res.
Variable Pfnm:
forall n m x y,
P [
Nn n x] [
Nn m y] (
fnm n m x y).
Variable f0t:
t_ ->
res.
Variable Pf0t:
forall x,
P 0 [
x] (
f0t x).
Variable ft0:
t_ ->
res.
Variable Pft0:
forall x,
P [
x] 0 (
ft0 x).
Definition same_level (
x y:
t_):
res :=
Eval lazy zeta beta iota delta [
extend0 extend1 extend2 extend3 extend4 extend5 extend6
DoubleBase.extend DoubleBase.extend_aux
]
in
match x,
y with
|
N0 wx,
N0 wy =>
f0 wx wy
|
N0 wx,
N1 wy =>
f1 (
extend0 0
wx)
wy
|
N0 wx,
N2 wy =>
f2 (
extend0 1
wx)
wy
|
N0 wx,
N3 wy =>
f3 (
extend0 2
wx)
wy
|
N0 wx,
N4 wy =>
f4 (
extend0 3
wx)
wy
|
N0 wx,
N5 wy =>
f5 (
extend0 4
wx)
wy
|
N0 wx,
N6 wy =>
f6 (
extend0 5
wx)
wy
|
N0 wx,
Nn m wy =>
fnn m (
extend6 m (
extend0 5
wx))
wy
|
N1 wx,
N0 wy =>
f1 wx (
extend0 0
wy)
|
N1 wx,
N1 wy =>
f1 wx wy
|
N1 wx,
N2 wy =>
f2 (
extend1 0
wx)
wy
|
N1 wx,
N3 wy =>
f3 (
extend1 1
wx)
wy
|
N1 wx,
N4 wy =>
f4 (
extend1 2
wx)
wy
|
N1 wx,
N5 wy =>
f5 (
extend1 3
wx)
wy
|
N1 wx,
N6 wy =>
f6 (
extend1 4
wx)
wy
|
N1 wx,
Nn m wy =>
fnn m (
extend6 m (
extend1 4
wx))
wy
|
N2 wx,
N0 wy =>
f2 wx (
extend0 1
wy)
|
N2 wx,
N1 wy =>
f2 wx (
extend1 0
wy)
|
N2 wx,
N2 wy =>
f2 wx wy
|
N2 wx,
N3 wy =>
f3 (
extend2 0
wx)
wy
|
N2 wx,
N4 wy =>
f4 (
extend2 1
wx)
wy
|
N2 wx,
N5 wy =>
f5 (
extend2 2
wx)
wy
|
N2 wx,
N6 wy =>
f6 (
extend2 3
wx)
wy
|
N2 wx,
Nn m wy =>
fnn m (
extend6 m (
extend2 3
wx))
wy
|
N3 wx,
N0 wy =>
f3 wx (
extend0 2
wy)
|
N3 wx,
N1 wy =>
f3 wx (
extend1 1
wy)
|
N3 wx,
N2 wy =>
f3 wx (
extend2 0
wy)
|
N3 wx,
N3 wy =>
f3 wx wy
|
N3 wx,
N4 wy =>
f4 (
extend3 0
wx)
wy
|
N3 wx,
N5 wy =>
f5 (
extend3 1
wx)
wy
|
N3 wx,
N6 wy =>
f6 (
extend3 2
wx)
wy
|
N3 wx,
Nn m wy =>
fnn m (
extend6 m (
extend3 2
wx))
wy
|
N4 wx,
N0 wy =>
f4 wx (
extend0 3
wy)
|
N4 wx,
N1 wy =>
f4 wx (
extend1 2
wy)
|
N4 wx,
N2 wy =>
f4 wx (
extend2 1
wy)
|
N4 wx,
N3 wy =>
f4 wx (
extend3 0
wy)
|
N4 wx,
N4 wy =>
f4 wx wy
|
N4 wx,
N5 wy =>
f5 (
extend4 0
wx)
wy
|
N4 wx,
N6 wy =>
f6 (
extend4 1
wx)
wy
|
N4 wx,
Nn m wy =>
fnn m (
extend6 m (
extend4 1
wx))
wy
|
N5 wx,
N0 wy =>
f5 wx (
extend0 4
wy)
|
N5 wx,
N1 wy =>
f5 wx (
extend1 3
wy)
|
N5 wx,
N2 wy =>
f5 wx (
extend2 2
wy)
|
N5 wx,
N3 wy =>
f5 wx (
extend3 1
wy)
|
N5 wx,
N4 wy =>
f5 wx (
extend4 0
wy)
|
N5 wx,
N5 wy =>
f5 wx wy
|
N5 wx,
N6 wy =>
f6 (
extend5 0
wx)
wy
|
N5 wx,
Nn m wy =>
fnn m (
extend6 m (
extend5 0
wx))
wy
|
N6 wx,
N0 wy =>
f6 wx (
extend0 5
wy)
|
N6 wx,
N1 wy =>
f6 wx (
extend1 4
wy)
|
N6 wx,
N2 wy =>
f6 wx (
extend2 3
wy)
|
N6 wx,
N3 wy =>
f6 wx (
extend3 2
wy)
|
N6 wx,
N4 wy =>
f6 wx (
extend4 1
wy)
|
N6 wx,
N5 wy =>
f6 wx (
extend5 0
wy)
|
N6 wx,
N6 wy =>
f6 wx wy
|
N6 wx,
Nn m wy =>
fnn m (
extend6 m wx)
wy
|
Nn n wx,
N0 wy =>
fnn n wx (
extend6 n (
extend0 5
wy))
|
Nn n wx,
N1 wy =>
fnn n wx (
extend6 n (
extend1 4
wy))
|
Nn n wx,
N2 wy =>
fnn n wx (
extend6 n (
extend2 3
wy))
|
Nn n wx,
N3 wy =>
fnn n wx (
extend6 n (
extend3 2
wy))
|
Nn n wx,
N4 wy =>
fnn n wx (
extend6 n (
extend4 1
wy))
|
Nn n wx,
N5 wy =>
fnn n wx (
extend6 n (
extend5 0
wy))
|
Nn n wx,
N6 wy =>
fnn n wx (
extend6 n wy)
|
Nn n wx,
Nn m wy =>
let mn :=
Max.max n m in
let d :=
diff n m in
fnn mn
(
castm (
diff_r n m) (
extend_tr wx (
snd d)))
(
castm (
diff_l n m) (
extend_tr wy (
fst d)))
end.
Lemma spec_same_level:
forall x y,
P [
x] [
y] (
same_level x y).
Definition same_level0 (
x y:
t_):
res :=
Eval lazy zeta beta iota delta [
extend0 extend1 extend2 extend3 extend4 extend5 extend6
DoubleBase.extend DoubleBase.extend_aux
]
in
match x with
|
N0 wx =>
if w0_eq0 wx then f0t y else
match y with
|
N0 wy =>
f0 wx wy
|
N1 wy =>
f1 (
extend0 0
wx)
wy
|
N2 wy =>
f2 (
extend0 1
wx)
wy
|
N3 wy =>
f3 (
extend0 2
wx)
wy
|
N4 wy =>
f4 (
extend0 3
wx)
wy
|
N5 wy =>
f5 (
extend0 4
wx)
wy
|
N6 wy =>
f6 (
extend0 5
wx)
wy
|
Nn m wy =>
fnn m (
extend6 m (
extend0 5
wx))
wy
end
|
N1 wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
f1 wx (
extend0 0
wy)
|
N1 wy =>
f1 wx wy
|
N2 wy =>
f2 (
extend1 0
wx)
wy
|
N3 wy =>
f3 (
extend1 1
wx)
wy
|
N4 wy =>
f4 (
extend1 2
wx)
wy
|
N5 wy =>
f5 (
extend1 3
wx)
wy
|
N6 wy =>
f6 (
extend1 4
wx)
wy
|
Nn m wy =>
fnn m (
extend6 m (
extend1 4
wx))
wy
end
|
N2 wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
f2 wx (
extend0 1
wy)
|
N1 wy =>
f2 wx (
extend1 0
wy)
|
N2 wy =>
f2 wx wy
|
N3 wy =>
f3 (
extend2 0
wx)
wy
|
N4 wy =>
f4 (
extend2 1
wx)
wy
|
N5 wy =>
f5 (
extend2 2
wx)
wy
|
N6 wy =>
f6 (
extend2 3
wx)
wy
|
Nn m wy =>
fnn m (
extend6 m (
extend2 3
wx))
wy
end
|
N3 wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
f3 wx (
extend0 2
wy)
|
N1 wy =>
f3 wx (
extend1 1
wy)
|
N2 wy =>
f3 wx (
extend2 0
wy)
|
N3 wy =>
f3 wx wy
|
N4 wy =>
f4 (
extend3 0
wx)
wy
|
N5 wy =>
f5 (
extend3 1
wx)
wy
|
N6 wy =>
f6 (
extend3 2
wx)
wy
|
Nn m wy =>
fnn m (
extend6 m (
extend3 2
wx))
wy
end
|
N4 wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
f4 wx (
extend0 3
wy)
|
N1 wy =>
f4 wx (
extend1 2
wy)
|
N2 wy =>
f4 wx (
extend2 1
wy)
|
N3 wy =>
f4 wx (
extend3 0
wy)
|
N4 wy =>
f4 wx wy
|
N5 wy =>
f5 (
extend4 0
wx)
wy
|
N6 wy =>
f6 (
extend4 1
wx)
wy
|
Nn m wy =>
fnn m (
extend6 m (
extend4 1
wx))
wy
end
|
N5 wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
f5 wx (
extend0 4
wy)
|
N1 wy =>
f5 wx (
extend1 3
wy)
|
N2 wy =>
f5 wx (
extend2 2
wy)
|
N3 wy =>
f5 wx (
extend3 1
wy)
|
N4 wy =>
f5 wx (
extend4 0
wy)
|
N5 wy =>
f5 wx wy
|
N6 wy =>
f6 (
extend5 0
wx)
wy
|
Nn m wy =>
fnn m (
extend6 m (
extend5 0
wx))
wy
end
|
N6 wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
f6 wx (
extend0 5
wy)
|
N1 wy =>
f6 wx (
extend1 4
wy)
|
N2 wy =>
f6 wx (
extend2 3
wy)
|
N3 wy =>
f6 wx (
extend3 2
wy)
|
N4 wy =>
f6 wx (
extend4 1
wy)
|
N5 wy =>
f6 wx (
extend5 0
wy)
|
N6 wy =>
f6 wx wy
|
Nn m wy =>
fnn m (
extend6 m wx)
wy
end
|
Nn n wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
fnn n wx (
extend6 n (
extend0 5
wy))
|
N1 wy =>
fnn n wx (
extend6 n (
extend1 4
wy))
|
N2 wy =>
fnn n wx (
extend6 n (
extend2 3
wy))
|
N3 wy =>
fnn n wx (
extend6 n (
extend3 2
wy))
|
N4 wy =>
fnn n wx (
extend6 n (
extend4 1
wy))
|
N5 wy =>
fnn n wx (
extend6 n (
extend5 0
wy))
|
N6 wy =>
fnn n wx (
extend6 n wy)
|
Nn m wy =>
let mn :=
Max.max n m in
let d :=
diff n m in
fnn mn
(
castm (
diff_r n m) (
extend_tr wx (
snd d)))
(
castm (
diff_l n m) (
extend_tr wy (
fst d)))
end
end.
Lemma spec_same_level0:
forall x y,
P [
x] [
y] (
same_level0 x y).
Definition iter (
x y:
t_):
res :=
Eval lazy zeta beta iota delta [
extend0 extend1 extend2 extend3 extend4 extend5 extend6
DoubleBase.extend DoubleBase.extend_aux
]
in
match x,
y with
|
N0 wx,
N0 wy =>
f0 wx wy
|
N0 wx,
N1 wy =>
f0n 0
wx wy
|
N0 wx,
N2 wy =>
f0n 1
wx wy
|
N0 wx,
N3 wy =>
f0n 2
wx wy
|
N0 wx,
N4 wy =>
f0n 3
wx wy
|
N0 wx,
N5 wy =>
f0n 4
wx wy
|
N0 wx,
N6 wy =>
f0n 5
wx wy
|
N0 wx,
Nn m wy =>
f6n m (
extend0 5
wx)
wy
|
N1 wx,
N0 wy =>
fn0 0
wx wy
|
N1 wx,
N1 wy =>
f1 wx wy
|
N1 wx,
N2 wy =>
f1n 0
wx wy
|
N1 wx,
N3 wy =>
f1n 1
wx wy
|
N1 wx,
N4 wy =>
f1n 2
wx wy
|
N1 wx,
N5 wy =>
f1n 3
wx wy
|
N1 wx,
N6 wy =>
f1n 4
wx wy
|
N1 wx,
Nn m wy =>
f6n m (
extend1 4
wx)
wy
|
N2 wx,
N0 wy =>
fn0 1
wx wy
|
N2 wx,
N1 wy =>
fn1 0
wx wy
|
N2 wx,
N2 wy =>
f2 wx wy
|
N2 wx,
N3 wy =>
f2n 0
wx wy
|
N2 wx,
N4 wy =>
f2n 1
wx wy
|
N2 wx,
N5 wy =>
f2n 2
wx wy
|
N2 wx,
N6 wy =>
f2n 3
wx wy
|
N2 wx,
Nn m wy =>
f6n m (
extend2 3
wx)
wy
|
N3 wx,
N0 wy =>
fn0 2
wx wy
|
N3 wx,
N1 wy =>
fn1 1
wx wy
|
N3 wx,
N2 wy =>
fn2 0
wx wy
|
N3 wx,
N3 wy =>
f3 wx wy
|
N3 wx,
N4 wy =>
f3n 0
wx wy
|
N3 wx,
N5 wy =>
f3n 1
wx wy
|
N3 wx,
N6 wy =>
f3n 2
wx wy
|
N3 wx,
Nn m wy =>
f6n m (
extend3 2
wx)
wy
|
N4 wx,
N0 wy =>
fn0 3
wx wy
|
N4 wx,
N1 wy =>
fn1 2
wx wy
|
N4 wx,
N2 wy =>
fn2 1
wx wy
|
N4 wx,
N3 wy =>
fn3 0
wx wy
|
N4 wx,
N4 wy =>
f4 wx wy
|
N4 wx,
N5 wy =>
f4n 0
wx wy
|
N4 wx,
N6 wy =>
f4n 1
wx wy
|
N4 wx,
Nn m wy =>
f6n m (
extend4 1
wx)
wy
|
N5 wx,
N0 wy =>
fn0 4
wx wy
|
N5 wx,
N1 wy =>
fn1 3
wx wy
|
N5 wx,
N2 wy =>
fn2 2
wx wy
|
N5 wx,
N3 wy =>
fn3 1
wx wy
|
N5 wx,
N4 wy =>
fn4 0
wx wy
|
N5 wx,
N5 wy =>
f5 wx wy
|
N5 wx,
N6 wy =>
f5n 0
wx wy
|
N5 wx,
Nn m wy =>
f6n m (
extend5 0
wx)
wy
|
N6 wx,
N0 wy =>
fn0 5
wx wy
|
N6 wx,
N1 wy =>
fn1 4
wx wy
|
N6 wx,
N2 wy =>
fn2 3
wx wy
|
N6 wx,
N3 wy =>
fn3 2
wx wy
|
N6 wx,
N4 wy =>
fn4 1
wx wy
|
N6 wx,
N5 wy =>
fn5 0
wx wy
|
N6 wx,
N6 wy =>
f6 wx wy
|
N6 wx,
Nn m wy =>
f6n m wx wy
|
Nn n wx,
N0 wy =>
fn6 n wx (
extend0 5
wy)
|
Nn n wx,
N1 wy =>
fn6 n wx (
extend1 4
wy)
|
Nn n wx,
N2 wy =>
fn6 n wx (
extend2 3
wy)
|
Nn n wx,
N3 wy =>
fn6 n wx (
extend3 2
wy)
|
Nn n wx,
N4 wy =>
fn6 n wx (
extend4 1
wy)
|
Nn n wx,
N5 wy =>
fn6 n wx (
extend5 0
wy)
|
Nn n wx,
N6 wy =>
fn6 n wx wy
|
Nn n wx,
Nn m wy =>
fnm n m wx wy
end.
Ltac zg_tac :=
try
(
red;
simpl Zcompare;
auto;
let t :=
fresh "H"
in (
intros t;
discriminate t)).
Lemma spec_iter:
forall x y,
P [
x] [
y] (
iter x y).
Definition iter0 (
x y:
t_):
res :=
Eval lazy zeta beta iota delta [
extend0 extend1 extend2 extend3 extend4 extend5 extend6
DoubleBase.extend DoubleBase.extend_aux
]
in
match x with
|
N0 wx =>
if w0_eq0 wx then f0t y else
match y with
|
N0 wy =>
f0 wx wy
|
N1 wy =>
f0n 0
wx wy
|
N2 wy =>
f0n 1
wx wy
|
N3 wy =>
f0n 2
wx wy
|
N4 wy =>
f0n 3
wx wy
|
N5 wy =>
f0n 4
wx wy
|
N6 wy =>
f0n 5
wx wy
|
Nn m wy =>
f6n m (
extend0 5
wx)
wy
end
|
N1 wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
fn0 0
wx wy
|
N1 wy =>
f1 wx wy
|
N2 wy =>
f1n 0
wx wy
|
N3 wy =>
f1n 1
wx wy
|
N4 wy =>
f1n 2
wx wy
|
N5 wy =>
f1n 3
wx wy
|
N6 wy =>
f1n 4
wx wy
|
Nn m wy =>
f6n m (
extend1 4
wx)
wy
end
|
N2 wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
fn0 1
wx wy
|
N1 wy =>
fn1 0
wx wy
|
N2 wy =>
f2 wx wy
|
N3 wy =>
f2n 0
wx wy
|
N4 wy =>
f2n 1
wx wy
|
N5 wy =>
f2n 2
wx wy
|
N6 wy =>
f2n 3
wx wy
|
Nn m wy =>
f6n m (
extend2 3
wx)
wy
end
|
N3 wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
fn0 2
wx wy
|
N1 wy =>
fn1 1
wx wy
|
N2 wy =>
fn2 0
wx wy
|
N3 wy =>
f3 wx wy
|
N4 wy =>
f3n 0
wx wy
|
N5 wy =>
f3n 1
wx wy
|
N6 wy =>
f3n 2
wx wy
|
Nn m wy =>
f6n m (
extend3 2
wx)
wy
end
|
N4 wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
fn0 3
wx wy
|
N1 wy =>
fn1 2
wx wy
|
N2 wy =>
fn2 1
wx wy
|
N3 wy =>
fn3 0
wx wy
|
N4 wy =>
f4 wx wy
|
N5 wy =>
f4n 0
wx wy
|
N6 wy =>
f4n 1
wx wy
|
Nn m wy =>
f6n m (
extend4 1
wx)
wy
end
|
N5 wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
fn0 4
wx wy
|
N1 wy =>
fn1 3
wx wy
|
N2 wy =>
fn2 2
wx wy
|
N3 wy =>
fn3 1
wx wy
|
N4 wy =>
fn4 0
wx wy
|
N5 wy =>
f5 wx wy
|
N6 wy =>
f5n 0
wx wy
|
Nn m wy =>
f6n m (
extend5 0
wx)
wy
end
|
N6 wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
fn0 5
wx wy
|
N1 wy =>
fn1 4
wx wy
|
N2 wy =>
fn2 3
wx wy
|
N3 wy =>
fn3 2
wx wy
|
N4 wy =>
fn4 1
wx wy
|
N5 wy =>
fn5 0
wx wy
|
N6 wy =>
f6 wx wy
|
Nn m wy =>
f6n m wx wy
end
|
Nn n wx =>
match y with
|
N0 wy =>
if w0_eq0 wy then ft0 x else
fn6 n wx (
extend0 5
wy)
|
N1 wy =>
fn6 n wx (
extend1 4
wy)
|
N2 wy =>
fn6 n wx (
extend2 3
wy)
|
N3 wy =>
fn6 n wx (
extend3 2
wy)
|
N4 wy =>
fn6 n wx (
extend4 1
wy)
|
N5 wy =>
fn6 n wx (
extend5 0
wy)
|
N6 wy =>
fn6 n wx wy
|
Nn m wy =>
fnm n m wx wy
end
end.
Lemma spec_iter0:
forall x y,
P [
x] [
y] (
iter0 x y).
End LevelAndIter.
Definition reduce_0 (
x:w) :=
N0 x.
Definition reduce_1 :=
Eval lazy beta iota delta[
reduce_n1]
in
reduce_n1 _ _ zero w0_eq0 N0 N1.
Definition reduce_2 :=
Eval lazy beta iota delta[
reduce_n1]
in
reduce_n1 _ _ zero w1_eq0 reduce_1 N2.
Definition reduce_3 :=
Eval lazy beta iota delta[
reduce_n1]
in
reduce_n1 _ _ zero w2_eq0 reduce_2 N3.
Definition reduce_4 :=
Eval lazy beta iota delta[
reduce_n1]
in
reduce_n1 _ _ zero w3_eq0 reduce_3 N4.
Definition reduce_5 :=
Eval lazy beta iota delta[
reduce_n1]
in
reduce_n1 _ _ zero w4_eq0 reduce_4 N5.
Definition reduce_6 :=
Eval lazy beta iota delta[
reduce_n1]
in
reduce_n1 _ _ zero w5_eq0 reduce_5 N6.
Definition reduce_7 :=
Eval lazy beta iota delta[
reduce_n1]
in
reduce_n1 _ _ zero w6_eq0 reduce_6 (
Nn 0).
Definition reduce_n n :=
Eval lazy beta iota delta[
reduce_n]
in
reduce_n _ _ zero reduce_7 Nn n.
Let spec_reduce_0:
forall x, [
reduce_0 x] = [
N0 x].
Let spec_reduce_1:
forall x, [
reduce_1 x] = [
N1 x].
Let spec_reduce_2:
forall x, [
reduce_2 x] = [
N2 x].
Let spec_reduce_3:
forall x, [
reduce_3 x] = [
N3 x].
Let spec_reduce_4:
forall x, [
reduce_4 x] = [
N4 x].
Let spec_reduce_5:
forall x, [
reduce_5 x] = [
N5 x].
Let spec_reduce_6:
forall x, [
reduce_6 x] = [
N6 x].
Let spec_reduce_7:
forall x, [
reduce_7 x] = [
Nn 0
x].
Let spec_reduce_n:
forall n x, [
reduce_n n x] = [
Nn n x].
Definition w0_succ_c :=
w0_op.(
znz_succ_c).
Definition w1_succ_c :=
w1_op.(
znz_succ_c).
Definition w2_succ_c :=
w2_op.(
znz_succ_c).
Definition w3_succ_c :=
w3_op.(
znz_succ_c).
Definition w4_succ_c :=
w4_op.(
znz_succ_c).
Definition w5_succ_c :=
w5_op.(
znz_succ_c).
Definition w6_succ_c :=
w6_op.(
znz_succ_c).
Definition w0_succ :=
w0_op.(
znz_succ).
Definition w1_succ :=
w1_op.(
znz_succ).
Definition w2_succ :=
w2_op.(
znz_succ).
Definition w3_succ :=
w3_op.(
znz_succ).
Definition w4_succ :=
w4_op.(
znz_succ).
Definition w5_succ :=
w5_op.(
znz_succ).
Definition w6_succ :=
w6_op.(
znz_succ).
Definition succ x :=
match x with
|
N0 wx =>
match w0_succ_c wx with
|
C0 r =>
N0 r
|
C1 r =>
N1 (
WW one0 r)
end
|
N1 wx =>
match w1_succ_c wx with
|
C0 r =>
N1 r
|
C1 r =>
N2 (
WW one1 r)
end
|
N2 wx =>
match w2_succ_c wx with
|
C0 r =>
N2 r
|
C1 r =>
N3 (
WW one2 r)
end
|
N3 wx =>
match w3_succ_c wx with
|
C0 r =>
N3 r
|
C1 r =>
N4 (
WW one3 r)
end
|
N4 wx =>
match w4_succ_c wx with
|
C0 r =>
N4 r
|
C1 r =>
N5 (
WW one4 r)
end
|
N5 wx =>
match w5_succ_c wx with
|
C0 r =>
N5 r
|
C1 r =>
N6 (
WW one5 r)
end
|
N6 wx =>
match w6_succ_c wx with
|
C0 r =>
N6 r
|
C1 r =>
Nn 0 (
WW one6 r)
end
|
Nn n wx =>
let op :=
make_op n in
match op.(
znz_succ_c)
wx with
|
C0 r =>
Nn n r
|
C1 r =>
Nn (
S n) (
WW op.(
znz_1)
r)
end
end.
Theorem spec_succ:
forall n, [
succ n] = [
n] + 1.
Definition w0_add_c :=
znz_add_c w0_op.
Definition w0_add x y :=
match w0_add_c x y with
|
C0 r =>
N0 r
|
C1 r =>
N1 (
WW one0 r)
end.
Definition w1_add_c :=
znz_add_c w1_op.
Definition w1_add x y :=
match w1_add_c x y with
|
C0 r =>
N1 r
|
C1 r =>
N2 (
WW one1 r)
end.
Definition w2_add_c :=
znz_add_c w2_op.
Definition w2_add x y :=
match w2_add_c x y with
|
C0 r =>
N2 r
|
C1 r =>
N3 (
WW one2 r)
end.
Definition w3_add_c :=
znz_add_c w3_op.
Definition w3_add x y :=
match w3_add_c x y with
|
C0 r =>
N3 r
|
C1 r =>
N4 (
WW one3 r)
end.
Definition w4_add_c :=
znz_add_c w4_op.
Definition w4_add x y :=
match w4_add_c x y with
|
C0 r =>
N4 r
|
C1 r =>
N5 (
WW one4 r)
end.
Definition w5_add_c :=
znz_add_c w5_op.
Definition w5_add x y :=
match w5_add_c x y with
|
C0 r =>
N5 r
|
C1 r =>
N6 (
WW one5 r)
end.
Definition w6_add_c :=
znz_add_c w6_op.
Definition w6_add x y :=
match w6_add_c x y with
|
C0 r =>
N6 r
|
C1 r =>
Nn 0 (
WW one6 r)
end.
Definition addn n (
x y :
word w6 (
S n)) :=
let op :=
make_op n in
match op.(
znz_add_c)
x y with
|
C0 r =>
Nn n r
|
C1 r =>
Nn (
S n) (
WW op.(
znz_1)
r)
end.
Let spec_w0_add:
forall x y, [
w0_add x y] = [
N0 x] + [
N0 y].
Hint Rewrite spec_w0_add:
addr.
Let spec_w1_add:
forall x y, [
w1_add x y] = [
N1 x] + [
N1 y].
Hint Rewrite spec_w1_add:
addr.
Let spec_w2_add:
forall x y, [
w2_add x y] = [
N2 x] + [
N2 y].
Hint Rewrite spec_w2_add:
addr.
Let spec_w3_add:
forall x y, [
w3_add x y] = [
N3 x] + [
N3 y].
Hint Rewrite spec_w3_add:
addr.
Let spec_w4_add:
forall x y, [
w4_add x y] = [
N4 x] + [
N4 y].
Hint Rewrite spec_w4_add:
addr.
Let spec_w5_add:
forall x y, [
w5_add x y] = [
N5 x] + [
N5 y].
Hint Rewrite spec_w5_add:
addr.
Let spec_w6_add:
forall x y, [
w6_add x y] = [
N6 x] + [
N6 y].
Hint Rewrite spec_w6_add:
addr.
Let spec_wn_add:
forall n x y, [
addn n x y] = [
Nn n x] + [
Nn n y].
Hint Rewrite spec_wn_add:
addr.
Definition add :=
Eval lazy beta delta [
same_level]
in
(
same_level t_ w0_add w1_add w2_add w3_add w4_add w5_add w6_add addn).
Theorem spec_add:
forall x y, [
add x y] = [
x] + [
y].
Definition w0_pred_c :=
w0_op.(
znz_pred_c).
Definition w1_pred_c :=
w1_op.(
znz_pred_c).
Definition w2_pred_c :=
w2_op.(
znz_pred_c).
Definition w3_pred_c :=
w3_op.(
znz_pred_c).
Definition w4_pred_c :=
w4_op.(
znz_pred_c).
Definition w5_pred_c :=
w5_op.(
znz_pred_c).
Definition w6_pred_c :=
w6_op.(
znz_pred_c).
Definition pred x :=
match x with
|
N0 wx =>
match w0_pred_c wx with
|
C0 r =>
reduce_0 r
|
C1 r =>
zero
end
|
N1 wx =>
match w1_pred_c wx with
|
C0 r =>
reduce_1 r
|
C1 r =>
zero
end
|
N2 wx =>
match w2_pred_c wx with
|
C0 r =>
reduce_2 r
|
C1 r =>
zero
end
|
N3 wx =>
match w3_pred_c wx with
|
C0 r =>
reduce_3 r
|
C1 r =>
zero
end
|
N4 wx =>
match w4_pred_c wx with
|
C0 r =>
reduce_4 r
|
C1 r =>
zero
end
|
N5 wx =>
match w5_pred_c wx with
|
C0 r =>
reduce_5 r
|
C1 r =>
zero
end
|
N6 wx =>
match w6_pred_c wx with
|
C0 r =>
reduce_6 r
|
C1 r =>
zero
end
|
Nn n wx =>
let op :=
make_op n in
match op.(
znz_pred_c)
wx with
|
C0 r =>
reduce_n n r
|
C1 r =>
zero
end
end.
Theorem spec_pred:
forall x, 0 < [
x] -> [
pred x] = [
x] - 1.
Let spec_pred0:
forall x, [
x] = 0 -> [
pred x] = 0.
Definition w0_sub_c :=
w0_op.(
znz_sub_c).
Definition w1_sub_c :=
w1_op.(
znz_sub_c).
Definition w2_sub_c :=
w2_op.(
znz_sub_c).
Definition w3_sub_c :=
w3_op.(
znz_sub_c).
Definition w4_sub_c :=
w4_op.(
znz_sub_c).
Definition w5_sub_c :=
w5_op.(
znz_sub_c).
Definition w6_sub_c :=
w6_op.(
znz_sub_c).
Definition w0_sub x y :=
match w0_sub_c x y with
|
C0 r =>
reduce_0 r
|
C1 r =>
zero
end.
Definition w1_sub x y :=
match w1_sub_c x y with
|
C0 r =>
reduce_1 r
|
C1 r =>
zero
end.
Definition w2_sub x y :=
match w2_sub_c x y with
|
C0 r =>
reduce_2 r
|
C1 r =>
zero
end.
Definition w3_sub x y :=
match w3_sub_c x y with
|
C0 r =>
reduce_3 r
|
C1 r =>
zero
end.
Definition w4_sub x y :=
match w4_sub_c x y with
|
C0 r =>
reduce_4 r
|
C1 r =>
zero
end.
Definition w5_sub x y :=
match w5_sub_c x y with
|
C0 r =>
reduce_5 r
|
C1 r =>
zero
end.
Definition w6_sub x y :=
match w6_sub_c x y with
|
C0 r =>
reduce_6 r
|
C1 r =>
zero
end.
Definition subn n (
x y :
word w6 (
S n)) :=
let op :=
make_op n in
match op.(
znz_sub_c)
x y with
|
C0 r =>
Nn n r
|
C1 r =>
N0 w_0
end.
Let spec_w0_sub:
forall x y, [
N0 y] <= [
N0 x] -> [
w0_sub x y] = [
N0 x] - [
N0 y].
Let spec_w1_sub:
forall x y, [
N1 y] <= [
N1 x] -> [
w1_sub x y] = [
N1 x] - [
N1 y].
Let spec_w2_sub:
forall x y, [
N2 y] <= [
N2 x] -> [
w2_sub x y] = [
N2 x] - [
N2 y].
Let spec_w3_sub:
forall x y, [
N3 y] <= [
N3 x] -> [
w3_sub x y] = [
N3 x] - [
N3 y].
Let spec_w4_sub:
forall x y, [
N4 y] <= [
N4 x] -> [
w4_sub x y] = [
N4 x] - [
N4 y].
Let spec_w5_sub:
forall x y, [
N5 y] <= [
N5 x] -> [
w5_sub x y] = [
N5 x] - [
N5 y].
Let spec_w6_sub:
forall x y, [
N6 y] <= [
N6 x] -> [
w6_sub x y] = [
N6 x] - [
N6 y].
Let spec_wn_sub:
forall n x y, [
Nn n y] <= [
Nn n x] -> [
subn n x y] = [
Nn n x] - [
Nn n y].
Definition sub :=
Eval lazy beta delta [
same_level]
in
(
same_level t_ w0_sub w1_sub w2_sub w3_sub w4_sub w5_sub w6_sub subn).
Theorem spec_sub:
forall x y, [
y] <= [
x] -> [
sub x y] = [
x] - [
y].
Let spec_w0_sub0:
forall x y, [
N0 x] < [
N0 y] -> [
w0_sub x y] = 0.
Let spec_w1_sub0:
forall x y, [
N1 x] < [
N1 y] -> [
w1_sub x y] = 0.
Let spec_w2_sub0:
forall x y, [
N2 x] < [
N2 y] -> [
w2_sub x y] = 0.
Let spec_w3_sub0:
forall x y, [
N3 x] < [
N3 y] -> [
w3_sub x y] = 0.
Let spec_w4_sub0:
forall x y, [
N4 x] < [
N4 y] -> [
w4_sub x y] = 0.
Let spec_w5_sub0:
forall x y, [
N5 x] < [
N5 y] -> [
w5_sub x y] = 0.
Let spec_w6_sub0:
forall x y, [
N6 x] < [
N6 y] -> [
w6_sub x y] = 0.
Let spec_wn_sub0:
forall n x y, [
Nn n x] < [
Nn n y] -> [
subn n x y] = 0.
Theorem spec_sub0:
forall x y, [
x] < [
y] -> [
sub x y] = 0.
Definition compare_0 :=
w0_op.(
znz_compare).
Definition comparen_0 :=
compare_mn_1 w0 w0 w_0 compare_0 (
compare_0 w_0)
compare_0.
Definition compare_1 :=
w1_op.(
znz_compare).
Definition comparen_1 :=
compare_mn_1 w1 w1 W0 compare_1 (
compare_1 W0)
compare_1.
Definition compare_2 :=
w2_op.(
znz_compare).
Definition comparen_2 :=
compare_mn_1 w2 w2 W0 compare_2 (
compare_2 W0)
compare_2.
Definition compare_3 :=
w3_op.(
znz_compare).
Definition comparen_3 :=
compare_mn_1 w3 w3 W0 compare_3 (
compare_3 W0)
compare_3.
Definition compare_4 :=
w4_op.(
znz_compare).
Definition comparen_4 :=
compare_mn_1 w4 w4 W0 compare_4 (
compare_4 W0)
compare_4.
Definition compare_5 :=
w5_op.(
znz_compare).
Definition comparen_5 :=
compare_mn_1 w5 w5 W0 compare_5 (
compare_5 W0)
compare_5.
Definition compare_6 :=
w6_op.(
znz_compare).
Definition comparen_6 :=
compare_mn_1 w6 w6 W0 compare_6 (
compare_6 W0)
compare_6.
Definition comparenm n m wx wy :=
let mn :=
Max.max n m in
let d :=
diff n m in
let op :=
make_op mn in
op.(
znz_compare)
(
castm (
diff_r n m) (
extend_tr wx (
snd d)))
(
castm (
diff_l n m) (
extend_tr wy (
fst d))).
Definition compare :=
Eval lazy beta delta [
iter]
in
(
iter _
compare_0
(
fun n x y =>
opp_compare (
comparen_0 (
S n)
y x))
(
fun n =>
comparen_0 (
S n))
compare_1
(
fun n x y =>
opp_compare (
comparen_1 (
S n)
y x))
(
fun n =>
comparen_1 (
S n))
compare_2
(
fun n x y =>
opp_compare (
comparen_2 (
S n)
y x))
(
fun n =>
comparen_2 (
S n))
compare_3
(
fun n x y =>
opp_compare (
comparen_3 (
S n)
y x))
(
fun n =>
comparen_3 (
S n))
compare_4
(
fun n x y =>
opp_compare (
comparen_4 (
S n)
y x))
(
fun n =>
comparen_4 (
S n))
compare_5
(
fun n x y =>
opp_compare (
comparen_5 (
S n)
y x))
(
fun n =>
comparen_5 (
S n))
compare_6
(
fun n x y =>
opp_compare (
comparen_6 (
S n)
y x))
(
fun n =>
comparen_6 (
S n))
comparenm).
Definition lt n m :=
compare n m =
Lt.
Definition le n m :=
compare n m <>
Gt.
Definition min n m :=
match compare n m with Gt =>
m |
_ =>
n end.
Definition max n m :=
match compare n m with Lt =>
m |
_ =>
n end.
Let spec_compare_0:
forall x y,
match compare_0 x y with
Eq => [
N0 x] = [
N0 y]
|
Lt => [
N0 x] < [
N0 y]
|
Gt => [
N0 x] > [
N0 y]
end.
Let spec_comparen_0:
forall (
n :
nat) (
x :
word w0 n) (
y :
w0),
match comparen_0 n x y with
|
Eq =>
eval0n n x = [
N0 y]
|
Lt =>
eval0n n x < [
N0 y]
|
Gt =>
eval0n n x > [
N0 y]
end.
Qed.
Let spec_compare_1:
forall x y,
match compare_1 x y with
Eq => [
N1 x] = [
N1 y]
|
Lt => [
N1 x] < [
N1 y]
|
Gt => [
N1 x] > [
N1 y]
end.
Let spec_comparen_1:
forall (
n :
nat) (
x :
word w1 n) (
y :
w1),
match comparen_1 n x y with
|
Eq =>
eval1n n x = [
N1 y]
|
Lt =>
eval1n n x < [
N1 y]
|
Gt =>
eval1n n x > [
N1 y]
end.
Qed.
Let spec_compare_2:
forall x y,
match compare_2 x y with
Eq => [
N2 x] = [
N2 y]
|
Lt => [
N2 x] < [
N2 y]
|
Gt => [
N2 x] > [
N2 y]
end.
Let spec_comparen_2:
forall (
n :
nat) (
x :
word w2 n) (
y :
w2),
match comparen_2 n x y with
|
Eq =>
eval2n n x = [
N2 y]
|
Lt =>
eval2n n x < [
N2 y]
|
Gt =>
eval2n n x > [
N2 y]
end.
Qed.
Let spec_compare_3:
forall x y,
match compare_3 x y with
Eq => [
N3 x] = [
N3 y]
|
Lt => [
N3 x] < [
N3 y]
|
Gt => [
N3 x] > [
N3 y]
end.
Let spec_comparen_3:
forall (
n :
nat) (
x :
word w3 n) (
y :
w3),
match comparen_3 n x y with
|
Eq =>
eval3n n x = [
N3 y]
|
Lt =>
eval3n n x < [
N3 y]
|
Gt =>
eval3n n x > [
N3 y]
end.
Qed.
Let spec_compare_4:
forall x y,
match compare_4 x y with
Eq => [
N4 x] = [
N4 y]
|
Lt => [
N4 x] < [
N4 y]
|
Gt => [
N4 x] > [
N4 y]
end.
Let spec_comparen_4:
forall (
n :
nat) (
x :
word w4 n) (
y :
w4),
match comparen_4 n x y with
|
Eq =>
eval4n n x = [
N4 y]
|
Lt =>
eval4n n x < [
N4 y]
|
Gt =>
eval4n n x > [
N4 y]
end.
Qed.
Let spec_compare_5:
forall x y,
match compare_5 x y with
Eq => [
N5 x] = [
N5 y]
|
Lt => [
N5 x] < [
N5 y]
|
Gt => [
N5 x] > [
N5 y]
end.
Let spec_comparen_5:
forall (
n :
nat) (
x :
word w5 n) (
y :
w5),
match comparen_5 n x y with
|
Eq =>
eval5n n x = [
N5 y]
|
Lt =>
eval5n n x < [
N5 y]
|
Gt =>
eval5n n x > [
N5 y]
end.
Qed.
Let spec_compare_6:
forall x y,
match compare_6 x y with
Eq => [
N6 x] = [
N6 y]
|
Lt => [
N6 x] < [
N6 y]
|
Gt => [
N6 x] > [
N6 y]
end.
Let spec_comparen_6:
forall (
n :
nat) (
x :
word w6 n) (
y :
w6),
match comparen_6 n x y with
|
Eq =>
eval6n n x = [
N6 y]
|
Lt =>
eval6n n x < [
N6 y]
|
Gt =>
eval6n n x > [
N6 y]
end.
Qed.
Let spec_opp_compare:
forall c (
u v:
Z),
match c with Eq =>
u =
v |
Lt =>
u <
v |
Gt =>
u >
v end ->
match opp_compare c with Eq =>
v =
u |
Lt =>
v <
u |
Gt =>
v >
u end.
Theorem spec_compare:
forall x y,
match compare x y with
Eq => [
x] = [
y]
|
Lt => [
x] < [
y]
|
Gt => [
x] > [
y]
end.
Definition eq_bool x y :=
match compare x y with
|
Eq =>
true
|
_ =>
false
end.
Theorem spec_eq_bool:
forall x y,
if eq_bool x y then [
x] = [
y]
else [
x] <> [
y].
Definition w0_mul_c :=
w0_op.(
znz_mul_c).
Definition w1_mul_c :=
w1_op.(
znz_mul_c).
Definition w2_mul_c :=
w2_op.(
znz_mul_c).
Definition w3_mul_c :=
w3_op.(
znz_mul_c).
Definition w4_mul_c :=
w4_op.(
znz_mul_c).
Definition w5_mul_c :=
w5_op.(
znz_mul_c).
Definition w6_mul_c :=
w6_op.(
znz_mul_c).
Definition w0_mul_add :=
Eval lazy beta delta [
w_mul_add]
in
@
w_mul_add w0 w_0 w0_succ w0_add_c w0_mul_c.
Definition w1_mul_add :=
Eval lazy beta delta [
w_mul_add]
in
@
w_mul_add w1 W0 w1_succ w1_add_c w1_mul_c.
Definition w2_mul_add :=
Eval lazy beta delta [
w_mul_add]
in
@
w_mul_add w2 W0 w2_succ w2_add_c w2_mul_c.
Definition w3_mul_add :=
Eval lazy beta delta [
w_mul_add]
in
@
w_mul_add w3 W0 w3_succ w3_add_c w3_mul_c.
Definition w4_mul_add :=
Eval lazy beta delta [
w_mul_add]
in
@
w_mul_add w4 W0 w4_succ w4_add_c w4_mul_c.
Definition w5_mul_add :=
Eval lazy beta delta [
w_mul_add]
in
@
w_mul_add w5 W0 w5_succ w5_add_c w5_mul_c.
Definition w6_mul_add :=
Eval lazy beta delta [
w_mul_add]
in
@
w_mul_add w6 W0 w6_succ w6_add_c w6_mul_c.
Definition w0_0W :=
znz_0W w0_op.
Definition w1_0W :=
znz_0W w1_op.
Definition w2_0W :=
znz_0W w2_op.
Definition w3_0W :=
znz_0W w3_op.
Definition w4_0W :=
znz_0W w4_op.
Definition w5_0W :=
znz_0W w5_op.
Definition w6_0W :=
znz_0W w6_op.
Definition w0_WW :=
znz_WW w0_op.
Definition w1_WW :=
znz_WW w1_op.
Definition w2_WW :=
znz_WW w2_op.
Definition w3_WW :=
znz_WW w3_op.
Definition w4_WW :=
znz_WW w4_op.
Definition w5_WW :=
znz_WW w5_op.
Definition w6_WW :=
znz_WW w6_op.
Definition w0_mul_add_n1 :=
@
double_mul_add_n1 w0 w_0 w0_WW w0_0W w0_mul_add.
Definition w1_mul_add_n1 :=
@
double_mul_add_n1 w1 W0 w1_WW w1_0W w1_mul_add.
Definition w2_mul_add_n1 :=
@
double_mul_add_n1 w2 W0 w2_WW w2_0W w2_mul_add.
Definition w3_mul_add_n1 :=
@
double_mul_add_n1 w3 W0 w3_WW w3_0W w3_mul_add.
Definition w4_mul_add_n1 :=
@
double_mul_add_n1 w4 W0 w4_WW w4_0W w4_mul_add.
Definition w5_mul_add_n1 :=
@
double_mul_add_n1 w5 W0 w5_WW w5_0W w5_mul_add.
Definition w6_mul_add_n1 :=
@
double_mul_add_n1 w6 W0 w6_WW w6_0W w6_mul_add.
Let to_Z0 n :=
match n return word w0 (
S n) ->
t_ with
| 0%nat =>
fun x =>
N1 x
| 1%nat =>
fun x =>
N2 x
| 2%nat =>
fun x =>
N3 x
| 3%nat =>
fun x =>
N4 x
| 4%nat =>
fun x =>
N5 x
| 5%nat =>
fun x =>
N6 x
| 6%nat =>
fun x =>
Nn 0
x
| 7%nat =>
fun x =>
Nn 1
x
|
_ =>
fun _ =>
N0 w_0
end.
Let to_Z1 n :=
match n return word w1 (
S n) ->
t_ with
| 0%nat =>
fun x =>
N2 x
| 1%nat =>
fun x =>
N3 x
| 2%nat =>
fun x =>
N4 x
| 3%nat =>
fun x =>
N5 x
| 4%nat =>
fun x =>
N6 x
| 5%nat =>
fun x =>
Nn 0
x
| 6%nat =>
fun x =>
Nn 1
x
|
_ =>
fun _ =>
N0 w_0
end.
Let to_Z2 n :=
match n return word w2 (
S n) ->
t_ with
| 0%nat =>
fun x =>
N3 x
| 1%nat =>
fun x =>
N4 x
| 2%nat =>
fun x =>
N5 x
| 3%nat =>
fun x =>
N6 x
| 4%nat =>
fun x =>
Nn 0
x
| 5%nat =>
fun x =>
Nn 1
x
|
_ =>
fun _ =>
N0 w_0
end.
Let to_Z3 n :=
match n return word w3 (
S n) ->
t_ with
| 0%nat =>
fun x =>
N4 x
| 1%nat =>
fun x =>
N5 x
| 2%nat =>
fun x =>
N6 x
| 3%nat =>
fun x =>
Nn 0
x
| 4%nat =>
fun x =>
Nn 1
x
|
_ =>
fun _ =>
N0 w_0
end.
Let to_Z4 n :=
match n return word w4 (
S n) ->
t_ with
| 0%nat =>
fun x =>
N5 x
| 1%nat =>
fun x =>
N6 x
| 2%nat =>
fun x =>
Nn 0
x
| 3%nat =>
fun x =>
Nn 1
x
|
_ =>
fun _ =>
N0 w_0
end.
Let to_Z5 n :=
match n return word w5 (
S n) ->
t_ with
| 0%nat =>
fun x =>
N6 x
| 1%nat =>
fun x =>
Nn 0
x
| 2%nat =>
fun x =>
Nn 1
x
|
_ =>
fun _ =>
N0 w_0
end.
Theorem to_Z0_spec:
forall n x,
Z_of_nat n <= 7 -> [
to_Z0 n x] =
znz_to_Z (
nmake_op _ w0_op (
S n))
x.
Theorem to_Z1_spec:
forall n x,
Z_of_nat n <= 6 -> [
to_Z1 n x] =
znz_to_Z (
nmake_op _ w1_op (
S n))
x.
Theorem to_Z2_spec:
forall n x,
Z_of_nat n <= 5 -> [
to_Z2 n x] =
znz_to_Z (
nmake_op _ w2_op (
S n))
x.
Theorem to_Z3_spec:
forall n x,
Z_of_nat n <= 4 -> [
to_Z3 n x] =
znz_to_Z (
nmake_op _ w3_op (
S n))
x.
Theorem to_Z4_spec:
forall n x,
Z_of_nat n <= 3 -> [
to_Z4 n x] =
znz_to_Z (
nmake_op _ w4_op (
S n))
x.
Theorem to_Z5_spec:
forall n x,
Z_of_nat n <= 2 -> [
to_Z5 n x] =
znz_to_Z (
nmake_op _ w5_op (
S n))
x.
Definition w0_mul n x y :=
let (
w,r) :=
w0_mul_add_n1 (
S n)
x y w_0 in
if w0_eq0 w then to_Z0 n r
else to_Z0 (
S n) (
WW (
extend0 n w)
r).
Definition w1_mul n x y :=
let (
w,r) :=
w1_mul_add_n1 (
S n)
x y W0 in
if w1_eq0 w then to_Z1 n r
else to_Z1 (
S n) (
WW (
extend1 n w)
r).
Definition w2_mul n x y :=
let (
w,r) :=
w2_mul_add_n1 (
S n)
x y W0 in
if w2_eq0 w then to_Z2 n r
else to_Z2 (
S n) (
WW (
extend2 n w)
r).
Definition w3_mul n x y :=
let (
w,r) :=
w3_mul_add_n1 (
S n)
x y W0 in
if w3_eq0 w then to_Z3 n r
else to_Z3 (
S n) (
WW (
extend3 n w)
r).
Definition w4_mul n x y :=
let (
w,r) :=
w4_mul_add_n1 (
S n)
x y W0 in
if w4_eq0 w then to_Z4 n r
else to_Z4 (
S n) (
WW (
extend4 n w)
r).
Definition w5_mul n x y :=
let (
w,r) :=
w5_mul_add_n1 (
S n)
x y W0 in
if w5_eq0 w then to_Z5 n r
else to_Z5 (
S n) (
WW (
extend5 n w)
r).
Definition w6_mul n x y :=
let (
w,r) :=
w6_mul_add_n1 (
S n)
x y W0 in
if w6_eq0 w then Nn n r
else Nn (
S n) (
WW (
extend6 n w)
r).
Definition mulnm n m x y :=
let mn :=
Max.max n m in
let d :=
diff n m in
let op :=
make_op mn in
reduce_n (
S mn) (
op.(
znz_mul_c)
(
castm (
diff_r n m) (
extend_tr x (
snd d)))
(
castm (
diff_l n m) (
extend_tr y (
fst d)))).
Definition mul :=
Eval lazy beta delta [
iter0]
in
(
iter0 t_
(
fun x y =>
reduce_1 (
w0_mul_c x y))
(
fun n x y =>
w0_mul n y x)
w0_mul
(
fun x y =>
reduce_2 (
w1_mul_c x y))
(
fun n x y =>
w1_mul n y x)
w1_mul
(
fun x y =>
reduce_3 (
w2_mul_c x y))
(
fun n x y =>
w2_mul n y x)
w2_mul
(
fun x y =>
reduce_4 (
w3_mul_c x y))
(
fun n x y =>
w3_mul n y x)
w3_mul
(
fun x y =>
reduce_5 (
w4_mul_c x y))
(
fun n x y =>
w4_mul n y x)
w4_mul
(
fun x y =>
reduce_6 (
w5_mul_c x y))
(
fun n x y =>
w5_mul n y x)
w5_mul
(
fun x y =>
reduce_7 (
w6_mul_c x y))
(
fun n x y =>
w6_mul n y x)
w6_mul
mulnm
(
fun _ =>
N0 w_0)
(
fun _ =>
N0 w_0)
).
Let spec_w0_mul_add:
forall x y z,
let (
q,r) :=
w0_mul_add x y z in
znz_to_Z w0_op q * (
base (
znz_digits w0_op)) +
znz_to_Z w0_op r =
znz_to_Z w0_op x *
znz_to_Z w0_op y +
znz_to_Z w0_op z :=
(
spec_mul_add w0_spec).
Let spec_w1_mul_add:
forall x y z,
let (
q,r) :=
w1_mul_add x y z in
znz_to_Z w1_op q * (
base (
znz_digits w1_op)) +
znz_to_Z w1_op r =
znz_to_Z w1_op x *
znz_to_Z w1_op y +
znz_to_Z w1_op z :=
(
spec_mul_add w1_spec).
Let spec_w2_mul_add:
forall x y z,
let (
q,r) :=
w2_mul_add x y z in
znz_to_Z w2_op q * (
base (
znz_digits w2_op)) +
znz_to_Z w2_op r =
znz_to_Z w2_op x *
znz_to_Z w2_op y +
znz_to_Z w2_op z :=
(
spec_mul_add w2_spec).
Let spec_w3_mul_add:
forall x y z,
let (
q,r) :=
w3_mul_add x y z in
znz_to_Z w3_op q * (
base (
znz_digits w3_op)) +
znz_to_Z w3_op r =
znz_to_Z w3_op x *
znz_to_Z w3_op y +
znz_to_Z w3_op z :=
(
spec_mul_add w3_spec).
Let spec_w4_mul_add:
forall x y z,
let (
q,r) :=
w4_mul_add x y z in
znz_to_Z w4_op q * (
base (
znz_digits w4_op)) +
znz_to_Z w4_op r =
znz_to_Z w4_op x *
znz_to_Z w4_op y +
znz_to_Z w4_op z :=
(
spec_mul_add w4_spec).
Let spec_w5_mul_add:
forall x y z,
let (
q,r) :=
w5_mul_add x y z in
znz_to_Z w5_op q * (
base (
znz_digits w5_op)) +
znz_to_Z w5_op r =
znz_to_Z w5_op x *
znz_to_Z w5_op y +
znz_to_Z w5_op z :=
(
spec_mul_add w5_spec).
Let spec_w6_mul_add:
forall x y z,
let (
q,r) :=
w6_mul_add x y z in
znz_to_Z w6_op q * (
base (
znz_digits w6_op)) +
znz_to_Z w6_op r =
znz_to_Z w6_op x *
znz_to_Z w6_op y +
znz_to_Z w6_op z :=
(
spec_mul_add w6_spec).
Theorem spec_w0_mul_add_n1:
forall n x y z,
let (
q,r) :=
w0_mul_add_n1 n x y z in
znz_to_Z w0_op q * (
base (
znz_digits (
nmake_op _ w0_op n))) +
znz_to_Z (
nmake_op _ w0_op n)
r =
znz_to_Z (
nmake_op _ w0_op n)
x *
znz_to_Z w0_op y +
znz_to_Z w0_op z.
Theorem spec_w1_mul_add_n1:
forall n x y z,
let (
q,r) :=
w1_mul_add_n1 n x y z in
znz_to_Z w1_op q * (
base (
znz_digits (
nmake_op _ w1_op n))) +
znz_to_Z (
nmake_op _ w1_op n)
r =
znz_to_Z (
nmake_op _ w1_op n)
x *
znz_to_Z w1_op y +
znz_to_Z w1_op z.
Theorem spec_w2_mul_add_n1:
forall n x y z,
let (
q,r) :=
w2_mul_add_n1 n x y z in
znz_to_Z w2_op q * (
base (
znz_digits (
nmake_op _ w2_op n))) +
znz_to_Z (
nmake_op _ w2_op n)
r =
znz_to_Z (
nmake_op _ w2_op n)
x *
znz_to_Z w2_op y +
znz_to_Z w2_op z.
Theorem spec_w3_mul_add_n1:
forall n x y z,
let (
q,r) :=
w3_mul_add_n1 n x y z in
znz_to_Z w3_op q * (
base (
znz_digits (
nmake_op _ w3_op n))) +
znz_to_Z (
nmake_op _ w3_op n)
r =
znz_to_Z (
nmake_op _ w3_op n)
x *
znz_to_Z w3_op y +
znz_to_Z w3_op z.
Theorem spec_w4_mul_add_n1:
forall n x y z,
let (
q,r) :=
w4_mul_add_n1 n x y z in
znz_to_Z w4_op q * (
base (
znz_digits (
nmake_op _ w4_op n))) +
znz_to_Z (
nmake_op _ w4_op n)
r =
znz_to_Z (
nmake_op _ w4_op n)
x *
znz_to_Z w4_op y +
znz_to_Z w4_op z.
Theorem spec_w5_mul_add_n1:
forall n x y z,
let (
q,r) :=
w5_mul_add_n1 n x y z in
znz_to_Z w5_op q * (
base (
znz_digits (
nmake_op _ w5_op n))) +
znz_to_Z (
nmake_op _ w5_op n)
r =
znz_to_Z (
nmake_op _ w5_op n)
x *
znz_to_Z w5_op y +
znz_to_Z w5_op z.
Theorem spec_w6_mul_add_n1:
forall n x y z,
let (
q,r) :=
w6_mul_add_n1 n x y z in
znz_to_Z w6_op q * (
base (
znz_digits (
nmake_op _ w6_op n))) +
znz_to_Z (
nmake_op _ w6_op n)
r =
znz_to_Z (
nmake_op _ w6_op n)
x *
znz_to_Z w6_op y +
znz_to_Z w6_op z.
Lemma nmake_op_WW:
forall ww ww1 n x y,
znz_to_Z (
nmake_op ww ww1 (
S n)) (
WW x y) =
znz_to_Z (
nmake_op ww ww1 n)
x *
base (
znz_digits (
nmake_op ww ww1 n)) +
znz_to_Z (
nmake_op ww ww1 n)
y.
Lemma extend0n_spec:
forall n x1,
znz_to_Z (
nmake_op _ w0_op (
S n)) (
extend0 n x1) =
znz_to_Z w0_op x1.
Lemma extend1n_spec:
forall n x1,
znz_to_Z (
nmake_op _ w1_op (
S n)) (
extend1 n x1) =
znz_to_Z w1_op x1.
Lemma extend2n_spec:
forall n x1,
znz_to_Z (
nmake_op _ w2_op (
S n)) (
extend2 n x1) =
znz_to_Z w2_op x1.
Lemma extend3n_spec:
forall n x1,
znz_to_Z (
nmake_op _ w3_op (
S n)) (
extend3 n x1) =
znz_to_Z w3_op x1.
Lemma extend4n_spec:
forall n x1,
znz_to_Z (
nmake_op _ w4_op (
S n)) (
extend4 n x1) =
znz_to_Z w4_op x1.
Lemma extend5n_spec:
forall n x1,
znz_to_Z (
nmake_op _ w5_op (
S n)) (
extend5 n x1) =
znz_to_Z w5_op x1.
Lemma extend6n_spec:
forall n x1,
znz_to_Z (
nmake_op _ w6_op (
S n)) (
extend6 n x1) =
znz_to_Z w6_op x1.
Lemma spec_muln:
forall n (
x:
word _ (
S n))
y,
[
Nn (
S n) (
znz_mul_c (
make_op n)
x y)] = [
Nn n x] * [
Nn n y].
Theorem spec_mul:
forall x y, [
mul x y] = [
x] * [
y].
Definition w0_square_c :=
w0_op.(
znz_square_c).
Definition w1_square_c :=
w1_op.(
znz_square_c).
Definition w2_square_c :=
w2_op.(
znz_square_c).
Definition w3_square_c :=
w3_op.(
znz_square_c).
Definition w4_square_c :=
w4_op.(
znz_square_c).
Definition w5_square_c :=
w5_op.(
znz_square_c).
Definition w6_square_c :=
w6_op.(
znz_square_c).
Definition square x :=
match x with
|
N0 wx =>
reduce_1 (
w0_square_c wx)
|
N1 wx =>
N2 (
w1_square_c wx)
|
N2 wx =>
N3 (
w2_square_c wx)
|
N3 wx =>
N4 (
w3_square_c wx)
|
N4 wx =>
N5 (
w4_square_c wx)
|
N5 wx =>
N6 (
w5_square_c wx)
|
N6 wx =>
Nn 0 (
w6_square_c wx)
|
Nn n wx =>
let op :=
make_op n in
Nn (
S n) (
op.(
znz_square_c)
wx)
end.
Theorem spec_square:
forall x, [
square x] = [
x] * [
x].
Fixpoint power_pos (
x:t) (
p:positive) {
struct p} :
t :=
match p with
|
xH =>
x
|
xO p =>
square (
power_pos x p)
|
xI p =>
mul (
square (
power_pos x p))
x
end.
Theorem spec_power_pos:
forall x n, [
power_pos x n] = [
x] ^
Zpos n.
Definition w0_sqrt :=
w0_op.(
znz_sqrt).
Definition w1_sqrt :=
w1_op.(
znz_sqrt).
Definition w2_sqrt :=
w2_op.(
znz_sqrt).
Definition w3_sqrt :=
w3_op.(
znz_sqrt).
Definition w4_sqrt :=
w4_op.(
znz_sqrt).
Definition w5_sqrt :=
w5_op.(
znz_sqrt).
Definition w6_sqrt :=
w6_op.(
znz_sqrt).
Definition sqrt x :=
match x with
|
N0 wx =>
reduce_0 (
w0_sqrt wx)
|
N1 wx =>
reduce_1 (
w1_sqrt wx)
|
N2 wx =>
reduce_2 (
w2_sqrt wx)
|
N3 wx =>
reduce_3 (
w3_sqrt wx)
|
N4 wx =>
reduce_4 (
w4_sqrt wx)
|
N5 wx =>
reduce_5 (
w5_sqrt wx)
|
N6 wx =>
reduce_6 (
w6_sqrt wx)
|
Nn n wx =>
let op :=
make_op n in
reduce_n n (
op.(
znz_sqrt)
wx)
end.
Theorem spec_sqrt:
forall x, [
sqrt x] ^ 2 <= [
x] < ([
sqrt x] + 1) ^ 2.
Definition w0_div_gt :=
w0_op.(
znz_div_gt).
Definition w1_div_gt :=
w1_op.(
znz_div_gt).
Definition w2_div_gt :=
w2_op.(
znz_div_gt).
Definition w3_div_gt :=
w3_op.(
znz_div_gt).
Definition w4_div_gt :=
w4_op.(
znz_div_gt).
Definition w5_div_gt :=
w5_op.(
znz_div_gt).
Definition w6_div_gt :=
w6_op.(
znz_div_gt).
Let spec_divn1 ww (
ww_op:
znz_op ww) (
ww_spec:
znz_spec ww_op) :=
(
spec_double_divn1
ww_op.(
znz_zdigits)
ww_op.(
znz_0)
(
znz_WW ww_op)
ww_op.(
znz_head0)
ww_op.(
znz_add_mul_div)
ww_op.(
znz_div21)
ww_op.(
znz_compare)
ww_op.(
znz_sub) (
znz_to_Z ww_op)
(
spec_to_Z ww_spec)
(
spec_zdigits ww_spec)
(
spec_0 ww_spec) (
spec_WW ww_spec) (
spec_head0 ww_spec)
(
spec_add_mul_div ww_spec) (
spec_div21 ww_spec)
(
CyclicAxioms.spec_compare ww_spec) (
CyclicAxioms.spec_sub ww_spec)).
Definition w0_divn1 n x y :=
let (
u,
v) :=
double_divn1 w0_op.(
znz_zdigits)
w0_op.(
znz_0)
(
znz_WW w0_op)
w0_op.(
znz_head0)
w0_op.(
znz_add_mul_div)
w0_op.(
znz_div21)
w0_op.(
znz_compare)
w0_op.(
znz_sub) (
S n)
x y in
(
to_Z0 _ u,
N0 v).
Definition w1_divn1 n x y :=
let (
u,
v) :=
double_divn1 w1_op.(
znz_zdigits)
w1_op.(
znz_0)
(
znz_WW w1_op)
w1_op.(
znz_head0)
w1_op.(
znz_add_mul_div)
w1_op.(
znz_div21)
w1_op.(
znz_compare)
w1_op.(
znz_sub) (
S n)
x y in
(
to_Z1 _ u,
N1 v).
Definition w2_divn1 n x y :=
let (
u,
v) :=
double_divn1 w2_op.(
znz_zdigits)
w2_op.(
znz_0)
(
znz_WW w2_op)
w2_op.(
znz_head0)
w2_op.(
znz_add_mul_div)
w2_op.(
znz_div21)
w2_op.(
znz_compare)
w2_op.(
znz_sub) (
S n)
x y in
(
to_Z2 _ u,
N2 v).
Definition w3_divn1 n x y :=
let (
u,
v) :=
double_divn1 w3_op.(
znz_zdigits)
w3_op.(
znz_0)
(
znz_WW w3_op)
w3_op.(
znz_head0)
w3_op.(
znz_add_mul_div)
w3_op.(
znz_div21)
w3_op.(
znz_compare)
w3_op.(
znz_sub) (
S n)
x y in
(
to_Z3 _ u,
N3 v).
Definition w4_divn1 n x y :=
let (
u,
v) :=
double_divn1 w4_op.(
znz_zdigits)
w4_op.(
znz_0)
(
znz_WW w4_op)
w4_op.(
znz_head0)
w4_op.(
znz_add_mul_div)
w4_op.(
znz_div21)
w4_op.(
znz_compare)
w4_op.(
znz_sub) (
S n)
x y in
(
to_Z4 _ u,
N4 v).
Definition w5_divn1 n x y :=
let (
u,
v) :=
double_divn1 w5_op.(
znz_zdigits)
w5_op.(
znz_0)
(
znz_WW w5_op)
w5_op.(
znz_head0)
w5_op.(
znz_add_mul_div)
w5_op.(
znz_div21)
w5_op.(
znz_compare)
w5_op.(
znz_sub) (
S n)
x y in
(
to_Z5 _ u,
N5 v).
Definition w6_divn1 n x y :=
let (
u,
v) :=
double_divn1 w6_op.(
znz_zdigits)
w6_op.(
znz_0)
(
znz_WW w6_op)
w6_op.(
znz_head0)
w6_op.(
znz_add_mul_div)
w6_op.(
znz_div21)
w6_op.(
znz_compare)
w6_op.(
znz_sub) (
S n)
x y in
(
Nn _ u,
N6 v).
Lemma spec_get_end0:
forall n x y,
eval0n n x <= [
N0 y] ->
[
N0 (
DoubleBase.get_low w_0 n x)] =
eval0n n x.
Lemma spec_get_end1:
forall n x y,
eval1n n x <= [
N1 y] ->
[
N1 (
DoubleBase.get_low W0 n x)] =
eval1n n x.
Lemma spec_get_end2:
forall n x y,
eval2n n x <= [
N2 y] ->
[
N2 (
DoubleBase.get_low W0 n x)] =
eval2n n x.
Lemma spec_get_end3:
forall n x y,
eval3n n x <= [
N3 y] ->
[
N3 (
DoubleBase.get_low W0 n x)] =
eval3n n x.
Lemma spec_get_end4:
forall n x y,
eval4n n x <= [
N4 y] ->
[
N4 (
DoubleBase.get_low W0 n x)] =
eval4n n x.
Lemma spec_get_end5:
forall n x y,
eval5n n x <= [
N5 y] ->
[
N5 (
DoubleBase.get_low W0 n x)] =
eval5n n x.
Lemma spec_get_end6:
forall n x y,
eval6n n x <= [
N6 y] ->
[
N6 (
DoubleBase.get_low W0 n x)] =
eval6n n x.
Let div_gt0 x y :=
let (
u,v) := (
w0_div_gt x y)
in (
reduce_0 u,
reduce_0 v).
Let div_gt1 x y :=
let (
u,v) := (
w1_div_gt x y)
in (
reduce_1 u,
reduce_1 v).
Let div_gt2 x y :=
let (
u,v) := (
w2_div_gt x y)
in (
reduce_2 u,
reduce_2 v).
Let div_gt3 x y :=
let (
u,v) := (
w3_div_gt x y)
in (
reduce_3 u,
reduce_3 v).
Let div_gt4 x y :=
let (
u,v) := (
w4_div_gt x y)
in (
reduce_4 u,
reduce_4 v).
Let div_gt5 x y :=
let (
u,v) := (
w5_div_gt x y)
in (
reduce_5 u,
reduce_5 v).
Let div_gt6 x y :=
let (
u,v) := (
w6_div_gt x y)
in (
reduce_6 u,
reduce_6 v).
Let div_gtnm n m wx wy :=
let mn :=
Max.max n m in
let d :=
diff n m in
let op :=
make_op mn in
let (
q,
r):=
op.(
znz_div_gt)
(
castm (
diff_r n m) (
extend_tr wx (
snd d)))
(
castm (
diff_l n m) (
extend_tr wy (
fst d)))
in
(
reduce_n mn q,
reduce_n mn r).
Definition div_gt :=
Eval lazy beta delta [
iter]
in
(
iter _
div_gt0
(
fun n x y =>
div_gt0 x (
DoubleBase.get_low w_0 (
S n)
y))
w0_divn1
div_gt1
(
fun n x y =>
div_gt1 x (
DoubleBase.get_low W0 (
S n)
y))
w1_divn1
div_gt2
(
fun n x y =>
div_gt2 x (
DoubleBase.get_low W0 (
S n)
y))
w2_divn1
div_gt3
(
fun n x y =>
div_gt3 x (
DoubleBase.get_low W0 (
S n)
y))
w3_divn1
div_gt4
(
fun n x y =>
div_gt4 x (
DoubleBase.get_low W0 (
S n)
y))
w4_divn1
div_gt5
(
fun n x y =>
div_gt5 x (
DoubleBase.get_low W0 (
S n)
y))
w5_divn1
div_gt6
(
fun n x y =>
div_gt6 x (
DoubleBase.get_low W0 (
S n)
y))
w6_divn1
div_gtnm).
Theorem spec_div_gt:
forall x y,
[
x] > [
y] -> 0 < [
y] ->
let (
q,r) :=
div_gt x y in
[
q] = [
x] / [
y] /\ [
r] = [
x]
mod [
y].
Definition div_eucl x y :=
match compare x y with
|
Eq => (
one,
zero)
|
Lt => (
zero,
x)
|
Gt =>
div_gt x y
end.
Theorem spec_div_eucl:
forall x y,
0 < [
y] ->
let (
q,r) :=
div_eucl x y in
([
q], [
r]) =
Zdiv_eucl [
x] [
y].
Definition div x y :=
fst (
div_eucl x y).
Theorem spec_div:
forall x y, 0 < [
y] -> [
div x y] = [
x] / [
y].
Definition w0_mod_gt :=
w0_op.(
znz_mod_gt).
Definition w1_mod_gt :=
w1_op.(
znz_mod_gt).
Definition w2_mod_gt :=
w2_op.(
znz_mod_gt).
Definition w3_mod_gt :=
w3_op.(
znz_mod_gt).
Definition w4_mod_gt :=
w4_op.(
znz_mod_gt).
Definition w5_mod_gt :=
w5_op.(
znz_mod_gt).
Definition w6_mod_gt :=
w6_op.(
znz_mod_gt).
Definition w0_modn1 :=
double_modn1 w0_op.(
znz_zdigits)
w0_op.(
znz_0)
w0_op.(
znz_head0)
w0_op.(
znz_add_mul_div)
w0_op.(
znz_div21)
w0_op.(
znz_compare)
w0_op.(
znz_sub).
Definition w1_modn1 :=
double_modn1 w1_op.(
znz_zdigits)
w1_op.(
znz_0)
w1_op.(
znz_head0)
w1_op.(
znz_add_mul_div)
w1_op.(
znz_div21)
w1_op.(
znz_compare)
w1_op.(
znz_sub).
Definition w2_modn1 :=
double_modn1 w2_op.(
znz_zdigits)
w2_op.(
znz_0)
w2_op.(
znz_head0)
w2_op.(
znz_add_mul_div)
w2_op.(
znz_div21)
w2_op.(
znz_compare)
w2_op.(
znz_sub).
Definition w3_modn1 :=
double_modn1 w3_op.(
znz_zdigits)
w3_op.(
znz_0)
w3_op.(
znz_head0)
w3_op.(
znz_add_mul_div)
w3_op.(
znz_div21)
w3_op.(
znz_compare)
w3_op.(
znz_sub).
Definition w4_modn1 :=
double_modn1 w4_op.(
znz_zdigits)
w4_op.(
znz_0)
w4_op.(
znz_head0)
w4_op.(
znz_add_mul_div)
w4_op.(
znz_div21)
w4_op.(
znz_compare)
w4_op.(
znz_sub).
Definition w5_modn1 :=
double_modn1 w5_op.(
znz_zdigits)
w5_op.(
znz_0)
w5_op.(
znz_head0)
w5_op.(
znz_add_mul_div)
w5_op.(
znz_div21)
w5_op.(
znz_compare)
w5_op.(
znz_sub).
Definition w6_modn1 :=
double_modn1 w6_op.(
znz_zdigits)
w6_op.(
znz_0)
w6_op.(
znz_head0)
w6_op.(
znz_add_mul_div)
w6_op.(
znz_div21)
w6_op.(
znz_compare)
w6_op.(
znz_sub).
Let mod_gtnm n m wx wy :=
let mn :=
Max.max n m in
let d :=
diff n m in
let op :=
make_op mn in
reduce_n mn (
op.(
znz_mod_gt)
(
castm (
diff_r n m) (
extend_tr wx (
snd d)))
(
castm (
diff_l n m) (
extend_tr wy (
fst d)))).
Definition mod_gt :=
Eval lazy beta delta[
iter]
in
(
iter _
(
fun x y =>
reduce_0 (
w0_mod_gt x y))
(
fun n x y =>
reduce_0 (
w0_mod_gt x (
DoubleBase.get_low w_0 (
S n)
y)))
(
fun n x y =>
reduce_0 (
w0_modn1 (
S n)
x y))
(
fun x y =>
reduce_1 (
w1_mod_gt x y))
(
fun n x y =>
reduce_1 (
w1_mod_gt x (
DoubleBase.get_low W0 (
S n)
y)))
(
fun n x y =>
reduce_1 (
w1_modn1 (
S n)
x y))
(
fun x y =>
reduce_2 (
w2_mod_gt x y))
(
fun n x y =>
reduce_2 (
w2_mod_gt x (
DoubleBase.get_low W0 (
S n)
y)))
(
fun n x y =>
reduce_2 (
w2_modn1 (
S n)
x y))
(
fun x y =>
reduce_3 (
w3_mod_gt x y))
(
fun n x y =>
reduce_3 (
w3_mod_gt x (
DoubleBase.get_low W0 (
S n)
y)))
(
fun n x y =>
reduce_3 (
w3_modn1 (
S n)
x y))
(
fun x y =>
reduce_4 (
w4_mod_gt x y))
(
fun n x y =>
reduce_4 (
w4_mod_gt x (
DoubleBase.get_low W0 (
S n)
y)))
(
fun n x y =>
reduce_4 (
w4_modn1 (
S n)
x y))
(
fun x y =>
reduce_5 (
w5_mod_gt x y))
(
fun n x y =>
reduce_5 (
w5_mod_gt x (
DoubleBase.get_low W0 (
S n)
y)))
(
fun n x y =>
reduce_5 (
w5_modn1 (
S n)
x y))
(
fun x y =>
reduce_6 (
w6_mod_gt x y))
(
fun n x y =>
reduce_6 (
w6_mod_gt x (
DoubleBase.get_low W0 (
S n)
y)))
(
fun n x y =>
reduce_6 (
w6_modn1 (
S n)
x y))
mod_gtnm).
Let spec_modn1 ww (
ww_op:
znz_op ww) (
ww_spec:
znz_spec ww_op) :=
(
spec_double_modn1
ww_op.(
znz_zdigits)
ww_op.(
znz_0)
(
znz_WW ww_op)
ww_op.(
znz_head0)
ww_op.(
znz_add_mul_div)
ww_op.(
znz_div21)
ww_op.(
znz_compare)
ww_op.(
znz_sub) (
znz_to_Z ww_op)
(
spec_to_Z ww_spec)
(
spec_zdigits ww_spec)
(
spec_0 ww_spec) (
spec_WW ww_spec) (
spec_head0 ww_spec)
(
spec_add_mul_div ww_spec) (
spec_div21 ww_spec)
(
CyclicAxioms.spec_compare ww_spec) (
CyclicAxioms.spec_sub ww_spec)).
Theorem spec_mod_gt:
forall x y, [
x] > [
y] -> 0 < [
y] -> [
mod_gt x y] = [
x]
mod [
y].
Definition modulo x y :=
match compare x y with
|
Eq =>
zero
|
Lt =>
x
|
Gt =>
mod_gt x y
end.
Theorem spec_modulo:
forall x y, 0 < [
y] -> [
modulo x y] = [
x]
mod [
y].
Definition digits x :=
match x with
|
N0 _ =>
w0_op.(
znz_digits)
|
N1 _ =>
w1_op.(
znz_digits)
|
N2 _ =>
w2_op.(
znz_digits)
|
N3 _ =>
w3_op.(
znz_digits)
|
N4 _ =>
w4_op.(
znz_digits)
|
N5 _ =>
w5_op.(
znz_digits)
|
N6 _ =>
w6_op.(
znz_digits)
|
Nn n _ => (
make_op n).(
znz_digits)
end.
Theorem spec_digits:
forall x, 0 <= [
x] < 2 ^
Zpos (
digits x).
Definition gcd_gt_body a b cont :=
match compare b zero with
|
Gt =>
let r :=
mod_gt a b in
match compare r zero with
|
Gt =>
cont r (
mod_gt b r)
|
_ =>
b
end
|
_ =>
a
end.
Theorem Zspec_gcd_gt_body:
forall a b cont p,
[
a] > [
b] -> [
a] < 2 ^
p ->
(
forall a1 b1, [
a1] < 2 ^ (
p - 1) -> [
a1] > [
b1] ->
Zis_gcd [
a1] [
b1] [
cont a1 b1]) ->
Zis_gcd [
a] [
b] [
gcd_gt_body a b cont].
Fixpoint gcd_gt_aux (
p:positive) (
cont:t->t->t) (
a b:t) {
struct p} :
t :=
gcd_gt_body a b
(
fun a b =>
match p with
|
xH =>
cont a b
|
xO p =>
gcd_gt_aux p (
gcd_gt_aux p cont)
a b
|
xI p =>
gcd_gt_aux p (
gcd_gt_aux p cont)
a b
end).
Theorem Zspec_gcd_gt_aux:
forall p n a b cont,
[
a] > [
b] -> [
a] < 2 ^ (
Zpos p +
n) ->
(
forall a1 b1, [
a1] < 2 ^
n -> [
a1] > [
b1] ->
Zis_gcd [
a1] [
b1] [
cont a1 b1]) ->
Zis_gcd [
a] [
b] [
gcd_gt_aux p cont a b].
Definition gcd_cont a b :=
match compare one b with
|
Eq =>
one
|
_ =>
a
end.
Definition gcd_gt a b :=
gcd_gt_aux (
digits a)
gcd_cont a b.
Theorem spec_gcd_gt:
forall a b,
[
a] > [
b] -> [
gcd_gt a b] =
Zgcd [
a] [
b].
Definition gcd a b :=
match compare a b with
|
Eq =>
a
|
Lt =>
gcd_gt b a
|
Gt =>
gcd_gt a b
end.
Theorem spec_gcd:
forall a b, [
gcd a b] =
Zgcd [
a] [
b].
Definition pheight p :=
Peano.pred (
nat_of_P (
get_height w0_op.(
znz_digits) (
plength p))).
Theorem pheight_correct:
forall p,
Zpos p < 2 ^ (
Zpos (
znz_digits w0_op) * 2 ^ (
Z_of_nat (
pheight p))).
Definition of_pos x :=
let h :=
pheight x in
match h with
| 0%nat =>
reduce_0 (
snd (
w0_op.(
znz_of_pos)
x))
| 1%nat =>
reduce_1 (
snd (
w1_op.(
znz_of_pos)
x))
| 2%nat =>
reduce_2 (
snd (
w2_op.(
znz_of_pos)
x))
| 3%nat =>
reduce_3 (
snd (
w3_op.(
znz_of_pos)
x))
| 4%nat =>
reduce_4 (
snd (
w4_op.(
znz_of_pos)
x))
| 5%nat =>
reduce_5 (
snd (
w5_op.(
znz_of_pos)
x))
| 6%nat =>
reduce_6 (
snd (
w6_op.(
znz_of_pos)
x))
|
_ =>
let n :=
minus h 7
in
reduce_n n (
snd ((
make_op n).(
znz_of_pos)
x))
end.
Theorem spec_of_pos:
forall x,
[
of_pos x] =
Zpos x.
Definition of_N x :=
match x with
|
BinNat.N0 =>
zero
|
Npos p =>
of_pos p
end.
Theorem spec_of_N:
forall x,
[
of_N x] =
Z_of_N x.
Definition head0 w :=
match w with
|
N0 w=>
reduce_0 (
w0_op.(
znz_head0)
w)
|
N1 w=>
reduce_1 (
w1_op.(
znz_head0)
w)
|
N2 w=>
reduce_2 (
w2_op.(
znz_head0)
w)
|
N3 w=>
reduce_3 (
w3_op.(
znz_head0)
w)
|
N4 w=>
reduce_4 (
w4_op.(
znz_head0)
w)
|
N5 w=>
reduce_5 (
w5_op.(
znz_head0)
w)
|
N6 w=>
reduce_6 (
w6_op.(
znz_head0)
w)
|
Nn n w=>
reduce_n n ((
make_op n).(
znz_head0)
w)
end.
Theorem spec_head00:
forall x, [
x] = 0 ->[
head0 x] =
Zpos (
digits x).
Theorem spec_head0:
forall x, 0 < [
x] ->
2 ^ (
Zpos (
digits x) - 1) <= 2 ^ [
head0 x] * [
x] < 2 ^
Zpos (
digits x).
Definition tail0 w :=
match w with
|
N0 w=>
reduce_0 (
w0_op.(
znz_tail0)
w)
|
N1 w=>
reduce_1 (
w1_op.(
znz_tail0)
w)
|
N2 w=>
reduce_2 (
w2_op.(
znz_tail0)
w)
|
N3 w=>
reduce_3 (
w3_op.(
znz_tail0)
w)
|
N4 w=>
reduce_4 (
w4_op.(
znz_tail0)
w)
|
N5 w=>
reduce_5 (
w5_op.(
znz_tail0)
w)
|
N6 w=>
reduce_6 (
w6_op.(
znz_tail0)
w)
|
Nn n w=>
reduce_n n ((
make_op n).(
znz_tail0)
w)
end.
Theorem spec_tail00:
forall x, [
x] = 0 ->[
tail0 x] =
Zpos (
digits x).
Theorem spec_tail0:
forall x,
0 < [
x] ->
exists y, 0 <=
y /\ [
x] = (2 *
y + 1) * 2 ^ [
tail0 x].
Definition Ndigits x :=
match x with
|
N0 _ =>
N0 w0_op.(
znz_zdigits)
|
N1 _ =>
reduce_1 w1_op.(
znz_zdigits)
|
N2 _ =>
reduce_2 w2_op.(
znz_zdigits)
|
N3 _ =>
reduce_3 w3_op.(
znz_zdigits)
|
N4 _ =>
reduce_4 w4_op.(
znz_zdigits)
|
N5 _ =>
reduce_5 w5_op.(
znz_zdigits)
|
N6 _ =>
reduce_6 w6_op.(
znz_zdigits)
|
Nn n _ =>
reduce_n n (
make_op n).(
znz_zdigits)
end.
Theorem spec_Ndigits:
forall x, [
Ndigits x] =
Zpos (
digits x).
Definition shiftr0 n x :=
w0_op.(
znz_add_mul_div) (
w0_op.(
znz_sub)
w0_op.(
znz_zdigits)
n)
w0_op.(
znz_0)
x.
Definition shiftr1 n x :=
w1_op.(
znz_add_mul_div) (
w1_op.(
znz_sub)
w1_op.(
znz_zdigits)
n)
w1_op.(
znz_0)
x.
Definition shiftr2 n x :=
w2_op.(
znz_add_mul_div) (
w2_op.(
znz_sub)
w2_op.(
znz_zdigits)
n)
w2_op.(
znz_0)
x.
Definition shiftr3 n x :=
w3_op.(
znz_add_mul_div) (
w3_op.(
znz_sub)
w3_op.(
znz_zdigits)
n)
w3_op.(
znz_0)
x.
Definition shiftr4 n x :=
w4_op.(
znz_add_mul_div) (
w4_op.(
znz_sub)
w4_op.(
znz_zdigits)
n)
w4_op.(
znz_0)
x.
Definition shiftr5 n x :=
w5_op.(
znz_add_mul_div) (
w5_op.(
znz_sub)
w5_op.(
znz_zdigits)
n)
w5_op.(
znz_0)
x.
Definition shiftr6 n x :=
w6_op.(
znz_add_mul_div) (
w6_op.(
znz_sub)
w6_op.(
znz_zdigits)
n)
w6_op.(
znz_0)
x.
Definition shiftrn n p x := (
make_op n).(
znz_add_mul_div) ((
make_op n).(
znz_sub) (
make_op n).(
znz_zdigits)
p) (
make_op n).(
znz_0)
x.
Definition shiftr :=
Eval lazy beta delta [
same_level]
in
same_level _ (
fun n x =>
N0 (
shiftr0 n x))
(
fun n x =>
reduce_1 (
shiftr1 n x))
(
fun n x =>
reduce_2 (
shiftr2 n x))
(
fun n x =>
reduce_3 (
shiftr3 n x))
(
fun n x =>
reduce_4 (
shiftr4 n x))
(
fun n x =>
reduce_5 (
shiftr5 n x))
(
fun n x =>
reduce_6 (
shiftr6 n x))
(
fun n p x =>
reduce_n n (
shiftrn n p x)).
Theorem spec_shiftr:
forall n x,
[
n] <= [
Ndigits x] -> [
shiftr n x] = [
x] / 2 ^ [
n].
Definition safe_shiftr n x :=
match compare n (
Ndigits x)
with
|
Lt =>
shiftr n x
|
_ =>
N0 w_0
end.
Theorem spec_safe_shiftr:
forall n x,
[
safe_shiftr n x] = [
x] / 2 ^ [
n].
Definition shiftl0 n x :=
w0_op.(
znz_add_mul_div)
n x w0_op.(
znz_0).
Definition shiftl1 n x :=
w1_op.(
znz_add_mul_div)
n x w1_op.(
znz_0).
Definition shiftl2 n x :=
w2_op.(
znz_add_mul_div)
n x w2_op.(
znz_0).
Definition shiftl3 n x :=
w3_op.(
znz_add_mul_div)
n x w3_op.(
znz_0).
Definition shiftl4 n x :=
w4_op.(
znz_add_mul_div)
n x w4_op.(
znz_0).
Definition shiftl5 n x :=
w5_op.(
znz_add_mul_div)
n x w5_op.(
znz_0).
Definition shiftl6 n x :=
w6_op.(
znz_add_mul_div)
n x w6_op.(
znz_0).
Definition shiftln n p x := (
make_op n).(
znz_add_mul_div)
p x (
make_op n).(
znz_0).
Definition shiftl :=
Eval lazy beta delta [
same_level]
in
same_level _ (
fun n x =>
N0 (
shiftl0 n x))
(
fun n x =>
reduce_1 (
shiftl1 n x))
(
fun n x =>
reduce_2 (
shiftl2 n x))
(
fun n x =>
reduce_3 (
shiftl3 n x))
(
fun n x =>
reduce_4 (
shiftl4 n x))
(
fun n x =>
reduce_5 (
shiftl5 n x))
(
fun n x =>
reduce_6 (
shiftl6 n x))
(
fun n p x =>
reduce_n n (
shiftln n p x)).
Theorem spec_shiftl:
forall n x,
[
n] <= [
head0 x] -> [
shiftl n x] = [
x] * 2 ^ [
n].
Definition double_size w :=
match w with
|
N0 x =>
N1 (
WW (
znz_0 w0_op)
x)
|
N1 x =>
N2 (
WW (
znz_0 w1_op)
x)
|
N2 x =>
N3 (
WW (
znz_0 w2_op)
x)
|
N3 x =>
N4 (
WW (
znz_0 w3_op)
x)
|
N4 x =>
N5 (
WW (
znz_0 w4_op)
x)
|
N5 x =>
N6 (
WW (
znz_0 w5_op)
x)
|
N6 x =>
Nn 0 (
WW (
znz_0 w6_op)
x)
|
Nn n x =>
Nn (
S n) (
WW (
znz_0 (
make_op n))
x)
end.
Theorem spec_double_size_digits:
forall x,
digits (
double_size x) =
xO (
digits x).
Theorem spec_double_size:
forall x, [
double_size x] = [
x].
Theorem spec_double_size_head0:
forall x, 2 * [
head0 x] <= [
head0 (
double_size x)].
Theorem spec_double_size_head0_pos:
forall x, 0 < [
head0 (
double_size x)].
Definition safe_shiftl_aux_body cont n x :=
match compare n (
head0 x)
with
Gt =>
cont n (
double_size x)
|
_ =>
shiftl n x
end.
Theorem spec_safe_shift_aux_body:
forall n p x cont,
2^
Zpos p <= [
head0 x] ->
(
forall x, 2 ^ (
Zpos p + 1) <= [
head0 x]->
[
cont n x] = [
x] * 2 ^ [
n]) ->
[
safe_shiftl_aux_body cont n x] = [
x] * 2 ^ [
n].
Fixpoint safe_shiftl_aux p cont n x {
struct p} :=
safe_shiftl_aux_body
(
fun n x =>
match p with
|
xH =>
cont n x
|
xO p =>
safe_shiftl_aux p (
safe_shiftl_aux p cont)
n x
|
xI p =>
safe_shiftl_aux p (
safe_shiftl_aux p cont)
n x
end)
n x.
Theorem spec_safe_shift_aux:
forall p q n x cont,
2 ^ (
Zpos q) <= [
head0 x] ->
(
forall x, 2 ^ (
Zpos p +
Zpos q) <= [
head0 x] ->
[
cont n x] = [
x] * 2 ^ [
n]) ->
[
safe_shiftl_aux p cont n x] = [
x] * 2 ^ [
n].
Definition safe_shiftl n x :=
safe_shiftl_aux_body
(
safe_shiftl_aux_body
(
safe_shiftl_aux (
digits n)
shiftl))
n x.
Theorem spec_safe_shift:
forall n x,
[
safe_shiftl n x] = [
x] * 2 ^ [
n].
Definition is_even x :=
match x with
|
N0 wx =>
w0_op.(
znz_is_even)
wx
|
N1 wx =>
w1_op.(
znz_is_even)
wx
|
N2 wx =>
w2_op.(
znz_is_even)
wx
|
N3 wx =>
w3_op.(
znz_is_even)
wx
|
N4 wx =>
w4_op.(
znz_is_even)
wx
|
N5 wx =>
w5_op.(
znz_is_even)
wx
|
N6 wx =>
w6_op.(
znz_is_even)
wx
|
Nn n wx => (
make_op n).(
znz_is_even)
wx
end.
Theorem spec_is_even:
forall x,
if is_even x then [
x]
mod 2 = 0
else [
x]
mod 2 = 1.
Theorem spec_0: [
zero] = 0.
Theorem spec_1: [
one] = 1.
End Make.