Library Coq.Numbers.Integer.Abstract.ZSgnAbs
An axiomatization of abs.
Since we already have max, we could have defined abs.
An Axiomatization of sgn.
We can deduce a sgn function from a compare function
Module Type ZDecAxiomsSig :=
ZAxiomsSig <+
HasCompare.
Module Type ZDecAxiomsSig' :=
ZAxiomsSig' <+
HasCompare.
Module Type GenericSgn (
Import Z :
ZDecAxiomsSig')
(
Import ZP :
ZMulOrderPropFunct 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.
Lemma sgn_pos :
forall n, 0
<n ->
sgn n == 1.
Lemma sgn_neg :
forall n,
n<0 ->
sgn n == -(1).
End GenericSgn.
Module Type ZAxiomsExtSig :=
ZAxiomsSig <+
HasAbs <+
HasSgn.
Module Type ZAxiomsExtSig' :=
ZAxiomsSig' <+
HasAbs <+
HasSgn.
Module Type ZSgnAbsPropSig (
Import Z :
ZAxiomsExtSig')
(
Import ZP :
ZMulOrderPropFunct 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.
Lemma abs_max :
forall n,
abs n == max n (
-n).
Lemma abs_neq' :
forall n, 0
<=-n ->
abs n == -n.
Lemma abs_nonneg :
forall n, 0
<= abs n.
Lemma abs_eq_iff :
forall n,
abs n == n <-> 0
<=n.
Lemma abs_neq_iff :
forall n,
abs n == -n <-> n<=0.
Lemma abs_opp :
forall n,
abs (
-n)
== abs n.
Lemma abs_0 :
abs 0
== 0.
Lemma abs_0_iff :
forall n,
abs n == 0
<-> n==0.
Lemma abs_pos :
forall n, 0
< abs n <-> n~=0.
Lemma abs_eq_or_opp :
forall n,
abs n == n \/ abs n == -n.
Lemma abs_or_opp_abs :
forall n,
n == abs n \/ n == - abs n.
Lemma abs_involutive :
forall n,
abs (
abs n)
== abs n.
Lemma abs_spec :
forall n,
(0
<= n /\ abs n == n) \/ (n < 0
/\ abs n == -n).
Lemma abs_case_strong :
forall (
P:
t->
Prop)
n,
Proper (
eq==>iff)
P ->
(0
<=n ->
P n) -> (
n<=0 ->
P (
-n)) ->
P (
abs n).
Lemma abs_case :
forall (
P:
t->
Prop)
n,
Proper (
eq==>iff)
P ->
P n ->
P (
-n) ->
P (
abs n).
Lemma abs_eq_cases :
forall n m,
abs n == abs m ->
n == m \/ n == - m.
Triangular inequality
Absolute value and multiplication
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.
Lemma sgn_spec :
forall n,
0
< n /\ sgn n == 1
\/
0
== n /\ sgn n == 0
\/
0
> n /\ sgn n == -(1).
Lemma sgn_0 :
sgn 0
== 0.
Lemma sgn_pos_iff :
forall n,
sgn n == 1
<-> 0
<n.
Lemma sgn_null_iff :
forall n,
sgn n == 0
<-> n==0.
Lemma sgn_neg_iff :
forall n,
sgn n == -(1)
<-> n<0.
Lemma sgn_opp :
forall n,
sgn (
-n)
== - sgn n.
Lemma sgn_nonneg :
forall n, 0
<= sgn n <-> 0
<= n.
Lemma sgn_nonpos :
forall n,
sgn n <= 0
<-> n <= 0.
Lemma sgn_mul :
forall n m,
sgn (
n*m)
== sgn n * sgn m.
Lemma sgn_abs :
forall n,
n * sgn n == abs n.
Lemma abs_sgn :
forall n,
abs n * sgn n == n.
End ZSgnAbsPropSig.