Ring31 : a ring structure and tactic for int31

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12685 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 223 insertions, 33 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 9ad1d019e..51df2fa38 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -373,3 +373,112 @@ Module Type CyclicType.
  Parameter w_op : znz_op w.
  Parameter w_spec : znz_spec w_op.
 End CyclicType.
+
+
+(** A Cyclic structure can be seen as a ring *)
+
+Module CyclicRing (Import Cyclic : CyclicType).
+
+Definition t := w.
+
+Local Notation "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99).
+
+Definition eq (n m : t) := [| n |] = [| m |].
+Definition zero : t := w_op.(znz_0).
+Definition one := w_op.(znz_1).
+Definition add := w_op.(znz_add).
+Definition sub := w_op.(znz_sub).
+Definition mul := w_op.(znz_mul).
+Definition opp := w_op.(znz_opp).
+
+Local Infix "=="  := eq (at level 70).
+Local Notation "0" := zero.
+Local Notation "1" := one.
+Local Infix "+" := add.
+Local Infix "-" := sub.
+Local Infix "*" := mul.
+Local Notation "!!" := (base (znz_digits w_op)).
+
+Hint Rewrite
+ w_spec.(spec_0) w_spec.(spec_1)
+ w_spec.(spec_add) w_spec.(spec_mul) w_spec.(spec_opp) w_spec.(spec_sub)
+ : cyclic.
+
+Ltac zify :=
+ unfold eq, zero, one, add, sub, mul, opp in *; autorewrite with cyclic.
+
+Lemma add_0_l : forall x, 0 + x == x.
+Proof.
+intros. zify. rewrite Zplus_0_l.
+apply Zmod_small. apply w_spec.(spec_to_Z).
+Qed.
+
+Lemma add_comm : forall x y, x + y == y + x.
+Proof.
+intros. zify. now rewrite Zplus_comm.
+Qed.
+
+Lemma add_assoc : forall x y z, x + (y + z) == x + y + z.
+Proof.
+intros. zify. now rewrite Zplus_mod_idemp_r, Zplus_mod_idemp_l, Zplus_assoc.
+Qed.
+
+Lemma mul_1_l : forall x, 1 * x == x.
+Proof.
+intros. zify. rewrite Zmult_1_l.
+apply Zmod_small. apply w_spec.(spec_to_Z).
+Qed.
+
+Lemma mul_comm : forall x y, x * y == y * x.
+Proof.
+intros. zify. now rewrite Zmult_comm.
+Qed.
+
+Lemma mul_assoc : forall x y z, x * (y * z) == x * y * z.
+Proof.
+intros. zify. now rewrite Zmult_mod_idemp_r, Zmult_mod_idemp_l, Zmult_assoc.
+Qed.
+
+Lemma mul_add_distr_r : forall x y z, (x+y)*z == x*z + y*z.
+Proof.
+intros. zify. now rewrite <- Zplus_mod, Zmult_mod_idemp_l, Zmult_plus_distr_l.
+Qed.
+
+Lemma add_opp_r : forall x y, x + opp y == x-y.
+Proof.
+intros. zify. rewrite <- Zminus_mod_idemp_r. unfold Zminus.
+destruct (Z_eq_dec ([|y|] mod !!) 0) as [EQ|NEQ].
+rewrite Z_mod_zero_opp_full, EQ, 2 Zplus_0_r; auto.
+rewrite Z_mod_nz_opp_full by auto.
+rewrite <- Zplus_mod_idemp_r, <- Zminus_mod_idemp_l.
+rewrite Z_mod_same_full. simpl. now rewrite Zplus_mod_idemp_r.
+Qed.
+
+Lemma add_opp_diag_r : forall x, x + opp x == 0.
+Proof.
+intros. red. rewrite add_opp_r. zify. now rewrite Zminus_diag, Zmod_0_l.
+Qed.
+
+Lemma CyclicRing : ring_theory 0 1 add mul sub opp eq.
+Proof.
+constructor.
+exact add_0_l. exact add_comm. exact add_assoc.
+exact mul_1_l. exact mul_comm. exact mul_assoc.
+exact mul_add_distr_r.
+symmetry. apply add_opp_r.
+exact add_opp_diag_r.
+Qed.
+
+Definition eqb x y :=
+ match w_op.(znz_compare) x y with Eq => true | _ => false end.
+
+Lemma eqb_eq : forall x y, eqb x y = true <-> x == y.
+Proof.
+ intros. unfold eqb, eq. generalize (w_spec.(spec_compare) x y).
+ destruct (w_op.(znz_compare) x y); intuition; try discriminate.
+Qed.
+
+Lemma eqb_correct : forall x y, eqb x y = true -> x==y.
+Proof. now apply eqb_eq. Qed.
+
+End CyclicRing.
\ No newline at end of file
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 7d795cf50..744f2f47c 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1140,7 +1140,7 @@ Definition int31_op := (mk_znz_op
  w_iszero
  (* Basic arithmetic operations *)
  (fun i => 0 -c i)
- (fun i => 0 - i)
+ opp31
  (fun i => 0-i-1)
  (fun i => i +c 1)
  add31c
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 23c2c36a2..cc224254f 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -274,6 +274,10 @@ Definition sub31carryc (n m : int31) :=
   | _ => C1 nmmmone
   end.
 
+(** Opposite *)
+
+Definition opp31 x := On - x.
+Notation "- x" := (opp31 x) : int31_scope.
 
 (** Multiplication *)
 
@@ -309,6 +313,9 @@ Notation "n / m" := (div31 n m) : int31_scope.
 Definition compare31 (n m : int31) := ((phi n)?=(phi m))%Z.
 Notation "n ?= m" := (compare31 n m) (at level 70, no associativity) : int31_scope.
 
+Definition eqb31 (n m : int31) :=
+ match n ?= m with Eq => true | _ => false end.
+
 
 (** Computing the [i]-th iterate of a function:
     [iter_int31 i A f = f^i] *)
diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v
new file mode 100644
index 000000000..2ec406b0f
--- /dev/null
+++ b/theories/Numbers/Cyclic/Int31/Ring31.v
@@ -0,0 +1,103 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(** * Int31 numbers defines Z/(2^31)Z, and can hence be equipped
+      with a ring structure and a ring tactic *)
+
+Require Import Int31 Cyclic31 CyclicAxioms.
+
+Local Open Scope int31_scope.
+
+(** Detection of constants *)
+
+Local Open Scope list_scope.
+
+Ltac isInt31cst_lst l :=
+ match l with
+ | nil => constr:true
+ | ?t::?l => match t with
+               | D1 => isInt31cst_lst l
+               | D0 => isInt31cst_lst l
+               | _ => constr:false
+             end
+ | _ => constr:false
+ end.
+
+Ltac isInt31cst t :=
+ match t with
+ | I31 ?i0 ?i1 ?i2 ?i3 ?i4 ?i5 ?i6 ?i7 ?i8 ?i9 ?i10
+       ?i11 ?i12 ?i13 ?i14 ?i15 ?i16 ?i17 ?i18 ?i19 ?i20
+       ?i21 ?i22 ?i23 ?i24 ?i25 ?i26 ?i27 ?i28 ?i29 ?i30 =>
+    let l :=
+      constr:(i0::i1::i2::i3::i4::i5::i6::i7::i8::i9::i10
+      ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20
+      ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil)
+    in isInt31cst_lst l
+ | Int31.On => constr:true
+ | Int31.In => constr:true
+ | Int31.Tn => constr:true
+ | Int31.Twon => constr:true
+ | _ => constr:false
+ end.
+
+Ltac Int31cst t :=
+ match isInt31cst t with
+ | true => constr:t
+ | false => constr:NotConstant
+ end.
+
+(** The generic ring structure inferred from the Cyclic structure *)
+
+Module Int31ring := CyclicRing Int31Cyclic.
+
+(** Unlike in the generic [CyclicRing], we can use Leibniz here. *)
+
+Lemma Int31_canonic : forall x y, phi x = phi y -> x = y.
+Proof.
+ intros x y EQ.
+ now rewrite <- (phi_inv_phi x), <- (phi_inv_phi y), EQ.
+Qed.
+
+Lemma ring_theory_switch_eq :
+ forall A (R R':A->A->Prop) zero one add mul sub opp,
+  (forall x y : A, R x y -> R' x y) ->
+  ring_theory zero one add mul sub opp R ->
+  ring_theory zero one add mul sub opp R'.
+Proof.
+intros A R R' zero one add mul sub opp Impl Ring.
+constructor; intros; apply Impl; apply Ring.
+Qed.
+
+Lemma Int31Ring : ring_theory 0 1 add31 mul31 sub31 opp31 Logic.eq.
+Proof.
+exact (ring_theory_switch_eq _ _ _ _ _ _ _ _ _ Int31_canonic Int31ring.CyclicRing).
+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.
+Qed.
+
+Lemma eqb31_correct : forall x y, eqb31 x y = true -> x=y.
+Proof. now apply eqb31_eq. Qed.
+
+Add Ring Int31Ring : Int31Ring
+ (decidable eqb31_correct,
+  constants [Int31cst]).
+
+Section TestRing.
+Let test : forall x y, 1 + x*y + x*x + 1 = 1*1 + 1 + y*x + 1*x*x.
+intros. ring.
+Qed.
+End TestRing.
+
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 9a4d7a9b0..cab4b1542 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -11,7 +11,7 @@
 (** Initial Author: Arnaud Spiwack *)
 
 Require Export Int31.
-Require Import CyclicAxioms Cyclic31 NSig NSigNAxioms NMake
+Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
   NProperties NDiv GenericMinMax.
 
 (** The following [BigN] module regroups both the operations and
@@ -137,36 +137,6 @@ Qed.
 
 (** Detection of constants *)
 
-Local Open Scope list_scope.
-
-Ltac isInt31cst_lst l :=
- match l with
- | nil => constr:true
- | ?t::?l => match t with
-               | D1 => isInt31cst_lst l
-               | D0 => isInt31cst_lst l
-               | _ => constr:false
-             end
- | _ => constr:false
- end.
-
-Ltac isInt31cst t :=
- match t with
- | I31 ?i0 ?i1 ?i2 ?i3 ?i4 ?i5 ?i6 ?i7 ?i8 ?i9 ?i10
-       ?i11 ?i12 ?i13 ?i14 ?i15 ?i16 ?i17 ?i18 ?i19 ?i20
-       ?i21 ?i22 ?i23 ?i24 ?i25 ?i26 ?i27 ?i28 ?i29 ?i30 =>
-    let l :=
-      constr:(i0::i1::i2::i3::i4::i5::i6::i7::i8::i9::i10
-      ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20
-      ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil)
-    in isInt31cst_lst l
- | Int31.On => constr:true
- | Int31.In => constr:true
- | Int31.Tn => constr:true
- | Int31.Twon => constr:true
- | _ => constr:false
- end.
-
 Ltac isStaticWordCst t :=
  match t with
  | W0 => constr:true
diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget
index 070149a11..25f8570ba 100644
--- a/theories/Numbers/vo.itarget
+++ b/theories/Numbers/vo.itarget
@@ -11,8 +11,9 @@ Cyclic/DoubleCyclic/DoubleMul.vo
 Cyclic/DoubleCyclic/DoubleSqrt.vo
 Cyclic/DoubleCyclic/DoubleSub.vo
 Cyclic/DoubleCyclic/DoubleType.vo
-Cyclic/Int31/Cyclic31.vo
 Cyclic/Int31/Int31.vo
+Cyclic/Int31/Cyclic31.vo
+Cyclic/Int31/Ring31.vo
 Cyclic/ZModulo/ZModulo.vo
 Integer/Abstract/ZAddOrder.vo
 Integer/Abstract/ZAdd.vo