Re: [Hol-info] Problem with SOS examples in HOL Light

[John H. <Joh...@cl...>]

Hi Madalina,

| I'm doing some tests with HOL Light, namely with the SOS
| implementation and I have unexpected results (although in the tutorial
| and in the paper describing the technique the result is different).

I think this may just be a typing issue. Note that numerals are   
interpreted as natural numbers (type :num) rather than reals, and
this gives all your subexpressions type :num as well. Your problem
should work if you use the natural number version SOS_RULE:

  SOS_RULE 
   `a1>=0 /\ a2>=0 /\
    (a1*a1 + a2*a2 = b1*b1 +b2*b2 +2) /\ 
    (a1*b1 + a2*b2 = 0) 
    ==> a1*a2 -b1*b2 >= 0`;;

or if you explicitly make the type :real, adding the type coercion
"&" to numerals:

 REAL_SOS
   `a1:real >= &0 /\ a2 >= &0 /\
    (a1*a1 + a2*a2 = b1*b1 +b2*b2 + &2) /\                              
    (a1*b1 + a2*b2 = &0)
    ==> a1*a2 - b1*b2 >= &0`;;

| I wonder what is wrong because both tactics use CSDP. I meantion that
| I have installed the version of Ocaml from 10.01.2010.

In principle there can be differences depending on the CSDP version,
the linear algebra subroutines underneath it etc. However, this seems
quite rare; I've only encountered it once.

John.