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

Re: [PVS-Help] elementary prove questions


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: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