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