评估COQ中的常数义务

Question

我正在尝试证明这一点：

Goal forall a : R, (forall e : R, e > 0 /\ Rabs a <= e) -> a = 0.

这是我到目前为止所做的：

Goal forall a : R, (forall e : R, e > 0 /\ Rabs a <= e) -> a = 0.
Proof.
  intros a H.
  destruct (classic (a = 0)) as [a_eq_0 | a_neq_0].

  - trivial.
  - apply (Rabs_pos_lt a) in a_neq_0 as Rabs_a_gt_0.
    pose (e := Rabs a / 2).
    cut (Rabs a <= e).

    * intro absurd_ineq.
      cbv [e] in absurd_ineq.
      apply (Rmult_le_compat_r (/(Rabs a))) in absurd_ineq.
      unfold Rdiv in absurd_ineq.
      rewrite (Rinv_r (Rabs a) (Rabs_no_R0 a a_neq_0)) in absurd_ineq.
      rewrite (Rinv_r_simpl_m (Rabs a) (/2) (Rabs_no_R0 a a_neq_0)) in absurd_ineq.

当前的目标是：

2 goals
  
  a : R
  H : forall e : R, e > 0 /\ Rabs a <= e
  a_neq_0 : a <> 0
  Rabs_a_gt_0 : 0 < Rabs a
  e := Rabs a / 2 : R
  absurd_ineq : 1 <= / 2
  ============================
  a = 0

goal 2 is:
 0 <= / Rabs a

给定 andurd_ineq：1＆lt; = / 2 < / code>，我如何告诉COQ，此比较评估为 false ，为了使用矛盾策略？

我尝试使用 vm_compute 和 cbv ，希望 absurd_ineq 被简化，评估，对 false ，但没有机会。

谢谢。

编辑 ： 语句 forall a：r，（forall e：r，e＆gt; 0 /\ rabs a＆lt; = e） - ＆gt; a = 0 不是正确的， forall a：r，（forall e：r，e＆gt; 0 - ＆gt; rabs a＆lt; = e） - ＆gt; a = 0 是。

这是证明：

Goal :
  forall a : R, (forall e : R, e > 0 -> Rabs a <= e) -> a = 0.
Proof.
  intros a H.
  destruct (classic (a = 0)) as [a_eq_0 | a_neq_0].

  - trivial.
  - apply (Rabs_pos_lt a) in a_neq_0 as Rabs_a_spos.
    pose (e := Rabs a / 2).
    cut (Rabs a <= e).

    * intro absurd_ineq.
      cbv [e] in absurd_ineq.
      apply (Rmult_le_compat_r (/(Rabs a))) in absurd_ineq; [| lra].
      unfold Rdiv in absurd_ineq.
      rewrite (Rinv_r (Rabs a) (Rabs_no_R0 a a_neq_0)) in absurd_ineq.
      rewrite (Rinv_r_simpl_m (Rabs a) (/2) (Rabs_no_R0 a a_neq_0)) in absurd_ineq.
      lra.
    * specialize (H e).
      apply Rlt_gt in Rabs_a_spos.
      apply Rgt_ge in Rabs_a_spos as Rabs_a_pos.
      cbv [e] in *.
      lra.
Qed.```

Answer 1

COQ的一部分实际数字是公理定义的（例如，请参阅此处：）。这意味着计算不能像与整数或自然数字一样直接工作。

通常，我倾向于使用 Micromega 工具来解决此类琐碎的目标。您可以在此处找到他们的完整文档： https://coq.inria.fr/refman/附录/micromega.html
我发现策略 lra 最有帮助。对于您的特定示例，以下代码对我有用：

From Coq
 Require Export Reals.Reals micromega.Psatz.

Goal forall a:R, (forall e:R, Rgt e  R0 /\ Rle (Rabs a) e) -> a = R0.
Proof.
  intros a H.
  destruct (Req_dec a R0 ) as [a_eq_0 | a_neq_0].
  - trivial.
  - apply (Rabs_pos_lt a) in a_neq_0 as Rabs_a_gt_0.
    pose (e := Rdiv (Rabs a) 2).
    cut (Rle (Rabs a) e).

    * intro absurd_ineq.
      cbv [e] in absurd_ineq.
      apply (Rmult_le_compat_r (/(Rabs a))) in absurd_ineq.
      unfold Rdiv in absurd_ineq.
      rewrite (Rinv_r (Rabs a) (Rabs_no_R0 a a_neq_0)) in absurd_ineq.
      rewrite (Rinv_r_simpl_m (Rabs a) (/2) (Rabs_no_R0 a a_neq_0)) in absurd_ineq.
      lra. lra.
    * specialize (H e). lra.
Qed.
  

Answer 2

您要证明的声明中是否有一个问题（例如连词而不是含义）？引理看起来很琐碎，而且其证明并没有使用有关真实事物的许多知识。

Goal forall a:R, (forall e:R, Rgt e  R0 /\ Rle (Rabs a) e) -> a = R0.
Proof.
  intros a Ha; destruct (Ha R0) as [He _];
    destruct (Rgt_irrefl _ He).
Qed.