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/Natural/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/Natural/Binary')
| -rw-r--r-- | theories/Numbers/Natural/Binary/NBinary.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 82380e9b47..bd59ef494b 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -180,7 +180,11 @@ Proof. intros. now destruct (Ngcd a b). Qed. (** Bitwise Operations *) -Definition testbit_spec a n (_:0<=n) := Ntestbit_spec a n. +Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) Ntestbit. +Definition testbit_odd_0 := Ntestbit_odd_0. +Definition testbit_even_0 := Ntestbit_even_0. +Definition testbit_odd_succ a n (_:0<=n) := Ntestbit_odd_succ a n. +Definition testbit_even_succ a n (_:0<=n) := Ntestbit_even_succ a n. Lemma testbit_neg_r a n (H:n<0) : Ntestbit a n = false. Proof. now destruct n. Qed. Definition shiftl_spec_low := Nshiftl_spec_low. |