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/Binary/ZBinary.v | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) (limited to 'theories/Numbers/Integer/Binary') diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 516827616..6a2745d34 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -18,7 +18,7 @@ Local Open Scope Z_scope. (** * Implementation of [ZAxiomsSig] by [BinInt.Z] *) -Module ZBinAxiomsMod <: ZAxiomsSig. +Module ZBinAxiomsMod <: ZAxiomsExtSig. (** Bi-directional induction. *) @@ -70,6 +70,18 @@ Definition succ_pred n := eq_sym (Zsucc_pred n). Definition opp_0 := Zopp_0. Definition opp_succ := Zopp_succ. +(** Absolute value and sign *) + +Definition abs_eq := Zabs_eq. +Definition abs_neq := Zabs_non_eq. + +Lemma sgn_null : forall x, x = 0 -> Zsgn x = 0. +Proof. intros. apply <- Zsgn_null; auto. Qed. +Lemma sgn_pos : forall x, 0 < x -> Zsgn x = 1. +Proof. intros. apply <- Zsgn_pos; auto. Qed. +Lemma sgn_neg : forall x, x < 0 -> Zsgn x = -1. +Proof. intros. apply <- Zsgn_neg; auto. Qed. + (** The instantiation of operations. Placing them at the very end avoids having indirections in above lemmas. *) @@ -86,6 +98,8 @@ Definition le := Zle. Definition min := Zmin. Definition max := Zmax. Definition opp := Zopp. +Definition abs := Zabs. +Definition sgn := Zsgn. End ZBinAxiomsMod. -- cgit v1.2.3