summaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic/Abstract
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract')
-rw-r--r--theories/Numbers/Cyclic/Abstract/CyclicAxioms.v21
-rw-r--r--theories/Numbers/Cyclic/Abstract/NZCyclic.v8
2 files changed, 17 insertions, 12 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 622ef225..8b84a484 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -88,8 +88,12 @@ Module ZnZ.
is_even : t -> bool;
(* square root *)
sqrt2 : t -> t -> t * carry t;
- sqrt : t -> t }.
-
+ sqrt : t -> t;
+ (* bitwise operations *)
+ lor : t -> t -> t;
+ land : t -> t -> t;
+ lxor : t -> t -> t }.
+
Section Specs.
Context {t : Type}{ops : Ops t}.
@@ -98,10 +102,10 @@ Module ZnZ.
Let wB := base digits.
Notation "[+| c |]" :=
- (interp_carry 1 wB to_Z c) (at level 0, x at level 99).
+ (interp_carry 1 wB to_Z c) (at level 0, c at level 99).
Notation "[-| c |]" :=
- (interp_carry (-1) wB to_Z c) (at level 0, x at level 99).
+ (interp_carry (-1) wB to_Z c) (at level 0, c at level 99).
Notation "[|| x ||]" :=
(zn2z_to_Z wB to_Z x) (at level 0, x at level 99).
@@ -199,7 +203,10 @@ Module ZnZ.
[||WW x y||] = [|s|] ^ 2 + [+|r|] /\
[+|r|] <= 2 * [|s|];
spec_sqrt : forall x,
- [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2
+ [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2;
+ spec_lor : forall x y, [|lor x y|] = Z.lor [|x|] [|y|];
+ spec_land : forall x y, [|land x y|] = Z.land [|x|] [|y|];
+ spec_lxor : forall x y, [|lxor x y|] = Z.lxor [|x|] [|y|]
}.
End Specs.
@@ -283,7 +290,7 @@ Module ZnZ.
intros p Hp.
generalize (spec_of_pos p).
case (of_pos p); intros n w1; simpl.
- case n; simpl Npos; auto with zarith.
+ case n; auto with zarith.
intros p1 Hp1; contradict Hp; apply Z.le_ngt.
replace (base digits) with (1 * base digits + 0) by ring.
rewrite Hp1.
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index d9089e18..8adeda37 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -106,7 +106,7 @@ Qed.
Theorem one_succ : one == succ zero.
Proof.
-zify; simpl. now rewrite one_mod_wB.
+zify; simpl Z.add. now rewrite one_mod_wB.
Qed.
Theorem two_succ : two == succ one.
@@ -126,9 +126,7 @@ Let B (n : Z) := A (ZnZ.of_Z n).
Lemma B0 : B 0.
Proof.
-unfold B.
-setoid_replace (ZnZ.of_Z 0) with zero. assumption.
-red; zify. apply ZnZ.of_Z_correct. auto using gt_wB_0 with zarith.
+unfold B. apply A0.
Qed.
Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).