From 7d220f8b61649646692983872626d6a8042446a9 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 20 Mar 2009 01:22:58 +0000
Subject: Directory 'contrib' renamed into 'plugins', to end confusion with
 archive of user contribs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/setoid_ring/ZArithRing.v | 60 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)
 create mode 100644 plugins/setoid_ring/ZArithRing.v

(limited to 'plugins/setoid_ring/ZArithRing.v')

diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v
new file mode 100644
index 000000000..942915abf
--- /dev/null
+++ b/plugins/setoid_ring/ZArithRing.v
@@ -0,0 +1,60 @@
+(************************************************************************)
+(*  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 Export Ring.
+Require Import ZArith_base.
+Require Import Zpow_def.
+
+Import InitialRing.
+
+Set Implicit Arguments.
+
+Ltac Zcst t :=
+  match isZcst t with
+    true => t
+  | _ => constr:NotConstant
+  end.
+
+Ltac isZpow_coef t :=
+  match t with 
+  | Zpos ?p => isPcst p
+  | Z0 => constr:true
+  | _ => constr:false
+  end.
+
+Definition N_of_Z x :=
+ match x with
+ | Zpos p => Npos p
+ | _ => N0
+ end.
+
+Ltac Zpow_tac t :=
+ match isZpow_coef t with
+ | true => constr:(N_of_Z t)
+ | _ => constr:NotConstant
+ end.
+
+Ltac Zpower_neg :=
+  repeat match goal with
+  | [|- ?G] => 
+    match G with 
+    | context c [Zpower _ (Zneg _)] =>
+      let t := context c [Z0] in
+      change t
+    end
+  end.   
+
+Add Ring Zr : Zth
+  (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
+   power_tac Zpower_theory [Zpow_tac],
+    (* The two following option are not needed, it is the default chose when the set of 
+        coefficiant is usual ring Z *)
+    div (InitialRing.Ztriv_div_th (@Eqsth Z) (@IDphi Z)),
+   sign get_signZ_th).
+
+
-- 
cgit v1.2.3