Tactics for Inequalities
This module defines tactics for automatically proving inequalities over real numbers.
This returs GT if x is clearly greater than e, returns LT if x
is clearly less than (-e), and returns Eq otherwise.
Definition CR_epsilon_sign_dec (e:Qpos) (x:CR) : comparison :=
let z := (approximate x e) in
match (Qle_total z (2*e)) with
| right p => Gt
| left _ =>
match (Qle_total (-(2)*e) z) with
| right p => Lt
| left _ => Eq
end
end.
let z := (approximate x e) in
match (Qle_total z (2*e)) with
| right p => Gt
| left _ =>
match (Qle_total (-(2)*e) z) with
| right p => Lt
| left _ => Eq
end
end.
This helper lemma reduces a CRpos problem to a sigma type with
a simple equality proposition.
Automatically solve the goal {e:Qpos | CR_epsilon_sign_dec e x = Gt}
by starting with approximating by e, and halving the allowed error until
the problem is solved. (This tactic may not terminate.)
This is the main tactic for solving goal of the from CRpos e.
It tries to clear the context to make sure that e is a closed term.
Then it applies the helper lemma and runs CR_solve_pos_loop.
This tactic is used to transform an inequality over IR into an
problem bout CRpos over CR. Some fancy work needs to be done because
autorewrite will not in CRpos, because it is in Type and not Prop.
This tactic solves inequalites over IR. It converts the problem
into a question about positivity over CR, and then tries to solve it.