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

existskwantor problem



Hello,

I'm working on a problem which acts on subsets of some specific sets.
Here is an simplified example of my problem:

First of all I have defined my own types and some specific constants of
that type:

    State: Type+

    StateS1: State
    StateS2: State
    StateS3: State
    StateRoot: State

After that, I need a set that contains all defined stateconstants.

    StateSet: type+ = finite_set[State]

I also need a record which contains two elements:
 - the first member: is the set of all stateconstants
 - the second member: defines a special state among those stateconstants

    StateRecord : type+ = [# States : StateSet,
                             Root : State #]

 Define a specific record with the above constants

    sm : StateRecord = (# States := add(StateS1, add(StateS2, add(StateS3, add(StateRoot, emptyset)))),
                          Root   := StateRoot #)

Now I define another set of states, which contains or must contain a
subset of the set of all stateconstants, but the Root always has to be a
member of this set.

    AState : type+ = finite_set[State]
    C1 : AState = add(StateS1, add(StateRoot, emptyset))

Because my problem has to search for such sets and it is not very good to
define such sets (like C1) by myself because there can be to many (and it
must be used with model-checking) And now the problem
arises:

The first theorem ("existstheorem") returns a QED. So there exists a
correctly formed subset which is C1. If I reject the second argument
(c=C1) I expect also a QED because we know there exists a correctly formed
subset. (C1 or another subset that contains the RootState). However this
QED is not generated.

  existstheorem: theorem exists(c:AState | subset?(c, States(sm))):
                           member(Root(sm), c) and c=C1
  existstheorem2: theorem exists(c:AState | subset?(c, States(sm))): member(Root(sm), c)

What am I missing? How can I force PVS to return a QED.
I also included the dumpfile.

Thx for the help,

Sara


%% PVS Version 3.0
%% 6.2 [Linux (x86)] (Dec 19, 2002 3:09)
$$$problem.pvs
problem : theory
  begin

    % Define some specific types and elements of that type
    State: Type+
    
    StateS1: State
    StateS2: State
    StateS3: State
    StateRoot: State

    % Define a set that contains State-elements
    StateSet: type+ = finite_set[State]
 
    % Define the following record
    StateRecord : type+ = [# States : StateSet,
                             Root : State #] 

    % Define a specific record
    sm : StateRecord = (# States := add(StateS1, add(StateS2, add(StateS3, add(StateRoot, emptyset)))),
                          Root   := StateRoot #) 

    % Define another sets of states
    AState : type+ = finite_set[State]

    C1 : AState = add(StateS1, add(StateRoot, emptyset))

    % Now I want to check the following theorem
    % Does there exists a set, subset of States, which contains the RootState? 
    %  (it must be automatically be found...)
    % The first theorem returns QED ... doest such a set can be found

    % The second theorem doesn`t return that. However we know that such a set exists, so 
    % I expect also a QED. What am I missing here? 
    existstheorem: theorem exists(c:AState | subset?(c, States(sm))): 
                           member(Root(sm), c) and c=C1
    existstheorem2: theorem exists(c:AState | subset?(c, States(sm))): member(Root(sm), c) 
    

  end problem

$$$problem.prf
(problem
 (existstheorem 0
  (existstheorem-1 nil 3223270809 3223270893 ("" (grind) nil nil)
   unchecked
   ((C1 const-decl "AState" problem nil)
    (member const-decl "bool" sets nil)
    (sm const-decl "StateRecord" problem nil)
    (emptyset const-decl "set" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (subset? const-decl "bool" sets nil))
   7765 170 t shostak))
 (existstheorem2 0
  (existstheorem2-1 nil 3223270991 3223270995 ("" (grind) nil nil)
   proved
   ((sm const-decl "StateRecord" problem nil)
    (member const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (subset? const-decl "bool" sets nil)
    (C1 const-decl "AState" problem nil))
   3234 350 t shostak)))