The Coq mailing list

[Castéran Pierre <pierre.casteran AT gmail.com>]

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