# 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: