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

Re: [PVS-Help] Extending the prelude?



Yes, you would have to import reals@abs_lems. If you opt for the prelude
extension solution, use the option -p <dir> of proveit to automatically
load the prelude extension in batch mode. In interactive mode, you may
have to add an appropriate code to your pvs-emacs to automatically execute
the command M-x load-prelude-library. Otherwise, you would have to issue
the command by hand the first time that you use the extension in a new
context. The prelude extension information is saved in .pvscontext, so you
don't have to use this command in subsequent PVS sessions on the same
context.

In any case, I will add your lemma to real@abs_lem in case you change your
mind. It will be immediately available in GitHub or you can wait until the
next official release.

Cesar

-- 
Cesar A. Munoz                             NASA Langley Research Center
Cesar.A.Munoz@xxxxxxxx                     Bldg. 1220  Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234




On 7/8/15 5:34 PM, "Ben Hocking" <benjaminhocking@xxxxxxxxx> wrote:

>Hi Cesar,
>
>My reasoning is that it would be great to have access to these lemmas
>without having to use an IMPORTING statement in the theory before
>beginning the proof. If I insert this lemma into the theory
>reals@abs_lems, then I would have to have “IMPORTING reals@abs_lems” in
>the body of my theory, correct?
>
>Thanks a lot for directing me to Section 2.4. That does seem like it will
>do the trick.
>
>Best Regards,
>-Ben
>
>> On Jul 9, 2015, at 12:37 AM, MUNOZ, CESAR (LARC-D320)
>><cesar.a.munoz@xxxxxxxx> wrote:
>> 
>> Ben, 
>> The short answer is yes (see page 20, Section 2.4, of our tutorial in
>> 
>>http://shemesh.larc.nasa.gov/people/cam/publications/NASA-CP-2003-212448.
>>pd
>> f). Proveit supports this type of extensions.
>> 
>> The short question is why? There is a theory reals@abs_lems in the NAS
>>PVS
>> Library, where your lemma is welcome. From there, you can easily import
>> that theory and set an auto-rewrite. Let me know if this option works
>>for
>> you and add the lemma there.
>> 
>> Cesar
>> -- 
>> Cesar A. Munoz                             NASA Langley Research Center
>> Cesar.A.Munoz@xxxxxxxx                     Bldg. 1220  Room 115 MS. 130
>> http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
>> Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234
>> 
>> 
>> 
>> 
>> On 7/7/15 9:35 PM, "pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx
>>on
>> behalf of Ben Hocking"
>> <pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx on behalf of
>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
>> 
>>> Is there a way to “extend” prelude.pvs? For example, if I want to make
>>> the following proven lemma available to proofs in any theory without
>>> requiring them to have an IMPORTING statement for the helper lemma:
>>> 
>>> 
>>> abs_bounding:
>>> 
>>> LEMMA          
>>> 
>>> FORALL(a: real, nnx: nnreal, b: real, nny: nnreal):
>>>    abs(a)
>>> 
>>> <= nnx 
>>> AND abs(b) 
>>> <= nny 
>>> IMPLIES        
>>> 
>>> -(nnx 
>>> * nny) 
>>> <= (a 
>>> * b) 
>>> AND            
>>>       (a
>>> 
>>> * b)     
>>> <= (nnx 
>>> * nny);        
>>> 
>>> 
>>> 
>>> Is there a way to do this? I’ve tried renaming the containing file
>>> prelude.pvs (in the current working directory), but that did not do the
>>> job.
>>> 
>>> 
>>> Best Regards,
>>> Ben Hocking
>>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>>> 
>>> 
>>> 
>>> 
>>> 
>>> 
>>> 
>> 
>