I would like to prove a bunch of theorems like 100 + 100 = 200 or 1 > - / 2 in real numbers, but I it seems like coq can't do this using auto tactic. Is there any way to prove thing like this without writing hundreds of lines?
ring will prove equalities
lra and nra will prove basic comparisons
interval will prove comparisons involving advanced functions and constants (sin, PI, exp). lra are available in Coq without installing extensions. interval requires an extension to be installed (coq-interval in the opam package index). Some pre-packaged installation of Coq already include interval.
Require Import Reals Lra Interval.Tactic.
Open Scope R_scope.
Lemma examples : 100 + 100 = 200 /\ 2 ^ 19 < 3 ^12 /\ 3.14 <= PI <= 3.15.
split.
(* your need. *)
ring.
split.
(* simpl comparison between constants (algebraic formulas). *)
lra.
(* advanced comparison between constants *)
interval.
Qed.
At the time of writing the first version of the answer, I was a little disappointed because interval only handled <= and not < .