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.
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.