The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

while competing with other provers at the ICMS conference, I was quite 
embarassed by some bugs in the fourier procedure. Here are some examples:

Require Import Reals.
Require Import Fourier.
Open Scope R_scope.

Theorem fourier1:
  0 <> 2.
try fourier.
intros H1; fourier.
Qed.

Theorem fourier2:
  forall x, 0 < x -> 0 < 1 * x * 2.
intros x Hx.
try fourier.
rewrite Rmult_1_l.
try fourier.
Qed.

Theorem fourier3:
  forall x, 0 <= x -> x <= 0 -> x = 0.
intros x Hx Hx1.
try fourier.
apply Rle_antisym; auto.
Qed.


I would also be nice if the procedure would not print some
message when it fails.

--
Laurent