Re: [PVS-Help] elementary prove questions

["Cesar A. Munoz" <munoz@nianet.org>]

This is a proof of lemma b in try2:


%|- b : PROOF
%|- (then (expand "a") (lemma "c") (skolem -1 "x") (inst -1 "x"))
%|- QED


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