在Coq中，有没有使用Rabs，Rineq的策略？

Question

我对Coq并不陌生，我的主要兴趣是使用它来进行简单的实际分析问题。对于第一个练习，我设法证明了x ^ 2 + 2x趋于0且x趋于0的证据。请参见下面的代码。

这似乎很笨拙，对于任何有关如何缩短此证明的通用反馈意见，或对提高其可读性的良好实践，我都会感兴趣。但是，我的主要问题是，是否有任何Coq策略来使涉及实数的简单任务自动化，沿着field和lra的路线，但更好。]

可能的示例1：

是否有任何策略可以证明Rbasic_fun中的函数的身份，例如绝对值？例如，我的一半证据专用于显示| x * x | + | 2 * x | = | x | | x | +2 | x | ！

可能的示例2：

是否有任何策略可以自动使用Rineq中的引理，例如Rlt_le，Rle_trans，Rplus_le_compat_r和Rmult_le_compat_r？也就是说，人类证明创建者将用来将一系列不等式“链接在一起”的引理。

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.

我对Coq并不陌生，我的主要兴趣是使用它来进行简单的实际分析问题。对于第一个练习，我设法证明了x ^ 2 + 2x趋于0且x趋于0的证据。请参见代码...

Answer 1

[这里是使用后遗症的证明，也许可以通过一些策略使其变得更好，但这很简单。每当我想知道使用什么引理时，我都会Search用结论中的术语找到引理...