Library Coq.Numbers.Natural.BigN.NMake_gen
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 ZArith CyclicAxioms
DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic
Wf_nat StreamMemo.
Module Make (
Import W0:
CyclicType).
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.
Let spec_extendn0_0:
forall n wx,
[Nn (
S n) (
WW W0 wx)
] = [Nn n wx].
Let spec_extend_tr:
forall m n (
w:
word _ (
S n)),
[Nn (
m + n) (
extend_tr w m)
] = [Nn n w].
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].
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].
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 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_pos :
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 =>
CompOpp (
comparen_0 (
S n)
y x))
(
fun n =>
comparen_0 (
S n))
compare_1
(
fun n x y =>
CompOpp (
comparen_1 (
S n)
y x))
(
fun n =>
comparen_1 (
S n))
compare_2
(
fun n x y =>
CompOpp (
comparen_2 (
S n)
y x))
(
fun n =>
comparen_2 (
S n))
compare_3
(
fun n x y =>
CompOpp (
comparen_3 (
S n)
y x))
(
fun n =>
comparen_3 (
S n))
compare_4
(
fun n x y =>
CompOpp (
comparen_4 (
S n)
y x))
(
fun n =>
comparen_4 (
S n))
compare_5
(
fun n x y =>
CompOpp (
comparen_5 (
S n)
y x))
(
fun n =>
comparen_5 (
S n))
compare_6
(
fun n x y =>
CompOpp (
comparen_6 (
S n)
y x))
(
fun n =>
comparen_6 (
S n))
comparenm).
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 CompOpp c with Eq =>
v = u |
Lt =>
v < u |
Gt =>
v > u end.
Theorem spec_compare_aux:
forall x y,
match compare x y with
Eq =>
[x] = [y]
|
Lt =>
[x] < [y]
|
Gt =>
[x] > [y]
end.
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_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].
digits: a measure for gcd
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 unsafe_shiftr0 n x :=
w0_op.(
znz_add_mul_div) (
w0_op.(
znz_sub)
w0_op.(
znz_zdigits)
n)
w0_op.(
znz_0)
x.
Definition unsafe_shiftr1 n x :=
w1_op.(
znz_add_mul_div) (
w1_op.(
znz_sub)
w1_op.(
znz_zdigits)
n)
w1_op.(
znz_0)
x.
Definition unsafe_shiftr2 n x :=
w2_op.(
znz_add_mul_div) (
w2_op.(
znz_sub)
w2_op.(
znz_zdigits)
n)
w2_op.(
znz_0)
x.
Definition unsafe_shiftr3 n x :=
w3_op.(
znz_add_mul_div) (
w3_op.(
znz_sub)
w3_op.(
znz_zdigits)
n)
w3_op.(
znz_0)
x.
Definition unsafe_shiftr4 n x :=
w4_op.(
znz_add_mul_div) (
w4_op.(
znz_sub)
w4_op.(
znz_zdigits)
n)
w4_op.(
znz_0)
x.
Definition unsafe_shiftr5 n x :=
w5_op.(
znz_add_mul_div) (
w5_op.(
znz_sub)
w5_op.(
znz_zdigits)
n)
w5_op.(
znz_0)
x.
Definition unsafe_shiftr6 n x :=
w6_op.(
znz_add_mul_div) (
w6_op.(
znz_sub)
w6_op.(
znz_zdigits)
n)
w6_op.(
znz_0)
x.
Definition unsafe_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 unsafe_shiftr :=
Eval lazy beta delta [
same_level]
in
same_level _ (
fun n x =>
N0 (
unsafe_shiftr0 n x))
(
fun n x =>
reduce_1 (
unsafe_shiftr1 n x))
(
fun n x =>
reduce_2 (
unsafe_shiftr2 n x))
(
fun n x =>
reduce_3 (
unsafe_shiftr3 n x))
(
fun n x =>
reduce_4 (
unsafe_shiftr4 n x))
(
fun n x =>
reduce_5 (
unsafe_shiftr5 n x))
(
fun n x =>
reduce_6 (
unsafe_shiftr6 n x))
(
fun n p x =>
reduce_n n (
unsafe_shiftrn n p x)).
Theorem spec_unsafe_shiftr:
forall n x,
[n] <= [Ndigits x] ->
[unsafe_shiftr n x] = [x] / 2
^ [n].
Definition unsafe_shiftl0 n x :=
w0_op.(
znz_add_mul_div)
n x w0_op.(
znz_0).
Definition unsafe_shiftl1 n x :=
w1_op.(
znz_add_mul_div)
n x w1_op.(
znz_0).
Definition unsafe_shiftl2 n x :=
w2_op.(
znz_add_mul_div)
n x w2_op.(
znz_0).
Definition unsafe_shiftl3 n x :=
w3_op.(
znz_add_mul_div)
n x w3_op.(
znz_0).
Definition unsafe_shiftl4 n x :=
w4_op.(
znz_add_mul_div)
n x w4_op.(
znz_0).
Definition unsafe_shiftl5 n x :=
w5_op.(
znz_add_mul_div)
n x w5_op.(
znz_0).
Definition unsafe_shiftl6 n x :=
w6_op.(
znz_add_mul_div)
n x w6_op.(
znz_0).
Definition unsafe_shiftln n p x := (
make_op n).(
znz_add_mul_div)
p x (
make_op n).(
znz_0).
Definition unsafe_shiftl :=
Eval lazy beta delta [
same_level]
in
same_level _ (
fun n x =>
N0 (
unsafe_shiftl0 n x))
(
fun n x =>
reduce_1 (
unsafe_shiftl1 n x))
(
fun n x =>
reduce_2 (
unsafe_shiftl2 n x))
(
fun n x =>
reduce_3 (
unsafe_shiftl3 n x))
(
fun n x =>
reduce_4 (
unsafe_shiftl4 n x))
(
fun n x =>
reduce_5 (
unsafe_shiftl5 n x))
(
fun n x =>
reduce_6 (
unsafe_shiftl6 n x))
(
fun n p x =>
reduce_n n (
unsafe_shiftln n p x)).
Theorem spec_unsafe_shiftl:
forall n x,
[n] <= [head0 x] ->
[unsafe_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 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.
End Make.