Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

# 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:
```
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools