# Library Coq.Numbers.Natural.BigN.NMake_gen

# 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 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.

# Reduction

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].

# Successor

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.

# Adddition

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].
Let spec_w1_add: forall x y, [w1_add x y] = [N1 x] + [N1 y].
Let spec_w2_add: forall x y, [w2_add x y] = [N2 x] + [N2 y].
Let spec_w3_add: forall x y, [w3_add x y] = [N3 x] + [N3 y].
Let spec_w4_add: forall x y, [w4_add x y] = [N4 x] + [N4 y].
Let spec_w5_add: forall x y, [w5_add x y] = [N5 x] + [N5 y].
Let spec_w6_add: forall x y, [w6_add x y] = [N6 x] + [N6 y].
Let spec_wn_add: forall n x y, [addn n x y] = [Nn n x] + [Nn n y].
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].

# Predecessor

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_pos : forall x, 0 < [x] -> [pred x] = [x] - 1.
Let spec_pred0: forall x, [x] = 0 -> [pred x] = 0.

# Subtraction

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.

# Comparison

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.

# Multiplication

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].

# Square

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].

# Square root

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.

# Division

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].

# Modulo

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].
digits: a measure for gcd
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).

# Conversion

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.

# Shift

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.