在 Coq 中，是否有与 Rabs、Rineq 合作的策略？答案

【问题标题】：In Coq, are there tactics for working with Rabs, Rineq?在 Coq 中，是否有与 Rabs、Rineq 合作的策略？
【发布时间】：2019-10-27 22:07:02
【问题描述】：

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

【问题讨论】：

您查看过Coquelicot 库吗？它有限制等的定义，我觉得更容易使用。他们使用常规的 Coq 实数，并具有转换引理等，因此他们也可以使用其他地方开发的关于实数的引理。
感谢您的回复！我简单地看了看 Coquelicot。但是，似乎 Coquelicot 的工具主要用于自动化限制/分析，而我想自动化我提到的实数的低级操作，但不自动化 epsilon-delta 分析本身。你知道 Coquelicot 中是否存在这种能力吗？
coquelicot 库的可读性非常好（许多其他库并非如此），它们阅读起来几乎就像教科书一样。我建议阅读代码（在 coq doc 中），展开定义等，您会发现定义非常“自然”。有一些技巧，比如过滤器的使用，不过还是好好学吧。
您还可以阅读Coquelicot 以及它们如何在this paper 中定义限制等。非常易读的演示文稿。

标签： coq theorem-proving coq-tactic real-number

【解决方案1】：

这是使用 coquelicot 的证明，它可能可以通过一些策略变得更好，但这很简单。每当我想知道要使用什么引理时，我都会使用Search 来找到一个带有该术语的引理...

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.

编辑：

这里是使用 Coq 标准库中的引理代替上述引理的证明。我通过严重依赖Search 找到了它们。也许这种方法可以减轻为您做类似证明的工作量。

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.

【讨论】：

感谢您写出这篇文章，它确实非常优雅！但是，我真的只想自动化我提到的那种低级任务，而不是 epsilon-delta 分析本身。并不是说我对过滤器有任何道德上的反对:)——相反，我想到的应用程序是用于教学，所以我想要一组库来自动化本科生认为显而易见的证明部分，而且只有那些部分。
@anon 我使用您对limit 的定义添加了一个证明，我希望通过使用标准库中的引理来展示一种不那么麻烦的方法来推理Rabs。
@anon（哎呀，刚刚看到你在下面的帖子中基本上做到了这一点！）
非常感谢——对于初学者来说，看到这种对代码的详细修改真的很有帮助。我不知道pose proof；现在我可以摆脱所有那些 assert 了！但是我更喜欢使用nra（如我的回答），而不是明确调用Rplus_lt_compat、Rmult_le_0_lt_compat等。

【解决方案2】：

我自己的问题的部分答案：我意识到 micromega 中的策略 nra 完全符合我在 “可能的示例 2” 中的要求。所以这是我之前代码的一个版本，其中关于不等式的推理由nra 自动完成。我仍然很想知道是否有一种推理绝对值和最小值/最大值的策略，对应于我的“可能示例 1”。

更新：下面的代码通过从@larsr 的回答中学到的一些习语（pose proof、exists）进行了改进。

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.

【讨论】：