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

PVS Bug 764


Synopsis:        ASSERT scraps a premise
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           open
Class:           sw-bug
Arrival-Date:    Sat Apr 12 06:25:00 2003
Originator:      Alfons Geser
Organization:    nianet.org
Release:         PVS 3.1
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  ASSERT is sometimes reducing an essential premise to a useless TRUE
  IFF TRUE. In contrast PROP works. There may be a correlation to Ben's
  bug report #573. The following circumstances differ: (1) there is no
  reference to the prelude; (2) the claim is a theorem.
  
  Alfons
  
  ---
  
  assert_bug : THEORY
  begin
  
    s, t : VAR nnreal
    p, q, r: VAR real
    f: [real -> nnreal]  % think about the "sq" function
    g: [nnreal -> nnreal]  % think about the "sqrt" function
  
    eq_char: AXIOM s = t IFF f(s) = f(t)
    inverse: AXIOM f(g(s)) = s
    f_times: AXIOM f(p*q) = f(p)*f(q)
  
    problem: LEMMA
      s > 0 AND
      r*g(s) = g(t) IMPLIES
         t - f(r) * s = 0
  
  end assert_bug
  
  ---
  
  The steps (SKOSIMP*)(LEMMA "eq_char")(INST - "r!1 * g(s!1 - t)" "g(t)")
  get you to
  
  problem.1 :  
  
  {-1}  r!1 * g(s!1 - t) = g(t) IFF f(r!1 * g(s!1 - t)) = f(g(t))
  [-2]  s!1 > t
  [-3]  r!1 * g(s!1 - t) = g(t)
    |-------
  [1]   g(s!1 - t) = 0
  [2]   (t + f(r!1) * t - f(r!1) * s!1) = 0
  
  plus a TCC. Now (ASSERT) produces
  
  problem.1 :  
  
  {-1}  TRUE IFF TRUE
  [-2]  s!1 > 0
  [-3]  r!1 * g(s!1) = g(t!1)
    |-------
  [1]   t!1 - f(r!1) * s!1 = 0
  
  whereas (FLATTEN)(HIDE -2)(PROP) achieves what we wanted instead:
  
  problem.1 :  
  
  {-1}  f(r!1 * g(s!1)) = f(g(t!1))
  [-2]  s!1 > 0
  [-3]  r!1 * g(s!1) = g(t!1)
    |-------
  [1]   t!1 - f(r!1) * s!1 = 0
  
  The steps (REWRITE "f_times")(REWRITE "inverse")(REWRITE "inverse")
  (ASSERT)(ASSERT) finish the proof.

How-To-Repeat: 

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