The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 08/09/2012 03:48 AM, Jason Gross wrote:
> Is there a good way to get [match goal with ... end] to respect the 
> typing/naming of hypotheses?  That is, is there a variant of
>     Goal forall (n m : nat) (n' m' : unit) (f : nat -> nat -> Type) 
> (f' : unit -> unit -> Type) (P : nat -> Prop) (fn : P n -> f n m -> f' 
> n' m'), False.
>       intros.
>       match goal with
>         | [ H : unit -> unit -> _, H1 : appcontext[?H ?a ?b] |- _ ] => 
> pose H
>       end.
> that gives me a new hypothesis [T := f' : unit -> unit -> Type] rather 
> than [T := f : nat -> nat -> Type]?  (I know that I can match for the 
> type of [H] after the fact, but this seems like it gets unwieldy 
> quickly, if I have multiple hypotheses that I'm trying to match 
> against simultaneously.)

Your question seems to be related to the fact that hypothesis patterns 
and question mark-prefaced unification variables are treated as distinct 
binders, apparently with the latter overriding the former.  Were you 
aware of this (admittedly counter-intuitive) behavior?  The issue 
doesn't seem so related to the idea of "hypotheses of certain types."

I don't know a way bind a hypothesis variable and use it elsewhere in a 
single pattern, but I agree it would be a worthwhile feature.