From 9764ebbb67edf73a147c536a3c4f4ed0f1a7ce9e Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 6 Dec 2010 15:47:32 +0000 Subject: Numbers and bitwise functions. See NatInt/NZBits.v for the common axiomatization of bitwise functions over naturals / integers. Some specs aren't pretty, but easier to prove, see alternate statements in property functors {N,Z}Bits. Negative numbers are considered via the two's complement convention. We provide implementations for N (in Ndigits.v), for nat (quite dummy, just for completeness), for Z (new file Zdigits_def), for BigN (for the moment partly by converting to N, to be improved soon) and for BigZ. NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in the reversed order (for consistency with the rest of the world): for instance BigN.shiftl 1 10 is 2^10. NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2) on negative numbers. For the moment I've kept it intact, and have just added a Zdiv2' which is truly equivalent to (Zdiv _ 2). To reorganize someday ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Structures/Equalities.v | 13 +++++++++++++ theories/Structures/EqualitiesFacts.v | 15 +-------------- 2 files changed, 14 insertions(+), 14 deletions(-) (limited to 'theories/Structures') diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index 14d34f1eb..8e72bd611 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -7,6 +7,7 @@ (***********************************************************************) Require Export RelationClasses. +Require Import Bool Morphisms Setoid. Set Implicit Arguments. Unset Strict Implicit. @@ -165,6 +166,18 @@ Module Dec2Bool (E:DecidableType) <: BooleanDecidableType Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType := E <+ HasEqBool2Dec. +(** In a BooleanEqualityType, [eqb] is compatible with [eq] *) + +Module BoolEqualityFacts (Import E : BooleanEqualityType). + +Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb. +Proof. +intros x x' Exx' y y' Eyy'. +apply eq_true_iff_eq. +now rewrite 2 eqb_eq, Exx', Eyy'. +Qed. + +End BoolEqualityFacts. (** * UsualDecidableType diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index d9b1d76fd..d8a1b7581 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -8,21 +8,8 @@ Require Import Equalities Bool SetoidList RelationPairs. -(** In a BooleanEqualityType, [eqb] is compatible with [eq] *) - -Module BoolEqualityFacts (Import E : BooleanEqualityType). - -Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb. -Proof. -intros x x' Exx' y y' Eyy'. -apply eq_true_iff_eq. -rewrite 2 eqb_eq, Exx', Eyy'; auto with *. -Qed. - -End BoolEqualityFacts. - - (** * Keys and datas used in FMap *) + Module KeyDecidableType(Import D:DecidableType). Section Elt. -- cgit v1.2.3