The Coq mailing list

[Duckki Oe <duckki AT mit.edu>]

I have similar issues, too. My solution was to destruct the lemma into two 
separate hypothesis first and apply one of them.  

Example foo : forall x y, x < y -> (x ?= y) = Lt.
Proof.
  intros.
  edestruct Qlt_alt.
  eassumption.
Qed.



-- Duckki


On Thursday, May 9, 2013 at 4:32 AM, Daniel de Rauglaudre 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/