# PVS Bug 920

Synopsis: invisible variables in PVS
Severity: serious
Priority: medium
Responsible: owre (Sam Owre)
State: analyzed
Class: sw-bug
Arrival-Date: Thu Nov 3 11:50:00 2005
Originator: "Mooij, A.J."
Organization: TUE.nl
Release: PVS 3.1
Environment:
System:
Architecture:
Description:
Hi,
Please consider the problem reported below for the PVS bug or enhancement dat
abase.
Kind regards, Arjan Mooij.
--------------------------
synopsis: invisible variables
pvs-version: PVS Version 3.1 - Allegro CL Enterprise Edition 6.2 [Linux (x86)] (Feb 14, 2003 18:46)
emacs-version: GNU Emacs 20.7.1 (i386-redhat-linux-gnu, X toolkit) of Fri Mar 16 2001 on porky.devel.redhat.com
uname -a: Linux gazelle 2.4.2-2enterprise #1 SMP Sun Apr 8 20:01:03 EDT 2001 i686 unknown
Consider the theory below that contains two related lemmas:
example0: THEORY BEGIN
X: TYPE
lemma0: LEMMA
FORALL (b:boolean):
(FORALL (x:X): b) => (EXISTS (x:X): true) => b
lemma1: LEMMA
FORALL (b:boolean, p:[X->boolean]):
(FORALL (x:X): p(x) => b) => (EXISTS (x:X): p(x)) => b
END example0
Although lemma0 looks simpler, it turns out that proving lemma1 in PVS
is much easier. Moreover, in proving lemma0 a strange phenomenon
occurs. Let us first consider the proof of lemma1. It can be proved
automatically using `(grind)', but for illustrating the problem we can
better study the result after `(skosimp*)':
{-1} FORALL (x: X): p!1(x) => b!1
{-2} p!1(x!1)
|-------
{1} b!1
Then let us compare this with the result after `(skosimp*)' for lemma0:
{-1} FORALL (x: X): b!1
|-------
{1} b!1
The big difference is that variable x!1 is now completely invisible. A
consequence is also that `(grind)' cannot prove lemma0, since it does not
exploit the invisible variable. The way we can complete this proof is by
explicitly re-introducing this invisible variable using `(inst -1
"x!1")'. Note that we must recall the existence of this variable from an
earlier proof-state. If we would apply `(grind)' initially on lemma0, we
reach a similar situation with the same phenomenon:
{-1} FORALL (x: X): FALSE
|-------
{1} b!1
How-To-Repeat:
Fix: