diff options
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Ints/Basic_type.v | 7 | ||||
-rw-r--r-- | theories/Ints/BigN.v | 16 | ||||
-rw-r--r-- | theories/Ints/Zaux.v (renamed from theories/Ints/Z/ZAux.v) | 0 | ||||
-rw-r--r-- | theories/Ints/num/BigQ.v | 10 | ||||
-rw-r--r-- | theories/Ints/num/GenAdd.v | 9 | ||||
-rw-r--r-- | theories/Ints/num/GenBase.v | 25 | ||||
-rw-r--r-- | theories/Ints/num/GenDiv.v | 2 | ||||
-rw-r--r-- | theories/Ints/num/GenDivn1.v | 2 | ||||
-rw-r--r-- | theories/Ints/num/GenLift.v | 2 | ||||
-rw-r--r-- | theories/Ints/num/GenMul.v | 2 | ||||
-rw-r--r-- | theories/Ints/num/GenSqrt.v | 2 | ||||
-rw-r--r-- | theories/Ints/num/GenSub.v | 2 | ||||
-rw-r--r-- | theories/Ints/num/MemoFn.v | 8 | ||||
-rw-r--r-- | theories/Ints/num/NMake.v | 36 | ||||
-rw-r--r-- | theories/Ints/num/Nbasic.v | 10 | ||||
-rw-r--r-- | theories/Ints/num/Q0Make.v | 19 | ||||
-rw-r--r-- | theories/Ints/num/QMake_base.v | 23 | ||||
-rw-r--r-- | theories/Ints/num/QbiMake.v | 28 | ||||
-rw-r--r-- | theories/Ints/num/QifMake.v | 24 | ||||
-rw-r--r-- | theories/Ints/num/QpMake.v | 15 | ||||
-rw-r--r-- | theories/Ints/num/QvMake.v | 16 | ||||
-rw-r--r-- | theories/Ints/num/ZMake.v | 10 | ||||
-rw-r--r-- | theories/Ints/num/Zn2Z.v | 2 | ||||
-rw-r--r-- | theories/Ints/num/ZnZ.v | 32 |
24 files changed, 220 insertions, 82 deletions
diff --git a/theories/Ints/Basic_type.v b/theories/Ints/Basic_type.v index 72a027cb6..2116aaddd 100644 --- a/theories/Ints/Basic_type.v +++ b/theories/Ints/Basic_type.v @@ -1,3 +1,10 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) (*************************************************************) (* This file is distributed under the terms of the *) diff --git a/theories/Ints/BigN.v b/theories/Ints/BigN.v index e8b92186b..b64a853fd 100644 --- a/theories/Ints/BigN.v +++ b/theories/Ints/BigN.v @@ -1,3 +1,17 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** * Natural numbers in base 2^31 *) + +(** +Author: Arnaud Spiwack +*) + Require Export Int31. Require Import NMake. Require Import ZnZ. @@ -90,7 +104,7 @@ Defined. Definition int31_spec : znz_spec int31_op. Admitted. - + Module Int31_words <: W0Type. Definition w := int31. diff --git a/theories/Ints/Z/ZAux.v b/theories/Ints/Zaux.v index 8e4b1d64f..8e4b1d64f 100644 --- a/theories/Ints/Z/ZAux.v +++ b/theories/Ints/Zaux.v diff --git a/theories/Ints/num/BigQ.v b/theories/Ints/num/BigQ.v index bd889e12f..33e5f669c 100644 --- a/theories/Ints/num/BigQ.v +++ b/theories/Ints/num/BigQ.v @@ -1,3 +1,13 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* *) + Require Export QMake_base. Require Import QpMake. Require Import QvMake. diff --git a/theories/Ints/num/GenAdd.v b/theories/Ints/num/GenAdd.v index 77f5e2301..fae16aad6 100644 --- a/theories/Ints/num/GenAdd.v +++ b/theories/Ints/num/GenAdd.v @@ -1,3 +1,10 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) (*************************************************************) (* This file is distributed under the terms of the *) @@ -9,7 +16,7 @@ Set Implicit Arguments. Require Import ZArith. -Require Import ZAux. +Require Import Zaux. Require Import Basic_type. Require Import GenBase. diff --git a/theories/Ints/num/GenBase.v b/theories/Ints/num/GenBase.v index a9936f1dd..e93e3a489 100644 --- a/theories/Ints/num/GenBase.v +++ b/theories/Ints/num/GenBase.v @@ -1,15 +1,26 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) +(* $Id:$ *) + +(** * *) + +(** +- Authors: Benjamin Grégoire, Laurent Théry +- Institution: INRIA +- Date: 2007 +- Remark: File automatically generated +*) Set Implicit Arguments. Require Import ZArith. -Require Import ZAux. +Require Import Zaux. Require Import Basic_type. Require Import JMeq. diff --git a/theories/Ints/num/GenDiv.v b/theories/Ints/num/GenDiv.v index 237adb48b..ea6868a90 100644 --- a/theories/Ints/num/GenDiv.v +++ b/theories/Ints/num/GenDiv.v @@ -9,7 +9,7 @@ Set Implicit Arguments. Require Import ZArith. -Require Import ZAux. +Require Import Zaux. Require Import Basic_type. Require Import GenBase. Require Import GenDivn1. diff --git a/theories/Ints/num/GenDivn1.v b/theories/Ints/num/GenDivn1.v index 7987741da..3c70adb61 100644 --- a/theories/Ints/num/GenDivn1.v +++ b/theories/Ints/num/GenDivn1.v @@ -9,7 +9,7 @@ Set Implicit Arguments. Require Import ZArith. -Require Import ZAux. +Require Import Zaux. Require Import Basic_type. Require Import GenBase. diff --git a/theories/Ints/num/GenLift.v b/theories/Ints/num/GenLift.v index 06c76067e..f74cdc30b 100644 --- a/theories/Ints/num/GenLift.v +++ b/theories/Ints/num/GenLift.v @@ -9,7 +9,7 @@ Set Implicit Arguments. Require Import ZArith. -Require Import ZAux. +Require Import Zaux. Require Import Basic_type. Require Import GenBase. diff --git a/theories/Ints/num/GenMul.v b/theories/Ints/num/GenMul.v index c7ac1ea3e..9a56f1ee3 100644 --- a/theories/Ints/num/GenMul.v +++ b/theories/Ints/num/GenMul.v @@ -9,7 +9,7 @@ Set Implicit Arguments. Require Import ZArith. -Require Import ZAux. +Require Import Zaux. Require Import Basic_type. Require Import GenBase. diff --git a/theories/Ints/num/GenSqrt.v b/theories/Ints/num/GenSqrt.v index d1ed6353d..63a0930ed 100644 --- a/theories/Ints/num/GenSqrt.v +++ b/theories/Ints/num/GenSqrt.v @@ -9,7 +9,7 @@ Set Implicit Arguments. Require Import ZArith. -Require Import ZAux. +Require Import Zaux. Require Import Basic_type. Require Import GenBase. diff --git a/theories/Ints/num/GenSub.v b/theories/Ints/num/GenSub.v index 9b0924853..6ffb24575 100644 --- a/theories/Ints/num/GenSub.v +++ b/theories/Ints/num/GenSub.v @@ -9,7 +9,7 @@ Set Implicit Arguments. Require Import ZArith. -Require Import ZAux. +Require Import Zaux. Require Import Basic_type. Require Import GenBase. diff --git a/theories/Ints/num/MemoFn.v b/theories/Ints/num/MemoFn.v index 7f3703a1b..7d2c7af01 100644 --- a/theories/Ints/num/MemoFn.v +++ b/theories/Ints/num/MemoFn.v @@ -1,3 +1,11 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + Require Import Eqdep_dec. Section MemoFunction. diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v index 5cc8f0284..c857da385 100644 --- a/theories/Ints/num/NMake.v +++ b/theories/Ints/num/NMake.v @@ -1,4 +1,23 @@ -Require Import ZAux. +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* $Id$ *) + +(** * *) + +(** +- Authors: Benjamin Grégoire, Laurent Théry +- Institution: INRIA +- Date: 2007 +- Remark: File automatically generated +*) + +Require Import Zaux. Require Import ZArith. Require Import Basic_type. Require Import ZnZ. @@ -9,20 +28,6 @@ Require Import GenDivn1. Require Import Wf_nat. Require Import MemoFn. -(***************************************************************) -(* *) -(* File automatically generated DO NOT EDIT *) -(* Constructors: 6 Generated Proofs: true *) -(* *) -(* To change this file, edit in genN.ml the two lines *) -(* let size = 6 *) -(* let gen_proof = true *) -(* Recompile the file *) -(* camlopt -o genN unix.cmxa genN.ml *) -(* Regenerate NMake.v *) -(* ./genN *) -(***************************************************************) - Module Type W0Type. Parameter w : Set. Parameter w_op : znz_op w. @@ -6796,4 +6801,3 @@ Qed. Qed. End Make. - diff --git a/theories/Ints/num/Nbasic.v b/theories/Ints/num/Nbasic.v index 0d85c92ed..1398e8f55 100644 --- a/theories/Ints/num/Nbasic.v +++ b/theories/Ints/num/Nbasic.v @@ -1,5 +1,13 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + Require Import ZArith. -Require Import ZAux. +Require Import Zaux. Require Import Basic_type. Require Import Max. Require Import GenBase. diff --git a/theories/Ints/num/Q0Make.v b/theories/Ints/num/Q0Make.v index c39a63301..d5809ea59 100644 --- a/theories/Ints/num/Q0Make.v +++ b/theories/Ints/num/Q0Make.v @@ -1,7 +1,15 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + Require Import Bool. Require Import ZArith. Require Import Znumtheory. -Require Import ZAux. +Require Import Zaux. Require Import Arith. Require Export BigN. Require Export BigZ. @@ -12,11 +20,10 @@ Require Import QMake_base. Module Q0. - (* Troisieme solution : - 0 a de nombreuse representation : - 0, -0, 1/0, ... n/0, - il faut alors faire attention avec la comparaison et l'addition - *) + (** The notation of a rational number is either an integer x, + interpreted as itself or a pair (x,y) of an integer x and a naturel + number y interpreted as x/y. The pairs (x,0) and (0,y) are all + interpreted as 0. *) Definition t := q_type. diff --git a/theories/Ints/num/QMake_base.v b/theories/Ints/num/QMake_base.v index f82c5d25b..0cd2d2122 100644 --- a/theories/Ints/num/QMake_base.v +++ b/theories/Ints/num/QMake_base.v @@ -1,15 +1,30 @@ -Require Export BigN. -Require Export BigZ. +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* $Id:$ *) +(** * An implementation of rational numbers based on big integers *) +(** +- Authors: Benjamin Grégoire, Laurent Théry +- Institution: INRIA +- Date: 2007 +*) + +Require Export BigN. +Require Export BigZ. (* Basic type for Q: a Z or a pair of a Z and an N *) + Inductive q_type : Set := | Qz : BigZ.t -> q_type | Qq : BigZ.t -> BigN.t -> q_type. - - Definition print_type x := match x with | Qz _ => Z diff --git a/theories/Ints/num/QbiMake.v b/theories/Ints/num/QbiMake.v index 9eb5de5e1..a98fda9d7 100644 --- a/theories/Ints/num/QbiMake.v +++ b/theories/Ints/num/QbiMake.v @@ -1,7 +1,15 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + Require Import Bool. Require Import ZArith. Require Import Znumtheory. -Require Import ZAux. +Require Import Zaux. Require Import Arith. Require Export BigN. Require Export BigZ. @@ -12,18 +20,14 @@ Require Import QMake_base. Module Qbi. - (* Troisieme solution : - 0 a de nombreuse representation : - 0, -0, 1/0, ... n/0, - il faut alors faire attention avec la comparaison et l'addition - - Les fonctions de normalization s'effectue seulement si les - nombres sont grands. - *) + (** The notation of a rational number is either an integer x, + interpreted as itself or a pair (x,y) of an integer x and a naturel + number y interpreted as x/y. The pairs (x,0) and (0,y) are all + interpreted as 0. *) Definition t := q_type. - Definition zero:t := Qz BigZ.zero. + Definition zero: t := Qz BigZ.zero. Definition one: t := Qz BigZ.one. Definition minus_one: t := Qz BigZ.minus_one. @@ -1052,7 +1056,3 @@ Module Qbi. End Qbi. - - - - diff --git a/theories/Ints/num/QifMake.v b/theories/Ints/num/QifMake.v index c5fc42520..83c182ee0 100644 --- a/theories/Ints/num/QifMake.v +++ b/theories/Ints/num/QifMake.v @@ -1,7 +1,15 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + Require Import Bool. Require Import ZArith. Require Import Znumtheory. -Require Import ZAux. +Require Import Zaux. Require Import Arith. Require Export BigN. Require Export BigZ. @@ -12,19 +20,15 @@ Require Import QMake_base. Module Qif. - (* Troisieme solution : - 0 a de nombreuse representation : - 0, -0, 1/0, ... n/0, - il faut alors faire attention avec la comparaison et l'addition - - Les fonctions de normalization s'effectue seulement si les - nombres sont grands. - *) + (** The notation of a rational number is either an integer x, + interpreted as itself or a pair (x,y) of an integer x and a naturel + number y interpreted as x/y. The pairs (x,0) and (0,y) are all + interpreted as 0. *) Definition t := q_type. Definition zero: t := Qz BigZ.zero. - Definition one: t := Qz BigZ.one. + Definition one: t := Qz BigZ.one. Definition minus_one: t := Qz BigZ.minus_one. Definition of_Z x: t := Qz (BigZ.of_Z x). diff --git a/theories/Ints/num/QpMake.v b/theories/Ints/num/QpMake.v index 906cf8d15..a28434baf 100644 --- a/theories/Ints/num/QpMake.v +++ b/theories/Ints/num/QpMake.v @@ -1,7 +1,15 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + Require Import Bool. Require Import ZArith. Require Import Znumtheory. -Require Import ZAux. +Require Import Zaux. Require Import Arith. Require Export BigN. Require Export BigZ. @@ -10,9 +18,12 @@ Require Import Qcanon. Require Import Qpower. Require Import QMake_base. - Module Qp. + (** The notation of a rational number is either an integer x, + interpreted as itself or a pair (x,y) of an integer x and a naturel + number y interpreted as x/(y+1). *) + Definition t := q_type. Definition zero: t := Qz BigZ.zero. diff --git a/theories/Ints/num/QvMake.v b/theories/Ints/num/QvMake.v index c3db44bc6..85655dafc 100644 --- a/theories/Ints/num/QvMake.v +++ b/theories/Ints/num/QvMake.v @@ -1,7 +1,15 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + Require Import Bool. Require Import ZArith. Require Import Znumtheory. -Require Import ZAux. +Require Import Zaux. Require Import Arith. Require Export BigN. Require Export BigZ. @@ -12,8 +20,10 @@ Require Import QMake_base. Module Qv. - (* /!\ Invariant maintenu par les fonctions : - - le denominateur n'est jamais nul *) + (** The notation of a rational number is either an integer x, + interpreted as itself or a pair (x,y) of an integer x and a naturel + number y interpreted as x/y. All functions maintain the invariant + that y is never zero. *) Definition t := q_type. diff --git a/theories/Ints/num/ZMake.v b/theories/Ints/num/ZMake.v index d00f14ec6..75fc19584 100644 --- a/theories/Ints/num/ZMake.v +++ b/theories/Ints/num/ZMake.v @@ -1,5 +1,13 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + Require Import ZArith. -Require Import ZAux. +Require Import Zaux. Open Scope Z_scope. diff --git a/theories/Ints/num/Zn2Z.v b/theories/Ints/num/Zn2Z.v index a244635ea..48cf26840 100644 --- a/theories/Ints/num/Zn2Z.v +++ b/theories/Ints/num/Zn2Z.v @@ -9,7 +9,7 @@ Set Implicit Arguments. Require Import ZArith. -Require Import ZAux. +Require Import Zaux. Require Import Basic_type. Require Import GenBase. Require Import GenAdd. diff --git a/theories/Ints/num/ZnZ.v b/theories/Ints/num/ZnZ.v index 61d1ced60..d5b798a18 100644 --- a/theories/Ints/num/ZnZ.v +++ b/theories/Ints/num/ZnZ.v @@ -1,10 +1,22 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) +(************************************************************************) +(* 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, INRIA Laurent Thery, INRIA *) +(************************************************************************) + +(* $Id:$ *) + +(** * Signature and specification of a bounded integer structure *) + +(** +- Authors: Benjamin Grégoire, Laurent Théry +- Institution: INRIA +- Date: 2007 +*) Set Implicit Arguments. @@ -20,6 +32,7 @@ Section ZnZ_Op. Variable znz : Set. Record znz_op : Set := mk_znz_op { + (* Conversion functions with Z *) znz_digits : positive; znz_zdigits: znz; @@ -27,6 +40,7 @@ Section ZnZ_Op. znz_of_pos : positive -> N * znz; znz_head0 : znz -> znz; znz_tail0 : znz -> znz; + (* Basic constructors *) znz_0 : znz; znz_1 : znz; @@ -42,7 +56,7 @@ Section ZnZ_Op. (* Basic arithmetic operations *) znz_opp_c : znz -> carry znz; znz_opp : znz -> znz; - znz_opp_carry : znz -> znz; (* the carry is know to be -1 *) + znz_opp_carry : znz -> znz; (* the carry is known to be -1 *) znz_succ_c : znz -> carry znz; znz_add_c : znz -> znz -> carry znz; @@ -87,7 +101,7 @@ Section Spec. Variable w_op : znz_op w. Let w_digits := w_op.(znz_digits). - Let w_zdigits := w_op.(znz_zdigits). + Let w_zdigits := w_op.(znz_zdigits). Let w_to_Z := w_op.(znz_to_Z). Let w_of_pos := w_op.(znz_of_pos). Let w_head0 := w_op.(znz_head0). |