The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Indeed, that does the job. I did not think that 'rewrite' could work
in that case. Thanks.

On Thu, May 09, 2013 at 10:37:30AM +0200, Beta Ziliani wrote:
>  I don't know what is the expected result from apply in this case, but
> you can always perform a rewrite in the goal or in the hypothesis:
> 
>   rewrite <- Qlt_alt.
> 
> or
> 
>   rewrite Qlt_alt in H.
> 
> 
> On Thu, May 9, 2013 at 10: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/

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