[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
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 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:
>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.
>> On Jul 9, 2015, at 12:37 AM, MUNOZ, CESAR (LARC-D320)
>> The short answer is yes (see page 20, Section 2.4, of our tutorial in
>> f). Proveit supports this type of extensions.
>> The short question is why? There is a theory reals@abs_lems in the NAS
>> 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
>> you and add the lemma there.
>> 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
>> 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:
>>> FORALL(a: real, nnx: nnreal, b: real, nny: nnreal):
>>> <= nnx
>>> AND abs(b)
>>> <= nny
>>> * nny)
>>> <= (a
>>> * b)
>>> * 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
>>> Best Regards,
>>> Ben Hocking