From 5db31bb0333810ccdd0a79e9855ae9d2fcdbf2d3 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 8 Jan 2010 14:44:56 +0000
Subject: Numbers: axiomatization + generic properties of abs and sgn.

 This allow to really finish files about division.
 An abs and sgn is added to BigZ.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12644 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/BigZ/ZMake.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'theories/Numbers/Integer/BigZ')

diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 615b8d1396..827877fc5b 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -488,4 +488,20 @@ Module Make (N:NType) <: ZType.
   case N.to_Z; simpl; auto with zarith.
  Qed.
 
+ Definition sgn x :=
+  match compare zero x with
+   | Lt => one
+   | Eq => zero
+   | Gt => minus_one
+  end.
+
+ Lemma spec_sgn : forall x, to_Z (sgn x) = Zsgn (to_Z x).
+ Proof.
+ intros. unfold sgn. generalize (spec_compare zero x).
+ destruct compare.
+ rewrite spec_0. intros <-; auto.
+ rewrite spec_0, spec_1. symmetry. rewrite Zsgn_pos; auto.
+ rewrite spec_0, spec_m1. symmetry. rewrite Zsgn_neg; auto with zarith.
+ Qed.
+
 End Make.
-- 
cgit v1.2.3