[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 Cesar,

thank you for your long informative reply, that clarified a great deal
to me. Though I use the NASA libs, I had not looked at the strategies, and so
ended up re-implementing SPLASH.

I was originally thinking along lines that since PVS already
identifies subsumption of TCCs in formula substructure, e.g. if I have
declared

l1: formula a(very_long_and_complex_expression)

then no addditional TCCs are generated for formulas involving
a(very_long_and_complex_expression), it would be possible to use the
same mechanism to discharge TCCs in proofs when
a(very_long_and_complex_expression) is used. But perhaps this is not
so, or not easily done.

Johannes


* Munoz, Cesar Augusto (LARC-D320) [Fri, Nov 27, 2009 at 10:21:16AM -0600]:
> 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
> libraries. 
> 
> 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:
> 
> a(very_long_and_complex_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".
> 
> TOWARDS A SOLUTION
> ------------------
> In PVS 3.2  (see Release Notes
> http://pvs.csl.sri.com/pvs-release-notes/pvs-release-notes_4.html#SEC35)
> 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
> time.
> 
> 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
> ("a(very_long_and_complex_expression)")
>  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"
> 
> 
> Cesar


-- 
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