The Coq mailing list

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

It seems that in Coq's rule for typing [match], the hypotheses for the
well-typedness of the branches have a more restrictive context than I'd
like (perhaps for a good reason!).

Here's an example of what I mean:

  Require Import ZArith.
  Require Import Coq.Init.Datatypes.
  Open Scope Z_scope.
  Require Import Coq.Init.Specif.

  Inductive test : Z -> Set :=
    | up   : forall z, test (z+1) -> test z
    | down : forall z, test  z    -> test (z+1).

  Definition next(z:Z)(t:test z) : sum (test (z+1)) (test (z-1)) :=
    match t with
      | down _ d => inr (test (z-1)) d
      | up   _ u => inl (test (z+1)) u
    end.

This example is greatly simplified from the actual case I'm working on,
so I apologize if I've accidentally made the solution trivial in the
process.  When typing the body of the second branch (everything between
the last [=>] and [end.]), we introduce a fresh variable [z0] and the
assumption [u:(test z0)].  But shouldn't it be safe for the typing
context to also include some sort of assumption along the lines of
[t:(test (z0+1))] or [(test z)=(test (z0+1))]?

It seems that Coq's typing rules do not include a provision for this --
am I mistaken?  Each branch of [match] gets typed as if it were a
function whose arguments are the constructor's arguments, but the context
is unchanged.  To put it less formally, it seems like when a constructor
definition for type [test] ends with

 Inductive test : Z -> Set :=
   | ... -> test XYZ

then the corresponding branch of a [match] ought to be granted the
assumption that the type of the value being [match]ed upon is equal to
[test XYZ].

My current workaround is to (1) add a recursively uniform parameter and
(2) stash a proof relating the uniform parameter to a nonuniform
parameter in each constructor:

  Inductive test (z:Z) : Z -> Set := ..
    | up   : forall z0,   z0=z -> test (z0+1) -> test z
    | down : forall z0, z0+1=z -> test  z0    -> test z
    ...

but the added verbosity is getting to be a problem.  Are there any other
solutions?

Thanks!

  - a