diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v')
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 71 |
1 files changed, 71 insertions, 0 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v new file mode 100644 index 00000000..28d40094 --- /dev/null +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v @@ -0,0 +1,71 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: DoubleType.v 10964 2008-05-22 11:08:13Z letouzey $ i*) + +Set Implicit Arguments. + +Require Import ZArith. +Open Local Scope Z_scope. + +Definition base digits := Zpower 2 (Zpos digits). + +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. + +Implicit 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. + |