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