diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZSgnAbs.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZSgnAbs.v | 88 |
1 files changed, 52 insertions, 36 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v index cecaa6a3..b2f6cc84 100644 --- a/theories/Numbers/Integer/Abstract/ZSgnAbs.v +++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.v @@ -1,25 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Export ZMulOrder. +(** Properties of [abs] and [sgn] *) -(** An axiomatization of [abs]. *) - -Module Type HasAbs(Import Z : ZAxiomsSig'). - Parameter Inline abs : t -> t. - Axiom abs_eq : forall n, 0<=n -> abs n == n. - Axiom abs_neq : forall n, n<=0 -> abs n == -n. -End HasAbs. +Require Import ZMulOrder. (** Since we already have [max], we could have defined [abs]. *) -Module GenericAbs (Import Z : ZAxiomsSig') - (Import ZP : ZMulOrderPropFunct Z) <: HasAbs Z. +Module GenericAbs (Import Z : ZAxiomsMiniSig') + (Import ZP : ZMulOrderProp Z) <: HasAbs Z. Definition abs n := max n (-n). Lemma abs_eq : forall n, 0<=n -> abs n == n. Proof. @@ -35,37 +29,28 @@ Module GenericAbs (Import Z : ZAxiomsSig') Qed. End GenericAbs. -(** An Axiomatization of [sgn]. *) - -Module Type HasSgn (Import Z : ZAxiomsSig'). - Parameter Inline sgn : t -> t. - Axiom sgn_null : forall n, n==0 -> sgn n == 0. - Axiom sgn_pos : forall n, 0<n -> sgn n == 1. - Axiom sgn_neg : forall n, n<0 -> sgn n == -(1). -End HasSgn. - (** We can deduce a [sgn] function from a [compare] function *) -Module Type ZDecAxiomsSig := ZAxiomsSig <+ HasCompare. -Module Type ZDecAxiomsSig' := ZAxiomsSig' <+ HasCompare. +Module Type ZDecAxiomsSig := ZAxiomsMiniSig <+ HasCompare. +Module Type ZDecAxiomsSig' := ZAxiomsMiniSig' <+ HasCompare. Module Type GenericSgn (Import Z : ZDecAxiomsSig') - (Import ZP : ZMulOrderPropFunct Z) <: HasSgn Z. + (Import ZP : ZMulOrderProp Z) <: HasSgn Z. Definition sgn n := - match compare 0 n with Eq => 0 | Lt => 1 | Gt => -(1) end. + match compare 0 n with Eq => 0 | Lt => 1 | Gt => -1 end. Lemma sgn_null : forall n, n==0 -> sgn n == 0. Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed. Lemma sgn_pos : forall n, 0<n -> sgn n == 1. Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed. - Lemma sgn_neg : forall n, n<0 -> sgn n == -(1). + Lemma sgn_neg : forall n, n<0 -> sgn n == -1. Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed. End GenericSgn. -Module Type ZAxiomsExtSig := ZAxiomsSig <+ HasAbs <+ HasSgn. -Module Type ZAxiomsExtSig' := ZAxiomsSig' <+ HasAbs <+ HasSgn. -Module Type ZSgnAbsPropSig (Import Z : ZAxiomsExtSig') - (Import ZP : ZMulOrderPropFunct Z). +(** Derived properties of [abs] and [sgn] *) + +Module Type ZSgnAbsProp (Import Z : ZAxiomsSig') + (Import ZP : ZMulOrderProp Z). Ltac destruct_max n := destruct (le_ge_cases 0 n); @@ -183,6 +168,28 @@ Proof. rewrite EQn, EQ, opp_inj_wd, eq_opp_l, or_comm. apply abs_eq_or_opp. Qed. +Lemma abs_lt : forall a b, abs a < b <-> -b < a < b. +Proof. + intros a b. + destruct (abs_spec a) as [[LE EQ]|[LT EQ]]; rewrite EQ; clear EQ. + split; try split; try destruct 1; try order. + apply lt_le_trans with 0; trivial. apply opp_neg_pos; order. + rewrite opp_lt_mono, opp_involutive. + split; try split; try destruct 1; try order. + apply lt_le_trans with 0; trivial. apply opp_nonpos_nonneg; order. +Qed. + +Lemma abs_le : forall a b, abs a <= b <-> -b <= a <= b. +Proof. + intros a b. + destruct (abs_spec a) as [[LE EQ]|[LT EQ]]; rewrite EQ; clear EQ. + split; try split; try destruct 1; try order. + apply le_trans with 0; trivial. apply opp_nonpos_nonneg; order. + rewrite opp_le_mono, opp_involutive. + split; try split; try destruct 1; try order. + apply le_trans with 0. order. apply opp_nonpos_nonneg; order. +Qed. + (** Triangular inequality *) Lemma abs_triangle : forall n m, abs (n + m) <= abs n + abs m. @@ -249,7 +256,7 @@ Qed. Lemma sgn_spec : forall n, 0 < n /\ sgn n == 1 \/ 0 == n /\ sgn n == 0 \/ - 0 > n /\ sgn n == -(1). + 0 > n /\ sgn n == -1. Proof. intros n. destruct_sgn n; [left|right;left|right;right]; auto with relations. @@ -264,7 +271,7 @@ Lemma sgn_pos_iff : forall n, sgn n == 1 <-> 0<n. Proof. split; try apply sgn_pos. destruct_sgn n; auto. intros. elim (lt_neq 0 1); auto. apply lt_0_1. - intros. elim (lt_neq (-(1)) 1); auto. + intros. elim (lt_neq (-1) 1); auto. apply lt_trans with 0. rewrite opp_neg_pos. apply lt_0_1. apply lt_0_1. Qed. @@ -272,16 +279,16 @@ Lemma sgn_null_iff : forall n, sgn n == 0 <-> n==0. Proof. split; try apply sgn_null. destruct_sgn n; auto with relations. intros. elim (lt_neq 0 1); auto with relations. apply lt_0_1. - intros. elim (lt_neq (-(1)) 0); auto. + intros. elim (lt_neq (-1) 0); auto. rewrite opp_neg_pos. apply lt_0_1. Qed. -Lemma sgn_neg_iff : forall n, sgn n == -(1) <-> n<0. +Lemma sgn_neg_iff : forall n, sgn n == -1 <-> n<0. Proof. split; try apply sgn_neg. destruct_sgn n; auto with relations. - intros. elim (lt_neq (-(1)) 1); auto with relations. + intros. elim (lt_neq (-1) 1); auto with relations. apply lt_trans with 0. rewrite opp_neg_pos. apply lt_0_1. apply lt_0_1. - intros. elim (lt_neq (-(1)) 0); auto with relations. + intros. elim (lt_neq (-1) 0); auto with relations. rewrite opp_neg_pos. apply lt_0_1. Qed. @@ -343,6 +350,15 @@ Proof. rewrite eq_opp_l. apply abs_neq. now apply lt_le_incl. Qed. -End ZSgnAbsPropSig. +Lemma sgn_sgn : forall x, sgn (sgn x) == sgn x. +Proof. + intros. + destruct (sgn_spec x) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ. + apply sgn_pos, lt_0_1. + now apply sgn_null. + apply sgn_neg. rewrite opp_neg_pos. apply lt_0_1. +Qed. + +End ZSgnAbsProp. |