The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Here's my reduced version of the problem I'm seeing:

Parameter X:Type.
Parameter next:option X -> option X.

Inductive iteration_reaches_rel (x0:option X) :
   option X -> option X -> Prop :=
| intro_iteration_reaches_rel: forall x:option X,
  x <> x0 -> iteration_reaches_rel x0 (next x) x.

Definition iteration_reaches (x y:option X):Prop :=
  Acc (iteration_reaches_rel y) x.

Notation "x ~~> y" := (iteration_reaches x y) (at level 100).

Lemma next_iteration_reaches: forall {x y:option X},
  (x ~~> y) -> (x <> y) -> (next x ~~> y).
Proof.
intros.
destruct H.
apply H.
constructor.
assumption.
Defined.  (* intentional, allows next definition to go through *)

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.  About the only unusual thing about the 
fixpoint definition is that the match statement is on x instead of on the 
decreasing parameter Hreach0 (which is broken down inside 
next_iteration_reaches).
-- 
Daniel Schepler