The Coq mailing list

[Dimitur Krustev <dkrustev AT gmail.com>]

'rewrite' works best for me in cases like this, but there are also the 'apply ->' and 'apply <-' variants of 'apply', specifically aimed at working with 'iff'.

In the example, 'apply -> Qlt_alt; auto' is enough to finish the proof.

On Thu, May 9, 2013 at 11:32 AM, Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr> wrote:

Hi,

I don't know if it is a bug or something I don't know, but I have a
problem with 'apply' when the applied theorem is a iff:

Example:

  Require Import QArith.
  Example foo : ∀ x y, x < y → (x ?= y) = Lt.
  Proof.
  intros.
  apply Qlt_alt.
--> nothing happens !
  apply Qlt_alt in H.
--> nothing happens !

Is there a way to tell 'apply' to apply Qlt_alt the direction I want?
Why was there no error message and nothing happened?

Tested on 8.4 and trunk.

Thanks.

--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/