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

Re: [PVS-Help] How to define a step for splitting withoutgenerating redundant TCCs

Hi Johannes,

I also write strategies and I'm constantly frustrated by the problem you
mention. I have a solution, but it's a hack that uses some low level PVS
manipulations I'm not proud of.

Let me tell you what I know about this problem.

First, let me decouple your problem in two problems. One is easy to solve,
the other one is not.

In PVS, when you use (split) you loose information. As you have certainly
noticed, when you have a consequent

{1}   a AND b

Rule? (split 1)
Splitting conjunctions,
this yields  2 subgoals:
foo0.1 :  

{1}   a

foo0.2 :  

{1}   b

The fact that you can use "a" to prove "b" is gone. For that reason, I
created the strategy SPLASH, which is available as part of the NASA PVS

Rule? (splash 1)

Splashing formula 1,
this yields  2 subgoals:
foo0.1 :  

{-1}  a
{1}   b

foo0.2 :  

{1}   a

Now, the second problem. Let's say that you have the following definition

a(x:posreal) : bool

and then a sequent with a "top level" expression:


any occurrence of "a(very_long_and_complex_expression)" as an explicit
parameter of a strategy, e.g., name, name-replace, case, etc,  will generate
a TCC sub-goal "very_long_and_complex_expression > 0".

I believe that this TCC is not needed as, by construction, it can be checked
that the TCC was already generated when the expression appeared for the
first time in the sequent.

When doing proofs interactively, this is not a big deal because in every
case, it is possible to use a "case" with the TCC before any manipulation
and thus the TCCs become trivial. But it's a nightmare for writing
strategies since TCCs are not easily to preview beforehand.

As consequence of this behavior in the PVS typechecker, my SPLASH strategy,
which is based on CASE, will generate the unwanted TCC
"very_long_and_complex_expression > 0".

In PVS 3.2  (see Release Notes
two new strategies were implemented: typepred! rule and all-typepreds
strategy. These strategies are supposed to add as hypothesis all
type-information that is available for an expression or a sequent at a given

However, for some reason, they don't work in this case:

foo :  

{1}   a(very_long_and_complex_expression) AND b

Rule? (all-typepreds 1)
Generating typepreds for expressions:
No change on: (all-typepreds 1)
foo :  

{1}   a(very_long_and_complex_expression) AND b

(typepred! "a(very_long_and_complex_expression)" :implicit? t)
No top-level occurrences of any of the terms in
 yielded type constraints
No change on: (typepred! "a(very_long_and_complex_expression)"
               :implicit? t)
foo :  

{1}   a(very_long_and_complex_expression) AND b

In both cases, I would have expected the following formula to be added as
hypothesis: "very_long_and_complex_expression > 0"

> Thanks. However, the theories I am dealing with are generated by a
> tool in a certain way that I would like to avoid changing at this
> point. Hence my interest in achieving this with a strategy.
> Johannes
> --
> Johannes W. E. Eriksson, M.Sc.
> Ph.D. Student / Turku Centre For Computer Science (TUCS)
> Åbo Akademi University / Department of Information Technologies
> e-mail: joheriks@abo.fi  www: http://www.abo.fi/~joheriks

Cesar A. Munoz                             NASA Langley Research Center
Cesar.A.Munoz@nasa.gov                     Bldg. 1220  Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234