summaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic/Int31
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /theories/Numbers/Cyclic/Int31
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'theories/Numbers/Cyclic/Int31')
-rw-r--r--theories/Numbers/Cyclic/Int31/Cyclic31.v326
-rw-r--r--theories/Numbers/Cyclic/Int31/Int31.v26
-rw-r--r--theories/Numbers/Cyclic/Int31/Ring31.v11
3 files changed, 154 insertions, 209 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 36a1157d..2dd1c3ee 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Cyclic31.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(** * Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z *)
(**
@@ -907,9 +905,11 @@ Section Basics.
apply nshiftr_n_0.
Qed.
- Lemma p2ibis_spec : forall n p, n<=size ->
- Zpos p = ((Z_of_N (fst (p2ibis n p)))*2^(Z_of_nat n) +
- phi (snd (p2ibis n p)))%Z.
+ Local Open Scope Z_scope.
+
+ Lemma p2ibis_spec : forall n p, (n<=size)%nat ->
+ Zpos p = (Z_of_N (fst (p2ibis n p)))*2^(Z_of_nat n) +
+ phi (snd (p2ibis n p)).
Proof.
induction n; intros.
simpl; rewrite Pmult_1_r; auto.
@@ -917,7 +917,7 @@ Section Basics.
(rewrite <- Zpower_Zsucc, <- Zpos_P_of_succ_nat;
auto with zarith).
rewrite (Zmult_comm 2).
- assert (n<=size) by omega.
+ assert (n<=size)%nat by omega.
destruct p; simpl; [ | | auto];
specialize (IHn p H0);
generalize (p2ibis_bounded n p);
@@ -973,7 +973,8 @@ Section Basics.
(** Moreover, [p2ibis] is also related with [p2i] and hence with
[positive_to_int31]. *)
- Lemma double_twice_firstl : forall x, firstl x = D0 -> Twon*x = twice x.
+ Lemma double_twice_firstl : forall x, firstl x = D0 ->
+ (Twon*x = twice x)%int31.
Proof.
intros.
unfold mul31.
@@ -981,7 +982,7 @@ Section Basics.
Qed.
Lemma double_twice_plus_one_firstl : forall x, firstl x = D0 ->
- Twon*x+In = twice_plus_one x.
+ (Twon*x+In = twice_plus_one x)%int31.
Proof.
intros.
rewrite double_twice_firstl; auto.
@@ -1015,8 +1016,8 @@ Section Basics.
Qed.
Lemma positive_to_int31_spec : forall p,
- Zpos p = ((Z_of_N (fst (positive_to_int31 p)))*2^(Z_of_nat size) +
- phi (snd (positive_to_int31 p)))%Z.
+ Zpos p = (Z_of_N (fst (positive_to_int31 p)))*2^(Z_of_nat size) +
+ phi (snd (positive_to_int31 p)).
Proof.
unfold positive_to_int31.
intros; rewrite p2i_p2ibis; auto.
@@ -1033,7 +1034,7 @@ Section Basics.
intros.
pattern x at 1; rewrite <- (phi_inv_phi x).
rewrite <- phi_inv_double.
- assert (0 <= Zdouble (phi x))%Z.
+ assert (0 <= Zdouble (phi x)).
rewrite Zdouble_mult; generalize (phi_bounded x); omega.
destruct (Zdouble (phi x)).
simpl; auto.
@@ -1047,7 +1048,7 @@ Section Basics.
intros.
pattern x at 1; rewrite <- (phi_inv_phi x).
rewrite <- phi_inv_double_plus_one.
- assert (0 <= Zdouble_plus_one (phi x))%Z.
+ assert (0 <= Zdouble_plus_one (phi x)).
rewrite Zdouble_plus_one_mult; generalize (phi_bounded x); omega.
destruct (Zdouble_plus_one (phi x)).
simpl; auto.
@@ -1061,7 +1062,7 @@ Section Basics.
intros.
pattern x at 1; rewrite <- (phi_inv_phi x).
rewrite <- phi_inv_incr.
- assert (0 <= Zsucc (phi x))%Z.
+ assert (0 <= Zsucc (phi x)).
change (Zsucc (phi x)) with ((phi x)+1)%Z;
generalize (phi_bounded x); omega.
destruct (Zsucc (phi x)).
@@ -1083,7 +1084,7 @@ Section Basics.
rewrite incr_twice, phi_twice_plus_one.
remember (phi (complement_negative p)) as q.
rewrite Zdouble_plus_one_mult.
- replace (2*q+1)%Z with (2*(Zsucc q)-1)%Z by omega.
+ replace (2*q+1) with (2*(Zsucc q)-1) by omega.
rewrite <- Zminus_mod_idemp_l, <- Zmult_mod_idemp_r, IHp.
rewrite Zmult_mod_idemp_r, Zminus_mod_idemp_l; auto with zarith.
@@ -1106,81 +1107,61 @@ Section Basics.
End Basics.
-
-Section Int31_Op.
-
-(** Nullity test *)
-Let w_iszero i := match i ?= 0 with Eq => true | _ => false end.
-
-(** Modulo [2^p] *)
-Let w_pos_mod p i :=
- match compare31 p 31 with
+Instance int31_ops : ZnZ.Ops int31 :=
+{
+ digits := 31%positive; (* number of digits *)
+ zdigits := 31; (* number of digits *)
+ to_Z := phi; (* conversion to Z *)
+ of_pos := positive_to_int31; (* positive -> N*int31 : p => N,i
+ where p = N*2^31+phi i *)
+ head0 := head031; (* number of head 0 *)
+ tail0 := tail031; (* number of tail 0 *)
+ zero := 0;
+ one := 1;
+ minus_one := Tn; (* 2^31 - 1 *)
+ compare := compare31;
+ eq0 := fun i => match i ?= 0 with Eq => true | _ => false end;
+ opp_c := fun i => 0 -c i;
+ opp := opp31;
+ opp_carry := fun i => 0-i-1;
+ succ_c := fun i => i +c 1;
+ add_c := add31c;
+ add_carry_c := add31carryc;
+ succ := fun i => i + 1;
+ add := add31;
+ add_carry := fun i j => i + j + 1;
+ pred_c := fun i => i -c 1;
+ sub_c := sub31c;
+ sub_carry_c := sub31carryc;
+ pred := fun i => i - 1;
+ sub := sub31;
+ sub_carry := fun i j => i - j - 1;
+ mul_c := mul31c;
+ mul := mul31;
+ square_c := fun x => x *c x;
+ div21 := div3121;
+ div_gt := div31; (* this is supposed to be the special case of
+ division a/b where a > b *)
+ div := div31;
+ modulo_gt := fun i j => let (_,r) := i/j in r;
+ modulo := fun i j => let (_,r) := i/j in r;
+ gcd_gt := gcd31;
+ gcd := gcd31;
+ add_mul_div := addmuldiv31;
+ pos_mod := (* modulo 2^p *)
+ fun p i =>
+ match p ?= 31 with
| Lt => addmuldiv31 p 0 (addmuldiv31 (31-p) i 0)
| _ => i
- end.
+ end;
+ is_even :=
+ fun i => let (_,r) := i/2 in
+ match r ?= 0 with Eq => true | _ => false end;
+ sqrt2 := sqrt312;
+ sqrt := sqrt31
+}.
-(** Parity test *)
-Let w_iseven i :=
- let (_,r) := i/2 in
- match r ?= 0 with Eq => true | _ => false end.
-
-Definition int31_op := (mk_znz_op
- 31%positive (* number of digits *)
- 31 (* number of digits *)
- phi (* conversion to Z *)
- positive_to_int31 (* positive -> N*int31 : p => N,i where p = N*2^31+phi i *)
- head031 (* number of head 0 *)
- tail031 (* number of tail 0 *)
- (* Basic constructors *)
- 0
- 1
- Tn (* 2^31 - 1 *)
- (* Comparison *)
- compare31
- w_iszero
- (* Basic arithmetic operations *)
- (fun i => 0 -c i)
- opp31
- (fun i => 0-i-1)
- (fun i => i +c 1)
- add31c
- add31carryc
- (fun i => i + 1)
- add31
- (fun i j => i + j + 1)
- (fun i => i -c 1)
- sub31c
- sub31carryc
- (fun i => i - 1)
- sub31
- (fun i j => i - j - 1)
- mul31c
- mul31
- (fun x => x *c x)
- (* special (euclidian) division operations *)
- div3121
- div31 (* this is supposed to be the special case of division a/b where a > b *)
- div31
- (* euclidian division remainder *)
- (* again special case for a > b *)
- (fun i j => let (_,r) := i/j in r)
- (fun i j => let (_,r) := i/j in r)
- gcd31 (*gcd_gt*)
- gcd31 (*gcd*)
- (* shift operations *)
- addmuldiv31 (*add_mul_div *)
- (* modulo 2^p *)
- w_pos_mod
- (* is i even ? *)
- w_iseven
- (* square root operations *)
- sqrt312 (* sqrt2 *)
- sqrt31 (* sqrt *)
-).
-
-End Int31_Op.
-
-Section Int31_Spec.
+Section Int31_Specs.
Local Open Scope Z_scope.
@@ -1222,22 +1203,14 @@ Section Int31_Spec.
reflexivity.
Qed.
- Lemma spec_Bm1 : [| Tn |] = wB - 1.
+ Lemma spec_m1 : [| Tn |] = wB - 1.
Proof.
reflexivity.
Qed.
Lemma spec_compare : forall x y,
- match (x ?= y)%int31 with
- | Eq => [|x|] = [|y|]
- | Lt => [|x|] < [|y|]
- | Gt => [|x|] > [|y|]
- end.
- Proof.
- clear; unfold compare31; simpl; intros.
- case_eq ([|x|] ?= [|y|]); auto.
- intros; apply Zcompare_Eq_eq; auto.
- Qed.
+ (x ?= y)%int31 = ([|x|] ?= [|y|]).
+ Proof. reflexivity. Qed.
(** Addition *)
@@ -1654,12 +1627,10 @@ Section Int31_Spec.
rewrite Zmult_comm, Z_div_mult; auto with zarith.
Qed.
- Let w_pos_mod := int31_op.(znz_pos_mod).
-
Lemma spec_pos_mod : forall w p,
- [|w_pos_mod p w|] = [|w|] mod (2 ^ [|p|]).
+ [|ZnZ.pos_mod p w|] = [|w|] mod (2 ^ [|p|]).
Proof.
- unfold w_pos_mod, znz_pos_mod, int31_op, compare31.
+ unfold ZnZ.pos_mod, int31_ops, compare31.
change [|31|] with 31%Z.
assert (forall w p, 31<=p -> [|w|] = [|w|] mod 2^p).
intros.
@@ -1721,7 +1692,7 @@ Section Int31_Spec.
unfold head031, recl.
change On with (phi_inv (Z_of_nat (31-size))).
replace (head031_alt size x) with
- (head031_alt size x + (31 - size))%nat by (apply plus_0_r; auto).
+ (head031_alt size x + (31 - size))%nat by auto.
assert (size <= 31)%nat by auto with arith.
revert x H; induction size; intros.
@@ -1829,7 +1800,7 @@ Section Int31_Spec.
unfold tail031, recr.
change On with (phi_inv (Z_of_nat (31-size))).
replace (tail031_alt size x) with
- (tail031_alt size x + (31 - size))%nat by (apply plus_0_r; auto).
+ (tail031_alt size x + (31 - size))%nat by auto.
assert (size <= 31)%nat by auto with arith.
revert x H; induction size; intros.
@@ -2018,8 +1989,8 @@ Section Int31_Spec.
Proof.
assert (Hp2: 0 < [|2|]) by exact (refl_equal Lt).
intros Hi Hj Hij H31 Hrec; rewrite sqrt31_step_def.
- generalize (spec_compare (fst (i/j)%int31) j); case compare31;
- rewrite div31_phi; auto; intros Hc;
+ rewrite spec_compare, div31_phi; auto.
+ case Zcompare_spec; auto; intros Hc;
try (split; auto; apply sqrt_test_true; auto with zarith; fail).
apply Hrec; repeat rewrite div31_phi; auto with zarith.
replace [|(j + fst (i / j)%int31)|] with ([|j|] + [|i|] / [|j|]).
@@ -2072,7 +2043,7 @@ Section Int31_Spec.
[|sqrt31 x|] ^ 2 <= [|x|] < ([|sqrt31 x|] + 1) ^ 2.
Proof.
intros i; unfold sqrt31.
- generalize (spec_compare 1 i); case compare31; change [|1|] with 1;
+ rewrite spec_compare. case Zcompare_spec; change [|1|] with 1;
intros Hi; auto with zarith.
repeat rewrite Zpower_2; auto with zarith.
apply iter31_sqrt_correct; auto with zarith.
@@ -2157,7 +2128,7 @@ Section Int31_Spec.
unfold phi2; apply Zlt_le_trans with ([|ih|] * base)%Z; auto with zarith.
apply Zmult_lt_0_compat; auto with zarith.
apply Zlt_le_trans with (2:= Hih); auto with zarith.
- generalize (spec_compare ih j); case compare31; intros Hc1.
+ rewrite spec_compare. case Zcompare_spec; intros Hc1.
split; auto.
apply sqrt_test_true; auto.
unfold phi2, base; auto with zarith.
@@ -2166,7 +2137,7 @@ Section Int31_Spec.
rewrite Zmult_comm, Z_div_plus_full_l; unfold base; auto with zarith.
unfold Zpower, Zpower_pos in Hj1; simpl in Hj1; auto with zarith.
case (Zle_or_lt (2 ^ 30) [|j|]); intros Hjj.
- generalize (spec_compare (fst (div3121 ih il j)) j); case compare31;
+ rewrite spec_compare; case Zcompare_spec;
rewrite div312_phi; auto; intros Hc;
try (split; auto; apply sqrt_test_true; auto with zarith; fail).
apply Hrec.
@@ -2274,7 +2245,7 @@ Section Int31_Spec.
2: simpl; unfold Zpower_pos; simpl; auto with zarith.
case (phi_bounded ih); case (phi_bounded il); intros H1 H2 H3 H4.
unfold base, Zpower, Zpower_pos in H2,H4; simpl in H2,H4.
- unfold phi2,Zpower, Zpower_pos; simpl iter_pos; auto with zarith.
+ unfold phi2,Zpower, Zpower_pos. simpl Pos.iter; auto with zarith.
case (iter312_sqrt_correct 31 (fun _ _ j => j) ih il Tn); auto with zarith.
change [|Tn|] with 2147483647; auto with zarith.
intros j1 _ HH; contradict HH.
@@ -2300,7 +2271,7 @@ Section Int31_Spec.
generalize (spec_sub_c il il1).
case sub31c; intros il2 Hil2.
simpl interp_carry in Hil2.
- generalize (spec_compare ih ih1); case compare31.
+ rewrite spec_compare; case Zcompare_spec.
unfold interp_carry.
intros H1; split.
rewrite Zpower_2, <- Hihl1.
@@ -2347,7 +2318,7 @@ Section Int31_Spec.
case (phi_bounded ih); intros H1 H2.
generalize Hih; change (2 ^ Z_of_nat size / 4) with 536870912.
split; auto with zarith.
- generalize (spec_compare (ih - 1) ih1); case compare31.
+ rewrite spec_compare; case Zcompare_spec.
rewrite Hsih.
intros H1; split.
rewrite Zpower_2, <- Hihl1.
@@ -2414,15 +2385,13 @@ Section Int31_Spec.
replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring.
rewrite <-Hil2.
change (-1 * 2 ^ Z_of_nat size) with (-base); ring.
- Qed.
+Qed.
(** [iszero] *)
- Let w_eq0 := int31_op.(znz_eq0).
-
- Lemma spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0.
+ Lemma spec_eq0 : forall x, ZnZ.eq0 x = true -> [|x|] = 0.
Proof.
- clear; unfold w_eq0, znz_eq0; simpl.
+ clear; unfold ZnZ.eq0; simpl.
unfold compare31; simpl; intros.
change [|0|] with 0 in H.
apply Zcompare_Eq_eq.
@@ -2431,12 +2400,10 @@ Section Int31_Spec.
(* Even *)
- Let w_is_even := int31_op.(znz_is_even).
-
Lemma spec_is_even : forall x,
- if w_is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1.
+ if ZnZ.is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1.
Proof.
- unfold w_is_even; simpl; intros.
+ unfold ZnZ.is_even; simpl; intros.
generalize (spec_div x 2).
destruct (x/2)%int31 as (q,r); intros.
unfold compare31.
@@ -2445,77 +2412,60 @@ Section Int31_Spec.
destruct H; auto with zarith.
replace ([|x|] mod 2) with [|r|].
destruct H; auto with zarith.
- case_eq ([|r|] ?= 0)%Z; intros.
- apply Zcompare_Eq_eq; auto.
- change ([|r|] < 0)%Z in H; auto with zarith.
- change ([|r|] > 0)%Z in H; auto with zarith.
+ case Zcompare_spec; auto with zarith.
apply Zmod_unique with [|q|]; auto with zarith.
Qed.
- Definition int31_spec : znz_spec int31_op.
- split.
- exact phi_bounded.
- exact positive_to_int31_spec.
- exact spec_zdigits.
- exact spec_more_than_1_digit.
-
- exact spec_0.
- exact spec_1.
- exact spec_Bm1.
-
- exact spec_compare.
- exact spec_eq0.
-
- exact spec_opp_c.
- exact spec_opp.
- exact spec_opp_carry.
-
- exact spec_succ_c.
- exact spec_add_c.
- exact spec_add_carry_c.
- exact spec_succ.
- exact spec_add.
- exact spec_add_carry.
-
- exact spec_pred_c.
- exact spec_sub_c.
- exact spec_sub_carry_c.
- exact spec_pred.
- exact spec_sub.
- exact spec_sub_carry.
-
- exact spec_mul_c.
- exact spec_mul.
- exact spec_square_c.
-
- exact spec_div21.
- intros; apply spec_div; auto.
- exact spec_div.
-
- intros; unfold int31_op; simpl; apply spec_mod; auto.
- exact spec_mod.
-
- intros; apply spec_gcd; auto.
- exact spec_gcd.
-
- exact spec_head00.
- exact spec_head0.
- exact spec_tail00.
- exact spec_tail0.
-
- exact spec_add_mul_div.
- exact spec_pos_mod.
-
- exact spec_is_even.
- exact spec_sqrt2.
- exact spec_sqrt.
- Qed.
-
-End Int31_Spec.
+ Global Instance int31_specs : ZnZ.Specs int31_ops := {
+ spec_to_Z := phi_bounded;
+ spec_of_pos := positive_to_int31_spec;
+ spec_zdigits := spec_zdigits;
+ spec_more_than_1_digit := spec_more_than_1_digit;
+ spec_0 := spec_0;
+ spec_1 := spec_1;
+ spec_m1 := spec_m1;
+ spec_compare := spec_compare;
+ spec_eq0 := spec_eq0;
+ spec_opp_c := spec_opp_c;
+ spec_opp := spec_opp;
+ spec_opp_carry := spec_opp_carry;
+ spec_succ_c := spec_succ_c;
+ spec_add_c := spec_add_c;
+ spec_add_carry_c := spec_add_carry_c;
+ spec_succ := spec_succ;
+ spec_add := spec_add;
+ spec_add_carry := spec_add_carry;
+ spec_pred_c := spec_pred_c;
+ spec_sub_c := spec_sub_c;
+ spec_sub_carry_c := spec_sub_carry_c;
+ spec_pred := spec_pred;
+ spec_sub := spec_sub;
+ spec_sub_carry := spec_sub_carry;
+ spec_mul_c := spec_mul_c;
+ spec_mul := spec_mul;
+ spec_square_c := spec_square_c;
+ spec_div21 := spec_div21;
+ spec_div_gt := fun a b _ => spec_div a b;
+ spec_div := spec_div;
+ spec_modulo_gt := fun a b _ => spec_mod a b;
+ spec_modulo := spec_mod;
+ spec_gcd_gt := fun a b _ => spec_gcd a b;
+ spec_gcd := spec_gcd;
+ spec_head00 := spec_head00;
+ spec_head0 := spec_head0;
+ spec_tail00 := spec_tail00;
+ spec_tail0 := spec_tail0;
+ spec_add_mul_div := spec_add_mul_div;
+ spec_pos_mod := spec_pos_mod;
+ spec_is_even := spec_is_even;
+ spec_sqrt2 := spec_sqrt2;
+ spec_sqrt := spec_sqrt }.
+
+End Int31_Specs.
Module Int31Cyclic <: CyclicType.
- Definition w := int31.
- Definition w_op := int31_op.
- Definition w_spec := int31_spec.
+ Definition t := int31.
+ Definition ops := int31_ops.
+ Definition specs := int31_specs.
End Int31Cyclic.
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 5e1cd0e1..20f750f6 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,15 +8,11 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: Int31.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import NaryFunctions.
Require Import Wf_nat.
Require Export ZArith.
Require Export DoubleType.
-Unset Boxed Definitions.
-
(** * 31-bit integers *)
(** This file contains basic definitions of a 31-bit integer
@@ -353,16 +349,16 @@ Register div31 as int31 div in "coq_int31" by True.
Register compare31 as int31 compare in "coq_int31" by True.
Register addmuldiv31 as int31 addmuldiv in "coq_int31" by True.
-Definition gcd31 (i j:int31) :=
- (fix euler (guard:nat) (i j:int31) {struct guard} :=
- match guard with
- | O => In
- | S p => match j ?= On with
- | Eq => i
- | _ => euler p j (let (_, r ) := i/j in r)
- end
- end)
- (2*size)%nat i j.
+Fixpoint euler (guard:nat) (i j:int31) {struct guard} :=
+ match guard with
+ | O => In
+ | S p => match j ?= On with
+ | Eq => i
+ | _ => euler p j (let (_, r ) := i/j in r)
+ end
+ end.
+
+Definition gcd31 (i j:int31) := euler (2*size)%nat i j.
(** Square root functions using newton iteration
we use a very naive upper-bound on the iteration
diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v
index 37dc0871..23e8bd33 100644
--- a/theories/Numbers/Cyclic/Int31/Ring31.v
+++ b/theories/Numbers/Cyclic/Int31/Ring31.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Ring31.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(** * Int31 numbers defines Z/(2^31)Z, and can hence be equipped
with a ring structure and a ring tactic *)
@@ -83,9 +81,10 @@ Qed.
Lemma eqb31_eq : forall x y, eqb31 x y = true <-> x=y.
Proof.
unfold eqb31. intros x y.
-generalize (Cyclic31.spec_compare x y).
-destruct (x ?= y); intuition; subst; auto with zarith; try discriminate.
-apply Int31_canonic; auto.
+rewrite Cyclic31.spec_compare. case Zcompare_spec.
+intuition. apply Int31_canonic; auto.
+intuition; subst; auto with zarith; try discriminate.
+intuition; subst; auto with zarith; try discriminate.
Qed.
Lemma eqb31_correct : forall x y, eqb31 x y = true -> x=y.