Example (20)

　前回の平方根の消去をconversionにしてみました．

let SQRT_SOS sqrt tm = prove
 (tm,
  REPEAT STRIP_TAC THEN
  REPEAT (FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP REAL_LT_IMP_LE))) THEN
  EVERY_ASSUM (MP_TAC o (MATCH_MP SQRT_POS_LE)) THEN
  MAP_EVERY ABBREV_TAC sqrt THEN
  REPEAT (FIRST_X_ASSUM (MP_TAC o (MATCH_MP SQRT_POW_2))) THEN
  ASM_SIMP_TAC[] THEN
  CONV_TAC REAL_SOS);;

　例えば

# SQRT_SOS[`a = sqrt x`]`&0 <= x ==> (x pow 2 + x * sqrt x <= &2 <=> &0 <= x /\
x <= &1)`;;
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 4
csdp warning: Reduced accuracy
csdp warning: Reduced accuracy
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 4
csdp warning: Reduced accuracy
Translating proof certificate to HOL
val it : thm =
  |- &0 <= x ==> (x pow 2 + x * sqrt x <= &2 <=> &0 <= x /\ x <= &1)

　さらに

let SQRT_SOS_TAC = CONV_TAC o SQRT_SOS;;

とすれば，tacticとして

# g`!x. &0 <= x ==> (sqrt(x + &3) = &3 - sqrt x <=> x = &1)`;;
val it : goalstack = 1 subgoal (1 total)

`!x. &0 <= x ==> (sqrt (x + &3) = &3 - sqrt x <=> x = &1)`

# e(ONCE_REWRITE_TAC[REAL_ARITH`&0 <= x <=> &0 <= x /\ &0 <= x + &3`]);;
val it : goalstack = 1 subgoal (1 total)

`!x. &0 <= x /\ &0 <= x + &3 ==> (sqrt (x + &3) = &3 - sqrt x <=> x = &1)`

# e(SQRT_SOS_TAC[`z=sqrt x`;`w=sqrt(x + &3)`]);;
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
csdp warning: Reduced accuracy
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
csdp warning: Reduced accuracy
csdp warning: Reduced accuracy
Translating proof certificate to HOL
val it : goalstack = No subgoals

のように使えます．