[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] elementary prove questions
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
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.
> Since PVS 2.?, types can be empty. Then
> 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.,
> then you can define
> and no tcc will be generated.
> 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:email@example.com
> 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