[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: Vladimir Voevodsky <vladimir@ias.edu>*Subject*: Re: [PVS-Help] elementary prove questions*From*: "Cesar A. Munoz" <munoz@nianet.org>*Date*: Tue, 15 Nov 2005 14:24:05 -0500*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <FE191763-F607-4009-A02F-0957B95BABA3@ias.edu>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Organization*: NIA*References*: <FE191763-F607-4009-A02F-0957B95BABA3@ias.edu>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

Vladimir, Since PVS 2.?, types can be empty. Then t:TYPE does not guarantee that exists an element of type t. To get around this problem you have to explicitly declare t to be a non-empty type, e.g., t:TYPE+ then you can define a:t and no tcc will be generated. Cesar On Tue, 2005-11-15 at 14:04, Vladimir Voevodsky wrote: > Hello, > > could you please help me with the following elementary (I hope!) > questions: > > 1. I am looking at the theory: > > try1: theory > begin > t:type > a:t > end try1 > > When I try to typecheck I get a tcc asking me to prove that t is non- > empty. On the other hand looking at the examples in the wift-tutorial > (e.g. the phonebook) I got the impression that a:t would be treated > as a declaration of a member in t and that it would imply rather than > require that t is non-empty. > > 2. I am looking at the theory > > try2: Theory > Begin > t: type > c: axiom exists (x: t): true > a: bool = (Forall (x: t): x/=x) > b: Theorem not a > End try2 > > How can I prove the theorem? If I add a line d:t then I get (as in 1) > a tcc which I can then prove using c. After that (grind) proves the > theorem. But I was not able to use c directly without an explicit > line saying d:t. > > Thank you, > Vladimir. -- Cesar A. Munoz H., Senior Staff Scientist mailto:munoz@nianet.org National Institute of Aerospace mailto:C.A.Munoz@larc.nasa.gov 100 Exploration Way http://research.nianet.org/~munoz Hampton, VA 23666, USA Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988

- Prev by Date:
**[PVS-Help] elementary prove questions** - Next by Date:
**Re: [PVS-Help] elementary prove questions** - Prev by thread:
**[PVS-Help] elementary prove questions** - Next by thread:
**Re: [PVS-Help] elementary prove questions** - Index(es):