The Coq mailing list

[Matthew Brecknell <matthew AT brecknell.net>]

Hi Adam,

Adam Megacz wrote:
> 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))]?

You can introduce such an equality explicitly by annotating the types of
the match branches using "match ... in ... return ... with ...":

Definition next (z: Z) (t: test z) : sum (test (z+1)) (test (z-1)).
  refine (fun z t =>
    match t in test z0
      return z = z0 -> sum (test (z0+1)) (test (z0-1)) with
      | up   _ u => fun Heq => inl _ u
      | down _ d => fun Heq => inr _ _
    end (refl_equal z)).
  (* easy proof to complete *)
Defined.

Note that the rest of the proof indeed involves the integer identity
that Adam Chlipala mentioned in his reply to your question!

You'll find this and many other excellent techniques in Adam's book.

Regards,
Matthew