Examples/solovay.ml

   1 (* ========================================================================= *)
   2 (* Simple universal variant of Bob Solovay's procedure for vector spaces.    *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/misc.ml";;
   6 needs "Multivariate/vectors.ml";;
   7
   8 (* ------------------------------------------------------------------------- *)
   9 (* Initial simplification so we just use dot products between vectors.       *)
  10 (* ------------------------------------------------------------------------- *)
  11
  12 let VECTOR_SUB_ELIM_THM = prove
  13  (`(--x = --(&1) % x) /\
  14    (x - y = x + --(&1) % y)`,
  15   VECTOR_ARITH_TAC);;
  16
  17 let NORM_ELIM_THM = prove
  18  (`!P t. P (norm t) = !x. &0 <= x /\ (x pow 2 = (t:real^N) dot t) ==> P x`,
  19   GEN_TAC THEN REWRITE_TAC[vector_norm] THEN
  20   MESON_TAC[DOT_POS_LE; SQRT_POW2; SQRT_UNIQUE;
  21             REAL_POW_2; REAL_POW2_ABS; REAL_ABS_POS]);;
  22
  23 let NORM_ELIM_CONV =
  24   let dest_norm tm =
  25     let nm,v = dest_comb tm in
  26     if fst(dest_const nm) <> "vector_norm" then failwith "dest_norm"
  27     else v in
  28   let is_norm = can dest_norm in
  29   fun tm ->
  30     let t = find_term (fun t -> is_norm t & free_in t tm) tm in
  31     let v = dest_norm t in
  32     let w = genvar(type_of t) in
  33     let th1 = ISPECL [mk_abs(w,subst[w,t] tm); v] NORM_ELIM_THM in
  34     CONV_RULE(COMB2_CONV (RAND_CONV BETA_CONV)
  35                          (BINDER_CONV(RAND_CONV BETA_CONV))) th1;;
  36
  37 let NORM_ELIM_TAC =
  38   CONV_TAC NORM_ELIM_CONV THEN GEN_TAC;;
  39
  40 let SOLOVAY_TAC =
  41   REWRITE_TAC[orthogonal; GSYM DOT_EQ_0] THEN
  42   REWRITE_TAC[VECTOR_EQ] THEN
  43   REWRITE_TAC[VECTOR_SUB_ELIM_THM] THEN
  44   REWRITE_TAC[NORM_EQ; NORM_LE; NORM_LT; real_gt; real_ge] THEN
  45   REPEAT NORM_ELIM_TAC THEN
  46   REWRITE_TAC[DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL];;
  47
  48 (* ------------------------------------------------------------------------- *)
  49 (* Iterative Gram-Schmidt type process.                                      *)
  50 (* ------------------------------------------------------------------------- *)
  51
  52 let component = new_definition
  53   `component (b:real^N) x = (b dot x) / (b dot b)`;;
  54
  55 let COMPONENT_ORTHOGONAL = prove
  56  (`!b:real^N x. orthogonal b (x - (component b x) % b)`,
  57   REPEAT GEN_TAC THEN ASM_CASES_TAC `b = vec 0 :real^N` THENL
  58    [ASM_REWRITE_TAC[orthogonal; DOT_LZERO]; ALL_TAC] THEN
  59   ASM_SIMP_TAC[orthogonal; component] THEN
  60   REWRITE_TAC[DOT_RSUB; DOT_RMUL] THEN
  61   ASM_SIMP_TAC[REAL_SUB_REFL; REAL_DIV_RMUL; DOT_EQ_0]);;
  62
  63 let ORTHOGONAL_SUM_LEMMA = prove
  64  (`!cs vs.
  65        ALL (orthogonal x) vs /\ orthogonal x z /\ (LENGTH cs = LENGTH vs)
  66         ==> orthogonal x (ITLIST2 (\a v s. a % v + s) cs vs z)`,
  67   LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN
  68   REWRITE_TAC[NOT_CONS_NIL; NOT_SUC; ITLIST2; LENGTH; ALL] THEN
  69   ASM_SIMP_TAC[ORTHOGONAL_CLAUSES; SUC_INJ]);;
  70
  71 let GRAM_SCHMIDT_LEMMA = prove
  72  (`!w:real^N vs. ?u as.
  73         ALL (orthogonal u) vs /\ (LENGTH as = LENGTH vs) /\
  74         (w = ITLIST2 (\a v s. a % v + s) as vs u)`,
  75   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN MATCH_MP_TAC list_INDUCT THEN
  76   SIMP_TAC[ALL; LENGTH; ITLIST2; LENGTH_EQ_NIL] THEN CONJ_TAC THENL
  77    [X_GEN_TAC `w:real^N` THEN EXISTS_TAC `w:real^N` THEN
  78     EXISTS_TAC `[]:real list` THEN REWRITE_TAC[ITLIST2];
  79     ALL_TAC] THEN
  80   MAP_EVERY X_GEN_TAC [`v:real^N`; `vs:(real^N)list`] THEN
  81   REWRITE_TAC[LENGTH_EQ_CONS] THEN DISCH_TAC THEN X_GEN_TAC `w:real^N` THEN
  82   FIRST_X_ASSUM(fun th ->
  83      MP_TAC(SPEC `w:real^N` th) THEN MP_TAC(SPEC `v:real^N` th)) THEN
  84   DISCH_THEN(X_CHOOSE_THEN `z:real^N` (X_CHOOSE_THEN `cs:real list`
  85     (STRIP_ASSUME_TAC o GSYM))) THEN
  86   DISCH_THEN(X_CHOOSE_THEN `u:real^N` (X_CHOOSE_THEN `as:real list`
  87     (STRIP_ASSUME_TAC o GSYM))) THEN
  88   MP_TAC(ISPECL [`z:real^N`; `u:real^N`] COMPONENT_ORTHOGONAL) THEN
  89   ABBREV_TAC `k = component z (u:real^N)` THEN
  90   ABBREV_TAC `x = u - k % z :real^N` THEN DISCH_TAC THEN
  91   MAP_EVERY EXISTS_TAC
  92    [`x:real^N`; `CONS k (MAP2 (\a c. a - k * c) as cs)`] THEN
  93   REWRITE_TAC[CONS_11; RIGHT_EXISTS_AND_THM; GSYM CONJ_ASSOC; UNWIND_THM1] THEN
  94   SUBGOAL_THEN `ALL (orthogonal(x:real^N)) vs` ASSUME_TAC THENL
  95    [UNDISCH_TAC `ALL (orthogonal(z:real^N)) vs` THEN
  96     UNDISCH_TAC `ALL (orthogonal(u:real^N)) vs` THEN
  97     REWRITE_TAC[IMP_IMP; AND_ALL] THEN
  98     MATCH_MP_TAC MONO_ALL THEN REWRITE_TAC[] THEN
  99     EXPAND_TAC "x" THEN SIMP_TAC[ORTHOGONAL_CLAUSES];
 100     ALL_TAC] THEN
 101   REPEAT CONJ_TAC THENL
 102    [EXPAND_TAC "v" THEN MATCH_MP_TAC ORTHOGONAL_SUM_LEMMA THEN
 103     ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[ORTHOGONAL_SYM];
 104     FIRST_ASSUM ACCEPT_TAC;
 105     ASM_MESON_TAC[LENGTH_MAP2];
 106     ALL_TAC] THEN
 107   REWRITE_TAC[ITLIST2; VECTOR_ARITH `(a = b + c:real^N) = (c = a - b)`] THEN
 108   MAP_EVERY EXPAND_TAC ["v"; "w"; "x"] THEN
 109   UNDISCH_TAC `LENGTH(vs:(real^N)list) = LENGTH(cs:real list)` THEN
 110   UNDISCH_TAC `LENGTH(vs:(real^N)list) = LENGTH(as:real list)` THEN
 111   REWRITE_TAC[IMP_CONJ] THEN
 112   MAP_EVERY (fun v -> SPEC_TAC(v,v))
 113    [`vs:(real^N)list`; `cs:real list`; `as:real list`] THEN
 114   POP_ASSUM_LIST(K ALL_TAC) THEN
 115   LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN
 116   REWRITE_TAC[NOT_CONS_NIL; NOT_SUC; ITLIST2; LENGTH; ALL; SUC_INJ; MAP2] THEN
 117   ASM_SIMP_TAC[] THEN REPEAT DISCH_TAC THEN VECTOR_ARITH_TAC);;
 118
 119 (* ------------------------------------------------------------------------- *)
 120 (* Hence this is a simple equality.                                          *)
 121 (* ------------------------------------------------------------------------- *)
 122
 123 let SOLOVAY_LEMMA = prove
 124  (`!P vs. (!w:real^N. P w vs) =
 125           (!as u. ALL (orthogonal u) vs /\ (LENGTH as = LENGTH vs)
 126                   ==> P (ITLIST2 (\a v s. a % v + s) as vs u) vs)`,
 127   REPEAT GEN_TAC THEN EQ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN DISCH_TAC THEN
 128   X_GEN_TAC `w:real^N` THEN
 129   MP_TAC(ISPECL [`w:real^N`; `vs:(real^N)list`] GRAM_SCHMIDT_LEMMA) THEN
 130   ASM_MESON_TAC[]);;
 131
 132 (* ------------------------------------------------------------------------- *)
 133 (* Set up the specific instances to get rid of list stuff.                   *)
 134 (* ------------------------------------------------------------------------- *)
 135
 136 let FORALL_LENGTH_CLAUSES = prove
 137  (`((!l. (LENGTH l = 0) ==> P l) = P []) /\
 138    ((!l. (LENGTH l = SUC n) ==> P l) =
 139          (!h t. (LENGTH t = n) ==> P (CONS h t)))`,
 140   MESON_TAC[LENGTH; LENGTH_EQ_NIL; NOT_SUC; LENGTH_EQ_CONS]);;
 141
 142 let ORTHOGONAL_SIMP_CLAUSES = prove
 143  (`orthogonal u x
 144    ==> (u dot x = &0) /\ (x dot u = &0) /\
 145        (u dot (a % x) = &0) /\ ((a % x) dot u = &0) /\
 146        (u dot (a % x + y) = u dot y) /\ ((a % x + y) dot u = y dot u) /\
 147        (u dot (y + a % x) = u dot y) /\ ((y + a % x) dot u = y dot u)`,
 148   SIMP_TAC[orthogonal; DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL] THEN
 149   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [DOT_SYM] THEN
 150   SIMP_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_ADD_LID; REAL_ADD_RID]);;
 151
 152 (* ------------------------------------------------------------------------- *)
 153 (* A nicer proforma version.                                                 *)
 154 (* ------------------------------------------------------------------------- *)
 155
 156 let ITLIST2_0_LEMMA = prove
 157  (`!u as vs. ITLIST2 (\a v s. a % v + s) as vs u =
 158              ITLIST2 (\a v s. a % v + s) as vs (vec 0) + u`,
 159   GEN_TAC THEN LIST_INDUCT_TAC THEN
 160   REWRITE_TAC[ITLIST2_DEF; VECTOR_ADD_LID] THEN
 161   ASM_REWRITE_TAC[VECTOR_ADD_ASSOC]);;
 162
 163 let SOLOVAY_PROFORMA_EQ = prove
 164  (`(!w:real^N. P (MAP ((dot) w) (CONS w vs)) vs) =
 165    (!u. ALL (orthogonal u) vs
 166         ==> !as. (LENGTH as = LENGTH vs)
 167                  ==> P (CONS
 168                           ((ITLIST2 (\a v s. a % v + s) as vs (vec 0)) dot
 169                            (ITLIST2 (\a v s. a % v + s) as vs (vec 0)) +
 170                            u dot u)
 171                           (MAP ((dot)
 172                                 (ITLIST2 (\a v s. a % v + s) as vs (vec 0)))
 173                                vs))
 174                  vs)`,
 175   MP_TAC(ISPEC `\w:real^N vs.  P (MAP ((dot) w) (CONS w vs)) vs :bool`
 176                SOLOVAY_LEMMA) THEN
 177   REWRITE_TAC[] THEN
 178   DISCH_THEN(fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
 179   GEN_REWRITE_TAC LAND_CONV [SWAP_FORALL_THM] THEN
 180   AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
 181   X_GEN_TAC `u:real^N` THEN REWRITE_TAC[] THEN
 182   REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
 183   AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
 184   X_GEN_TAC `as:(real)list` THEN REWRITE_TAC[IMP_IMP] THEN
 185   MATCH_MP_TAC(TAUT `(a ==> (b = c)) ==> (a ==> b <=> a ==> c)`) THEN
 186   STRIP_TAC THEN REWRITE_TAC[MAP] THEN BINOP_TAC THEN
 187   REWRITE_TAC[CONS_11] THEN ONCE_REWRITE_TAC[ITLIST2_0_LEMMA] THEN
 188   REWRITE_TAC[VECTOR_ADD_RID] THEN
 189   REWRITE_TAC[VECTOR_ARITH
 190    `(a + u) dot (a + u) = a dot a + &2 * (u dot a) + u dot u`] THEN
 191   REWRITE_TAC[REAL_ARITH `(a + &2 * b + c = a + c) <=> (b = &0)`] THEN
 192   GEN_REWRITE_TAC (RAND_CONV o BINOP_CONV o LAND_CONV) [GSYM ETA_AX] THEN
 193   REWRITE_TAC[DOT_LADD] THEN CONJ_TAC THENL
 194    [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
 195     SPEC_TAC(`vs:(real^N)list`,`vs:(real^N)list`) THEN
 196     SPEC_TAC(`as:(real)list`,`as:(real)list`) THEN
 197     REPEAT LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; NOT_SUC] THEN
 198     REWRITE_TAC[ALL; ITLIST2; DOT_RZERO; SUC_INJ] THEN
 199     ASM_SIMP_TAC[DOT_RADD] THEN
 200     REWRITE_TAC[REAL_ADD_RID; DOT_RMUL] THEN
 201     SIMP_TAC[orthogonal] THEN REWRITE_TAC[REAL_MUL_RZERO];
 202     MATCH_MP_TAC MAP_EQ THEN
 203     REWRITE_TAC[REAL_ARITH `(a + b = a) <=> (b = &0)`] THEN
 204     MATCH_MP_TAC ALL_IMP THEN EXISTS_TAC `orthogonal (u:real^N)` THEN
 205     ASM_REWRITE_TAC[] THEN SIMP_TAC[orthogonal]]);;
 206
 207 (* ------------------------------------------------------------------------- *)
 208 (* The implication that we normally use.                                     *)
 209 (* ------------------------------------------------------------------------- *)
 210
 211 let SOLOVAY_PROFORMA = prove
 212  (`!P vs.
 213    (!c. &0 <= c
 214         ==> !as. (LENGTH as = LENGTH vs)
 215                  ==> P (CONS ((ITLIST2 (\a v s. a % v + s) as vs (vec 0)) dot
 216                               (ITLIST2 (\a v s. a % v + s) as vs (vec 0)) + c)
 217                              (MAP ((dot)
 218                                    (ITLIST2 (\a v s. a % v + s) as vs (vec 0)))
 219                                   vs))
 220                     vs)
 221    ==> !w:real^N. P (MAP ((dot) w) (CONS w vs)) vs`,
 222   REPEAT GEN_TAC THEN
 223   GEN_REWRITE_TAC RAND_CONV [SOLOVAY_PROFORMA_EQ] THEN
 224   REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP] THEN
 225   REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
 226   ASM_REWRITE_TAC[DOT_POS_LE]);;
 227
 228 (* ------------------------------------------------------------------------- *)
 229 (* Automatically set up an implication for n (+1 eliminated) quantifier.     *)
 230 (* ------------------------------------------------------------------------- *)
 231
 232 let SOLOVAY_RULE =
 233   let v_tm = `v:(real^N)list` and d_tm = `d:real list`
 234   and elv_tm = `EL:num->(real^N)list->real^N`
 235   and eld_tm = `EL:num->(real)list->real`
 236   and rn_ty = `:real^N`
 237   and rewr_rule = REWRITE_RULE
 238    [MAP; EL; HD; TL; LENGTH; FORALL_LENGTH_CLAUSES;
 239     ITLIST2; VECTOR_ADD_RID; VECTOR_ADD_LID; DOT_LZERO]
 240   and sewr_rule = PURE_ONCE_REWRITE_RULE[DOT_SYM] in
 241   fun n ->
 242     let args =
 243       map (fun i -> mk_comb(mk_comb(elv_tm,mk_small_numeral i),v_tm))
 244           (0--(n-1)) @
 245       map (fun i -> mk_comb(mk_comb(eld_tm,mk_small_numeral i),d_tm))
 246           (1--n) @
 247       [mk_comb(mk_comb(eld_tm,mk_small_numeral 0),d_tm)] in
 248     let pty = itlist (mk_fun_ty o type_of) args bool_ty in
 249     let p_tm = list_mk_abs([d_tm;v_tm],list_mk_comb(mk_var("P",pty),args))
 250     and vs = make_args "v" [] (replicate rn_ty n) in
 251     let th1 = ISPECL [p_tm; mk_list(vs,rn_ty)] SOLOVAY_PROFORMA in
 252     let th2 = rewr_rule(CONV_RULE(TOP_DEPTH_CONV num_CONV) th1) in
 253     let th3 = sewr_rule th2 in
 254     itlist (fun v -> MATCH_MP MONO_FORALL o GEN v) vs th3;;
 255
 256 (* ------------------------------------------------------------------------- *)
 257 (* Now instantiate it to some special cases.                                 *)
 258 (* ------------------------------------------------------------------------- *)
 259
 260 let MK_SOLOVAY_PROFORMA =
 261   let preths = map SOLOVAY_RULE (0--9) in
 262   fun n -> if n < 10 then el n preths else SOLOVAY_RULE n;;
 263
 264 (* ------------------------------------------------------------------------- *)
 265 (* Apply it to a goal.                                                       *)
 266 (* ------------------------------------------------------------------------- *)
 267
 268 let is_vector_ty ty =
 269   match ty with
 270    Tyapp("cart",[Tyapp("real",[]);_]) -> true
 271   | _ -> false;;
 272
 273 let SOLOVAY_REDUCE_TAC (asl,w) =
 274   let avs = sort (<) (filter (is_vector_ty o type_of) (frees w)) in
 275   (REWRITE_TAC[DOT_SYM] THEN
 276    MAP_EVERY (fun v -> SPEC_TAC(v,v)) (rev avs) THEN
 277    MATCH_MP_TAC(MK_SOLOVAY_PROFORMA (length avs - 1)) THEN
 278    REWRITE_TAC[DOT_LADD; DOT_LMUL; DOT_RADD; DOT_RMUL; DOT_LZERO;
 279                DOT_RZERO] THEN
 280    REPEAT GEN_TAC) (asl,w);;
 281
 282 (* ------------------------------------------------------------------------- *)
 283 (* Overall tactic.                                                           *)
 284 (* ------------------------------------------------------------------------- *)
 285
 286 let SOLOVAY_VECTOR_TAC =
 287   REWRITE_TAC[dist; real_gt; real_ge; NORM_LT; NORM_LE; GSYM DOT_POS_LT] THEN
 288   REPEAT GEN_TAC THEN SOLOVAY_TAC THEN
 289   REWRITE_TAC[DOT_LZERO; DOT_RZERO] THEN
 290   REPEAT SOLOVAY_REDUCE_TAC THEN
 291   REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_MUL_LID; REAL_MUL_RID;
 292               REAL_ADD_LID; REAL_ADD_RID] THEN
 293   REWRITE_TAC[IMP_IMP; RIGHT_IMP_FORALL_THM; GSYM CONJ_ASSOC] THEN
 294   REPEAT GEN_TAC THEN
 295   REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG;
 296               REAL_MUL_LID; REAL_MUL_RID; GSYM real_sub];;
 297
 298 (* ------------------------------------------------------------------------- *)
 299 (* An example where REAL_RING then works.                                    *)
 300 (* ------------------------------------------------------------------------- *)
 301
 302 let PYTHAGORAS = prove
 303  (`!A B C:real^N.
 304         orthogonal (A - B) (C - B)
 305         ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2`,
 306   SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_RING);;
 307
 308 (*** Actually in this case we can fairly easily do things manually, though
 309      we do need to explicitly use symmetry of the dot product.
 310
 311 let PYTHAGORAS = prove
 312  (`!A B C:real^N.
 313         orthogonal (A - B) (C - B)
 314         ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2`,
 315   REWRITE_TAC[NORM_POW_2; orthogonal; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
 316   CONV_TAC REAL_RING);;
 317
 318  ***)
 319
 320 (* ------------------------------------------------------------------------- *)
 321 (* Examples.                                                                 *)
 322 (* ------------------------------------------------------------------------- *)
 323
 324 needs "Examples/sos.ml";;
 325
 326 let EXAMPLE_1 = prove
 327  (`!x y:real^N. x dot y <= norm x * norm y`,
 328   SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_SOS);;
 329
 330 let EXAMPLE_2 = prove
 331  (`!x y:real^N. a % (x + y) = a % x + a % y`,
 332   SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_SOS);;
 333
 334 (*** Takes a few minutes but does work
 335
 336 let EXAMPLE_3 = prove
 337  (`!x y:real^N. norm (x + y) <= norm x + norm y`,
 338   SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_SOS);;
 339
 340 ****)
 341
 342 let EXAMPLE_4 = prove
 343  (`!x y z. x dot (y + z) = (x dot y) + (x dot z)`,
 344   SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_SOS);;
 345
 346 let EXAMPLE_5 = prove
 347  (`!x y. (x dot x = &0) ==> (x dot y = &0)`,
 348   SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_SOS);;
 349
 350 (* ------------------------------------------------------------------------- *)
 351 (* This is NORM_INCREASES_ONLINE.                                            *)
 352 (* ------------------------------------------------------------------------- *)
 353
 354 g `!a d:real^N.
 355     ~(d = vec 0) ==> norm (a + d) > norm a \/ norm (a - d) > norm a`;;
 356
 357 time e SOLOVAY_VECTOR_TAC;;
 358
 359 time e (CONV_TAC REAL_SOS);;
 360
 361 (* ------------------------------------------------------------------------- *)
 362 (* DIST_INCREASES_ONLINE                                                     *)
 363 (* ------------------------------------------------------------------------- *)
 364
 365 g `!b a d:real^N.
 366     ~(d = vec 0) ==> dist(a,b + d) > dist(a,b) \/ dist(a,b - d) > dist(a,b)`;;
 367
 368 time e SOLOVAY_VECTOR_TAC;;
 369
 370 time e (CONV_TAC REAL_SOS);;
 371
 372 (* ------------------------------------------------------------------------- *)
 373 (* This one doesn't seem to work easily, but I think it does eventually.     *)
 374 (* ------------------------------------------------------------------------- *)
 375
 376 (****
 377 let EXAMPLE_6 = prove
 378  (`!a x. norm(a % x) = abs(a) * norm x`;;
 379   SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_SOS);;
 380  ****)
 381
 382 let EXAMPLE_7 = prove
 383  (`!x. abs(norm x) = norm x`,
 384    SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_SOS);;
 385
 386 (*** But this is (at least) really slow
 387
 388 let EXAMPLE_8 = prove
 389  (`!x y. abs(norm(x) - norm(y)) <= abs(norm(x - y))`,
 390   SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_SOS);;
 391 ****)
 392
 393 (* ------------------------------------------------------------------------- *)
 394 (* One from separating hyperplanes with a richer structure.                  *)
 395 (* ------------------------------------------------------------------------- *)
 396
 397 needs "Rqe/make.ml";;
 398
 399 let EXAMPLE_9 = prove
 400  (`!x:real^N y. x dot y > &0 ==> ?u. &0 < u /\ norm(u % y - x) < norm x`,
 401   SOLOVAY_VECTOR_TAC THEN
 402   W(fun (asl,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) THEN
 403   CONV_TAC REAL_QELIM_CONV);;
 404
 405 (* ------------------------------------------------------------------------- *)
 406 (* Even richer set of quantifier alternations.                               *)
 407 (* ------------------------------------------------------------------------- *)
 408
 409 let EXAMPLE_10 = prove
 410  (`!x:real^N y.
 411         x dot y > &0
 412         ==> ?u. &0 < u /\
 413                 !v. &0 < v /\ v <= u ==> norm(v % y - x) < norm x`,
 414   SOLOVAY_VECTOR_TAC THEN
 415   W(fun (asl,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) THEN
 416   CONV_TAC REAL_QELIM_CONV);;