The Coq mailing list

[Hai WAN <wan.whyhigh AT gmail.com>]

Dear all,

 

I am not sure whether the subject is proper. I will describe my problem using a simple example, hoping it works.

 

Soppose we have:

 

(***********************)

Variable V : Set.
Variable D : V->Set.
Definition States := forall v:V, D v.

Variable t : V.
Hypothesis t_nat :
  D t = nat.
(***********************)

 

where V is a set of variables, D is a function which assigns a domain to a variable, States is the set of states, which is a type-consistent valuation of variables, and t is a variable of type nat.

 

Based on this, I want to make the following hypothesis:

 

(***********************)

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?

 

Any suggestions? Thank you in advance!

--
Best regards,
Hai WAN