Evaluate constant inequation in Coq

Question

I am trying to prove this :

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

This is what I've done so far :

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.

With the current goal being :

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

Given absurd_ineq : 1 <= / 2, how can I tell Coq that this comparison evaluates to False, in order to then use the contradiction tactic ?

I have tried using vm_compute and cbv in hope that absurd_ineq is simplified, evaluated, to False, but no chance.

Thanks.

EDIT : The statement forall a : R, (forall e : R, e > 0 /\ Rabs a <= e) -> a = 0 wasn't the right one, forall a : R, (forall e : R, e > 0 -> Rabs a <= e) -> a = 0 was.

Here's the proof :

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

user_2728035 · Answer

part of Coq's real numbers are defined axiomatically (see e.g. here: https://coq.inria.fr/stdlib/Coq.Reals.Rdefinitions.html). This means that computation does not work as straight-forwardly as it works with e.g. integers or natural numbers.

In general, I tend to use the micromega tools for solving such trivial goals. You can find their full documentation here: https://coq.inria.fr/refman/addendum/micromega.html I found the tactic lra to be most helpful. For your particular example, the following code works for me:

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.

user_9415192 · Answer

Is there an issue in the statement you want to prove (e.g. a conjunction instead of an implication) ? The lemma looks to be trivial as it is stated, and its proof doesn't use many knowledge about the reals.

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.

Evaluate constant inequation in Coq

2 Answers