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

  Please consider the problem reported below for the PVS bug or enhancement dat
  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


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