2

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

2 回答 2

2

这是使用 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.
于 2019-10-28T22:07:24.297 回答
1

对我自己的问题的部分回答：我意识到nrafrom的策略micromega正是我在“可能的示例 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.
于 2019-10-28T22:34:43.483 回答