The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

I see, thanks very much!

Jeremy

On 4/8/20 7:14 pm, Castéran Pierre wrote:
> Hi,
>
> It looks like the « apply iff-refl » destructs the iff into two implications, 
> and generates a new goal without any error.
>
> Lemma test (A B: Prop): A <-> B.
>   Show Proof.
>    apply iff_refl.
>    Show Proof.
> (*
>
> (fun A B : Prop =>
>   let H : forall A0 : Prop, A0 -> A0 :=
>     fun A0 : Prop => match iff_refl A0 with
>                      | conj _ x0 => x0
>                      end in
>   H (A <-> B) ?Goal)
> *)
>
> In short, « apply" seems to do a lot of smart things, we have to look at the 
> doc …
>
> Best regards,
>
> Pierre
>
> > Le 4 août 2020 à 09:10, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :
> >
> >
> > Hi,
> >
> > In this sequence,
> >
> > Lemma test (Y Z : Prop) : (Y <-> Z).
> > Proof. apply iff_refl. Abort.
> >
> > the  tactic apply iff_refl does nothing - it doesn't succeed (naturally) but 
> > it doesn't produce the usual failure message either; can anyone tell why this 
> > is?
> >
> > Thanks,
> >
> > Jeremy
> >
> > PS what follows is a query I made a while back, but I didn't get any replies 
> > then, does anyone know how to stop Coq unfolding a constant in this situation?
> >
> > On 9/7/20 11:46 pm, Jeremy Dawson wrote:
> > > Hi,
> > > I have a goal
> > > swapped ((single a ++ qs) ++ vs) ((qs ++ vs) ++ single a)
> > > where single is defined by
> > > Definition single X (a : X) := [a].
> > > When I try
> > > rewrite - !app_comm_cons.
> > > it unfolds one of the occurrences of single x
> > > (which stops my carefully written Ltac function from working and took ages to 
> > > pinpoint what was happening).
> > > How do I stop this from happening?
> > > Thanks
> > > Jeremy