ZSgnAbs.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Properties of abs and sgn

Require Import ZMulOrder.

Since we already have max, we could have defined abs.

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.forall n : t, 0 <= n -> abs n == n
 Proof.forall n : t, 0 <= n -> abs n == n
  intros.n:t
H:0 <= n
abs n == n unfold abs.n:t
H:0 <= n
max n (- n) == n apply max_l.n:t
H:0 <= n
- n <= n
  apply le_trans with 0; auto.n:t
H:0 <= n
- n <= 0
  rewrite opp_nonpos_nonneg; auto.
 Qed.
 Lemma abs_neq : forall n, n<=0 -> abs n == -n.forall n : t, n <= 0 -> abs n == - n
 Proof.forall n : t, n <= 0 -> abs n == - n
  intros.n:t
H:n <= 0
abs n == - n unfold abs.n:t
H:n <= 0
max n (- n) == - n apply max_r.n:t
H:n <= 0
n <= - n
  apply le_trans with 0; auto.n:t
H:n <= 0
0 <= - n
  rewrite opp_nonneg_nonpos; auto.
 Qed.
End GenericAbs.

We can deduce a sgn function from a compare function

Module Type ZDecAxiomsSig := ZAxiomsMiniSig <+ HasCompare.
Module Type ZDecAxiomsSig' := ZAxiomsMiniSig' <+ HasCompare.

Module Type GenericSgn (Import Z : ZDecAxiomsSig')
                       (Import ZP : ZMulOrderProp Z) <: HasSgn Z.
 Definition sgn n :=
  match compare 0 n with Eq => 0 | Lt => 1 | Gt => -1 end.
 Lemma sgn_null : forall n, n==0 -> sgn n == 0.forall n : t, n == 0 -> sgn n == 0
 Proof.forall n : t, n == 0 -> sgn n == 0 unfold sgn; intros.n:t
H:n == 0
match compare 0 n with
| Eq => 0
| Lt => 1
| Gt => -1
end == 0 destruct (compare_spec 0 n); order. Qed.
 Lemma sgn_pos : forall n, 0<n -> sgn n == 1.forall n : t, 0 < n -> sgn n == 1
 Proof.forall n : t, 0 < n -> sgn n == 1 unfold sgn; intros.n:t
H:0 < n
match compare 0 n with
| Eq => 0
| Lt => 1
| Gt => -1
end == 1 destruct (compare_spec 0 n); order. Qed.
 Lemma sgn_neg : forall n, n<0 -> sgn n == -1.forall n : t, n < 0 -> sgn n == -1
 Proof.forall n : t, n < 0 -> sgn n == -1 unfold sgn; intros.n:t
H:n < 0
match compare 0 n with
| Eq => 0
| Lt => 1
| Gt => -1
end == -1 destruct (compare_spec 0 n); order. Qed.
End GenericSgn.

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);
  [rewrite (abs_eq n) by auto | rewrite (abs_neq n) by auto].

Instance abs_wd : Proper (eq==>eq) abs.Proper (eq ==> eq) abs
Proof.Proper (eq ==> eq) abs
 intros x y EQ.x, y:t
EQ:x == y
abs x == abs y destruct_max x.x, y:t
EQ:x == y
H:0 <= x
x == abs y
x, y:t
EQ:x == y
H:x <= 0
- x == abs y
 rewrite abs_eq; trivial.x, y:t
EQ:x == y
H:0 <= x
0 <= y
x, y:t
EQ:x == y
H:x <= 0
- x == abs y now rewrite <- EQ.x, y:t
EQ:x == y
H:x <= 0
- x == abs y
 rewrite abs_neq; try order.x, y:t
EQ:x == y
H:x <= 0
- x == - y now rewrite opp_inj_wd.
Qed.

Lemma abs_max : forall n, abs n == max n (-n).forall n : t, abs n == max n (- n)
Proof.forall n : t, abs n == max n (- n)
 intros n.n:t
abs n == max n (- n) destruct_max n.n:t
H:0 <= n
n == max n (- n)
n:t
H:n <= 0
- n == max n (- n)
 rewrite max_l; auto with relations.n:t
H:0 <= n
- n <= n
n:t
H:n <= 0
- n == max n (- n)
 apply le_trans with 0; auto.n:t
H:0 <= n
- n <= 0
n:t
H:n <= 0
- n == max n (- n)
 rewrite opp_nonpos_nonneg; auto.n:t
H:n <= 0
- n == max n (- n)
 rewrite max_r; auto with relations.n:t
H:n <= 0
n <= - n
 apply le_trans with 0; auto.n:t
H:n <= 0
0 <= - n
 rewrite opp_nonneg_nonpos; auto.
Qed.

Lemma abs_neq' : forall n, 0<=-n -> abs n == -n.forall n : t, 0 <= - n -> abs n == - n
Proof.forall n : t, 0 <= - n -> abs n == - n
 intros.n:t
H:0 <= - n
abs n == - n apply abs_neq.n:t
H:0 <= - n
n <= 0 now rewrite <- opp_nonneg_nonpos.
Qed.

Lemma abs_nonneg : forall n, 0 <= abs n.forall n : t, 0 <= abs n
Proof.forall n : t, 0 <= abs n
 intros n.n:t
0 <= abs n destruct_max n; auto.n:t
H:n <= 0
0 <= - n
 now rewrite opp_nonneg_nonpos.
Qed.

Lemma abs_eq_iff : forall n, abs n == n <-> 0<=n.forall n : t, abs n == n <-> 0 <= n
Proof.forall n : t, abs n == n <-> 0 <= n
 split; try apply abs_eq.n:t
abs n == n -> 0 <= n intros EQ.n:t
EQ:abs n == n
0 <= n
 rewrite <- EQ.n:t
EQ:abs n == n
0 <= abs n apply abs_nonneg.
Qed.

Lemma abs_neq_iff : forall n, abs n == -n <-> n<=0.forall n : t, abs n == - n <-> n <= 0
Proof.forall n : t, abs n == - n <-> n <= 0
 split; try apply abs_neq.n:t
abs n == - n -> n <= 0 intros EQ.n:t
EQ:abs n == - n
n <= 0
 rewrite <- opp_nonneg_nonpos, <- EQ.n:t
EQ:abs n == - n
0 <= abs n apply abs_nonneg.
Qed.

Lemma abs_opp : forall n, abs (-n) == abs n.forall n : t, abs (- n) == abs n
Proof.forall n : t, abs (- n) == abs n
 intros.n:t
abs (- n) == abs n destruct_max n.n:t
H:0 <= n
abs (- n) == n
n:t
H:n <= 0
abs (- n) == - n
 rewrite (abs_neq (-n)), opp_involutive.n:t
H:0 <= n
n == n
n:t
H:0 <= n
- n <= 0
n:t
H:n <= 0
abs (- n) == - n reflexivity.n:t
H:0 <= n
- n <= 0
n:t
H:n <= 0
abs (- n) == - n
 now rewrite opp_nonpos_nonneg.n:t
H:n <= 0
abs (- n) == - n
 rewrite (abs_eq (-n)).n:t
H:n <= 0
- n == - n
n:t
H:n <= 0
0 <= - n reflexivity.n:t
H:n <= 0
0 <= - n
 now rewrite opp_nonneg_nonpos.
Qed.

Lemma abs_0 : abs 0 == 0.abs 0 == 0
Proof.abs 0 == 0
 apply abs_eq.0 <= 0 apply le_refl.
Qed.

Lemma abs_0_iff : forall n, abs n == 0 <-> n==0.forall n : t, abs n == 0 <-> n == 0
Proof.forall n : t, abs n == 0 <-> n == 0
 split.n:t
abs n == 0 -> n == 0
n:t
n == 0 -> abs n == 0 destruct_max n; auto.n:t
H:n <= 0
- n == 0 -> n == 0
n:t
n == 0 -> abs n == 0
 now rewrite eq_opp_l, opp_0.n:t
n == 0 -> abs n == 0
 intros EQ; rewrite EQ.n:t
EQ:n == 0
abs 0 == 0 rewrite abs_eq; auto using eq_refl, le_refl.
Qed.

Lemma abs_pos : forall n, 0 < abs n <-> n~=0.forall n : t, 0 < abs n <-> n ~= 0
Proof.forall n : t, 0 < abs n <-> n ~= 0
 intros.n:t
0 < abs n <-> n ~= 0 rewrite <- abs_0_iff.n:t
0 < abs n <-> abs n ~= 0 split; [intros LT| intros NEQ].n:t
LT:0 < abs n
abs n ~= 0
n:t
NEQ:abs n ~= 0
0 < abs n
 intro EQ.n:t
LT:0 < abs n
EQ:abs n == 0
False
n:t
NEQ:abs n ~= 0
0 < abs n rewrite EQ in LT.n:t
LT:0 < 0
EQ:abs n == 0
False
n:t
NEQ:abs n ~= 0
0 < abs n now elim (lt_irrefl 0).n:t
NEQ:abs n ~= 0
0 < abs n
 assert (LE : 0 <= abs n) by apply abs_nonneg.n:t
NEQ:abs n ~= 0
LE:0 <= abs n
0 < abs n
 rewrite lt_eq_cases in LE; destruct LE; auto.n:t
NEQ:abs n ~= 0
H:0 == abs n
0 < abs n
 elim NEQ; auto with relations.
Qed.

Lemma abs_eq_or_opp : forall n, abs n == n \/ abs n == -n.forall n : t, abs n == n \/ abs n == - n
Proof.forall n : t, abs n == n \/ abs n == - n
 intros.n:t
abs n == n \/ abs n == - n destruct_max n; auto with relations.
Qed.

Lemma abs_or_opp_abs : forall n, n == abs n \/ n == - abs n.forall n : t, n == abs n \/ n == - abs n
Proof.forall n : t, n == abs n \/ n == - abs n
 intros.n:t
n == abs n \/ n == - abs n destruct_max n; rewrite ? opp_involutive; auto with relations.
Qed.

Lemma abs_involutive : forall n, abs (abs n) == abs n.forall n : t, abs (abs n) == abs n
Proof.forall n : t, abs (abs n) == abs n
 intros.n:t
abs (abs n) == abs n apply abs_eq.n:t
0 <= abs n apply abs_nonneg.
Qed.

Lemma abs_spec : forall n,
  (0 <= n /\ abs n == n) \/ (n < 0 /\ abs n == -n).forall n : t,
0 <= n /\ abs n == n \/ n < 0 /\ abs n == - n
Proof.forall n : t,
0 <= n /\ abs n == n \/ n < 0 /\ abs n == - n
 intros.n:t
0 <= n /\ abs n == n \/ n < 0 /\ abs n == - n destruct (le_gt_cases 0 n).n:t
H:0 <= n
0 <= n /\ abs n == n \/ n < 0 /\ abs n == - n
n:t
H:n < 0
0 <= n /\ abs n == n \/ n < 0 /\ abs n == - n
 left; split; auto.n:t
H:0 <= n
abs n == n
n:t
H:n < 0
0 <= n /\ abs n == n \/ n < 0 /\ abs n == - n now apply abs_eq.n:t
H:n < 0
0 <= n /\ abs n == n \/ n < 0 /\ abs n == - n
 right; split; auto.n:t
H:n < 0
abs n == - n apply abs_neq.n:t
H:n < 0
n <= 0 now apply lt_le_incl.
Qed.

Lemma abs_case_strong :
  forall (P:t->Prop) n, Proper (eq==>iff) P ->
    (0<=n -> P n) -> (n<=0 -> P (-n)) -> P (abs n).forall (P : t -> Prop) (n : t),
Proper (eq ==> iff) P ->
(0 <= n -> P n) -> (n <= 0 -> P (- n)) -> P (abs n)
Proof.forall (P : t -> Prop) (n : t),
Proper (eq ==> iff) P ->
(0 <= n -> P n) -> (n <= 0 -> P (- n)) -> P (abs n)
 intros.P:t -> Prop
n:t
H:Proper (eq ==> iff) P
H0:0 <= n -> P n
H1:n <= 0 -> P (- n)
P (abs n) destruct_max n; auto.
Qed.

Lemma abs_case : forall (P:t->Prop) n, Proper (eq==>iff) P ->
 P n -> P (-n) -> P (abs n).forall (P : t -> Prop) (n : t),
Proper (eq ==> iff) P -> P n -> P (- n) -> P (abs n)
Proof.forall (P : t -> Prop) (n : t),
Proper (eq ==> iff) P -> P n -> P (- n) -> P (abs n) intros.P:t -> Prop
n:t
H:Proper (eq ==> iff) P
H0:P n
H1:P (- n)
P (abs n) now apply abs_case_strong. Qed.

Lemma abs_eq_cases : forall n m, abs n == abs m -> n == m \/ n == - m.forall n m : t, abs n == abs m -> n == m \/ n == - m
Proof.forall n m : t, abs n == abs m -> n == m \/ n == - m
 intros n m EQ.n, m:t
EQ:abs n == abs m
n == m \/ n == - m destruct (abs_or_opp_abs n) as [EQn|EQn].n, m:t
EQ:abs n == abs m
EQn:n == abs n
n == m \/ n == - m
n, m:t
EQ:abs n == abs m
EQn:n == - abs n
n == m \/ n == - m
 rewrite EQn, EQ.n, m:t
EQ:abs n == abs m
EQn:n == abs n
abs m == m \/ abs m == - m
n, m:t
EQ:abs n == abs m
EQn:n == - abs n
n == m \/ n == - m apply abs_eq_or_opp.n, m:t
EQ:abs n == abs m
EQn:n == - abs n
n == m \/ n == - m
 rewrite EQn, EQ, opp_inj_wd, eq_opp_l, or_comm.n, m:t
EQ:abs n == abs m
EQn:n == - abs n
abs m == m \/ abs m == - m apply abs_eq_or_opp.
Qed.

Lemma abs_lt : forall a b, abs a < b <-> -b < a < b.forall a b : t, abs a < b <-> - b < a < b
Proof.forall a b : t, abs a < b <-> - b < a < b
 intros a b.a, b:t
abs a < b <-> - b < a < b
 destruct (abs_spec a) as [[LE EQ]|[LT EQ]]; rewrite EQ; clear EQ.a, b:t
LE:0 <= a
a < b <-> - b < a < b
a, b:t
LT:a < 0
- a < b <-> - b < a < b
 split; try split; try destruct 1; try order.a, b:t
LE:0 <= a
H:a < b
- b < a
a, b:t
LT:a < 0
- a < b <-> - b < a < b
 apply lt_le_trans with 0; trivial.a, b:t
LE:0 <= a
H:a < b
- b < 0
a, b:t
LT:a < 0
- a < b <-> - b < a < b apply opp_neg_pos; order.a, b:t
LT:a < 0
- a < b <-> - b < a < b
 rewrite opp_lt_mono, opp_involutive.a, b:t
LT:a < 0
- b < a <-> - b < a < b
 split; try split; try destruct 1; try order.a, b:t
LT:a < 0
H:- b < a
a < b
 apply lt_le_trans with 0; trivial.a, b:t
LT:a < 0
H:- b < a
0 <= b apply opp_nonpos_nonneg; order.
Qed.

Lemma abs_le : forall a b, abs a <= b <-> -b <= a <= b.forall a b : t, abs a <= b <-> - b <= a <= b
Proof.forall a b : t, abs a <= b <-> - b <= a <= b
 intros a b.a, b:t
abs a <= b <-> - b <= a <= b
 destruct (abs_spec a) as [[LE EQ]|[LT EQ]]; rewrite EQ; clear EQ.a, b:t
LE:0 <= a
a <= b <-> - b <= a <= b
a, b:t
LT:a < 0
- a <= b <-> - b <= a <= b
 split; try split; try destruct 1; try order.a, b:t
LE:0 <= a
H:a <= b
- b <= a
a, b:t
LT:a < 0
- a <= b <-> - b <= a <= b
 apply le_trans with 0; trivial.a, b:t
LE:0 <= a
H:a <= b
- b <= 0
a, b:t
LT:a < 0
- a <= b <-> - b <= a <= b apply opp_nonpos_nonneg; order.a, b:t
LT:a < 0
- a <= b <-> - b <= a <= b
 rewrite opp_le_mono, opp_involutive.a, b:t
LT:a < 0
- b <= a <-> - b <= a <= b
 split; try split; try destruct 1; try order.a, b:t
LT:a < 0
H:- b <= a
a <= b
 apply le_trans with 0.a, b:t
LT:a < 0
H:- b <= a
a <= 0
a, b:t
LT:a < 0
H:- b <= a
0 <= b order.a, b:t
LT:a < 0
H:- b <= a
0 <= b apply opp_nonpos_nonneg; order.
Qed.

Triangular inequality

Lemma abs_triangle : forall n m, abs (n + m) <= abs n + abs m.forall n m : t, abs (n + m) <= abs n + abs m
Proof.forall n m : t, abs (n + m) <= abs n + abs m
 intros.n, m:t
abs (n + m) <= abs n + abs m destruct_max n; destruct_max m.n, m:t
H:0 <= n
H0:0 <= m
abs (n + m) <= n + m
n, m:t
H:0 <= n
H0:m <= 0
abs (n + m) <= n + - m
n, m:t
H:n <= 0
H0:0 <= m
abs (n + m) <= - n + m
n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m
 rewrite abs_eq.n, m:t
H:0 <= n
H0:0 <= m
n + m <= n + m
n, m:t
H:0 <= n
H0:0 <= m
0 <= n + m
n, m:t
H:0 <= n
H0:m <= 0
abs (n + m) <= n + - m
n, m:t
H:n <= 0
H0:0 <= m
abs (n + m) <= - n + m
n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m apply le_refl.n, m:t
H:0 <= n
H0:0 <= m
0 <= n + m
n, m:t
H:0 <= n
H0:m <= 0
abs (n + m) <= n + - m
n, m:t
H:n <= 0
H0:0 <= m
abs (n + m) <= - n + m
n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m now apply add_nonneg_nonneg.n, m:t
H:0 <= n
H0:m <= 0
abs (n + m) <= n + - m
n, m:t
H:n <= 0
H0:0 <= m
abs (n + m) <= - n + m
n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m
 destruct_max (n+m); try rewrite opp_add_distr;
  apply add_le_mono_l || apply add_le_mono_r.n, m:t
H:0 <= n
H0:m <= 0
H1:0 <= n + m
m <= - m
n, m:t
H:0 <= n
H0:m <= 0
H1:n + m <= 0
- n <= n
n, m:t
H:n <= 0
H0:0 <= m
abs (n + m) <= - n + m
n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m
 apply le_trans with 0; auto.n, m:t
H:0 <= n
H0:m <= 0
H1:0 <= n + m
0 <= - m
n, m:t
H:0 <= n
H0:m <= 0
H1:n + m <= 0
- n <= n
n, m:t
H:n <= 0
H0:0 <= m
abs (n + m) <= - n + m
n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m now rewrite opp_nonneg_nonpos.n, m:t
H:0 <= n
H0:m <= 0
H1:n + m <= 0
- n <= n
n, m:t
H:n <= 0
H0:0 <= m
abs (n + m) <= - n + m
n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m
 apply le_trans with 0; auto.n, m:t
H:0 <= n
H0:m <= 0
H1:n + m <= 0
- n <= 0
n, m:t
H:n <= 0
H0:0 <= m
abs (n + m) <= - n + m
n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m now rewrite opp_nonpos_nonneg.n, m:t
H:n <= 0
H0:0 <= m
abs (n + m) <= - n + m
n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m
 destruct_max (n+m); try rewrite opp_add_distr;
  apply add_le_mono_l || apply add_le_mono_r.n, m:t
H:n <= 0
H0:0 <= m
H1:0 <= n + m
n <= - n
n, m:t
H:n <= 0
H0:0 <= m
H1:n + m <= 0
- m <= m
n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m
 apply le_trans with 0; auto.n, m:t
H:n <= 0
H0:0 <= m
H1:0 <= n + m
0 <= - n
n, m:t
H:n <= 0
H0:0 <= m
H1:n + m <= 0
- m <= m
n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m now rewrite opp_nonneg_nonpos.n, m:t
H:n <= 0
H0:0 <= m
H1:n + m <= 0
- m <= m
n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m
 apply le_trans with 0; auto.n, m:t
H:n <= 0
H0:0 <= m
H1:n + m <= 0
- m <= 0
n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m now rewrite opp_nonpos_nonneg.n, m:t
H:n <= 0
H0:m <= 0
abs (n + m) <= - n + - m
 rewrite abs_neq, opp_add_distr.n, m:t
H:n <= 0
H0:m <= 0
- n + - m <= - n + - m
n, m:t
H:n <= 0
H0:m <= 0
n + m <= 0 apply le_refl.n, m:t
H:n <= 0
H0:m <= 0
n + m <= 0
 now apply add_nonpos_nonpos.
Qed.

Lemma abs_sub_triangle : forall n m, abs n - abs m <= abs (n-m).forall n m : t, abs n - abs m <= abs (n - m)
Proof.forall n m : t, abs n - abs m <= abs (n - m)
 intros.n, m:t
abs n - abs m <= abs (n - m)
 rewrite le_sub_le_add_l, add_comm.n, m:t
abs n <= abs (n - m) + abs m
 rewrite <- (sub_simpl_r n m) at 1.n, m:t
abs (n - m + m) <= abs (n - m) + abs m
 apply abs_triangle.
Qed.

Absolute value and multiplication

Lemma abs_mul : forall n m, abs (n * m) == abs n * abs m.forall n m : t, abs (n * m) == abs n * abs m
Proof.forall n m : t, abs (n * m) == abs n * abs m
 assert (H : forall n m, 0<=n -> abs (n*m) == n * abs m).forall n m : t, 0 <= n -> abs (n * m) == n * abs m
H:forall n m : t, 0 <= n -> abs (n * m) == n * abs m
forall n m : t, abs (n * m) == abs n * abs m
  intros.n, m:t
H:0 <= n
abs (n * m) == n * abs m
H:forall n m : t, 0 <= n -> abs (n * m) == n * abs m
forall n m : t, abs (n * m) == abs n * abs m destruct_max m.n, m:t
H:0 <= n
H0:0 <= m
abs (n * m) == n * m
n, m:t
H:0 <= n
H0:m <= 0
abs (n * m) == n * - m
H:forall n m : t, 0 <= n -> abs (n * m) == n * abs m
forall n m : t, abs (n * m) == abs n * abs m
  rewrite abs_eq.n, m:t
H:0 <= n
H0:0 <= m
n * m == n * m
n, m:t
H:0 <= n
H0:0 <= m
0 <= n * m
n, m:t
H:0 <= n
H0:m <= 0
abs (n * m) == n * - m
H:forall n m : t, 0 <= n -> abs (n * m) == n * abs m
forall n m : t, abs (n * m) == abs n * abs m apply eq_refl.n, m:t
H:0 <= n
H0:0 <= m
0 <= n * m
n, m:t
H:0 <= n
H0:m <= 0
abs (n * m) == n * - m
H:forall n m : t, 0 <= n -> abs (n * m) == n * abs m
forall n m : t, abs (n * m) == abs n * abs m now apply mul_nonneg_nonneg.n, m:t
H:0 <= n
H0:m <= 0
abs (n * m) == n * - m
H:forall n m : t, 0 <= n -> abs (n * m) == n * abs m
forall n m : t, abs (n * m) == abs n * abs m
  rewrite abs_neq, mul_opp_r.n, m:t
H:0 <= n
H0:m <= 0
- (n * m) == - (n * m)
n, m:t
H:0 <= n
H0:m <= 0
n * m <= 0
H:forall n m : t, 0 <= n -> abs (n * m) == n * abs m
forall n m : t, abs (n * m) == abs n * abs m reflexivity.n, m:t
H:0 <= n
H0:m <= 0
n * m <= 0
H:forall n m : t, 0 <= n -> abs (n * m) == n * abs m
forall n m : t, abs (n * m) == abs n * abs m now apply mul_nonneg_nonpos .H:forall n m : t, 0 <= n -> abs (n * m) == n * abs m
forall n m : t, abs (n * m) == abs n * abs m
 intros.H:forall n0 m0 : t,
0 <= n0 -> abs (n0 * m0) == n0 * abs m0
n, m:t
abs (n * m) == abs n * abs m destruct_max n.H:forall n0 m0 : t,
0 <= n0 -> abs (n0 * m0) == n0 * abs m0
n, m:t
H0:0 <= n
abs (n * m) == n * abs m
H:forall n0 m0 : t,
0 <= n0 -> abs (n0 * m0) == n0 * abs m0
n, m:t
H0:n <= 0
abs (n * m) == - n * abs m now apply H.H:forall n0 m0 : t,
0 <= n0 -> abs (n0 * m0) == n0 * abs m0
n, m:t
H0:n <= 0
abs (n * m) == - n * abs m
 rewrite <- mul_opp_opp, H, abs_opp.H:forall n0 m0 : t,
0 <= n0 -> abs (n0 * m0) == n0 * abs m0
n, m:t
H0:n <= 0
- n * abs m == - n * abs m
H:forall n0 m0 : t,
0 <= n0 -> abs (n0 * m0) == n0 * abs m0
n, m:t
H0:n <= 0
0 <= - n reflexivity.H:forall n0 m0 : t,
0 <= n0 -> abs (n0 * m0) == n0 * abs m0
n, m:t
H0:n <= 0
0 <= - n
 now apply opp_nonneg_nonpos.
Qed.

Lemma abs_square : forall n, abs n * abs n == n * n.forall n : t, abs n * abs n == n * n
Proof.forall n : t, abs n * abs n == n * n
 intros.n:t
abs n * abs n == n * n rewrite <- abs_mul.n:t
abs (n * n) == n * n apply abs_eq.n:t
0 <= n * n apply le_0_square.
Qed.

Some results about the sign function.

Ltac destruct_sgn n :=
 let LT := fresh "LT" in
 let EQ := fresh "EQ" in
 let GT := fresh "GT" in
 destruct (lt_trichotomy 0 n) as [LT|[EQ|GT]];
 [rewrite (sgn_pos n) by auto|
  rewrite (sgn_null n) by auto with relations|
  rewrite (sgn_neg n) by auto].

Instance sgn_wd : Proper (eq==>eq) sgn.Proper (eq ==> eq) sgn
Proof.Proper (eq ==> eq) sgn
 intros x y Hxy.x, y:t
Hxy:x == y
sgn x == sgn y destruct_sgn x.x, y:t
Hxy:x == y
LT:0 < x
1 == sgn y
x, y:t
Hxy:x == y
EQ:0 == x
0 == sgn y
x, y:t
Hxy:x == y
GT:x < 0
-1 == sgn y
 rewrite sgn_pos; auto with relations.x, y:t
Hxy:x == y
LT:0 < x
0 < y
x, y:t
Hxy:x == y
EQ:0 == x
0 == sgn y
x, y:t
Hxy:x == y
GT:x < 0
-1 == sgn y rewrite <- Hxy; auto.x, y:t
Hxy:x == y
EQ:0 == x
0 == sgn y
x, y:t
Hxy:x == y
GT:x < 0
-1 == sgn y
 rewrite sgn_null; auto with relations.x, y:t
Hxy:x == y
EQ:0 == x
y == 0
x, y:t
Hxy:x == y
GT:x < 0
-1 == sgn y rewrite <- Hxy; auto with relations.x, y:t
Hxy:x == y
GT:x < 0
-1 == sgn y
 rewrite sgn_neg; auto with relations.x, y:t
Hxy:x == y
GT:x < 0
y < 0 rewrite <- Hxy; auto.
Qed.

Lemma sgn_spec : forall n,
  0 < n /\ sgn n == 1 \/
  0 == n /\ sgn n == 0 \/
  0 > n /\ sgn n == -1.forall n : t,
0 < n /\ sgn n == 1 \/
0 == n /\ sgn n == 0 \/ n < 0 /\ sgn n == -1
Proof.forall n : t,
0 < n /\ sgn n == 1 \/
0 == n /\ sgn n == 0 \/ n < 0 /\ sgn n == -1
 intros n.n:t
0 < n /\ sgn n == 1 \/
0 == n /\ sgn n == 0 \/ n < 0 /\ sgn n == -1
 destruct_sgn n; [left|right;left|right;right]; auto with relations.
Qed.

Lemma sgn_0 : sgn 0 == 0.sgn 0 == 0
Proof.sgn 0 == 0
 now apply sgn_null.
Qed.

Lemma sgn_pos_iff : forall n, sgn n == 1 <-> 0<n.forall n : t, sgn n == 1 <-> 0 < n
Proof.forall n : t, sgn n == 1 <-> 0 < n
 split; try apply sgn_pos.n:t
sgn n == 1 -> 0 < n destruct_sgn n; auto.n:t
EQ:0 == n
0 == 1 -> 0 < n
n:t
GT:n < 0
-1 == 1 -> 0 < n
 intros.n:t
EQ:0 == n
H:0 == 1
0 < n
n:t
GT:n < 0
-1 == 1 -> 0 < n elim (lt_neq 0 1); auto.n:t
EQ:0 == n
H:0 == 1
0 < 1
n:t
GT:n < 0
-1 == 1 -> 0 < n apply lt_0_1.n:t
GT:n < 0
-1 == 1 -> 0 < n
 intros.n:t
GT:n < 0
H:-1 == 1
0 < n elim (lt_neq (-1) 1); auto.n:t
GT:n < 0
H:-1 == 1
-1 < 1
 apply lt_trans with 0.n:t
GT:n < 0
H:-1 == 1
-1 < 0
n:t
GT:n < 0
H:-1 == 1
0 < 1 rewrite opp_neg_pos.n:t
GT:n < 0
H:-1 == 1
0 < 1
n:t
GT:n < 0
H:-1 == 1
0 < 1 apply lt_0_1.n:t
GT:n < 0
H:-1 == 1
0 < 1 apply lt_0_1.
Qed.

Lemma sgn_null_iff : forall n, sgn n == 0 <-> n==0.forall n : t, sgn n == 0 <-> n == 0
Proof.forall n : t, sgn n == 0 <-> n == 0
 split; try apply sgn_null.n:t
sgn n == 0 -> n == 0 destruct_sgn n; auto with relations.n:t
LT:0 < n
1 == 0 -> n == 0
n:t
GT:n < 0
-1 == 0 -> n == 0
 intros.n:t
LT:0 < n
H:1 == 0
n == 0
n:t
GT:n < 0
-1 == 0 -> n == 0 elim (lt_neq 0 1); auto with relations.n:t
LT:0 < n
H:1 == 0
0 < 1
n:t
GT:n < 0
-1 == 0 -> n == 0 apply lt_0_1.n:t
GT:n < 0
-1 == 0 -> n == 0
 intros.n:t
GT:n < 0
H:-1 == 0
n == 0 elim (lt_neq (-1) 0); auto.n:t
GT:n < 0
H:-1 == 0
-1 < 0
 rewrite opp_neg_pos.n:t
GT:n < 0
H:-1 == 0
0 < 1 apply lt_0_1.
Qed.

Lemma sgn_neg_iff : forall n, sgn n == -1 <-> n<0.forall n : t, sgn n == -1 <-> n < 0
Proof.forall n : t, sgn n == -1 <-> n < 0
 split; try apply sgn_neg.n:t
sgn n == -1 -> n < 0 destruct_sgn n; auto with relations.n:t
LT:0 < n
1 == -1 -> n < 0
n:t
EQ:0 == n
0 == -1 -> n < 0
 intros.n:t
LT:0 < n
H:1 == -1
n < 0
n:t
EQ:0 == n
0 == -1 -> n < 0 elim (lt_neq (-1) 1); auto with relations.n:t
LT:0 < n
H:1 == -1
-1 < 1
n:t
EQ:0 == n
0 == -1 -> n < 0
 apply lt_trans with 0.n:t
LT:0 < n
H:1 == -1
-1 < 0
n:t
LT:0 < n
H:1 == -1
0 < 1
n:t
EQ:0 == n
0 == -1 -> n < 0 rewrite opp_neg_pos.n:t
LT:0 < n
H:1 == -1
0 < 1
n:t
LT:0 < n
H:1 == -1
0 < 1
n:t
EQ:0 == n
0 == -1 -> n < 0 apply lt_0_1.n:t
LT:0 < n
H:1 == -1
0 < 1
n:t
EQ:0 == n
0 == -1 -> n < 0 apply lt_0_1.n:t
EQ:0 == n
0 == -1 -> n < 0
 intros.n:t
EQ:0 == n
H:0 == -1
n < 0 elim (lt_neq (-1) 0); auto with relations.n:t
EQ:0 == n
H:0 == -1
-1 < 0
 rewrite opp_neg_pos.n:t
EQ:0 == n
H:0 == -1
0 < 1 apply lt_0_1.
Qed.

Lemma sgn_opp : forall n, sgn (-n) == - sgn n.forall n : t, sgn (- n) == - sgn n
Proof.forall n : t, sgn (- n) == - sgn n
 intros.n:t
sgn (- n) == - sgn n destruct_sgn n.n:t
LT:0 < n
sgn (- n) == -1
n:t
EQ:0 == n
sgn (- n) == - 0
n:t
GT:n < 0
sgn (- n) == - -1
 apply sgn_neg.n:t
LT:0 < n
- n < 0
n:t
EQ:0 == n
sgn (- n) == - 0
n:t
GT:n < 0
sgn (- n) == - -1 now rewrite opp_neg_pos.n:t
EQ:0 == n
sgn (- n) == - 0
n:t
GT:n < 0
sgn (- n) == - -1
 setoid_replace n with 0 by auto with relations.n:t
EQ:0 == n
sgn (- 0) == - 0
n:t
GT:n < 0
sgn (- n) == - -1
  rewrite opp_0.n:t
EQ:0 == n
sgn 0 == 0
n:t
GT:n < 0
sgn (- n) == - -1 apply sgn_0.n:t
GT:n < 0
sgn (- n) == - -1
 rewrite opp_involutive.n:t
GT:n < 0
sgn (- n) == 1 apply sgn_pos.n:t
GT:n < 0
0 < - n now rewrite opp_pos_neg.
Qed.

Lemma sgn_nonneg : forall n, 0 <= sgn n <-> 0 <= n.forall n : t, 0 <= sgn n <-> 0 <= n
Proof.forall n : t, 0 <= sgn n <-> 0 <= n
 split.n:t
0 <= sgn n -> 0 <= n
n:t
0 <= n -> 0 <= sgn n
 destruct_sgn n; intros.n:t
LT:0 < n
H:0 <= 1
0 <= n
n:t
EQ:0 == n
H:0 <= 0
0 <= n
n:t
GT:n < 0
H:0 <= -1
0 <= n
n:t
0 <= n -> 0 <= sgn n
 now apply lt_le_incl.n:t
EQ:0 == n
H:0 <= 0
0 <= n
n:t
GT:n < 0
H:0 <= -1
0 <= n
n:t
0 <= n -> 0 <= sgn n
 order.n:t
GT:n < 0
H:0 <= -1
0 <= n
n:t
0 <= n -> 0 <= sgn n
 elim (lt_irrefl 0).n:t
GT:n < 0
H:0 <= -1
0 < 0
n:t
0 <= n -> 0 <= sgn n apply lt_le_trans with 1; auto using lt_0_1.n:t
GT:n < 0
H:0 <= -1
1 <= 0
n:t
0 <= n -> 0 <= sgn n
  now rewrite <- opp_nonneg_nonpos.n:t
0 <= n -> 0 <= sgn n
 rewrite lt_eq_cases; destruct 1.n:t
H:0 < n
0 <= sgn n
n:t
H:0 == n
0 <= sgn n
 rewrite sgn_pos by auto.n:t
H:0 < n
0 <= 1
n:t
H:0 == n
0 <= sgn n apply lt_le_incl, lt_0_1.n:t
H:0 == n
0 <= sgn n
 rewrite sgn_null by auto with relations.n:t
H:0 == n
0 <= 0 apply le_refl.
Qed.

Lemma sgn_nonpos : forall n, sgn n <= 0 <-> n <= 0.forall n : t, sgn n <= 0 <-> n <= 0
Proof.forall n : t, sgn n <= 0 <-> n <= 0
 intros.n:t
sgn n <= 0 <-> n <= 0 rewrite <- 2 opp_nonneg_nonpos, <- sgn_opp.n:t
0 <= sgn (- n) <-> 0 <= - n apply sgn_nonneg.
Qed.

Lemma sgn_mul : forall n m, sgn (n*m) == sgn n * sgn m.forall n m : t, sgn (n * m) == sgn n * sgn m
Proof.forall n m : t, sgn (n * m) == sgn n * sgn m
 intros.n, m:t
sgn (n * m) == sgn n * sgn m destruct_sgn n; nzsimpl.n, m:t
LT:0 < n
sgn (n * m) == sgn m
n, m:t
EQ:0 == n
sgn (n * m) == 0
n, m:t
GT:n < 0
sgn (n * m) == -1 * sgn m
 destruct_sgn m.n, m:t
LT:0 < n
LT0:0 < m
sgn (n * m) == 1
n, m:t
LT:0 < n
EQ:0 == m
sgn (n * m) == 0
n, m:t
LT:0 < n
GT:m < 0
sgn (n * m) == -1
n, m:t
EQ:0 == n
sgn (n * m) == 0
n, m:t
GT:n < 0
sgn (n * m) == -1 * sgn m
  apply sgn_pos.n, m:t
LT:0 < n
LT0:0 < m
0 < n * m
n, m:t
LT:0 < n
EQ:0 == m
sgn (n * m) == 0
n, m:t
LT:0 < n
GT:m < 0
sgn (n * m) == -1
n, m:t
EQ:0 == n
sgn (n * m) == 0
n, m:t
GT:n < 0
sgn (n * m) == -1 * sgn m now apply mul_pos_pos.n, m:t
LT:0 < n
EQ:0 == m
sgn (n * m) == 0
n, m:t
LT:0 < n
GT:m < 0
sgn (n * m) == -1
n, m:t
EQ:0 == n
sgn (n * m) == 0
n, m:t
GT:n < 0
sgn (n * m) == -1 * sgn m
  apply sgn_null.n, m:t
LT:0 < n
EQ:0 == m
n * m == 0
n, m:t
LT:0 < n
GT:m < 0
sgn (n * m) == -1
n, m:t
EQ:0 == n
sgn (n * m) == 0
n, m:t
GT:n < 0
sgn (n * m) == -1 * sgn m rewrite eq_mul_0; auto with relations.n, m:t
LT:0 < n
GT:m < 0
sgn (n * m) == -1
n, m:t
EQ:0 == n
sgn (n * m) == 0
n, m:t
GT:n < 0
sgn (n * m) == -1 * sgn m
  apply sgn_neg.n, m:t
LT:0 < n
GT:m < 0
n * m < 0
n, m:t
EQ:0 == n
sgn (n * m) == 0
n, m:t
GT:n < 0
sgn (n * m) == -1 * sgn m now apply mul_pos_neg.n, m:t
EQ:0 == n
sgn (n * m) == 0
n, m:t
GT:n < 0
sgn (n * m) == -1 * sgn m
 apply sgn_null.n, m:t
EQ:0 == n
n * m == 0
n, m:t
GT:n < 0
sgn (n * m) == -1 * sgn m rewrite eq_mul_0; auto with relations.n, m:t
GT:n < 0
sgn (n * m) == -1 * sgn m
 destruct_sgn m; try rewrite mul_opp_opp; nzsimpl.n, m:t
GT:n < 0
LT:0 < m
sgn (n * m) == -1
n, m:t
GT:n < 0
EQ:0 == m
sgn (n * m) == 0
n, m:t
GT:n < 0
GT0:m < 0
sgn (n * m) == 1
  apply sgn_neg.n, m:t
GT:n < 0
LT:0 < m
n * m < 0
n, m:t
GT:n < 0
EQ:0 == m
sgn (n * m) == 0
n, m:t
GT:n < 0
GT0:m < 0
sgn (n * m) == 1 now apply mul_neg_pos.n, m:t
GT:n < 0
EQ:0 == m
sgn (n * m) == 0
n, m:t
GT:n < 0
GT0:m < 0
sgn (n * m) == 1
  apply sgn_null.n, m:t
GT:n < 0
EQ:0 == m
n * m == 0
n, m:t
GT:n < 0
GT0:m < 0
sgn (n * m) == 1 rewrite eq_mul_0; auto with relations.n, m:t
GT:n < 0
GT0:m < 0
sgn (n * m) == 1
  apply sgn_pos.n, m:t
GT:n < 0
GT0:m < 0
0 < n * m now apply mul_neg_neg.
Qed.

Lemma sgn_abs : forall n, n * sgn n == abs n.forall n : t, n * sgn n == abs n
Proof.forall n : t, n * sgn n == abs n
 intros.n:t
n * sgn n == abs n symmetry.n:t
abs n == n * sgn n
 destruct_sgn n; try rewrite mul_opp_r; nzsimpl.n:t
LT:0 < n
abs n == n
n:t
EQ:0 == n
abs n == 0
n:t
GT:n < 0
abs n == - n
 apply abs_eq.n:t
LT:0 < n
0 <= n
n:t
EQ:0 == n
abs n == 0
n:t
GT:n < 0
abs n == - n now apply lt_le_incl.n:t
EQ:0 == n
abs n == 0
n:t
GT:n < 0
abs n == - n
 rewrite abs_0_iff; auto with relations.n:t
GT:n < 0
abs n == - n
 apply abs_neq.n:t
GT:n < 0
n <= 0 now apply lt_le_incl.
Qed.

Lemma abs_sgn : forall n, abs n * sgn n == n.forall n : t, abs n * sgn n == n
Proof.forall n : t, abs n * sgn n == n
 intros.n:t
abs n * sgn n == n
 destruct_sgn n; try rewrite mul_opp_r; nzsimpl; auto.n:t
LT:0 < n
abs n == n
n:t
GT:n < 0
- abs n == n
 apply abs_eq.n:t
LT:0 < n
0 <= n
n:t
GT:n < 0
- abs n == n now apply lt_le_incl.n:t
GT:n < 0
- abs n == n
 rewrite eq_opp_l.n:t
GT:n < 0
abs n == - n apply abs_neq.n:t
GT:n < 0
n <= 0 now apply lt_le_incl.
Qed.

Lemma sgn_sgn : forall x, sgn (sgn x) == sgn x.forall x : t, sgn (sgn x) == sgn x
Proof.forall x : t, sgn (sgn x) == sgn x
 intros.x:t
sgn (sgn x) == sgn x
 destruct (sgn_spec x) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ.x:t
LT:0 < x
EQ:sgn x == 1
sgn 1 == 1
x:t
EQ':0 == x
EQ:sgn x == 0
sgn 0 == 0
x:t
LT:x < 0
EQ:sgn x == -1
sgn (-1) == -1
 apply sgn_pos, lt_0_1.x:t
EQ':0 == x
EQ:sgn x == 0
sgn 0 == 0
x:t
LT:x < 0
EQ:sgn x == -1
sgn (-1) == -1
 now apply sgn_null.x:t
LT:x < 0
EQ:sgn x == -1
sgn (-1) == -1
 apply sgn_neg.x:t
LT:x < 0
EQ:sgn x == -1
-1 < 0 rewrite opp_neg_pos.x:t
LT:x < 0
EQ:sgn x == -1
0 < 1 apply lt_0_1.
Qed.

End ZSgnAbsProp.