diff options
Diffstat (limited to 'theories/Numbers/Integer')
24 files changed, 144 insertions, 1709 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index f7fdc179..c4c5174d 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index 6bf5e9d4..7f5b0df6 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index ad10e65f..4f1ab775 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 9b1b30f8..7fdd018d 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index c919e121..2da44528 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index c2fa69e5..d7f25a66 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. @@ -602,6 +604,14 @@ Proof. apply div_mod; order. Qed. +Lemma mod_div: forall a b, b~=0 -> + a mod b / b == 0. +Proof. + intros a b Hb. + rewrite div_small_iff by assumption. + auto using mod_always_pos. +Qed. + (** A last inequality: *) Theorem div_mul_le: diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index 310748dd..a0d1821b 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. @@ -650,6 +652,14 @@ Proof. apply div_mod; order. Qed. +Lemma mod_div: forall a b, b~=0 -> + a mod b / b == 0. +Proof. + intros a b Hb. + rewrite div_small_iff by assumption. + auto using mod_bound_or. +Qed. + (** A last inequality: *) Theorem div_mul_le: diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index 04301077..31e42738 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. @@ -622,6 +624,14 @@ Proof. apply quot_rem; order. Qed. +Lemma rem_quot: forall a b, b~=0 -> + a rem b ÷ b == 0. +Proof. + intros a b Hb. + rewrite quot_small_iff by assumption. + auto using rem_bound_abs. +Qed. + (** A last inequality: *) Theorem quot_mul_le: diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v index 30adaeb4..f0b7bf9d 100644 --- a/theories/Numbers/Integer/Abstract/ZGcd.v +++ b/theories/Numbers/Integer/Abstract/ZGcd.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Properties of the greatest common divisor *) diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v index ef33308c..0ab528de 100644 --- a/theories/Numbers/Integer/Abstract/ZLcm.v +++ b/theories/Numbers/Integer/Abstract/ZLcm.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 0c92918d..726b041c 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZMaxMin.v b/theories/Numbers/Integer/Abstract/ZMaxMin.v index 24a47f00..f3f3a861 100644 --- a/theories/Numbers/Integer/Abstract/ZMaxMin.v +++ b/theories/Numbers/Integer/Abstract/ZMaxMin.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import ZAxioms ZMulOrder GenericMinMax. diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v index 830c0a7d..120647dc 100644 --- a/theories/Numbers/Integer/Abstract/ZMul.v +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index 320c8f35..cd9523d3 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v index 952d8e9c..a5e53b36 100644 --- a/theories/Numbers/Integer/Abstract/ZParity.v +++ b/theories/Numbers/Integer/Abstract/ZParity.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Bool ZMulOrder NZParity. diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v index 02b8501c..a4b964e5 100644 --- a/theories/Numbers/Integer/Abstract/ZPow.v +++ b/theories/Numbers/Integer/Abstract/ZPow.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Properties of the power function *) diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index 1dec3c58..e4b997cf 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZDivTrunc ZDivFloor diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v index a10552ab..dda12872 100644 --- a/theories/Numbers/Integer/Abstract/ZSgnAbs.v +++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Properties of [abs] and [sgn] *) diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v deleted file mode 100644 index 7c76011f..00000000 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ /dev/null @@ -1,208 +0,0 @@ -(************************************************************************) -(* 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 *) -(************************************************************************) - -Require Export BigN. -Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake. - -(** * [BigZ] : arbitrary large efficient integers. - - The following [BigZ] module regroups both the operations and - all the abstract properties: - - - [ZMake.Make BigN] provides the operations and basic specs w.r.t. ZArith - - [ZTypeIsZAxioms] shows (mainly) that these operations implement - the interface [ZAxioms] - - [ZProp] adds all generic properties derived from [ZAxioms] - - [MinMax*Properties] provides properties of [min] and [max] - -*) - -Delimit Scope bigZ_scope with bigZ. - -Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder := - ZMake.Make BigN - <+ ZTypeIsZAxioms - <+ ZBasicProp [no inline] <+ ZExtraProp [no inline] - <+ HasEqBool2Dec [no inline] - <+ MinMaxLogicalProperties [no inline] - <+ MinMaxDecProperties [no inline]. - -(** For precision concerning the above scope handling, see comment in BigN *) - -(** Notations about [BigZ] *) - -Local Open Scope bigZ_scope. - -Notation bigZ := BigZ.t. -Bind Scope bigZ_scope with bigZ BigZ.t BigZ.t_. -Arguments BigZ.Pos _%bigN. -Arguments BigZ.Neg _%bigN. -Local Notation "0" := BigZ.zero : bigZ_scope. -Local Notation "1" := BigZ.one : bigZ_scope. -Local Notation "2" := BigZ.two : bigZ_scope. -Infix "+" := BigZ.add : bigZ_scope. -Infix "-" := BigZ.sub : bigZ_scope. -Notation "- x" := (BigZ.opp x) : bigZ_scope. -Infix "*" := BigZ.mul : bigZ_scope. -Infix "/" := BigZ.div : bigZ_scope. -Infix "^" := BigZ.pow : bigZ_scope. -Infix "?=" := BigZ.compare : bigZ_scope. -Infix "=?" := BigZ.eqb (at level 70, no associativity) : bigZ_scope. -Infix "<=?" := BigZ.leb (at level 70, no associativity) : bigZ_scope. -Infix "<?" := BigZ.ltb (at level 70, no associativity) : bigZ_scope. -Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope. -Notation "x != y" := (~x==y) (at level 70, no associativity) : bigZ_scope. -Infix "<" := BigZ.lt : bigZ_scope. -Infix "<=" := BigZ.le : bigZ_scope. -Notation "x > y" := (y < x) (only parsing) : bigZ_scope. -Notation "x >= y" := (y <= x) (only parsing) : bigZ_scope. -Notation "x < y < z" := (x<y /\ y<z) : bigZ_scope. -Notation "x < y <= z" := (x<y /\ y<=z) : bigZ_scope. -Notation "x <= y < z" := (x<=y /\ y<z) : bigZ_scope. -Notation "x <= y <= z" := (x<=y /\ y<=z) : bigZ_scope. -Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope. -Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigZ_scope. -Infix "÷" := BigZ.quot (at level 40, left associativity) : bigZ_scope. - -(** Some additional results about [BigZ] *) - -Theorem spec_to_Z: forall n : bigZ, - BigN.to_Z (BigZ.to_N n) = ((Z.sgn [n]) * [n])%Z. -Proof. -intros n; case n; simpl; intros p; - generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. -intros p1 H1; case H1; auto. -intros p1 H1; case H1; auto. -Qed. - -Theorem spec_to_N n: - ([n] = Z.sgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z. -Proof. -case n; simpl; intros p; - generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. -intros p1 H1; case H1; auto. -intros p1 H1; case H1; auto. -Qed. - -Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z -> - BigN.to_Z (BigZ.to_N n) = [n]. -Proof. -intros n; case n; simpl; intros p; - generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. -intros p1 _ H1; case H1; auto. -intros p1 H1; case H1; auto. -Qed. - -(** [BigZ] is a ring *) - -Lemma BigZring : - ring_theory 0 1 BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq. -Proof. -constructor. -exact BigZ.add_0_l. exact BigZ.add_comm. exact BigZ.add_assoc. -exact BigZ.mul_1_l. exact BigZ.mul_comm. exact BigZ.mul_assoc. -exact BigZ.mul_add_distr_r. -symmetry. apply BigZ.add_opp_r. -exact BigZ.add_opp_diag_r. -Qed. - -Lemma BigZeqb_correct : forall x y, (x =? y) = true -> x==y. -Proof. now apply BigZ.eqb_eq. Qed. - -Definition BigZ_of_N n := BigZ.of_Z (Z.of_N n). - -Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq BigZ_of_N BigZ.pow. -Proof. -constructor. -intros. unfold BigZ.eq, BigZ_of_N. rewrite BigZ.spec_pow, BigZ.spec_of_Z. -rewrite Zpower_theory.(rpow_pow_N). -destruct n; simpl. reflexivity. -induction p; simpl; intros; BigZ.zify; rewrite ?IHp; auto. -Qed. - -Lemma BigZdiv : div_theory BigZ.eq BigZ.add BigZ.mul (@id _) - (fun a b => if b =? 0 then (0,a) else BigZ.div_eucl a b). -Proof. -constructor. unfold id. intros a b. -BigZ.zify. -case Z.eqb_spec. -BigZ.zify. auto with zarith. -intros NEQ. -generalize (BigZ.spec_div_eucl a b). -generalize (Z_div_mod_full [a] [b] NEQ). -destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r'). -intros (EQ,_). injection 1 as EQr EQq. -BigZ.zify. rewrite EQr, EQq; auto. -Qed. - -(** Detection of constants *) - -Ltac isBigZcst t := - match t with - | BigZ.Pos ?t => isBigNcst t - | BigZ.Neg ?t => isBigNcst t - | BigZ.zero => constr:(true) - | BigZ.one => constr:(true) - | BigZ.two => constr:(true) - | BigZ.minus_one => constr:(true) - | _ => constr:(false) - end. - -Ltac BigZcst t := - match isBigZcst t with - | true => constr:(t) - | false => constr:(NotConstant) - end. - -Ltac BigZ_to_N t := - match t with - | BigZ.Pos ?t => BigN_to_N t - | BigZ.zero => constr:(0%N) - | BigZ.one => constr:(1%N) - | BigZ.two => constr:(2%N) - | _ => constr:(NotConstant) - end. - -(** Registration for the "ring" tactic *) - -Add Ring BigZr : BigZring - (decidable BigZeqb_correct, - constants [BigZcst], - power_tac BigZpower [BigZ_to_N], - div BigZdiv). - -Section TestRing. -Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + (y + 1*x)*x. -Proof. -intros. ring_simplify. reflexivity. -Qed. -Let test' : forall x y, 1 + x*y + x^2 - 1*1 - y*x + 1*(-x)*x == 0. -Proof. -intros. ring_simplify. reflexivity. -Qed. -End TestRing. - -(** [BigZ] also benefits from an "order" tactic *) - -Ltac bigZ_order := BigZ.order. - -Section TestOrder. -Let test : forall x y : bigZ, x<=y -> y<=x -> x==y. -Proof. bigZ_order. Qed. -End TestOrder. - -(** We can use at least a bit of (r)omega by translating to [Z]. *) - -Section TestOmega. -Let test : forall x y : bigZ, x<=y -> y<=x -> x==y. -Proof. intros x y. BigZ.zify. omega. Qed. -End TestOmega. - -(** Todo: micromega *) diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v deleted file mode 100644 index fec6e068..00000000 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ /dev/null @@ -1,759 +0,0 @@ -(************************************************************************) -(* 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 *) -(************************************************************************) - -Require Import ZArith. -Require Import BigNumPrelude. -Require Import NSig. -Require Import ZSig. - -Open Scope Z_scope. - -(** * ZMake - - A generic transformation from a structure of natural numbers - [NSig.NType] to a structure of integers [ZSig.ZType]. -*) - -Module Make (NN:NType) <: ZType. - - Inductive t_ := - | Pos : NN.t -> t_ - | Neg : NN.t -> t_. - - Definition t := t_. - - Definition zero := Pos NN.zero. - Definition one := Pos NN.one. - Definition two := Pos NN.two. - Definition minus_one := Neg NN.one. - - Definition of_Z x := - match x with - | Zpos x => Pos (NN.of_N (Npos x)) - | Z0 => zero - | Zneg x => Neg (NN.of_N (Npos x)) - end. - - Definition to_Z x := - match x with - | Pos nx => NN.to_Z nx - | Neg nx => Z.opp (NN.to_Z nx) - end. - - Theorem spec_of_Z: forall x, to_Z (of_Z x) = x. - Proof. - intros x; case x; unfold to_Z, of_Z, zero. - exact NN.spec_0. - intros; rewrite NN.spec_of_N; auto. - intros; rewrite NN.spec_of_N; auto. - Qed. - - Definition eq x y := (to_Z x = to_Z y). - - Theorem spec_0: to_Z zero = 0. - exact NN.spec_0. - Qed. - - Theorem spec_1: to_Z one = 1. - exact NN.spec_1. - Qed. - - Theorem spec_2: to_Z two = 2. - exact NN.spec_2. - Qed. - - Theorem spec_m1: to_Z minus_one = -1. - simpl; rewrite NN.spec_1; auto. - Qed. - - Definition compare x y := - match x, y with - | Pos nx, Pos ny => NN.compare nx ny - | Pos nx, Neg ny => - match NN.compare nx NN.zero with - | Gt => Gt - | _ => NN.compare ny NN.zero - end - | Neg nx, Pos ny => - match NN.compare NN.zero nx with - | Lt => Lt - | _ => NN.compare NN.zero ny - end - | Neg nx, Neg ny => NN.compare ny nx - end. - - Theorem spec_compare : - forall x y, compare x y = Z.compare (to_Z x) (to_Z y). - Proof. - unfold compare, to_Z. - destruct x as [x|x], y as [y|y]; - rewrite ?NN.spec_compare, ?NN.spec_0, ?Z.compare_opp; auto; - assert (Hx:=NN.spec_pos x); assert (Hy:=NN.spec_pos y); - set (X:=NN.to_Z x) in *; set (Y:=NN.to_Z y) in *; clearbody X Y. - - destruct (Z.compare_spec X 0) as [EQ|LT|GT]. - + rewrite <- Z.opp_0 in EQ. now rewrite EQ, Z.compare_opp. - + exfalso. omega. - + symmetry. change (X > -Y). omega. - - destruct (Z.compare_spec 0 X) as [EQ|LT|GT]. - + rewrite <- EQ, Z.opp_0; auto. - + symmetry. change (-X < Y). omega. - + exfalso. omega. - Qed. - - Definition eqb x y := - match compare x y with - | Eq => true - | _ => false - end. - - Theorem spec_eqb x y : eqb x y = Z.eqb (to_Z x) (to_Z y). - Proof. - apply Bool.eq_iff_eq_true. - unfold eqb. rewrite Z.eqb_eq, <- Z.compare_eq_iff, spec_compare. - split; [now destruct Z.compare | now intros ->]. - Qed. - - Definition lt n m := to_Z n < to_Z m. - Definition le n m := to_Z n <= to_Z m. - - - Definition ltb (x y : t) : bool := - match compare x y with - | Lt => true - | _ => false - end. - - Theorem spec_ltb x y : ltb x y = Z.ltb (to_Z x) (to_Z y). - Proof. - apply Bool.eq_iff_eq_true. - rewrite Z.ltb_lt. unfold Z.lt, ltb. rewrite spec_compare. - split; [now destruct Z.compare | now intros ->]. - Qed. - - Definition leb (x y : t) : bool := - match compare x y with - | Gt => false - | _ => true - end. - - Theorem spec_leb x y : leb x y = Z.leb (to_Z x) (to_Z y). - Proof. - apply Bool.eq_iff_eq_true. - rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. - now destruct Z.compare; split. - Qed. - - Definition min n m := match compare n m with Gt => m | _ => n end. - Definition max n m := match compare n m with Lt => m | _ => n end. - - Theorem spec_min : forall n m, to_Z (min n m) = Z.min (to_Z n) (to_Z m). - Proof. - unfold min, Z.min. intros. rewrite spec_compare. destruct Z.compare; auto. - Qed. - - Theorem spec_max : forall n m, to_Z (max n m) = Z.max (to_Z n) (to_Z m). - Proof. - unfold max, Z.max. intros. rewrite spec_compare. destruct Z.compare; auto. - Qed. - - Definition to_N x := - match x with - | Pos nx => nx - | Neg nx => nx - end. - - Definition abs x := Pos (to_N x). - - Theorem spec_abs: forall x, to_Z (abs x) = Z.abs (to_Z x). - Proof. - intros x; case x; clear x; intros x; assert (F:=NN.spec_pos x). - simpl; rewrite Z.abs_eq; auto. - simpl; rewrite Z.abs_neq; simpl; auto with zarith. - Qed. - - Definition opp x := - match x with - | Pos nx => Neg nx - | Neg nx => Pos nx - end. - - Theorem spec_opp: forall x, to_Z (opp x) = - to_Z x. - Proof. - intros x; case x; simpl; auto with zarith. - Qed. - - Definition succ x := - match x with - | Pos n => Pos (NN.succ n) - | Neg n => - match NN.compare NN.zero n with - | Lt => Neg (NN.pred n) - | _ => one - end - end. - - Theorem spec_succ: forall n, to_Z (succ n) = to_Z n + 1. - Proof. - intros x; case x; clear x; intros x. - exact (NN.spec_succ x). - simpl. rewrite NN.spec_compare. case Z.compare_spec; rewrite ?NN.spec_0; simpl. - intros HH; rewrite <- HH; rewrite NN.spec_1; ring. - intros HH; rewrite NN.spec_pred, Z.max_r; auto with zarith. - generalize (NN.spec_pos x); auto with zarith. - Qed. - - Definition add x y := - match x, y with - | Pos nx, Pos ny => Pos (NN.add nx ny) - | Pos nx, Neg ny => - match NN.compare nx ny with - | Gt => Pos (NN.sub nx ny) - | Eq => zero - | Lt => Neg (NN.sub ny nx) - end - | Neg nx, Pos ny => - match NN.compare nx ny with - | Gt => Neg (NN.sub nx ny) - | Eq => zero - | Lt => Pos (NN.sub ny nx) - end - | Neg nx, Neg ny => Neg (NN.add nx ny) - end. - - Theorem spec_add: forall x y, to_Z (add x y) = to_Z x + to_Z y. - Proof. - unfold add, to_Z; intros [x | x] [y | y]; - try (rewrite NN.spec_add; auto with zarith); - rewrite NN.spec_compare; case Z.compare_spec; - unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; omega with *. - Qed. - - Definition pred x := - match x with - | Pos nx => - match NN.compare NN.zero nx with - | Lt => Pos (NN.pred nx) - | _ => minus_one - end - | Neg nx => Neg (NN.succ nx) - end. - - Theorem spec_pred: forall x, to_Z (pred x) = to_Z x - 1. - Proof. - unfold pred, to_Z, minus_one; intros [x | x]; - try (rewrite NN.spec_succ; ring). - rewrite NN.spec_compare; case Z.compare_spec; - rewrite ?NN.spec_0, ?NN.spec_1, ?NN.spec_pred; - generalize (NN.spec_pos x); omega with *. - Qed. - - Definition sub x y := - match x, y with - | Pos nx, Pos ny => - match NN.compare nx ny with - | Gt => Pos (NN.sub nx ny) - | Eq => zero - | Lt => Neg (NN.sub ny nx) - end - | Pos nx, Neg ny => Pos (NN.add nx ny) - | Neg nx, Pos ny => Neg (NN.add nx ny) - | Neg nx, Neg ny => - match NN.compare nx ny with - | Gt => Neg (NN.sub nx ny) - | Eq => zero - | Lt => Pos (NN.sub ny nx) - end - end. - - Theorem spec_sub: forall x y, to_Z (sub x y) = to_Z x - to_Z y. - Proof. - unfold sub, to_Z; intros [x | x] [y | y]; - try (rewrite NN.spec_add; auto with zarith); - rewrite NN.spec_compare; case Z.compare_spec; - unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; omega with *. - Qed. - - Definition mul x y := - match x, y with - | Pos nx, Pos ny => Pos (NN.mul nx ny) - | Pos nx, Neg ny => Neg (NN.mul nx ny) - | Neg nx, Pos ny => Neg (NN.mul nx ny) - | Neg nx, Neg ny => Pos (NN.mul nx ny) - end. - - Theorem spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y. - Proof. - unfold mul, to_Z; intros [x | x] [y | y]; rewrite NN.spec_mul; ring. - Qed. - - Definition square x := - match x with - | Pos nx => Pos (NN.square nx) - | Neg nx => Pos (NN.square nx) - end. - - Theorem spec_square: forall x, to_Z (square x) = to_Z x * to_Z x. - Proof. - unfold square, to_Z; intros [x | x]; rewrite NN.spec_square; ring. - Qed. - - Definition pow_pos x p := - match x with - | Pos nx => Pos (NN.pow_pos nx p) - | Neg nx => - match p with - | xH => x - | xO _ => Pos (NN.pow_pos nx p) - | xI _ => Neg (NN.pow_pos nx p) - end - end. - - Theorem spec_pow_pos: forall x n, to_Z (pow_pos x n) = to_Z x ^ Zpos n. - Proof. - assert (F0: forall x, (-x)^2 = x^2). - intros x; rewrite Z.pow_2_r; ring. - unfold pow_pos, to_Z; intros [x | x] [p | p |]; - try rewrite NN.spec_pow_pos; try ring. - assert (F: 0 <= 2 * Zpos p). - assert (0 <= Zpos p); auto with zarith. - rewrite Pos2Z.inj_xI; repeat rewrite Zpower_exp; auto with zarith. - repeat rewrite Z.pow_mul_r; auto with zarith. - rewrite F0; ring. - assert (F: 0 <= 2 * Zpos p). - assert (0 <= Zpos p); auto with zarith. - rewrite Pos2Z.inj_xO; repeat rewrite Zpower_exp; auto with zarith. - repeat rewrite Z.pow_mul_r; auto with zarith. - rewrite F0; ring. - Qed. - - Definition pow_N x n := - match n with - | N0 => one - | Npos p => pow_pos x p - end. - - Theorem spec_pow_N: forall x n, to_Z (pow_N x n) = to_Z x ^ Z.of_N n. - Proof. - destruct n; simpl. apply NN.spec_1. - apply spec_pow_pos. - Qed. - - Definition pow x y := - match to_Z y with - | Z0 => one - | Zpos p => pow_pos x p - | Zneg p => zero - end. - - Theorem spec_pow: forall x y, to_Z (pow x y) = to_Z x ^ to_Z y. - Proof. - intros. unfold pow. destruct (to_Z y); simpl. - apply NN.spec_1. - apply spec_pow_pos. - apply NN.spec_0. - Qed. - - Definition log2 x := - match x with - | Pos nx => Pos (NN.log2 nx) - | Neg nx => zero - end. - - Theorem spec_log2: forall x, to_Z (log2 x) = Z.log2 (to_Z x). - Proof. - intros. destruct x as [p|p]; simpl. apply NN.spec_log2. - rewrite NN.spec_0. - destruct (Z_le_lt_eq_dec _ _ (NN.spec_pos p)) as [LT|EQ]. - rewrite Z.log2_nonpos; auto with zarith. - now rewrite <- EQ. - Qed. - - Definition sqrt x := - match x with - | Pos nx => Pos (NN.sqrt nx) - | Neg nx => Neg NN.zero - end. - - Theorem spec_sqrt: forall x, to_Z (sqrt x) = Z.sqrt (to_Z x). - Proof. - destruct x as [p|p]; simpl. - apply NN.spec_sqrt. - rewrite NN.spec_0. - destruct (Z_le_lt_eq_dec _ _ (NN.spec_pos p)) as [LT|EQ]. - rewrite Z.sqrt_neg; auto with zarith. - now rewrite <- EQ. - Qed. - - Definition div_eucl x y := - match x, y with - | Pos nx, Pos ny => - let (q, r) := NN.div_eucl nx ny in - (Pos q, Pos r) - | Pos nx, Neg ny => - let (q, r) := NN.div_eucl nx ny in - if NN.eqb NN.zero r - then (Neg q, zero) - else (Neg (NN.succ q), Neg (NN.sub ny r)) - | Neg nx, Pos ny => - let (q, r) := NN.div_eucl nx ny in - if NN.eqb NN.zero r - then (Neg q, zero) - else (Neg (NN.succ q), Pos (NN.sub ny r)) - | Neg nx, Neg ny => - let (q, r) := NN.div_eucl nx ny in - (Pos q, Neg r) - end. - - Ltac break_nonneg x px EQx := - let H := fresh "H" in - assert (H:=NN.spec_pos x); - destruct (NN.to_Z x) as [|px|px] eqn:EQx; - [clear H|clear H|elim H; reflexivity]. - - Theorem spec_div_eucl: forall x y, - let (q,r) := div_eucl x y in - (to_Z q, to_Z r) = Z.div_eucl (to_Z x) (to_Z y). - Proof. - unfold div_eucl, to_Z. intros [x | x] [y | y]. - (* Pos Pos *) - generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y); auto. - (* Pos Neg *) - generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). - break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr; - simpl; rewrite Hq, NN.spec_0; auto). - change (- Zpos py) with (Zneg py). - assert (GT : Zpos py > 0) by (compute; auto). - generalize (Z_div_mod (Zpos px) (Zpos py) GT). - unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). - intros (EQ,MOD). injection 1 as Hq' Hr'. - rewrite NN.spec_eqb, NN.spec_0, Hr'. - break_nonneg r pr EQr. - subst; simpl. rewrite NN.spec_0; auto. - subst. lazy iota beta delta [Z.eqb]. - rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. omega with *. - (* Neg Pos *) - generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). - break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr; - simpl; rewrite Hq, NN.spec_0; auto). - change (- Zpos px) with (Zneg px). - assert (GT : Zpos py > 0) by (compute; auto). - generalize (Z_div_mod (Zpos px) (Zpos py) GT). - unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). - intros (EQ,MOD). injection 1 as Hq' Hr'. - rewrite NN.spec_eqb, NN.spec_0, Hr'. - break_nonneg r pr EQr. - subst; simpl. rewrite NN.spec_0; auto. - subst. lazy iota beta delta [Z.eqb]. - rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. omega with *. - (* Neg Neg *) - generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). - break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1 as -> ->; auto). - simpl. intros <-; auto. - Qed. - - Definition div x y := fst (div_eucl x y). - - Definition spec_div: forall x y, - to_Z (div x y) = to_Z x / to_Z y. - Proof. - intros x y; generalize (spec_div_eucl x y); unfold div, Z.div. - case div_eucl; case Z.div_eucl; simpl; auto. - intros q r q11 r1 H; injection H; auto. - Qed. - - Definition modulo x y := snd (div_eucl x y). - - Theorem spec_modulo: - forall x y, to_Z (modulo x y) = to_Z x mod to_Z y. - Proof. - intros x y; generalize (spec_div_eucl x y); unfold modulo, Z.modulo. - case div_eucl; case Z.div_eucl; simpl; auto. - intros q r q11 r1 H; injection H; auto. - Qed. - - Definition quot x y := - match x, y with - | Pos nx, Pos ny => Pos (NN.div nx ny) - | Pos nx, Neg ny => Neg (NN.div nx ny) - | Neg nx, Pos ny => Neg (NN.div nx ny) - | Neg nx, Neg ny => Pos (NN.div nx ny) - end. - - Definition rem x y := - if eqb y zero then x - else - match x, y with - | Pos nx, Pos ny => Pos (NN.modulo nx ny) - | Pos nx, Neg ny => Pos (NN.modulo nx ny) - | Neg nx, Pos ny => Neg (NN.modulo nx ny) - | Neg nx, Neg ny => Neg (NN.modulo nx ny) - end. - - Lemma spec_quot : forall x y, to_Z (quot x y) = (to_Z x) ÷ (to_Z y). - Proof. - intros [x|x] [y|y]; simpl; symmetry; rewrite NN.spec_div; - (* Nota: we rely here on [forall a b, a ÷ 0 = b / 0] *) - destruct (Z.eq_dec (NN.to_Z y) 0) as [EQ|NEQ]; - try (rewrite EQ; now destruct (NN.to_Z x)); - rewrite ?Z.quot_opp_r, ?Z.quot_opp_l, ?Z.opp_involutive, ?Z.opp_inj_wd; - trivial; apply Z.quot_div_nonneg; - generalize (NN.spec_pos x) (NN.spec_pos y); Z.order. - Qed. - - Lemma spec_rem : forall x y, - to_Z (rem x y) = Z.rem (to_Z x) (to_Z y). - Proof. - intros x y. unfold rem. rewrite spec_eqb, spec_0. - case Z.eqb_spec; intros Hy. - (* Nota: we rely here on [Z.rem a 0 = a] *) - rewrite Hy. now destruct (to_Z x). - destruct x as [x|x], y as [y|y]; simpl in *; symmetry; - rewrite ?Z.eq_opp_l, ?Z.opp_0 in Hy; - rewrite NN.spec_modulo, ?Z.rem_opp_r, ?Z.rem_opp_l, ?Z.opp_involutive, - ?Z.opp_inj_wd; - trivial; apply Z.rem_mod_nonneg; - generalize (NN.spec_pos x) (NN.spec_pos y); Z.order. - Qed. - - Definition gcd x y := - match x, y with - | Pos nx, Pos ny => Pos (NN.gcd nx ny) - | Pos nx, Neg ny => Pos (NN.gcd nx ny) - | Neg nx, Pos ny => Pos (NN.gcd nx ny) - | Neg nx, Neg ny => Pos (NN.gcd nx ny) - end. - - Theorem spec_gcd: forall a b, to_Z (gcd a b) = Z.gcd (to_Z a) (to_Z b). - Proof. - unfold gcd, Z.gcd, to_Z; intros [x | x] [y | y]; rewrite NN.spec_gcd; unfold Z.gcd; - auto; case NN.to_Z; simpl; auto with zarith; - try rewrite Z.abs_opp; auto; - case NN.to_Z; simpl; auto with zarith. - Qed. - - Definition sgn x := - match compare zero x with - | Lt => one - | Eq => zero - | Gt => minus_one - end. - - Lemma spec_sgn : forall x, to_Z (sgn x) = Z.sgn (to_Z x). - Proof. - intros. unfold sgn. rewrite spec_compare. case Z.compare_spec. - rewrite spec_0. intros <-; auto. - rewrite spec_0, spec_1. symmetry. rewrite Z.sgn_pos_iff; auto. - rewrite spec_0, spec_m1. symmetry. rewrite Z.sgn_neg_iff; auto with zarith. - Qed. - - Definition even z := - match z with - | Pos n => NN.even n - | Neg n => NN.even n - end. - - Definition odd z := - match z with - | Pos n => NN.odd n - | Neg n => NN.odd n - end. - - Lemma spec_even : forall z, even z = Z.even (to_Z z). - Proof. - intros [n|n]; simpl; rewrite NN.spec_even; trivial. - destruct (NN.to_Z n) as [|p|p]; now try destruct p. - Qed. - - Lemma spec_odd : forall z, odd z = Z.odd (to_Z z). - Proof. - intros [n|n]; simpl; rewrite NN.spec_odd; trivial. - destruct (NN.to_Z n) as [|p|p]; now try destruct p. - Qed. - - Definition norm_pos z := - match z with - | Pos _ => z - | Neg n => if NN.eqb n NN.zero then Pos n else z - end. - - Definition testbit a n := - match norm_pos n, norm_pos a with - | Pos p, Pos a => NN.testbit a p - | Pos p, Neg a => negb (NN.testbit (NN.pred a) p) - | Neg p, _ => false - end. - - Definition shiftl a n := - match norm_pos a, n with - | Pos a, Pos n => Pos (NN.shiftl a n) - | Pos a, Neg n => Pos (NN.shiftr a n) - | Neg a, Pos n => Neg (NN.shiftl a n) - | Neg a, Neg n => Neg (NN.succ (NN.shiftr (NN.pred a) n)) - end. - - Definition shiftr a n := shiftl a (opp n). - - Definition lor a b := - match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (NN.lor a b) - | Neg a, Pos b => Neg (NN.succ (NN.ldiff (NN.pred a) b)) - | Pos a, Neg b => Neg (NN.succ (NN.ldiff (NN.pred b) a)) - | Neg a, Neg b => Neg (NN.succ (NN.land (NN.pred a) (NN.pred b))) - end. - - Definition land a b := - match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (NN.land a b) - | Neg a, Pos b => Pos (NN.ldiff b (NN.pred a)) - | Pos a, Neg b => Pos (NN.ldiff a (NN.pred b)) - | Neg a, Neg b => Neg (NN.succ (NN.lor (NN.pred a) (NN.pred b))) - end. - - Definition ldiff a b := - match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (NN.ldiff a b) - | Neg a, Pos b => Neg (NN.succ (NN.lor (NN.pred a) b)) - | Pos a, Neg b => Pos (NN.land a (NN.pred b)) - | Neg a, Neg b => Pos (NN.ldiff (NN.pred b) (NN.pred a)) - end. - - Definition lxor a b := - match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (NN.lxor a b) - | Neg a, Pos b => Neg (NN.succ (NN.lxor (NN.pred a) b)) - | Pos a, Neg b => Neg (NN.succ (NN.lxor a (NN.pred b))) - | Neg a, Neg b => Pos (NN.lxor (NN.pred a) (NN.pred b)) - end. - - Definition div2 x := shiftr x one. - - Lemma Zlnot_alt1 : forall x, -(x+1) = Z.lnot x. - Proof. - unfold Z.lnot, Z.pred; auto with zarith. - Qed. - - Lemma Zlnot_alt2 : forall x, Z.lnot (x-1) = -x. - Proof. - unfold Z.lnot, Z.pred; auto with zarith. - Qed. - - Lemma Zlnot_alt3 : forall x, Z.lnot (-x) = x-1. - Proof. - unfold Z.lnot, Z.pred; auto with zarith. - Qed. - - Lemma spec_norm_pos : forall x, to_Z (norm_pos x) = to_Z x. - Proof. - intros [x|x]; simpl; trivial. - rewrite NN.spec_eqb, NN.spec_0. - case Z.eqb_spec; simpl; auto with zarith. - Qed. - - Lemma spec_norm_pos_pos : forall x y, norm_pos x = Neg y -> - 0 < NN.to_Z y. - Proof. - intros [x|x] y; simpl; try easy. - rewrite NN.spec_eqb, NN.spec_0. - case Z.eqb_spec; simpl; try easy. - inversion 2. subst. generalize (NN.spec_pos y); auto with zarith. - Qed. - - Ltac destr_norm_pos x := - rewrite <- (spec_norm_pos x); - let H := fresh in - let x' := fresh x in - assert (H := spec_norm_pos_pos x); - destruct (norm_pos x) as [x'|x']; - specialize (H x' (eq_refl _)) || clear H. - - Lemma spec_testbit: forall x p, testbit x p = Z.testbit (to_Z x) (to_Z p). - Proof. - intros x p. unfold testbit. - destr_norm_pos p; simpl. destr_norm_pos x; simpl. - apply NN.spec_testbit. - rewrite NN.spec_testbit, NN.spec_pred, Z.max_r by auto with zarith. - symmetry. apply Z.bits_opp. apply NN.spec_pos. - symmetry. apply Z.testbit_neg_r; auto with zarith. - Qed. - - Lemma spec_shiftl: forall x p, to_Z (shiftl x p) = Z.shiftl (to_Z x) (to_Z p). - Proof. - intros x p. unfold shiftl. - destr_norm_pos x; destruct p as [p|p]; simpl; - assert (Hp := NN.spec_pos p). - apply NN.spec_shiftl. - rewrite Z.shiftl_opp_r. apply NN.spec_shiftr. - rewrite !NN.spec_shiftl. - rewrite !Z.shiftl_mul_pow2 by apply NN.spec_pos. - symmetry. apply Z.mul_opp_l. - rewrite Z.shiftl_opp_r, NN.spec_succ, NN.spec_shiftr, NN.spec_pred, Z.max_r - by auto with zarith. - now rewrite Zlnot_alt1, Z.lnot_shiftr, Zlnot_alt2. - Qed. - - Lemma spec_shiftr: forall x p, to_Z (shiftr x p) = Z.shiftr (to_Z x) (to_Z p). - Proof. - intros. unfold shiftr. rewrite spec_shiftl, spec_opp. - apply Z.shiftl_opp_r. - Qed. - - Lemma spec_land: forall x y, to_Z (land x y) = Z.land (to_Z x) (to_Z y). - Proof. - intros x y. unfold land. - destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor, - ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. - now rewrite Z.ldiff_land, Zlnot_alt2. - now rewrite Z.ldiff_land, Z.land_comm, Zlnot_alt2. - now rewrite Z.lnot_lor, !Zlnot_alt2. - Qed. - - Lemma spec_lor: forall x y, to_Z (lor x y) = Z.lor (to_Z x) (to_Z y). - Proof. - intros x y. unfold lor. - destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor, - ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. - now rewrite Z.lnot_ldiff, Z.lor_comm, Zlnot_alt2. - now rewrite Z.lnot_ldiff, Zlnot_alt2. - now rewrite Z.lnot_land, !Zlnot_alt2. - Qed. - - Lemma spec_ldiff: forall x y, to_Z (ldiff x y) = Z.ldiff (to_Z x) (to_Z y). - Proof. - intros x y. unfold ldiff. - destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor, - ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. - now rewrite Z.ldiff_land, Zlnot_alt3. - now rewrite Z.lnot_lor, Z.ldiff_land, <- Zlnot_alt2. - now rewrite 2 Z.ldiff_land, Zlnot_alt2, Z.land_comm, Zlnot_alt3. - Qed. - - Lemma spec_lxor: forall x y, to_Z (lxor x y) = Z.lxor (to_Z x) (to_Z y). - Proof. - intros x y. unfold lxor. - destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?NN.spec_succ, ?NN.spec_lxor, ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; - auto with zarith. - now rewrite !Z.lnot_lxor_r, Zlnot_alt2. - now rewrite !Z.lnot_lxor_l, Zlnot_alt2. - now rewrite <- Z.lxor_lnot_lnot, !Zlnot_alt2. - Qed. - - Lemma spec_div2: forall x, to_Z (div2 x) = Z.div2 (to_Z x). - Proof. - intros x. unfold div2. now rewrite spec_shiftr, Z.div2_spec, spec_1. - Qed. - -End Make. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index eae8204d..bed827fd 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 0aaf3365..4b2d5c13 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \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 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v deleted file mode 100644 index a360327a..00000000 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ /dev/null @@ -1,135 +0,0 @@ -(************************************************************************) -(* 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 *) -(************************************************************************) - -Require Import BinInt. - -Open Scope Z_scope. - -(** * ZSig *) - -(** Interface of a rich structure about integers. - Specifications are written via translation to Z. -*) - -Module Type ZType. - - Parameter t : Type. - - Parameter to_Z : t -> Z. - Local Notation "[ x ]" := (to_Z x). - - Definition eq x y := [x] = [y]. - Definition lt x y := [x] < [y]. - Definition le x y := [x] <= [y]. - - Parameter of_Z : Z -> t. - Parameter spec_of_Z: forall x, to_Z (of_Z x) = x. - - Parameter compare : t -> t -> comparison. - Parameter eqb : t -> t -> bool. - Parameter ltb : t -> t -> bool. - Parameter leb : t -> t -> bool. - Parameter min : t -> t -> t. - Parameter max : t -> t -> t. - Parameter zero : t. - Parameter one : t. - Parameter two : t. - Parameter minus_one : t. - Parameter succ : t -> t. - Parameter add : t -> t -> t. - Parameter pred : t -> t. - Parameter sub : t -> t -> t. - Parameter opp : t -> t. - Parameter mul : t -> t -> t. - Parameter square : t -> t. - Parameter pow_pos : t -> positive -> t. - Parameter pow_N : t -> N -> t. - Parameter pow : t -> t -> t. - Parameter sqrt : t -> t. - Parameter log2 : t -> t. - Parameter div_eucl : t -> t -> t * t. - Parameter div : t -> t -> t. - Parameter modulo : t -> t -> t. - Parameter quot : t -> t -> t. - Parameter rem : t -> t -> t. - Parameter gcd : t -> t -> t. - Parameter sgn : t -> t. - Parameter abs : t -> t. - Parameter even : t -> bool. - Parameter odd : t -> bool. - Parameter testbit : t -> t -> bool. - Parameter shiftr : t -> t -> t. - Parameter shiftl : t -> t -> t. - Parameter land : t -> t -> t. - Parameter lor : t -> t -> t. - Parameter ldiff : t -> t -> t. - Parameter lxor : t -> t -> t. - Parameter div2 : t -> t. - - Parameter spec_compare: forall x y, compare x y = ([x] ?= [y]). - Parameter spec_eqb : forall x y, eqb x y = ([x] =? [y]). - Parameter spec_ltb : forall x y, ltb x y = ([x] <? [y]). - Parameter spec_leb : forall x y, leb x y = ([x] <=? [y]). - Parameter spec_min : forall x y, [min x y] = Z.min [x] [y]. - Parameter spec_max : forall x y, [max x y] = Z.max [x] [y]. - Parameter spec_0: [zero] = 0. - Parameter spec_1: [one] = 1. - Parameter spec_2: [two] = 2. - Parameter spec_m1: [minus_one] = -1. - Parameter spec_succ: forall n, [succ n] = [n] + 1. - Parameter spec_add: forall x y, [add x y] = [x] + [y]. - Parameter spec_pred: forall x, [pred x] = [x] - 1. - Parameter spec_sub: forall x y, [sub x y] = [x] - [y]. - Parameter spec_opp: forall x, [opp x] = - [x]. - Parameter spec_mul: forall x y, [mul x y] = [x] * [y]. - Parameter spec_square: forall x, [square x] = [x] * [x]. - Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n. - Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z.of_N n. - Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n]. - Parameter spec_sqrt: forall x, [sqrt x] = Z.sqrt [x]. - Parameter spec_log2: forall x, [log2 x] = Z.log2 [x]. - Parameter spec_div_eucl: forall x y, - let (q,r) := div_eucl x y in ([q], [r]) = Z.div_eucl [x] [y]. - Parameter spec_div: forall x y, [div x y] = [x] / [y]. - Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y]. - Parameter spec_quot: forall x y, [quot x y] = [x] ÷ [y]. - Parameter spec_rem: forall x y, [rem x y] = Z.rem [x] [y]. - Parameter spec_gcd: forall a b, [gcd a b] = Z.gcd [a] [b]. - Parameter spec_sgn : forall x, [sgn x] = Z.sgn [x]. - Parameter spec_abs : forall x, [abs x] = Z.abs [x]. - Parameter spec_even : forall x, even x = Z.even [x]. - Parameter spec_odd : forall x, odd x = Z.odd [x]. - Parameter spec_testbit: forall x p, testbit x p = Z.testbit [x] [p]. - Parameter spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p]. - Parameter spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p]. - Parameter spec_land: forall x y, [land x y] = Z.land [x] [y]. - Parameter spec_lor: forall x y, [lor x y] = Z.lor [x] [y]. - Parameter spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y]. - Parameter spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y]. - Parameter spec_div2: forall x, [div2 x] = Z.div2 [x]. - -End ZType. - -Module Type ZType_Notation (Import Z:ZType). - Notation "[ x ]" := (to_Z x). - Infix "==" := eq (at level 70). - Notation "0" := zero. - Notation "1" := one. - Notation "2" := two. - Infix "+" := add. - Infix "-" := sub. - Infix "*" := mul. - Infix "^" := pow. - Notation "- x" := (opp x). - Infix "<=" := le. - Infix "<" := lt. -End ZType_Notation. - -Module Type ZType' := ZType <+ ZType_Notation. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v deleted file mode 100644 index 32410d1d..00000000 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ /dev/null @@ -1,527 +0,0 @@ -(************************************************************************) -(* 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 *) -(************************************************************************) - -Require Import Bool ZArith OrdersFacts Nnat ZAxioms ZSig. - -(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *) - -Module ZTypeIsZAxioms (Import ZZ : ZType'). - -Hint Rewrite - spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ - spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_square spec_sqrt - spec_compare spec_eqb spec_ltb spec_leb spec_max spec_min - spec_abs spec_sgn spec_pow spec_log2 spec_even spec_odd spec_gcd - spec_quot spec_rem spec_testbit spec_shiftl spec_shiftr - spec_land spec_lor spec_ldiff spec_lxor spec_div2 - : zsimpl. - -Ltac zsimpl := autorewrite with zsimpl. -Ltac zcongruence := repeat red; intros; zsimpl; congruence. -Ltac zify := unfold eq, lt, le in *; zsimpl. - -Instance eq_equiv : Equivalence eq. -Proof. unfold eq. firstorder. Qed. - -Local Obligation Tactic := zcongruence. - -Program Instance succ_wd : Proper (eq ==> eq) succ. -Program Instance pred_wd : Proper (eq ==> eq) pred. -Program Instance add_wd : Proper (eq ==> eq ==> eq) add. -Program Instance sub_wd : Proper (eq ==> eq ==> eq) sub. -Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul. - -Theorem pred_succ : forall n, pred (succ n) == n. -Proof. -intros. zify. auto with zarith. -Qed. - -Theorem one_succ : 1 == succ 0. -Proof. -now zify. -Qed. - -Theorem two_succ : 2 == succ 1. -Proof. -now zify. -Qed. - -Section Induction. - -Variable A : ZZ.t -> Prop. -Hypothesis A_wd : Proper (eq==>iff) A. -Hypothesis A0 : A 0. -Hypothesis AS : forall n, A n <-> A (succ n). - -Let B (z : Z) := A (of_Z z). - -Lemma B0 : B 0. -Proof. -unfold B; simpl. -rewrite <- (A_wd 0); auto. -zify. auto. -Qed. - -Lemma BS : forall z : Z, B z -> B (z + 1). -Proof. -intros z H. -unfold B in *. apply -> AS in H. -setoid_replace (of_Z (z + 1)) with (succ (of_Z z)); auto. -zify. auto. -Qed. - -Lemma BP : forall z : Z, B z -> B (z - 1). -Proof. -intros z H. -unfold B in *. rewrite AS. -setoid_replace (succ (of_Z (z - 1))) with (of_Z z); auto. -zify. auto with zarith. -Qed. - -Lemma B_holds : forall z : Z, B z. -Proof. -intros; destruct (Z_lt_le_dec 0 z). -apply natlike_ind; auto with zarith. -apply B0. -intros; apply BS; auto. -replace z with (-(-z))%Z in * by (auto with zarith). -remember (-z)%Z as z'. -pattern z'; apply natlike_ind. -apply B0. -intros; rewrite Z.opp_succ; unfold Z.pred; apply BP; auto. -subst z'; auto with zarith. -Qed. - -Theorem bi_induction : forall n, A n. -Proof. -intro n. setoid_replace n with (of_Z (to_Z n)). -apply B_holds. -zify. auto. -Qed. - -End Induction. - -Theorem add_0_l : forall n, 0 + n == n. -Proof. -intros. zify. auto with zarith. -Qed. - -Theorem add_succ_l : forall n m, (succ n) + m == succ (n + m). -Proof. -intros. zify. auto with zarith. -Qed. - -Theorem sub_0_r : forall n, n - 0 == n. -Proof. -intros. zify. auto with zarith. -Qed. - -Theorem sub_succ_r : forall n m, n - (succ m) == pred (n - m). -Proof. -intros. zify. auto with zarith. -Qed. - -Theorem mul_0_l : forall n, 0 * n == 0. -Proof. -intros. zify. auto with zarith. -Qed. - -Theorem mul_succ_l : forall n m, (succ n) * m == n * m + m. -Proof. -intros. zify. ring. -Qed. - -(** Order *) - -Lemma eqb_eq x y : eqb x y = true <-> x == y. -Proof. - zify. apply Z.eqb_eq. -Qed. - -Lemma leb_le x y : leb x y = true <-> x <= y. -Proof. - zify. apply Z.leb_le. -Qed. - -Lemma ltb_lt x y : ltb x y = true <-> x < y. -Proof. - zify. apply Z.ltb_lt. -Qed. - -Lemma compare_eq_iff n m : compare n m = Eq <-> n == m. -Proof. - intros. zify. apply Z.compare_eq_iff. -Qed. - -Lemma compare_lt_iff n m : compare n m = Lt <-> n < m. -Proof. - intros. zify. reflexivity. -Qed. - -Lemma compare_le_iff n m : compare n m <> Gt <-> n <= m. -Proof. - intros. zify. reflexivity. -Qed. - -Lemma compare_antisym n m : compare m n = CompOpp (compare n m). -Proof. - intros. zify. apply Z.compare_antisym. -Qed. - -Include BoolOrderFacts ZZ ZZ ZZ [no inline]. - -Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare. -Proof. -intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. -Qed. - -Instance eqb_wd : Proper (eq ==> eq ==> Logic.eq) eqb. -Proof. -intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. -Qed. - -Instance ltb_wd : Proper (eq ==> eq ==> Logic.eq) ltb. -Proof. -intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. -Qed. - -Instance leb_wd : Proper (eq ==> eq ==> Logic.eq) leb. -Proof. -intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. -Qed. - -Instance lt_wd : Proper (eq ==> eq ==> iff) lt. -Proof. -intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition. -Qed. - -Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m. -Proof. -intros. zify. omega. -Qed. - -Theorem min_l : forall n m, n <= m -> min n m == n. -Proof. -intros n m. zify. omega with *. -Qed. - -Theorem min_r : forall n m, m <= n -> min n m == m. -Proof. -intros n m. zify. omega with *. -Qed. - -Theorem max_l : forall n m, m <= n -> max n m == n. -Proof. -intros n m. zify. omega with *. -Qed. - -Theorem max_r : forall n m, n <= m -> max n m == m. -Proof. -intros n m. zify. omega with *. -Qed. - -(** Part specific to integers, not natural numbers *) - -Theorem succ_pred : forall n, succ (pred n) == n. -Proof. -intros. zify. auto with zarith. -Qed. - -(** Opp *) - -Program Instance opp_wd : Proper (eq ==> eq) opp. - -Theorem opp_0 : - 0 == 0. -Proof. -intros. zify. auto with zarith. -Qed. - -Theorem opp_succ : forall n, - (succ n) == pred (- n). -Proof. -intros. zify. auto with zarith. -Qed. - -(** Abs / Sgn *) - -Theorem abs_eq : forall n, 0 <= n -> abs n == n. -Proof. -intros n. zify. omega with *. -Qed. - -Theorem abs_neq : forall n, n <= 0 -> abs n == -n. -Proof. -intros n. zify. omega with *. -Qed. - -Theorem sgn_null : forall n, n==0 -> sgn n == 0. -Proof. -intros n. zify. omega with *. -Qed. - -Theorem sgn_pos : forall n, 0<n -> sgn n == 1. -Proof. -intros n. zify. omega with *. -Qed. - -Theorem sgn_neg : forall n, n<0 -> sgn n == opp 1. -Proof. -intros n. zify. omega with *. -Qed. - -(** Power *) - -Program Instance pow_wd : Proper (eq==>eq==>eq) pow. - -Lemma pow_0_r : forall a, a^0 == 1. -Proof. - intros. now zify. -Qed. - -Lemma pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b. -Proof. - intros a b. zify. intros. now rewrite Z.add_1_r, Z.pow_succ_r. -Qed. - -Lemma pow_neg_r : forall a b, b<0 -> a^b == 0. -Proof. - intros a b. zify. intros Hb. - destruct [b]; reflexivity || discriminate. -Qed. - -Lemma pow_pow_N : forall a b, 0<=b -> a^b == pow_N a (Z.to_N (to_Z b)). -Proof. - intros a b. zify. intros Hb. now rewrite spec_pow_N, Z2N.id. -Qed. - -Lemma pow_pos_N : forall a p, pow_pos a p == pow_N a (Npos p). -Proof. - intros a b. red. now rewrite spec_pow_N, spec_pow_pos. -Qed. - -(** Square *) - -Lemma square_spec n : square n == n * n. -Proof. - now zify. -Qed. - -(** Sqrt *) - -Lemma sqrt_spec : forall n, 0<=n -> - (sqrt n)*(sqrt n) <= n /\ n < (succ (sqrt n))*(succ (sqrt n)). -Proof. - intros n. zify. apply Z.sqrt_spec. -Qed. - -Lemma sqrt_neg : forall n, n<0 -> sqrt n == 0. -Proof. - intros n. zify. apply Z.sqrt_neg. -Qed. - -(** Log2 *) - -Lemma log2_spec : forall n, 0<n -> - 2^(log2 n) <= n /\ n < 2^(succ (log2 n)). -Proof. - intros n. zify. apply Z.log2_spec. -Qed. - -Lemma log2_nonpos : forall n, n<=0 -> log2 n == 0. -Proof. - intros n. zify. apply Z.log2_nonpos. -Qed. - -(** Even / Odd *) - -Definition Even n := exists m, n == 2*m. -Definition Odd n := exists m, n == 2*m+1. - -Lemma even_spec n : even n = true <-> Even n. -Proof. - unfold Even. zify. rewrite Z.even_spec. - split; intros (m,Hm). - - exists (of_Z m). now zify. - - exists [m]. revert Hm. now zify. -Qed. - -Lemma odd_spec n : odd n = true <-> Odd n. -Proof. - unfold Odd. zify. rewrite Z.odd_spec. - split; intros (m,Hm). - - exists (of_Z m). now zify. - - exists [m]. revert Hm. now zify. -Qed. - -(** Div / Mod *) - -Program Instance div_wd : Proper (eq==>eq==>eq) div. -Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. - -Theorem div_mod : forall a b, ~b==0 -> a == b*(div a b) + (modulo a b). -Proof. -intros a b. zify. intros. apply Z.div_mod; auto. -Qed. - -Theorem mod_pos_bound : - forall a b, 0 < b -> 0 <= modulo a b /\ modulo a b < b. -Proof. -intros a b. zify. intros. apply Z_mod_lt; auto with zarith. -Qed. - -Theorem mod_neg_bound : - forall a b, b < 0 -> b < modulo a b /\ modulo a b <= 0. -Proof. -intros a b. zify. intros. apply Z_mod_neg; auto with zarith. -Qed. - -Definition mod_bound_pos : - forall a b, 0<=a -> 0<b -> 0 <= modulo a b /\ modulo a b < b := - fun a b _ H => mod_pos_bound a b H. - -(** Quot / Rem *) - -Program Instance quot_wd : Proper (eq==>eq==>eq) quot. -Program Instance rem_wd : Proper (eq==>eq==>eq) rem. - -Theorem quot_rem : forall a b, ~b==0 -> a == b*(quot a b) + rem a b. -Proof. -intros a b. zify. apply Z.quot_rem. -Qed. - -Theorem rem_bound_pos : - forall a b, 0<=a -> 0<b -> 0 <= rem a b /\ rem a b < b. -Proof. -intros a b. zify. apply Z.rem_bound_pos. -Qed. - -Theorem rem_opp_l : forall a b, ~b==0 -> rem (-a) b == -(rem a b). -Proof. -intros a b. zify. apply Z.rem_opp_l. -Qed. - -Theorem rem_opp_r : forall a b, ~b==0 -> rem a (-b) == rem a b. -Proof. -intros a b. zify. apply Z.rem_opp_r. -Qed. - -(** Gcd *) - -Definition divide n m := exists p, m == p*n. -Local Notation "( x | y )" := (divide x y) (at level 0). - -Lemma spec_divide : forall n m, (n|m) <-> Z.divide [n] [m]. -Proof. - intros n m. split. - - intros (p,H). exists [p]. revert H; now zify. - - intros (z,H). exists (of_Z z). now zify. -Qed. - -Lemma gcd_divide_l : forall n m, (gcd n m | n). -Proof. - intros n m. apply spec_divide. zify. apply Z.gcd_divide_l. -Qed. - -Lemma gcd_divide_r : forall n m, (gcd n m | m). -Proof. - intros n m. apply spec_divide. zify. apply Z.gcd_divide_r. -Qed. - -Lemma gcd_greatest : forall n m p, (p|n) -> (p|m) -> (p|gcd n m). -Proof. - intros n m p. rewrite !spec_divide. zify. apply Z.gcd_greatest. -Qed. - -Lemma gcd_nonneg : forall n m, 0 <= gcd n m. -Proof. - intros. zify. apply Z.gcd_nonneg. -Qed. - -(** Bitwise operations *) - -Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit. - -Lemma testbit_odd_0 : forall a, testbit (2*a+1) 0 = true. -Proof. - intros. zify. apply Z.testbit_odd_0. -Qed. - -Lemma testbit_even_0 : forall a, testbit (2*a) 0 = false. -Proof. - intros. zify. apply Z.testbit_even_0. -Qed. - -Lemma testbit_odd_succ : forall a n, 0<=n -> - testbit (2*a+1) (succ n) = testbit a n. -Proof. - intros a n. zify. apply Z.testbit_odd_succ. -Qed. - -Lemma testbit_even_succ : forall a n, 0<=n -> - testbit (2*a) (succ n) = testbit a n. -Proof. - intros a n. zify. apply Z.testbit_even_succ. -Qed. - -Lemma testbit_neg_r : forall a n, n<0 -> testbit a n = false. -Proof. - intros a n. zify. apply Z.testbit_neg_r. -Qed. - -Lemma shiftr_spec : forall a n m, 0<=m -> - testbit (shiftr a n) m = testbit a (m+n). -Proof. - intros a n m. zify. apply Z.shiftr_spec. -Qed. - -Lemma shiftl_spec_high : forall a n m, 0<=m -> n<=m -> - testbit (shiftl a n) m = testbit a (m-n). -Proof. - intros a n m. zify. intros Hn H. - now apply Z.shiftl_spec_high. -Qed. - -Lemma shiftl_spec_low : forall a n m, m<n -> - testbit (shiftl a n) m = false. -Proof. - intros a n m. zify. intros H. now apply Z.shiftl_spec_low. -Qed. - -Lemma land_spec : forall a b n, - testbit (land a b) n = testbit a n && testbit b n. -Proof. - intros a n m. zify. now apply Z.land_spec. -Qed. - -Lemma lor_spec : forall a b n, - testbit (lor a b) n = testbit a n || testbit b n. -Proof. - intros a n m. zify. now apply Z.lor_spec. -Qed. - -Lemma ldiff_spec : forall a b n, - testbit (ldiff a b) n = testbit a n && negb (testbit b n). -Proof. - intros a n m. zify. now apply Z.ldiff_spec. -Qed. - -Lemma lxor_spec : forall a b n, - testbit (lxor a b) n = xorb (testbit a n) (testbit b n). -Proof. - intros a n m. zify. now apply Z.lxor_spec. -Qed. - -Lemma div2_spec : forall a, div2 a == shiftr a 1. -Proof. - intros a. zify. now apply Z.div2_spec. -Qed. - -End ZTypeIsZAxioms. - -Module ZType_ZAxioms (ZZ : ZType) - <: ZAxiomsSig <: OrderFunctions ZZ <: HasMinMax ZZ - := ZZ <+ ZTypeIsZAxioms. |