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

Re: [PVS-Help] Help with (both-sides) strategy



Hi Ben,

I'm having trouble recreating this.  With the spec

-----
test: THEORY
BEGIN
 p_Data_Type_Conversion: nat
 f: formula 1 <= p_Data_Type_Conversion => p_Data_Type_Conversion - 1 >= 0
END test
-----

I get:

f :  

  |-------
{1}   1 <= p_Data_Type_Conversion IMPLIES p_Data_Type_Conversion - 1 >= 0

Rule? (flatten)
Applying disjunctive simplification to flatten sequent,
this simplifies to: 
f :  

{-1}  1 <= p_Data_Type_Conversion
  |-------
{1}   p_Data_Type_Conversion - 1 >= 0

Rule? (both-sides "+" "1" 1)
Applying + 1 to both sides of an inequality/equality conjunction,
this simplifies to: 
f :  

[-1]  1 <= p_Data_Type_Conversion
  |-------
{1}   p_Data_Type_Conversion - 1 + 1 >= 0 + 1

Rule?

I suspect that the decision procedures have already recorded something in
your case that is affecting the behavior of both-sides (yours shows that
you're in the fourth branch of the proof).  Is it possible for you to send
me your specs?

Thanks,
Sam

Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

> From: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>
> Date: Mon, 23 May 2016 11:54:20 -0400
> To: pvs-help@xxxxxxxxxxx
> Subject: [PVS-Help] Help with (both-sides) strategy
> Sender: pvs-help-bounces+owre=csl.sri.com@xxxxxxxxxxx
> 
> I don’t use the (both-sides) strategy very often, so perhaps I’m using it wrong, but I’m not sure what I’m doing
> wrong in the following:
> Selector_TCC2.4 :
> 
> [-1] (1 <= p_Data_Type_Conversion)
> |-------
> [1] p_Data_Type_Conversion - 1 >= 0
> 
> Rule? (both-sides "+" "1" 1)
> Applying + 1 to both sides of an inequality/equality conjunction,
> this yields 3 subgoals:
> Selector_TCC2.4.1 :
> 
> [-1] (1 <= p_Data_Type_Conversion)
> |-------
> {1} p_Data_Type_Conversion - 1 + 1 >= 0 + 1
> 
> Rule? (grind)
> Trying repeated skolemization, instantiation, and if-lifting,
> 
> This completes the proof of Selector_TCC2.4.1.
> 
> Selector_TCC2.4.2 :
> 
> [-1] (1 <= p_Data_Type_Conversion)
> |-------
> {1} p_Data_Type_Conversion - 1 >= 0 =
> p_Data_Type_Conversion - 1 + 1 >= 0 + 1
> [2] p_Data_Type_Conversion - 1 >= 0
> 
> Rule? (assert)
> Simplifying, rewriting, and recording with decision procedures,
> this simplifies to:
> Selector_TCC2.4.2 :
> 
> [-1] (1 <= p_Data_Type_Conversion)
> |-------
> {1} FALSE = TRUE
> [2] p_Data_Type_Conversion - 1 >= 0
> 
> At this point, since {1} is clearly false, I’m back to where I started (notwithstanding an additional TCC to prove
> that real_pred(p_Data_Type_Conversion - 1), which can be proved with (lemma "reals.closed_minus" ("x"
> "p_Data_Type_Conversion" "y" "1"))).
> 
> Any idea what I’m doing wrong?
> 
> And how does:
> {1} p_Data_Type_Conversion - 1 >= 0 =
> p_Data_Type_Conversion - 1 + 1 >= 0 + 1
> get resolved to:
> {1} FALSE = TRUE
> upon using (assert)?
> 
> Best Regards,
> Ben Hocking
> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx