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

PVS Bug 705


Synopsis:        lift[T].down(bottom)
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Fri Aug  9 19:45:00 2002
Originator:      Sanjai Rayadurgam
Organization:    cs.umn.edu
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  
  Hi,
  
  I ran into a problem with auto-rewrite/grind when used in certain sequence.
  I ended up with a formula that is incorrect w.r.t the type of the constants:
  
  %--------------------------------------------------------------------------
  bug?: theory
   begin
  
    State: Type = {A, B}
  
    i: lift[State]
  
    equality: LEMMA FORALL (x, y: (up?[State])): x = y IFF down(x) = down(y)
  
    iDef: AXIOM  i = bottom
  
    dummy: THEOREM  NOT(i = up(A))
    %
    % (then (auto-rewrite "equality") (grind) (rewrite "iDef"))
    % gives a single antecedent formula  A?(down(bottom))
    % which cannot be shown false, whereas (grind :rewrites ("iDef"))
    % would prove the theorem.
  
   end bug?
  %--------------------------------------------------------------------------
  
  
     
  
     
  
  
  

How-To-Repeat: 

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