diff options
| author | letouzey | 2011-01-20 11:53:58 +0000 |
|---|---|---|
| committer | letouzey | 2011-01-20 11:53:58 +0000 |
| commit | ddcbe6e926666cdc4bd5cd4a88d637efc338290c (patch) | |
| tree | 75ebb40b14683b18bf454eed439deb60ef171d7b /theories/Numbers/Integer/Binary | |
| parent | c7c3fd68b065bcdee45585b2241c91360223b249 (diff) | |
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
Diffstat (limited to 'theories/Numbers/Integer/Binary')
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 6 |
1 files changed, 5 insertions, 1 deletions
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. |