Library Coq.Reals.DiscrR
Require Import RIneq.
Require Import Omega.
Open Local Scope R_scope.
Lemma Rlt_R0_R2 : 0 < 2.
Lemma Rplus_lt_pos :
forall x y:R, 0 <
x -> 0 <
y -> 0 <
x +
y.
Lemma IZR_eq :
forall z1 z2:Z,
z1 =
z2 ->
IZR z1 =
IZR z2.
Lemma IZR_neq :
forall z1 z2:Z,
z1 <>
z2 ->
IZR z1 <>
IZR z2.
Ltac discrR :=
try
match goal with
| |- (?X1 <> ?X2) =>
change 2
with (
IZR 2);
change 1
with (
IZR 1);
change 0
with (
IZR 0);
repeat
rewrite <-
plus_IZR ||
rewrite <-
mult_IZR ||
rewrite <-
Ropp_Ropp_IZR ||
rewrite Z_R_minus;
apply IZR_neq;
try discriminate
end.
Ltac prove_sup0 :=
match goal with
| |- (0 < 1) =>
apply Rlt_0_1
| |- (0 < ?X1) =>
repeat
(
apply Rmult_lt_0_compat ||
apply Rplus_lt_pos;
try apply Rlt_0_1 ||
apply Rlt_R0_R2)
| |- (?X1 > 0) =>
change (0 <
X1)
in |- *;
prove_sup0
end.
Ltac omega_sup :=
change 2
with (
IZR 2);
change 1
with (
IZR 1);
change 0
with (
IZR 0);
repeat
rewrite <-
plus_IZR ||
rewrite <-
mult_IZR ||
rewrite <-
Ropp_Ropp_IZR ||
rewrite Z_R_minus;
apply IZR_lt;
omega.
Ltac prove_sup :=
match goal with
| |- (?X1 > ?X2) =>
change (
X2 <
X1)
in |- *;
prove_sup
| |- (0 < ?X1) =>
prove_sup0
| |- (- ?X1 < 0) =>
rewrite <-
Ropp_0;
prove_sup
| |- (- ?X1 < - ?X2) =>
apply Ropp_lt_gt_contravar;
prove_sup
| |- (- ?X1 < ?X2) =>
apply Rlt_trans with 0;
prove_sup
| |- (?X1 < ?X2) =>
omega_sup
|
_ =>
idtac
end.
Ltac Rcompute :=
change 2
with (
IZR 2);
change 1
with (
IZR 1);
change 0
with (
IZR 0);
repeat
rewrite <-
plus_IZR ||
rewrite <-
mult_IZR ||
rewrite <-
Ropp_Ropp_IZR ||
rewrite Z_R_minus;
apply IZR_eq;
try reflexivity.