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

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



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