1 (* ========================================================================= *)
2 (* Simple universal variant of Bob Solovay's procedure for vector spaces. *)
3 (* ========================================================================= *)
5 needs "Multivariate/misc.ml";;
6 needs "Multivariate/vectors.ml";;
8 (* ------------------------------------------------------------------------- *)
9 (* Initial simplification so we just use dot products between vectors. *)
10 (* ------------------------------------------------------------------------- *)
12 let VECTOR_SUB_ELIM_THM = prove
13 (`(--x = --(&1) % x) /\
14 (x - y = x + --(&1) % y)`,
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]);;
25 let nm,v = dest_comb tm in
26 if fst(dest_const nm) <> "vector_norm" then failwith "dest_norm"
28 let is_norm = can dest_norm in
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;;
38 CONV_TAC NORM_ELIM_CONV THEN GEN_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];;
48 (* ------------------------------------------------------------------------- *)
49 (* Iterative Gram-Schmidt type process. *)
50 (* ------------------------------------------------------------------------- *)
52 let component = new_definition
53 `component (b:real^N) x = (b dot x) / (b dot b)`;;
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]);;
63 let ORTHOGONAL_SUM_LEMMA = prove
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]);;
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];
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
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];
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];
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);;
119 (* ------------------------------------------------------------------------- *)
120 (* Hence this is a simple equality. *)
121 (* ------------------------------------------------------------------------- *)
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
132 (* ------------------------------------------------------------------------- *)
133 (* Set up the specific instances to get rid of list stuff. *)
134 (* ------------------------------------------------------------------------- *)
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]);;
142 let ORTHOGONAL_SIMP_CLAUSES = prove
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]);;
152 (* ------------------------------------------------------------------------- *)
153 (* A nicer proforma version. *)
154 (* ------------------------------------------------------------------------- *)
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]);;
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)
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)) +
172 (ITLIST2 (\a v s. a % v + s) as vs (vec 0)))
175 MP_TAC(ISPEC `\w:real^N vs. P (MAP ((dot) w) (CONS w vs)) vs :bool`
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]]);;
207 (* ------------------------------------------------------------------------- *)
208 (* The implication that we normally use. *)
209 (* ------------------------------------------------------------------------- *)
211 let SOLOVAY_PROFORMA = prove
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)
218 (ITLIST2 (\a v s. a % v + s) as vs (vec 0)))
221 ==> !w:real^N. P (MAP ((dot) w) (CONS w vs)) vs`,
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]);;
228 (* ------------------------------------------------------------------------- *)
229 (* Automatically set up an implication for n (+1 eliminated) quantifier. *)
230 (* ------------------------------------------------------------------------- *)
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
243 map (fun i -> mk_comb(mk_comb(elv_tm,mk_small_numeral i),v_tm))
245 map (fun i -> mk_comb(mk_comb(eld_tm,mk_small_numeral i),d_tm))
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;;
256 (* ------------------------------------------------------------------------- *)
257 (* Now instantiate it to some special cases. *)
258 (* ------------------------------------------------------------------------- *)
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;;
264 (* ------------------------------------------------------------------------- *)
265 (* Apply it to a goal. *)
266 (* ------------------------------------------------------------------------- *)
268 let is_vector_ty ty =
270 Tyapp("cart",[Tyapp("real",[]);_]) -> true
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;
280 REPEAT GEN_TAC) (asl,w);;
282 (* ------------------------------------------------------------------------- *)
283 (* Overall tactic. *)
284 (* ------------------------------------------------------------------------- *)
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
295 REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG;
296 REAL_MUL_LID; REAL_MUL_RID; GSYM real_sub];;
298 (* ------------------------------------------------------------------------- *)
299 (* An example where REAL_RING then works. *)
300 (* ------------------------------------------------------------------------- *)
302 let PYTHAGORAS = prove
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);;
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.
311 let PYTHAGORAS = prove
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);;
320 (* ------------------------------------------------------------------------- *)
322 (* ------------------------------------------------------------------------- *)
324 needs "Examples/sos.ml";;
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);;
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);;
334 (*** Takes a few minutes but does work
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);;
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);;
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);;
350 (* ------------------------------------------------------------------------- *)
351 (* This is NORM_INCREASES_ONLINE. *)
352 (* ------------------------------------------------------------------------- *)
355 ~(d = vec 0) ==> norm (a + d) > norm a \/ norm (a - d) > norm a`;;
357 time e SOLOVAY_VECTOR_TAC;;
359 time e (CONV_TAC REAL_SOS);;
361 (* ------------------------------------------------------------------------- *)
362 (* DIST_INCREASES_ONLINE *)
363 (* ------------------------------------------------------------------------- *)
366 ~(d = vec 0) ==> dist(a,b + d) > dist(a,b) \/ dist(a,b - d) > dist(a,b)`;;
368 time e SOLOVAY_VECTOR_TAC;;
370 time e (CONV_TAC REAL_SOS);;
372 (* ------------------------------------------------------------------------- *)
373 (* This one doesn't seem to work easily, but I think it does eventually. *)
374 (* ------------------------------------------------------------------------- *)
377 let EXAMPLE_6 = prove
378 (`!a x. norm(a % x) = abs(a) * norm x`;;
379 SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_SOS);;
382 let EXAMPLE_7 = prove
383 (`!x. abs(norm x) = norm x`,
384 SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_SOS);;
386 (*** But this is (at least) really slow
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);;
393 (* ------------------------------------------------------------------------- *)
394 (* One from separating hyperplanes with a richer structure. *)
395 (* ------------------------------------------------------------------------- *)
397 needs "Rqe/make.ml";;
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);;
405 (* ------------------------------------------------------------------------- *)
406 (* Even richer set of quantifier alternations. *)
407 (* ------------------------------------------------------------------------- *)
409 let EXAMPLE_10 = prove
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);;