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

PVS Bug 768


Synopsis:        ASSERT unable to infer >= from =
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           open
Class:           sw-bug
Arrival-Date:    Fri May  2 16:40:00 2003
Originator:      Alfons Geser
Organization:    shrimp.nianet.org
Release:         PVS 3.1
Environment: 
 System:          
 Architecture: 

Description: 
  Sam,
  
  under PVS 3.1, ASSERT may be unable to infer A >= B from A =
  B. REPLACE however works. In PVS 2.4 this problem does not show up.
  
  bug2 : THEORY
  BEGIN
  
    IMPORTING reals@sign
  
    H : posreal
    x, y, t: VAR real
    eps: VAR Sign
  
    vert_at_char: LEMMA
      t /= 0 AND t*y = (eps*H - x) IMPLIES abs(x+t*y) = H
  
    t1: LEMMA
      0 < t AND
      t*y = (eps*H-x) IMPLIES abs(x+t*y) >= H
  
  END bug2
  
  Lemma vert_at_char is proven by GRIND. The proof of Lemma t1 starts by
  
   (skosimp*)
   (lemma "vert_at_char")
   (inst?)
   (assert)
  
  This yields the sequent
  
  {-1}  abs(t!1 * y!1 + x!1) = H
  [-2]  0 < t!1
  [-3]  t!1 * y!1 = (eps!1 * H - x!1)
    |-------
  {1}   abs(t!1 * y!1 + x!1) >= H
  
  An ASSERT does no change to this sequent. C-u M-x
  show-expanded-sequent shows that everything is fine except that = in
  formula -1 is equalities[numbers.number].= and >= in formula 1 is
  reals.>=.
  
  In contrast, (REPLACE -1)(ASSERT) finishes the proof.
  
  Kind Regards,
  Alfons

How-To-Repeat: 

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