Library Coq.Numbers.Natural.BigN.NMake_gen
NMake_gen
From a cyclic Z/nZ representation to arbitrary precision natural numbers.
Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT !
The operation type classes for the word types
The main type t, isomorphic with exists n, word w0 n
A generic toolbox for building and deconstructing t
Regular make op, without memoization or karatsuba
This will normally never be used for actual computations,
but only for specification purpose when using
word (dom_t n) m intermediate values.
The specification proofs for the word operators
Conversion between zn2z (dom_t n) and dom_t (S n).
These two types are provably equal, but not convertible,
hence we need some work. We now avoid using generic casts
(i.e. rewrite via proof of equalities in types), since
proving things with them is a mess.
We can hence project from zn2z (dom_t n) to t :
Conversion from word (dom_t n) m to dom_t (m+n).
Things are more complex here. We start with a naive version
that breaks zn2z-trees and reconstruct them. Doing this is
quite unfortunate, but I don't know how to fully avoid that.
(cast someday ?). Then we build an optimized version where
all basic cases (n<=6 or m<=7) are nicely handled.
The naive version
The optimized version.
NB: the last particular case for m could depend on n,
but it's simplier to just expand everywhere up to m=7
(cf
mk_t_w' later).
Particular cases Nk x = eval i j x with specific k,i,j
can be solved by the following tactic
The last particular case that remains useful
An optimized
mk_t_w.
We could say mk_t_w' := mk_t _ (plus_t' n m x)
(TODO: WHY NOT, BTW ??).
Instead we directly define functions for all intersting
n,
reverting to naive
mk_t_w at places that should normally
never be used (see
mul and
div_gt).
Extend : injecting dom_t n into word (dom_t n) (S m)
A particular case of extend, used in same_level:
extend_size is extend Size
Misc results about extensions
same_level
Generic binary operator construction, by extending the smaller
argument to the level of the other.
Section SameLevel.
Variable res:
Type.
Variable P :
Z ->
Z ->
res ->
Prop.
Variable f :
forall n,
dom_t n ->
dom_t n ->
res.
Variable Pf :
forall n x y,
P (
ZnZ.to_Z x) (
ZnZ.to_Z y) (
f n x y).
Let f0 :
w0 ->
w0 ->
res :=
f 0.
Let f1 :
w1 ->
w1 ->
res :=
f 1.
Let f2 :
w2 ->
w2 ->
res :=
f 2.
Let f3 :
w3 ->
w3 ->
res :=
f 3.
Let f4 :
w4 ->
w4 ->
res :=
f 4.
Let f5 :
w5 ->
w5 ->
res :=
f 5.
Let f6 :
w6 ->
w6 ->
res :=
f 6.
Let fn n :=
f (
SizePlus (
S n)).
Let Pf' :
forall n x y u v,
u = [mk_t n x] ->
v = [mk_t n y] ->
P u v (
f n x y).
Notation same_level_folded := (
fun x y =>
match x,
y with
|
N0 wx,
N0 wy =>
f0 wx wy
|
N0 wx,
N1 wy =>
f1 (
extend 0 0
wx)
wy
|
N0 wx,
N2 wy =>
f2 (
extend 0 1
wx)
wy
|
N0 wx,
N3 wy =>
f3 (
extend 0 2
wx)
wy
|
N0 wx,
N4 wy =>
f4 (
extend 0 3
wx)
wy
|
N0 wx,
N5 wy =>
f5 (
extend 0 4
wx)
wy
|
N0 wx,
N6 wy =>
f6 (
extend 0 5
wx)
wy
|
N0 wx,
Nn m wy =>
fn m (
extend_size m (
extend 0 5
wx))
wy
|
N1 wx,
N0 wy =>
f1 wx (
extend 0 0
wy)
|
N1 wx,
N1 wy =>
f1 wx wy
|
N1 wx,
N2 wy =>
f2 (
extend 1 0
wx)
wy
|
N1 wx,
N3 wy =>
f3 (
extend 1 1
wx)
wy
|
N1 wx,
N4 wy =>
f4 (
extend 1 2
wx)
wy
|
N1 wx,
N5 wy =>
f5 (
extend 1 3
wx)
wy
|
N1 wx,
N6 wy =>
f6 (
extend 1 4
wx)
wy
|
N1 wx,
Nn m wy =>
fn m (
extend_size m (
extend 1 4
wx))
wy
|
N2 wx,
N0 wy =>
f2 wx (
extend 0 1
wy)
|
N2 wx,
N1 wy =>
f2 wx (
extend 1 0
wy)
|
N2 wx,
N2 wy =>
f2 wx wy
|
N2 wx,
N3 wy =>
f3 (
extend 2 0
wx)
wy
|
N2 wx,
N4 wy =>
f4 (
extend 2 1
wx)
wy
|
N2 wx,
N5 wy =>
f5 (
extend 2 2
wx)
wy
|
N2 wx,
N6 wy =>
f6 (
extend 2 3
wx)
wy
|
N2 wx,
Nn m wy =>
fn m (
extend_size m (
extend 2 3
wx))
wy
|
N3 wx,
N0 wy =>
f3 wx (
extend 0 2
wy)
|
N3 wx,
N1 wy =>
f3 wx (
extend 1 1
wy)
|
N3 wx,
N2 wy =>
f3 wx (
extend 2 0
wy)
|
N3 wx,
N3 wy =>
f3 wx wy
|
N3 wx,
N4 wy =>
f4 (
extend 3 0
wx)
wy
|
N3 wx,
N5 wy =>
f5 (
extend 3 1
wx)
wy
|
N3 wx,
N6 wy =>
f6 (
extend 3 2
wx)
wy
|
N3 wx,
Nn m wy =>
fn m (
extend_size m (
extend 3 2
wx))
wy
|
N4 wx,
N0 wy =>
f4 wx (
extend 0 3
wy)
|
N4 wx,
N1 wy =>
f4 wx (
extend 1 2
wy)
|
N4 wx,
N2 wy =>
f4 wx (
extend 2 1
wy)
|
N4 wx,
N3 wy =>
f4 wx (
extend 3 0
wy)
|
N4 wx,
N4 wy =>
f4 wx wy
|
N4 wx,
N5 wy =>
f5 (
extend 4 0
wx)
wy
|
N4 wx,
N6 wy =>
f6 (
extend 4 1
wx)
wy
|
N4 wx,
Nn m wy =>
fn m (
extend_size m (
extend 4 1
wx))
wy
|
N5 wx,
N0 wy =>
f5 wx (
extend 0 4
wy)
|
N5 wx,
N1 wy =>
f5 wx (
extend 1 3
wy)
|
N5 wx,
N2 wy =>
f5 wx (
extend 2 2
wy)
|
N5 wx,
N3 wy =>
f5 wx (
extend 3 1
wy)
|
N5 wx,
N4 wy =>
f5 wx (
extend 4 0
wy)
|
N5 wx,
N5 wy =>
f5 wx wy
|
N5 wx,
N6 wy =>
f6 (
extend 5 0
wx)
wy
|
N5 wx,
Nn m wy =>
fn m (
extend_size m (
extend 5 0
wx))
wy
|
N6 wx,
N0 wy =>
f6 wx (
extend 0 5
wy)
|
N6 wx,
N1 wy =>
f6 wx (
extend 1 4
wy)
|
N6 wx,
N2 wy =>
f6 wx (
extend 2 3
wy)
|
N6 wx,
N3 wy =>
f6 wx (
extend 3 2
wy)
|
N6 wx,
N4 wy =>
f6 wx (
extend 4 1
wy)
|
N6 wx,
N5 wy =>
f6 wx (
extend 5 0
wy)
|
N6 wx,
N6 wy =>
f6 wx wy
|
N6 wx,
Nn m wy =>
fn m (
extend_size m wx)
wy
|
Nn n wx,
N0 wy =>
fn n wx (
extend_size n (
extend 0 5
wy))
|
Nn n wx,
N1 wy =>
fn n wx (
extend_size n (
extend 1 4
wy))
|
Nn n wx,
N2 wy =>
fn n wx (
extend_size n (
extend 2 3
wy))
|
Nn n wx,
N3 wy =>
fn n wx (
extend_size n (
extend 3 2
wy))
|
Nn n wx,
N4 wy =>
fn n wx (
extend_size n (
extend 4 1
wy))
|
Nn n wx,
N5 wy =>
fn n wx (
extend_size n (
extend 5 0
wy))
|
Nn n wx,
N6 wy =>
fn n wx (
extend_size n wy)
|
Nn n wx,
Nn m wy =>
let mn :=
Max.max n m in
let d :=
diff n m in
fn mn
(
castm (
diff_r n m) (
extend_tr wx (
snd d)))
(
castm (
diff_l n m) (
extend_tr wy (
fst d)))
end).
Definition same_level :=
Eval lazy beta iota delta
[
DoubleBase.extend DoubleBase.extend_aux extend zeron ]
in same_level_folded.
Lemma spec_same_level_0:
forall x y,
P [x] [y] (
same_level x y).
End SameLevel.
Theorem spec_same_level_dep :
forall res
(
P :
nat ->
Z ->
Z ->
res ->
Prop)
(
Pantimon :
forall n m z z' r,
n <= m ->
P m z z' r ->
P n z z' r)
(
f :
forall n,
dom_t n ->
dom_t n ->
res)
(
Pf:
forall n x y,
P n (
ZnZ.to_Z x) (
ZnZ.to_Z y) (
f n x y)),
forall x y,
P (
level x)
[x] [y] (
same_level f x y).
iter
Generic binary operator construction, by splitting the larger
argument in blocks and applying the smaller argument to them.
Section Iter.
Variable res:
Type.
Variable P:
Z ->
Z ->
res ->
Prop.
Variable f :
forall n,
dom_t n ->
dom_t n ->
res.
Variable Pf :
forall n x y,
P (
ZnZ.to_Z x) (
ZnZ.to_Z y) (
f n x y).
Variable fd :
forall n m,
dom_t n ->
word (
dom_t n) (
S m) ->
res.
Variable fg :
forall n m,
word (
dom_t n) (
S m) ->
dom_t n ->
res.
Variable Pfd :
forall n m x y,
P (
ZnZ.to_Z x) (
eval n (
S m)
y) (
fd n m x y).
Variable Pfg :
forall n m x y,
P (
eval n (
S m)
x) (
ZnZ.to_Z y) (
fg n m x y).
Variable fnm:
forall n m,
word (
dom_t Size) (
S n) ->
word (
dom_t Size) (
S m) ->
res.
Variable Pfnm:
forall n m x y,
P [Nn n x] [Nn m y] (
fnm n m x y).
Let Pf' :
forall n x y u v,
u = [mk_t n x] ->
v = [mk_t n y] ->
P u v (
f n x y).
Let Pfd' :
forall n m x y u v,
u = [mk_t n x] ->
v = eval n (
S m)
y ->
P u v (
fd n m x y).
Let Pfg' :
forall n m x y u v,
u = eval n (
S m)
x ->
v = [mk_t n y] ->
P u v (
fg n m x y).
Let f0 :=
f 0.
Let f1 :=
f 1.
Let f2 :=
f 2.
Let f3 :=
f 3.
Let f4 :=
f 4.
Let f5 :=
f 5.
Let f6 :=
f 6.
Let f0n :=
fd 0.
Let fn0 :=
fg 0.
Let f1n :=
fd 1.
Let fn1 :=
fg 1.
Let f2n :=
fd 2.
Let fn2 :=
fg 2.
Let f3n :=
fd 3.
Let fn3 :=
fg 3.
Let f4n :=
fd 4.
Let fn4 :=
fg 4.
Let f5n :=
fd 5.
Let fn5 :=
fg 5.
Let f6n :=
fd 6.
Let fn6 :=
fg 6.
Notation iter_folded := (
fun x y =>
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 (
extend 0 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 (
extend 1 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 (
extend 2 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 (
extend 3 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 (
extend 4 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 (
extend 5 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 (
extend 0 5
wy)
|
Nn n wx,
N1 wy =>
fn6 n wx (
extend 1 4
wy)
|
Nn n wx,
N2 wy =>
fn6 n wx (
extend 2 3
wy)
|
Nn n wx,
N3 wy =>
fn6 n wx (
extend 3 2
wy)
|
Nn n wx,
N4 wy =>
fn6 n wx (
extend 4 1
wy)
|
Nn n wx,
N5 wy =>
fn6 n wx (
extend 5 0
wy)
|
Nn n wx,
N6 wy =>
fn6 n wx wy
|
Nn n wx,
Nn m wy =>
fnm n m wx wy
end).
Definition iter :=
Eval lazy beta iota delta
[
extend DoubleBase.extend DoubleBase.extend_aux zeron]
in iter_folded.
Lemma spec_iter:
forall x y,
P [x] [y] (
iter x y).
End Iter.
Definition switch
(
P:
nat->
Type)(
f0:
P 0)(
f1:
P 1)(
f2:
P 2)(
f3:
P 3)(
f4:
P 4)(
f5:
P 5)(
f6:
P 6)
(
fn:
forall n,
P n)
n :=
match n return P n with
| 0 =>
f0
| 1 =>
f1
| 2 =>
f2
| 3 =>
f3
| 4 =>
f4
| 5 =>
f5
| 6 =>
f6
|
n =>
fn n
end.
Lemma spec_switch :
forall P (
f:
forall n,
P n)
n,
switch P (
f 0) (
f 1) (
f 2) (
f 3) (
f 4) (
f 5) (
f 6)
f n = f n.
iter_sym
A variant of
iter for symmetric functions, or pseudo-symmetric
functions (when f y x can be deduced from f x y).
Reduction
reduce can be used instead of
mk_t, it will choose the
lowest possible level. NB: We only search and remove leftmost
W0's via ZnZ.eq0, any non-W0 block ends the process, even
if its value is 0.
First, a direct version ...
... then a specialized one