From ddcbe6e926666cdc4bd5cd4a88d637efc338290c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 20 Jan 2011 11:53:58 +0000
Subject: Numbers: simplier spec for testbit

 We now specify testbit by some initial and recursive equations.
 The previous spec (via a complex split of the number in
 low and high parts) is now a derived property in {N,Z}Bits.v
 This way, proofs of implementations are quite simplier.
 Note that these new specs doesn't imply anymore that testbit is a
 morphism, we have to add this as a extra spec (but this lead
 to trivial proofs when implementing).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13792 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/Binary/ZBinary.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'theories/Numbers/Integer/Binary')

diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index cad5152d7a..3664180357 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -193,7 +193,11 @@ Definition rem := Zrem.
 
 (** Bitwise operations *)
 
-Definition testbit_spec := Ztestbit_spec.
+Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) Ztestbit.
+Definition testbit_odd_0 := Ztestbit_odd_0.
+Definition testbit_even_0 := Ztestbit_even_0.
+Definition testbit_odd_succ := Ztestbit_odd_succ.
+Definition testbit_even_succ := Ztestbit_even_succ.
 Definition testbit_neg_r := Ztestbit_neg_r.
 Definition shiftr_spec := Zshiftr_spec.
 Definition shiftl_spec_low := Zshiftl_spec_low.
-- 
cgit v1.2.3