Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 589


Synopsis:        load-prelude-library theory invisible without importings
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Jul 31 19:05:00 2001
Originator:      Ben L. Di Vito
Organization:    larc.nasa.gov
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 


First I created a test directory and included a subdirectory "extend"
  having the following PVS file:
  
  extra_real_props: THEORY
  BEGIN
  
    w, x, y, z: VAR real
    n0w, n0x, n0y, n0z: VAR nonzero_real
    nnw, nnx, nny, nnz: VAR nonneg_real
    pw, px, py, pz: VAR posreal
    npw, npx, npy, npz: VAR nonpos_real
    nw, nx, ny, nz: VAR negreal
  
    div_cancel4: LEMMA x = y/n0z IFF x * n0z = y
  
    zero_times4: LEMMA 0 = x * y IFF x = 0 OR y = 0
  
  END extra_real_props
  
  
  Then I typechecked extra_real_props and exited to save the context
  (in "extend").
  
  Next I restarted PVS (in the parent directory) and typechecked the
  following test file:
  
  test : THEORY
  BEGIN
  
    a,b,c : real  
   
    t1 : LEMMA a = b/c
  
  END test
  
  I invoked M-x load-prelude-library and gave it the path for extend.
  This worked fine.
  
  Then I started a proof of t1 to produce the following error, in which
  the prover is unable to find the lemma div_cancel4.
  
  t1 :  
  
    |-------
  {1}   a = b / c
  
  Rule? (lemma "div_cancel4")
  Couldn't find a definition or lemma named div_cancel4Expecting a formula or c
 onstant
  No resolution for div_cancel4
                    
  
  No change on: (LEMMA "div_cancel4")
  
  
  Then I edited the theory as follows to add a superfluous importing
  statement:
  
  test : THEORY
  BEGIN
  
    IMPORTING real_props
  
    a,b,c : real  
   
    t1 : LEMMA a = b/c
  
  END test
  
  
  This caused the prover to behave as expected on the next attempt:
  
  
  t1 :  
  
    |-------
  {1}   a = b / c
  
  Rule? (lemma "div_cancel4")
  Applying div_cancel4 
  this simplifies to: 
  t1 :  
  
  {-1}  FORALL (n0z: nonzero_real, x, y: real): x = y / n0z IFF x * n0z = y
    |-------
  [1]   a = b / c
  
  
  Even more curious is that when I restarted PVS after deleting the
  context file and used the following alternative version of the test
  theory, the proof step failed in the same way.  In other words, the
  importing statement didn't solve the problem in this case.
  
  test2 : THEORY
  BEGIN
  
    IMPORTING real_props
  
    a,b,c : real  
   
    t1 : LEMMA a = b/c
  
  END test2
  

How-To-Repeat: 

Fix: 
The context is in some cases ignoring the prelude libraries.
Fixed decl-context to do the right thing.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools