1 files changed, 70 insertions, 0 deletions
diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v
new file mode 100644
index 00000000..5060bc69
--- /dev/null
+++ b/contrib/setoid_ring/ArithRing.v
@@ -0,0 +1,70 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Require Import Mult.
+Require Export Ring.
+Set Implicit Arguments.
+
+Ltac isnatcst t :=
+  let t := eval hnf in t in
+  match t with
+    O => true
+  | S ?p => isnatcst p
+  | _ => false
+  end.
+Ltac natcst t :=
+  match isnatcst t with
+    true => t
+  | _ => NotConstant
+  end.
+
+Ltac Ss_to_add f acc :=
+  match f with
+  | S ?f1 => Ss_to_add f1 (S acc)
+  | _ => constr:(acc + f)%nat
+  end.
+
+Ltac natprering :=
+  match goal with
+    |- context C [S ?p] =>
+    match p with
+      O => fail 1 (* avoid replacing 1 with 1+0 ! *)
+    | p => match isnatcst p with 
+           | true => fail 1
+           | false => let v := Ss_to_add p (S 0) in
+                         fold v; natprering
+           end
+    end
+  | _ => idtac
+  end.
+
+ Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat).
+ Proof.
+  constructor. exact plus_0_l. exact plus_comm. exact plus_assoc.
+  exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc.
+  exact mult_plus_distr_r. 
+ Qed.
+
+
+Unboxed Fixpoint nateq (n m:nat) {struct m} : bool :=
+  match n, m with
+  | O, O => true
+  | S n', S m' => nateq n' m'
+  | _, _ => false
+  end.
+
+Lemma nateq_ok : forall n m:nat, nateq n m = true -> n = m.
+Proof.
+  simple induction n; simple induction m; simpl; intros; try discriminate.
+  trivial.
+  rewrite (H n1 H1).
+  trivial.
+Qed.
+
+Add Ring natr : natSRth
+  (decidable nateq_ok, constants [natcst], preprocess [natprering]).