Re: [PVS-Help] elementary prove questions

[Natarajan Shankar <shankar@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