In Coq, are there tactics for working with Rabs, Rineq?

Question

I am new to Coq, and my primary interest is in using it to do simple real analysis problems. For a first exercise, I managed to bash through a proof that x^2+2x tends to 0 as x tends to 0. See code below.

This seems pretty clunky, and I would be interested in any general feedback on how to shorten this proof, or good practice for improving its readability. However, my main question is whether there are any Coq tactics for automating simple tasks involving the real numbers, along the lines of field and lra but better.

possible example 1: are there any tactics to prove identities for the functions from Rbasic_fun, such as the absolute value? For example, half my proof is dedicated to showing that |x*x|+|2*x|=|x||x|+2|x| !

possible example 2: are there any tactics to automate the use of the lemmas from Rineq, such as Rlt_le, Rle_trans, Rplus_le_compat_r and Rmult_le_compat_r? That is, lemmas that a human proof-creator would use to "chain together" a sequence of inequalities.

Require Import Rbase.
Require Import Rbasic_fun.
Require Import Lra.
Local Open Scope R_scope.

Definition limit (f:R -> R)
  (D:R -> Prop) (l:R) (x0:R) :=
  forall eps:R,
    eps > 0 ->
    exists delta : R,
      delta > 0 /\
      (forall x:R, D x /\ Rabs (x - x0) < delta -> Rabs ((f x) - l) < eps).

Lemma limitf : limit (fun (x:R) => x*x + 2 *x) (fun x => True) 0 0.
Proof.
  unfold limit; intros.
  split with (Rmin (eps/3) 1); split.
  assert (eps / 3 > 0) by lra; clear H.
  assert (1>0) by lra.
  apply (Rmin_Rgt_r (eps/3) 1). apply (conj H0 H).
  intros. destruct H0. clear H0.  replace (x-0) with x in H1 by field.
  apply (Rmin_Rgt_l (eps/3) 1) in H1. destruct H1.
  assert (Rabs (x*x+2*x -0) <= Rabs(x*x)+Rabs(2*x)).
    replace (x*x+2*x-0) with (x*x+2*x) by field.
    apply Rabs_triang.
  assert (Rabs(2*x) =  2 * Rabs(x)). 
    assert (Rabs(2*x) =  Rabs(2) * Rabs(x)).
      apply (Rabs_mult _ _).
    assert (Rabs 2 = 2).
      apply (Rabs_right _). lra.
    replace (Rabs 2) with 2 in H3 by H4. apply H3.
  replace (Rabs (2 * x)) with (2 * Rabs x) in H2 by H3.  clear H3.
  assert (Rabs(x*x) = Rabs(x)*Rabs(x)). 
    apply Rabs_mult.
  replace (Rabs(x*x)) with (Rabs(x)*Rabs(x)) in H2 by H3.  clear H3.
  assert (Rabs x * Rabs x <= 1 * Rabs x).
    apply Rmult_le_compat_r.  apply Rabs_pos.  apply Rlt_le. auto.
  apply (Rplus_le_compat_r (2 * Rabs x) _ _) in H3.
  apply  (Rle_trans _ _ _ H2) in H3. clear H2.
  replace (1 * Rabs x + 2 * Rabs x) with (3 * Rabs x) in H3 by field.
  assert (3 * Rabs x < eps) by lra.
  apply  (Rle_lt_trans _ _ _ H3). auto.
Qed.

Answer 1

Here is the proof using coquelicot, it can probably be made nicer with some of the tactics, but this was quite straight forward. Whenever I wondered what lemma to use, I did Search to find a lemma with the term in its conclusion...

Require Import Reals.
From Coquelicot Require Import Coquelicot.
Open Scope R.

Lemma limitf : is_lim (fun x => x*x + 2 * x) 0 0.
  eapply is_lim_plus.
  eapply is_lim_mult.
  eapply is_lim_id.
  eapply is_lim_id.
  compute. apply I.
  eapply is_lim_mult.
  eapply is_lim_const.
  eapply is_lim_id.
  compute. apply I.
  compute. f_equal.  f_equal.
  ring.  
Qed.

Edit:

Here is the proof of your lemma above using lemmas from Coq's standard library instead. I found them by relying heavily on Search. Perhaps this approach makes it less heavy to do similar proofs for you.

Require Import Reals Lra.
Local Open Scope R_scope.

Definition limit (f:R -> R)
  (D:R -> Prop) (l:R) (x0:R) :=
  forall eps:R,
    eps > 0 ->
    exists delta : R,
      delta > 0 /\
      (forall x:R, D x /\ Rabs (x - x0) < delta -> Rabs ((f x) - l) < eps).

Lemma limitf : limit (fun (x:R) => x*x + 2 *x) (fun x => True) 0 0.
  intros eps Heps.
  exists (Rmin (eps/3) 1).
  split. apply Rmin_Rgt. lra.
  intros x [_ H].
  destruct (Rmin_Rgt_l _ _ _ H); clear H.
  rewrite Rminus_0_r in *.
  eapply Rle_lt_trans.
  apply Rabs_triang.
  do 2 erewrite Rabs_mult.
  pose proof (Rabs_pos x).
  remember (Rabs x) as a; clear Heqa.
  rewrite (Rabs_right 2) by lra.
  replace eps with (((eps/3)*1) + (2*eps/3)) by lra.
  apply Rplus_lt_compat; try lra.
  apply Rmult_le_0_lt_compat; lra.
Qed.

Answer 2

A partial answer to my own question: I realised that the tactic nra from micromega does exactly what I had asked for in my "possible example 2". So here is a version of my previous code in which reasoning about inequalities is done automatically by nra. I am still interested to know whether there is a tactic for reasoning about the absolute-value and min/max, corresponding to my "possible example 1".

Update: code below improved by some idioms (pose proof, exists) learned from the answer of @larsr.

Require Import Psatz.
.....

Lemma limitf : limit (fun (x:R) => x*x + 2 *x) (fun x => True) 0 0.
Proof.
  unfold limit; intros.
  exists (Rmin (eps/3) 1); split.
  apply Rmin_Rgt; lra.
  intros; destruct H0.  
  replace (x-0) with x in H1 by field; replace (x*x+2*x-0) with (x*x+2*x) by field.
  apply Rmin_Rgt_l in H1; destruct H1.
  pose proof (Rabs_triang (x*x) (2*x)).
  pose proof (Rabs_mult 2 x).
  pose proof (Rabs_mult x x).
  pose proof (Rabs_pos x).
  epose proof (Rabs_right 2).
  nra.
Qed.