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