The Coq mailing list

[Roger Witte <rogerwite AT yahoo.co.uk>]

It is worth noting that the rewrite here is a setoid rewrite using the iff_setoid and will only work if Setoid has been imported.

---

From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
To: Coq Club <coq-club AT inria.fr>
Sent: Thursday, 9 May 2013, 9:52
Subject: Re: [Coq-Club] How to force apply on the other way?

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/