The Coq mailing list

[Damien Pous <Damien.Pous AT ens-lyon.fr>]

Maybe you could replace the inductive type with the following one?

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

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


Damien

2010/3/24 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
>
>
>