Skip to Content.
Sympa Menu

coq-club - [Coq-Club] how to state a hypothesis with the help of another hypothesis

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] how to state a hypothesis with the help of another hypothesis


chronological Thread 
  • From: Hai WAN <wan.whyhigh AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] how to state a hypothesis with the help of another hypothesis
  • Date: Sun, 7 Nov 2010 00:58:56 +0800
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=nhbZvJJXy/xf20OY53awCfy78S4iV46KMf6+QAJ6PKrFmbEVvwUQiF2zweDhBDNpmE z8w+I0DMSQ4eGpbtJdkb5E5kqTHW4Mi6Oo51mVjlyLbKRjIVYO1GaNWQFrpVOs8VvFpp vPjrFyFCKh0PaZIku1G5cjPKPUXN0pUUsdP2s=

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



Archive powered by MhonArc 2.6.16.

Top of Page