The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Hai WAN wrote:
> Variable V : Set.
> Variable D : V->Set.
> Definition States := forall v:V, D v.
>
> Variable t : V.
> Hypothesis t_nat :
>   D t = nat.
>
> Hypothesis t_full :
>   forall n:nat, exists s:States, s t = n.
> (***********************)
> Of course, I get an error message saying that (s t) is of type (D t), 
> while n is of type nat.
> I already have hypothesis t_nat stating "D t = nat". How to define 
> t_full with the help of t_nat?

There are two main options.  First, you can use a cast:

Hypothesis t_full :
  forall n:nat, exists s:States, match t_nat in _ = T return T with 
refl_equal => s t end = n.

Second, you can use an alternate notion of equality, e.g., [JMeq]:

Require Import JMeq.
Hypothesis t_full :
  forall n:nat, exists s:States, JMeq (s t) n.

I prefer the former approach, wherever it doesn't lead to too much 
inconvenience.  The main issues here are discussed in Chapter 9 of CPDT 
(http://adam.chlipala.net/cpdt/).