The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Adam Megacz wrote:
> If you try the [refl_equal] trick, the typechecker -- which checks
> expressions in a more-or-less bottom-up traversal of the syntax tree --
> will fail before it gets up to the level where the equality hypothesis
> becomes available:
>
>    Definition next (z: Z) (t: test z) (q:test (z+1)) : Z.
>      refine (fix next (z:Z) (t:test z) (q:test (z+1)) :=
>        match t in test z0
>          return z = z0 ->  Z with
>          | down _ d =>  fun Heq =>  next z t d
>          | up   _ u =>  fun Heq =>  3
>        end (refl_equal z)).
>    

I really think this is the point where it makes sense for you to read 
something that introduces the key techniques of dependently-typed 
programming in Coq.  Matthew didn't say that [refine] would use [Heq] 
automatically to perform type-casts.  For that, you would need something 
like Program.

I think your function definition has a typo, where the last two 
recursive arguments to [next] are reversed.  Switching that, it's easy 
to arrive at an accepted program using the technique Matthew suggested.  
(I'm starting from your structurally recursive version, not the above code.)

Fixpoint next(n:nat)(z:Z)(t:test z)(q:test (z+1)) : Z :=
  match n with
    | 0%nat => 3
    | (S n') =>
      match t in test z0 return z = z0 -> Z with
        | down _ d => fun Heq : z = _ + 1 =>
          next n' _ d (match Heq in _ = Z return test Z with
                         | refl_equal => t
                       end)
        | up   _ u => fun _ => 3
      end (refl_equal _)
  end.