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

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



Note that I’ve solved my problem by using this lemma:
(lemma "both_sides_plus_ge1" ("x" "p_Data_Type_Conversion - 1" "y" "0" "z" "1"))

…but I’m still puzzled as to how (both-sides) is supposed to be used, and how I ended up with my FALSE = TRUE statement.

Best Regards,
Ben Hocking

On May 23, 2016, at 11:54 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

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