[Hol-info] Different bug/feature in REAL_SOS

[Stephen B. <ste...@ve...>]

Okay, so I'm stubborn, but this time I've got the bug/feature of REAL_SOS
that I'd earlier tried to argue was different from the
embed-the-naturals-in-the-reals problem _SOS that I'd identified still
earlier. I thought I'd already tried the solution John Harrison proposed -
including facts about the natural numbers all being non-negative - and I
had; I made an error in trying to narrow down the problem before telling
Info-hol about it. Now I've isolated the problem:

 

For the two terms:

 

let badcase =
`T
 ==> &q > &0
 ==> ~(&q = &0)
 ==> &p pow 2 = &2 * &q pow 2
 ==> &0 <= &p
 ==> &0 <= &q
 ==> ~(&p + -- &1 * &q = &0)
 ==> &p pow 2 + -- &4 * &p * &q + &4 * &q pow 2 =
     &2 * &p pow 2 + -- &4 * &p * &q + &2 * &q pow 2
 ==> &p + -- &1 * &q > &0`;;
 
let goodcase =
`T
 ==> &q > &0
 ==> &p pow 2 = &2 * &q pow 2
 ==> &0 <= &p
 ==> &0 <= &q
 ==> ~(&p + -- &1 * &q = &0)
 ==> &p pow 2 + -- &4 * &p * &q + &4 * &q pow 2 =
     &2 * &p pow 2 + -- &4 * &p * &q + &2 * &q pow 2
 ==> &p + -- &1 * &q > &0`;;
 

REAL_SOS goodcase;; terminates with the desired theorem in a little over a
second.

REAL_SOS badcase;; doesn't terminate at all, as far as I know. The
difference is the hypothesis ~(&q = &0), which I'd assumed would be
redundant and harmless, since it follows from the hypothesis &q > &0. It
means less for a real number to not equal zero than it means for a natural
number to not equal zero, but things shouldn't hang. (Note that there's
another not-equal-zero hypothesis that doesn't cause a problem.) If this
isn't a bug, then it's something that the software and/or general knowledge
should warn about.

 

Steve