The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

Matthew Brecknell 
<matthew AT brecknell.net>
 writes:
> You can introduce such an equality explicitly by annotating the types of
> the match branches using "match ... in ... return ... with ...":
> ...
>       return z = z0 -> sum (test (z0+1)) (test (z0-1)) with
> ...
>    end (refl_equal z)).

Thanks Matthew, but the good old [refl_equal] trick doesn't recover the
equality until after we've finished typing the branch.

While it will work for my simplified example, it doesn't appear to
handle more complicated situations, like where you're making a recursive
call inside the branch.  Here's an incredibly contrived example (*) of
what I'm talking about:

  Fixpoint next(z:Z)(t:test z)(q:test (z+1)) : Z :=
    match t with
      | down _ d => next z t d
      | up   _ u => 3
    end.

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)).

Sorry to do this back-and-forth thing where I incrementally increase the
complexity of my counterexample, but it's probably still simpler than me
dumping the full gigantic real-world case onto you all :)

  - a





(*) I left out the necessary structurally-decreasing parameter to reduce
    clutter irrelevant to this thread.  Here's one heavy-handed way to
    put it back in:

    Fixpoint next(n:nat)(z:Z)(t:test z)(q:test (z+1)) {struct n} : Z :=
      match n with
        | 0%nat => 3
        | (S n') => match t with
          | down _ d => next n' z t d
          | up   _ u => 3
        end
      end.