[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] unprovable sequent proved



Dear Sam, or other help-desk-worker,

Attached is a small dump with one lemma that is valid and proved.
The problem is that the last sequent in the lefthand branch is
unprovable, but PVS nevertheless accepts it by (assert).
I assume PVS has kept some knowledge in some database, but how can the
user know this and reckon with it?

Best regards,
Wim
-- 
Wim H. Hesselink

Dept. of Computing Science       /   Bernoulliborg, office 374
   University of Groningen      /    Nijenborgh 9, 9747 AG
               P.O.Box 407     /     phone +31 50 3633933 (or *3939)
         9700 AK Groningen    /      fax   +31 50 3633800
           The Netherlands   /       http://www.cs.rug.nl/~wim

%% PVS Version 5.0 - Allegro CL Enterprise Edition 8.2 [64-bit Linux (x86-64)] (Apr 14, 2011 1:38)
%% 8.2 [64-bit Linux (x86-64)] (Apr 14, 2011 1:38)
$$$try.pvs
try: THEORY % Wim H. Hesselink, 24 february 2012

BEGIN
  Process: TYPE FROM nat

  state: TYPE = [#
    hello, welcome: [Process -> [Process -> nat]],
    pc: [Process -> nat],
    nbh, newusers: [Process -> pred[Process]]
  #]

  x, y: VAR state
  p, q, r: VAR Process

  next34(p, x): state =
    x WITH [
      `pc(p) := 35
    ]

  step34(p, x, y): bool =
    x`pc(p) = 34 AND empty?(x`nbh(p))
    AND y = next34(p, x)

  mq0(q, r, x): bool =
    x`hello(q)(r) + b2n(x`newusers(r)(q)) + x`welcome(r)(q) 
    = b2n(x`pc(q) = 34 AND x`nbh(q)(r))
  
  mq0_34: LEMMA    
    mq0(q, r, x) AND step34(p, x, y)
    IMPLIES mq0(q, r, y)

% This lemma is valid and proved, but the last assert command 
% in the lefthand branch proves an unprovable sequent.
% There is nothing against the equality: hello + welcome = 0. 
% If there is knowledge hidden in a data base, how can the user know this?
% Or is this a bug?
  
END try

$$$try.prf
(try
 (mq0_34 0
  (mq0_34-1 nil 3539066263
   ("" (expand "mq0")
    (("" (expand "step34")
      (("" (skosimp)
        (("" (replace -4 :hide? t)
          (("" (expand "next34")
            (("" (case "p!1=q!1")
              (("1" (assert)
                (("1" (replace -1)
                  (("1" (expand "b2n")
                    (("1" (lift-if)
                      (("1" (lift-if)
                        (("1" (assert)
                          (("1" (expand "empty?")
                            (("1" (expand "member")
                              (("1"
                                (inst?)
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((mq0 const-decl "bool" try nil) (next34 const-decl "state" try nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (b2n const-decl "nbit" bit nil) (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Process_pred const-decl "[nat -> boolean]" try nil)
    (Process type-from-decl nil try nil)
    (step34 const-decl "bool" try nil))
   shostak)))