diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Int31/Z_31Z.v')
-rw-r--r-- | theories/Numbers/Cyclic/Int31/Z_31Z.v | 114 |
1 files changed, 114 insertions, 0 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Z_31Z.v b/theories/Numbers/Cyclic/Int31/Z_31Z.v new file mode 100644 index 000000000..3b5944ed3 --- /dev/null +++ b/theories/Numbers/Cyclic/Int31/Z_31Z.v @@ -0,0 +1,114 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id$ i*) + +(** * Int31 numbers defines indeed a cyclic structure : Z/31Z *) + +(** +Author: Arnaud Spiwack +*) + +Require Export Int31. +Require Import Z_nZ. + +Open Scope int31_scope. + +Definition int31_op : znz_op int31. + split. + + (* Conversion functions with Z *) + exact (31%positive). (* number of digits *) + exact (31). (* number of digits *) + exact (phi). (* conversion to Z *) + exact (positive_to_int31). (* positive -> N*int31 : p => N,i where p = N*2^31+phi i *) + exact head031. (* number of head 0 *) + exact tail031. (* number of tail 0 *) + + (* Basic constructors *) + exact 0. (* 0 *) + exact 1. (* 1 *) + exact Tn. (* 2^31 - 1 *) + (* A function which given two int31 i and j, returns a double word + which is worth i*2^31+j *) + exact (fun i j => match (match i ?= 0 with | Eq => j ?= 0 | not0 => not0 end) with | Eq => W0 | _ => WW i j end). + (* two special cases where i and j are respectively taken equal to 0 *) + exact (fun i => match i ?= 0 with | Eq => W0 | _ => WW i 0 end). + exact (fun j => match j ?= 0 with | Eq => W0 | _ => WW 0 j end). + + (* Comparison *) + exact compare31. + exact (fun i => match i ?= 0 with | Eq => true | _ => false end). + + (* Basic arithmetic operations *) + (* opposite functions *) + exact (fun i => 0 -c i). + exact (fun i => 0 - i). + exact (fun i => 0-i-1). (* the carry is always -1*) + (* successor and addition functions *) + exact (fun i => i +c 1). + exact add31c. + exact add31carryc. + exact (fun i => i + 1). + exact add31. + exact (fun i j => i + j + 1). + (* predecessor and subtraction functions *) + exact (fun i => i -c 1). + exact sub31c. + exact sub31carryc. + exact (fun i => i - 1). + exact sub31. + exact (fun i j => i - j - 1). + (* multiplication functions *) + exact mul31c. + exact mul31. + exact (fun x => x *c x). + + (* special (euclidian) division operations *) + exact div3121. + exact div31. (* this is supposed to be the special case of division a/b where a > b *) + exact div31. + (* euclidian division remainder *) + (* again special case for a > b *) + exact (fun i j => let (_,r) := i/j in r). + exact (fun i j => let (_,r) := i/j in r). + (* gcd functions *) + exact gcd31. (*gcd_gt*) + exact gcd31. (*gcd*) + + (* shift operations *) + exact addmuldiv31. (*add_mul_div *) +(*modulo 2^p *) + exact (fun p i => + match compare31 p 32 with + | Lt => addmuldiv31 p 0 (addmuldiv31 (31-p) i 0) + | _ => i + end). + + (* is i even ? *) + exact (fun i => let (_,r) := i/2 in + match r ?= 0 with + | Eq => true + | _ => false + end). + + (* square root operations *) + exact sqrt312. (* sqrt2 *) + exact sqrt31. (* sqr *) +Defined. + + +Definition int31_spec : znz_spec int31_op. +Admitted. + + +Module Int31_words <: CyclicType. + Definition w := int31. + Definition w_op := int31_op. + Definition w_spec := int31_spec. +End Int31_words. |