The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Daniel Schepler wrote:
> Fixpoint iter_sub (x y:option X) (Hreach0 : x ~~>  None) : option X.
> refine (match x as x' return (x=x' ->  option X) with
> | Some x0 =>  fun _ =>
>       iter_sub (next x) (next y) (next_iteration_reaches Hreach0 _)
> | None =>  fun _ =>  y
> end (eq_refl _)).
> rewrite _H; discriminate.
> Defined.
>
> Lemma iter_sub_None: forall (y:option X) (Hreach0 : None ~~>  None),
>    iter_sub None y Hreach0 = y.
> Proof.
> intros.
> reflexivity.  (* fails *)
>
> I don't see the problem here: it should be obvious that the match statement
> goes to the None case and returns y.
>    

The beta reduction rule for [fix] terms only fires when the top-level 
structure of the recursive argument of the [fix] is known.  In your 
example, the reduction you need is stuck on a [fix] whose recursive 
argument is the variable [Hreach0].  That's why no further progress can 
be made.

I found this problem quickly by running [compute] at the point where you 
wrote [reflexivity].  If you see what looks like a redex in the result 
of [compute], you know your assumptions about reduction need adjusting. :)