blob: abd567a851a817bea053b9a76e9132f0aa8d6639 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
Set Implicit Arguments.
Require Import ZArith.
Local Open Scope Z_scope.
Definition base digits := Z.pow 2 (Zpos digits).
Arguments base digits: simpl never.
Section Carry.
Variable A : Type.
Inductive carry :=
| C0 : A -> carry
| C1 : A -> carry.
Definition interp_carry (sign:Z)(B:Z)(interp:A -> Z) c :=
match c with
| C0 x => interp x
| C1 x => sign*B + interp x
end.
End Carry.
Section Zn2Z.
Variable znz : Type.
(** From a type [znz] representing a cyclic structure Z/nZ,
we produce a representation of Z/2nZ by pairs of elements of [znz]
(plus a special case for zero). High half of the new number comes
first.
*)
Inductive zn2z :=
| W0 : zn2z
| WW : znz -> znz -> zn2z.
Definition zn2z_to_Z (wB:Z) (w_to_Z:znz->Z) (x:zn2z) :=
match x with
| W0 => 0
| WW xh xl => w_to_Z xh * wB + w_to_Z xl
end.
End Zn2Z.
Arguments W0 {znz}.
(** From a cyclic representation [w], we iterate the [zn2z] construct
[n] times, gaining the type of binary trees of depth at most [n],
whose leafs are either W0 (if depth < n) or elements of w
(if depth = n).
*)
Fixpoint word (w:Type) (n:nat) : Type :=
match n with
| O => w
| S n => zn2z (word w n)
end.
|
