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

*To*: "Cesar A. Munoz" <munoz@nianet.org>*Subject*: Re: [PVS-Help] elementary prove questions*From*: Natarajan Shankar <shankar@csl.sri.com>*Date*: Tue, 15 Nov 2005 17:30:44 -0800*Cc*: Vladimir Voevodsky <vladimir@ias.edu>, pvs-help@csl.sri.com*In-Reply-To*: Message from "Cesar A. Munoz" <munoz@nianet.org> of "Tue,15 Nov 2005 14:24:05 EST." <1132082644.16229.3.camel@squirt.nianet.org>*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>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

Vladimir: As Cesar's response indicates, an uninterpreted type, i.e., one that is is declared without a definition, can be empty (under a theory interpretation) so that declaring a constant of that type is potentially problematic. For the second part of your question, you can do M-x show-skolem-constants to see the active skolem constants so that you can use it to instantiate the antecedent universal quantifier. Thanks to a complaint of Mooij and Wesselink, there is a fix in the forthcoming version of PVS to automatically use skolem constants for heuristic instantiation in commands like inst? and grind. With this, (lemma "c") (grind) gets it. Cheers, Shankar > 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

**References**:**Re: [PVS-Help] elementary prove questions***From:*"Cesar A. Munoz" <munoz@nianet.org>

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