The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Marco Servetto wrote:
> if I make
> unfold rK;intros n myR.
>   generalize (refl_equal (f n)).
>
> I obtain
>
> forall e : f n = f n,
> Some myR =
> (if f n as x return (x = f n ->  option R)
>   then fun p : true = f n =>  Some (r n p)
>   else fun _ : false = f n =>  None) e ->  data myR = n
>
> that is quite unexpected. I was expecting
>
> f n = f n ->
> Some myR =
> (if f n as x return (x = f n ->  option R)
>   then fun p : true = f n =>  Some (r n p)
>   else fun _ : false = f n =>  None) (refl_equal (f n)) ->  data myR = n
>
> (that is exactly what I obtain doing
> intros n myR.
>   generalize (refl_equal (f n)).
> unfold rK.)
>
> It looks like generalize is much more complex that I expected. When
> this forall e is generated??
>    

It's not that complex.  [generalize] only matches syntactic occurrences 
of the argument in the conclusion.  Unfolding [rK] exposes another 
occurrence, which [generalize] is able to grab.