(* ========================================================================= *)
(* Real vectors in Euclidean space, and elementary linear algebra. *)
(* *)
(* (c) Copyright, John Harrison 1998-2008 *)
(* ========================================================================= *)
needs "Multivariate/misc.ml";;
(* ------------------------------------------------------------------------- *)
(* Some common special cases. *)
(* ------------------------------------------------------------------------- *)
let FORALL_2 = prove
(`!P. (!i. 1 <= i /\ i <= 2 ==> P i) <=> P 1 /\ P 2`,
MESON_TAC[ARITH_RULE `1 <= i /\ i <= 2 <=> i = 1 \/ i = 2`]);;
let FORALL_3 = prove
(`!P. (!i. 1 <= i /\ i <= 3 ==> P i) <=> P 1 /\ P 2 /\ P 3`,
MESON_TAC[ARITH_RULE `1 <= i /\ i <= 3 <=> i = 1 \/ i = 2 \/ i = 3`]);;
let FORALL_4 = prove
(`!P. (!i. 1 <= i /\ i <= 4 ==> P i) <=> P 1 /\ P 2 /\ P 3 /\ P 4`,
MESON_TAC[ARITH_RULE `1 <= i /\ i <= 4 <=>
i = 1 \/ i = 2 \/ i = 3 \/ i = 4`]);;
(* ------------------------------------------------------------------------- *)
(* Basic componentwise operations on vectors. *)
(* ------------------------------------------------------------------------- *)
let vector_add = new_definition
`(vector_add:real^N->real^N->real^N) x y = lambda i. x$i + y$i`;;
let vector_sub = new_definition
`(vector_sub:real^N->real^N->real^N) x y = lambda i. x$i - y$i`;;
overload_interface ("+",`(vector_add):real^N->real^N->real^N`);;
overload_interface ("-",`(vector_sub):real^N->real^N->real^N`);;
overload_interface ("--",`(vector_neg):real^N->real^N`);;
prioritize_real();;
let prioritize_vector = let ty = `:real^N` in
fun () -> prioritize_overload ty;;
(* ------------------------------------------------------------------------- *)
(* Also the scalar-vector multiplication. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("%",(21,"right"));;
(* ------------------------------------------------------------------------- *)
(* Vectors corresponding to small naturals. Perhaps should overload "&"? *)
(* ------------------------------------------------------------------------- *)
let vec = new_definition
`(vec:num->real^N) n = lambda i. &n`;;
(* ------------------------------------------------------------------------- *)
(* Dot products. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("dot",(20,"right"));;
let dot = new_definition
`(x:real^N) dot (y:real^N) = sum(1..dimindex(:N)) (\i. x$i * y$i)`;;
let DOT_3 = prove
(`(x:real^3)
dot (y:real^3) = x$1 * y$1 + x$2 * y$2 + x$3 * y$3`,
let DOT_4 = prove
(`(x:real^4)
dot (y:real^4) = x$1 * y$1 + x$2 * y$2 + x$3 * y$3 + x$4 * y$4`,
(* ------------------------------------------------------------------------- *)
(* A naive proof procedure to lift really trivial arithmetic stuff from R. *)
(* ------------------------------------------------------------------------- *)
let VECTOR_ARITH_TAC =
let RENAMED_LAMBDA_BETA th =
if fst(dest_fun_ty(type_of(funpow 3 rand (concl th)))) = aty
then INST_TYPE [aty,bty; bty,aty] LAMBDA_BETA else LAMBDA_BETA in
POP_ASSUM_LIST(K ALL_TAC) THEN
REPEAT(GEN_TAC ORELSE CONJ_TAC ORELSE DISCH_TAC ORELSE EQ_TAC) THEN
REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC] THEN
REWRITE_TAC[dot; GSYM SUM_ADD_NUMSEG; GSYM SUM_SUB_NUMSEG;
GSYM SUM_LMUL; GSYM SUM_RMUL; GSYM SUM_NEG] THEN
(MATCH_MP_TAC SUM_EQ_NUMSEG ORELSE MATCH_MP_TAC SUM_EQ_0_NUMSEG ORELSE
GEN_REWRITE_TAC ONCE_DEPTH_CONV [CART_EQ]) THEN
REWRITE_TAC[AND_FORALL_THM] THEN TRY EQ_TAC THEN
TRY(MATCH_MP_TAC MONO_FORALL) THEN GEN_TAC THEN
REWRITE_TAC[TAUT `(a ==> b) /\ (a ==> c) <=> a ==> b /\ c`;
TAUT `(a ==> b) \/ (a ==> c) <=> a ==> b \/ c`] THEN
TRY(MATCH_MP_TAC(TAUT `(a ==> b ==> c) ==> (a ==> b) ==> (a ==> c)`)) THEN
REWRITE_TAC[vector_add; vector_sub; vector_neg; vector_mul; vec] THEN
DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP(RENAMED_LAMBDA_BETA th) th]) THEN
REAL_ARITH_TAC;;
let VECTOR_ARITH tm = prove(tm,VECTOR_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Obvious "component-pushing". *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some frequently useful arithmetic lemmas over vectors. *)
(* ------------------------------------------------------------------------- *)
let VECTOR_ADD_AC = VECTOR_ARITH
`(m + n = n + m:real^N) /\
((m + n) + p = m + n + p) /\
(m + n + p = n + m + p)`;;
(* ------------------------------------------------------------------------- *)
(* Infinitude of Euclidean space. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Properties of the dot product. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Introduce norms, but defer many properties till we get square roots. *)
(* ------------------------------------------------------------------------- *)
make_overloadable "norm" `:A->real`;;
overload_interface("norm",`vector_norm:real^N->real`);;
(* ------------------------------------------------------------------------- *)
(* Useful for the special cases of 1 dimension. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* The collapse of the general concepts to the real line R^1. *)
(* ------------------------------------------------------------------------- *)
let FORALL_REAL_ONE = prove
(`(!x:real^1. P x) <=> (!x. P(
lambda i. x))`,
EQ_TAC THEN SIMP_TAC[] THEN DISCH_TAC THEN GEN_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `(x:real^1)$1`) THEN
REWRITE_TAC[GSYM
VECTOR_ONE]);;
(* ------------------------------------------------------------------------- *)
(* Metric function. *)
(* ------------------------------------------------------------------------- *)
override_interface("dist",`distance:real^N#real^N->real`);;
(* ------------------------------------------------------------------------- *)
(* A connectedness or intermediate value lemma with several applications. *)
(* ------------------------------------------------------------------------- *)
let CONNECTED_REAL_LEMMA = prove
(`!f:real->real^N a b e1 e2.
a <= b /\ f(a)
IN e1 /\ f(b)
IN e2 /\
(!e x. a <= x /\ x <= b /\ &0 < e
==> ?d. &0 < d /\
!y. abs(y - x) < d ==>
dist(f(y),f(x)) < e) /\
(!y. y
IN e1 ==> ?e. &0 < e /\ !y'.
dist(y',y) < e ==> y'
IN e1) /\
(!y. y
IN e2 ==> ?e. &0 < e /\ !y'.
dist(y',y) < e ==> y'
IN e2) /\
~(?x. a <= x /\ x <= b /\ f(x)
IN e1 /\ f(x)
IN e2)
==> ?x. a <= x /\ x <= b /\ ~(f(x)
IN e1) /\ ~(f(x)
IN e2)`,
let tac = ASM_MESON_TAC[
REAL_LT_IMP_LE;
REAL_LE_TOTAL; REAL_LE_ANTISYM] in
REWRITE_TAC[
EXTENSION;
NOT_IN_EMPTY] THEN REPEAT STRIP_TAC THEN
MP_TAC(SPEC `\c. !x. a <= x /\ x <= c ==> (f(x):real^N)
IN e1`
REAL_COMPLETE) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL [tac; ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `x:real` THEN STRIP_TAC THEN
SUBGOAL_THEN `a <= x /\ x <= b` STRIP_ASSUME_TAC THENL [tac; ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `!z. a <= z /\ z < x ==> (f(z):real^N)
IN e1` ASSUME_TAC THENL
[ASM_MESON_TAC[
REAL_NOT_LT;
REAL_LT_IMP_LE]; ALL_TAC] THEN
REPEAT STRIP_TAC THENL
[SUBGOAL_THEN
`?d. &0 < d /\ !y. abs(y - x) < d ==> (f(y):real^N)
IN e1`
STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_MESON_TAC[REAL_ARITH `z <= x + e /\ e < d ==> z < x \/ abs(z - x) < d`;
REAL_ARITH `&0 < e ==> ~(x + e <= x)`;
REAL_DOWN];
SUBGOAL_THEN
`?d. &0 < d /\ !y. abs(y - x) < d ==> (f(y):real^N)
IN e2`
STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
MP_TAC(SPECL [`x - a`; `d:real`]
REAL_DOWN2) THEN ANTS_TAC THENL
[ASM_MESON_TAC[
REAL_LT_LE;
REAL_SUB_LT]; ALL_TAC] THEN
ASM_MESON_TAC[REAL_ARITH `e < x - a ==> a <= x - e`;
REAL_ARITH `&0 < e /\ x <= b ==> x - e <= b`;
REAL_ARITH `&0 < e /\ e < d ==> x - e < x /\ abs((x - e) - x) < d`]]);;
(* ------------------------------------------------------------------------- *)
(* One immediately useful corollary is the existence of square roots! *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Hence derive more interesting properties of the norm. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Squaring equations and inequalities involving norms. *)
(* ------------------------------------------------------------------------- *)
let NORM_LT_SQUARE_ALT = prove
(`!x:real^N.
norm(x) < a <=> &0 <= a /\ x
dot x < a pow 2`,
REWRITE_TAC[REAL_ARITH `x < a <=> ~(x >= a)`;
NORM_GE_SQUARE] THEN
REPEAT GEN_TAC THEN ASM_CASES_TAC `a = &0` THENL
[ASM_REWRITE_TAC[
real_ge] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
REWRITE_TAC[
DOT_POS_LE];
ASM_REAL_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* General linear decision procedure for normed spaces. *)
(* ------------------------------------------------------------------------- *)
let NORM_ARITH =
let find_normedterms =
let augment_norm b tm acc =
match tm with
Comb(Const("vector_norm",_),v) -> insert (b,v) acc
| _ -> acc in
let rec find_normedterms tm acc =
match tm with
Comb(Comb(Const("real_add",_),l),r) ->
find_normedterms l (find_normedterms r acc)
| Comb(Comb(Const("real_mul",_),c),n) ->
if not (is_ratconst c) then acc else
augment_norm (rat_of_term c >=/ Int 0) n acc
| _ -> augment_norm true tm acc in
find_normedterms in
let lincomb_neg t = mapf minus_num t in
let lincomb_cmul c t = if c =/ Int 0 then undefined else mapf (( */ ) c) t in
let lincomb_add l r = combine (+/) (fun x -> x =/ Int 0) l r in
let lincomb_sub l r = lincomb_add l (lincomb_neg r) in
let lincomb_eq l r = lincomb_sub l r = undefined in
let rec vector_lincomb tm =
match tm with
Comb(Comb(Const("vector_add",_),l),r) ->
lincomb_add (vector_lincomb l) (vector_lincomb r)
| Comb(Comb(Const("vector_sub",_),l),r) ->
lincomb_sub (vector_lincomb l) (vector_lincomb r)
| Comb(Comb(Const("%",_),l),r) ->
lincomb_cmul (rat_of_term l) (vector_lincomb r)
| Comb(Const("vector_neg",_),t) ->
lincomb_neg (vector_lincomb t)
| Comb(Const("vec",_),n) when is_numeral n & dest_numeral n =/ Int 0 ->
undefined
| _ -> (tm |=> Int 1) in
let vector_lincombs tms =
itlist (fun t fns ->
if can (assoc t) fns then fns else
let f = vector_lincomb t in
try let _,f' = find (fun (_,f') -> lincomb_eq f f') fns in
(t,f')::fns
with Failure _ -> (t,f)::fns) tms [] in
let rec replacenegnorms fn tm =
match tm with
Comb(Comb(Const("real_add",_),l),r) ->
BINOP_CONV (replacenegnorms fn) tm
| Comb(Comb(Const("real_mul",_),c),n) when rat_of_term c </ Int 0 ->
RAND_CONV fn tm
| _ -> REFL tm in
let flip v eq =
if defined eq v then (v |-> minus_num(apply eq v)) eq else eq in
let rec allsubsets s =
match s with
[] -> [[]]
| (a::t) -> let res = allsubsets t in
map (fun b -> a::b) res @ res in
let evaluate env lin =
foldr (fun x c s -> s +/ c */ apply env x) lin (Int 0) in
let rec solve (vs,eqs) =
match (vs,eqs) with
[],[] -> (0 |=> Int 1)
| _,eq::oeqs ->
let v = hd(intersect vs (dom eq)) in
let c = apply eq v in
let vdef = lincomb_cmul (Int(-1) // c) eq in
let eliminate eqn =
if not(defined eqn v) then eqn else
lincomb_add (lincomb_cmul (apply eqn v) vdef) eqn in
let soln = solve (subtract vs [v],map eliminate oeqs) in
(v |-> evaluate soln (undefine v vdef)) soln in
let rec combinations k l =
if k = 0 then [[]] else
match l with
[] -> []
| h::t -> map (fun c -> h::c) (combinations (k - 1) t) @
combinations k t in
let vertices vs eqs =
let vertex cmb =
let soln = solve(vs,cmb) in
map (fun v -> tryapplyd soln v (Int 0)) vs in
let rawvs = mapfilter vertex (combinations (length vs) eqs) in
let unset = filter (forall (fun c -> c >=/ Int 0)) rawvs in
itlist (insert' (forall2 (=/))) unset [] in
let subsumes l m = forall2 (fun x y -> abs_num x <=/ abs_num y) l m in
let rec subsume todo dun =
match todo with
[] -> dun
| v::ovs -> let dun' = if exists (fun w -> subsumes w v) dun then dun
else v::(filter (fun w -> not(subsumes v w)) dun) in
subsume ovs dun' in
let NORM_CMUL_RULE =
let MATCH_pth = (MATCH_MP o prove)
(`!b x. b >= norm(x) ==> !c. abs(c) * b >= norm(c % x)`,
SIMP_TAC[NORM_MUL; real_ge; REAL_LE_LMUL; REAL_ABS_POS]) in
fun c th -> ISPEC(term_of_rat c) (MATCH_pth th) in
let NORM_ADD_RULE =
let MATCH_pth = (MATCH_MP o prove)
(`!b1 b2 x1 x2. b1 >= norm(x1) /\ b2 >= norm(x2)
==> b1 + b2 >= norm(x1 + x2)`,
REWRITE_TAC[real_ge] THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC NORM_TRIANGLE_LE THEN ASM_SIMP_TAC[REAL_LE_ADD2]) in
fun th1 th2 -> MATCH_pth (CONJ th1 th2) in
let INEQUALITY_CANON_RULE =
CONV_RULE(LAND_CONV REAL_POLY_CONV) o
CONV_RULE(LAND_CONV REAL_RAT_REDUCE_CONV) o
GEN_REWRITE_RULE I [REAL_ARITH `s >= t <=> s - t >= &0`] in
let NORM_CANON_CONV =
let APPLY_pth1 = GEN_REWRITE_CONV I
[VECTOR_ARITH `x:real^N = &1 % x`]
and APPLY_pth2 = GEN_REWRITE_CONV I
[VECTOR_ARITH `x - y:real^N = x + --y`]
and APPLY_pth3 = GEN_REWRITE_CONV I
[VECTOR_ARITH `--x:real^N = -- &1 % x`]
and APPLY_pth4 = GEN_REWRITE_CONV I
[VECTOR_ARITH `&0 % x:real^N = vec 0`;
VECTOR_ARITH `c % vec 0:real^N = vec 0`]
and APPLY_pth5 = GEN_REWRITE_CONV I
[VECTOR_ARITH `c % (d % x) = (c * d) % x`]
and APPLY_pth6 = GEN_REWRITE_CONV I
[VECTOR_ARITH `c % (x + y) = c % x + c % y`]
and APPLY_pth7 = GEN_REWRITE_CONV I
[VECTOR_ARITH `vec 0 + x = x`;
VECTOR_ARITH `x + vec 0 = x`]
and APPLY_pth8 =
GEN_REWRITE_CONV I [VECTOR_ARITH `c % x + d % x = (c + d) % x`] THENC
LAND_CONV REAL_RAT_ADD_CONV THENC
GEN_REWRITE_CONV TRY_CONV [VECTOR_ARITH `&0 % x = vec 0`]
and APPLY_pth9 =
GEN_REWRITE_CONV I
[VECTOR_ARITH `(c % x + z) + d % x = (c + d) % x + z`;
VECTOR_ARITH `c % x + (d % x + z) = (c + d) % x + z`;
VECTOR_ARITH `(c % x + w) + (d % x + z) = (c + d) % x + (w + z)`] THENC
LAND_CONV(LAND_CONV REAL_RAT_ADD_CONV)
and APPLY_ptha =
GEN_REWRITE_CONV I [VECTOR_ARITH `&0 % x + y = y`]
and APPLY_pthb =
GEN_REWRITE_CONV I
[VECTOR_ARITH `c % x + d % y = c % x + d % y`;
VECTOR_ARITH `(c % x + z) + d % y = c % x + (z + d % y)`;
VECTOR_ARITH `c % x + (d % y + z) = c % x + (d % y + z)`;
VECTOR_ARITH `(c % x + w) + (d % y + z) = c % x + (w + (d % y + z))`]
and APPLY_pthc =
GEN_REWRITE_CONV I
[VECTOR_ARITH `c % x + d % y = d % y + c % x`;
VECTOR_ARITH `(c % x + z) + d % y = d % y + (c % x + z)`;
VECTOR_ARITH `c % x + (d % y + z) = d % y + (c % x + z)`;
VECTOR_ARITH `(c % x + w) + (d % y + z) = d % y + ((c % x + w) + z)`]
and APPLY_pthd =
GEN_REWRITE_CONV TRY_CONV
[VECTOR_ARITH `x + vec 0 = x`] in
let headvector tm =
match tm with
Comb(Comb(Const("vector_add",_),Comb(Comb(Const("%",_),l),v)),r) -> v
| Comb(Comb(Const("%",_),l),v) -> v
| _ -> failwith "headvector: non-canonical term" in
let rec VECTOR_CMUL_CONV tm =
((APPLY_pth5 THENC LAND_CONV REAL_RAT_MUL_CONV) ORELSEC
(APPLY_pth6 THENC BINOP_CONV VECTOR_CMUL_CONV)) tm
and VECTOR_ADD_CONV tm =
try APPLY_pth7 tm with Failure _ ->
try APPLY_pth8 tm with Failure _ ->
match tm with
Comb(Comb(Const("vector_add",_),lt),rt) ->
let l = headvector lt and r = headvector rt in
if l < r then (APPLY_pthb THENC
RAND_CONV VECTOR_ADD_CONV THENC
APPLY_pthd) tm
else if r < l then (APPLY_pthc THENC
RAND_CONV VECTOR_ADD_CONV THENC
APPLY_pthd) tm else
(APPLY_pth9 THENC
((APPLY_ptha THENC VECTOR_ADD_CONV) ORELSEC
RAND_CONV VECTOR_ADD_CONV THENC
APPLY_pthd)) tm
| _ -> REFL tm in
let rec VECTOR_CANON_CONV tm =
match tm with
Comb(Comb(Const("vector_add",_),l),r) ->
let lth = VECTOR_CANON_CONV l and rth = VECTOR_CANON_CONV r in
let th = MK_COMB(AP_TERM (rator(rator tm)) lth,rth) in
CONV_RULE (RAND_CONV VECTOR_ADD_CONV) th
| Comb(Comb(Const("%",_),l),r) ->
let rth = AP_TERM (rator tm) (VECTOR_CANON_CONV r) in
CONV_RULE (RAND_CONV(APPLY_pth4 ORELSEC VECTOR_CMUL_CONV)) rth
| Comb(Comb(Const("vector_sub",_),l),r) ->
(APPLY_pth2 THENC VECTOR_CANON_CONV) tm
| Comb(Const("vector_neg",_),t) ->
(APPLY_pth3 THENC VECTOR_CANON_CONV) tm
| Comb(Const("vec",_),n) when is_numeral n & dest_numeral n =/ Int 0 ->
REFL tm
| _ -> APPLY_pth1 tm in
fun tm ->
match tm with
Comb(Const("vector_norm",_),e) -> RAND_CONV VECTOR_CANON_CONV tm
| _ -> failwith "NORM_CANON_CONV" in
let REAL_VECTOR_COMBO_PROVER =
let pth_zero = prove(`
norm(
vec 0:real^N) = &0`,
REWRITE_TAC[
NORM_0])
and tv_n = mk_vartype "N" in
fun translator (nubs,ges,gts) ->
let sources = map (rand o rand o concl) nubs
and rawdests = itlist (find_normedterms o lhand o concl) (ges @ gts) [] in
if not (forall fst rawdests) then failwith "Sanity check" else
let dests = setify (map snd rawdests) in
let srcfuns = map vector_lincomb sources
and destfuns = map vector_lincomb dests in
let vvs = itlist (union o dom) (srcfuns @ destfuns) [] in
let n =
length srcfuns in
let nvs = 1--n in
let srccombs = zip srcfuns nvs in
let consider d =
let coefficients x =
let inp = if defined d x then 0 |=> minus_num(apply d x)
else undefined in
itlist (fun (f,v) g -> if defined f x then (v |-> apply f x) g else g)
srccombs inp in
let equations = map coefficients vvs
and inequalities = map (fun n -> (n |=> Int 1)) nvs in
let plausiblevertices f =
let flippedequations = map (itlist flip f) equations in
let constraints = flippedequations @ inequalities in
let rawverts =
vertices nvs constraints in
let check_solution v =
let f = itlist2 (|->) nvs v (0 |=> Int 1) in
forall (fun e -> evaluate f e =/ Int 0) flippedequations in
let goodverts = filter check_solution rawverts in
let signfixups = map (fun n -> if mem n f then -1 else 1) nvs in
map (map2 (fun s c -> Int s */ c) signfixups) goodverts in
let allverts = itlist (@) (map plausiblevertices (allsubsets nvs)) [] in
subsume allverts [] in
let compute_ineq v =
let ths = mapfilter (fun (v,t) -> if v =/ Int 0 then fail()
else NORM_CMUL_RULE v t)
(zip v nubs) in
INEQUALITY_CANON_RULE (end_itlist NORM_ADD_RULE ths) in
let ges' = mapfilter compute_ineq (itlist ((@) o consider) destfuns []) @
map INEQUALITY_CANON_RULE nubs @ ges in
let zerodests = filter
(fun t -> dom(vector_lincomb t) = []) (map snd rawdests) in
REAL_LINEAR_PROVER translator
(map (fun t -> INST_TYPE [last(snd(dest_type(type_of t))),tv_n]
pth_zero)
zerodests,
map (CONV_RULE(ONCE_DEPTH_CONV NORM_CANON_CONV THENC
LAND_CONV REAL_POLY_CONV)) ges',
map (CONV_RULE(ONCE_DEPTH_CONV NORM_CANON_CONV THENC
LAND_CONV REAL_POLY_CONV)) gts) in
let REAL_VECTOR_INEQ_PROVER =
let pth = prove
(`norm(x) = n ==> norm(x) >= &0 /\ n >= norm(x)`,
DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
REWRITE_TAC[real_ge; NORM_POS_LE] THEN REAL_ARITH_TAC) in
let NORM_MP = MATCH_MP pth in
fun translator (ges,gts) ->
let ntms = itlist find_normedterms (map (lhand o concl) (ges @ gts)) [] in
let lctab = vector_lincombs (map snd (filter (not o fst) ntms)) in
let asl = map (fun (t,_) ->
ASSUME(mk_eq(mk_icomb(mk_const("vector_norm",[]),t),
genvar `:real`))) lctab in
let replace_conv = GEN_REWRITE_CONV TRY_CONV asl in
let replace_rule = CONV_RULE (LAND_CONV (replacenegnorms replace_conv)) in
let ges' =
itlist (fun th ths -> CONJUNCT1(NORM_MP th)::ths)
asl (map replace_rule ges)
and gts' = map replace_rule gts
and nubs = map (CONJUNCT2 o NORM_MP) asl in
let th1 = REAL_VECTOR_COMBO_PROVER translator (nubs,ges',gts') in
let th2 = INST
(map (fun th -> let l,r = dest_eq(concl th) in (l,r)) asl) th1 in
itlist PROVE_HYP (map (REFL o lhand o concl) asl) th2 in
let REAL_VECTOR_PROVER =
let rawrule =
GEN_REWRITE_RULE I [REAL_ARITH `x = &0 <=> x >= &0 /\ --x >= &0`] in
let splitequation th acc =
let th1,th2 = CONJ_PAIR(rawrule th) in
th1::CONV_RULE(LAND_CONV REAL_POLY_NEG_CONV) th2::acc in
fun translator (eqs,ges,gts) ->
REAL_VECTOR_INEQ_PROVER translator
(itlist splitequation eqs ges,gts) in
let pth = prove
(`(!x y:real^N. x = y <=> norm(x - y) <= &0) /\
(!x y:real^N. ~(x = y) <=> ~(norm(x - y) <= &0))`,
REWRITE_TAC[NORM_LE_0; VECTOR_SUB_EQ]) in
let conv1 = GEN_REWRITE_CONV TRY_CONV [pth] in
let conv2 tm = (conv1 tm,conv1(mk_neg tm)) in
let init = GEN_REWRITE_CONV ONCE_DEPTH_CONV [DECIMAL] THENC
REAL_RAT_REDUCE_CONV THENC
GEN_REWRITE_CONV ONCE_DEPTH_CONV [dist] THENC
GEN_NNF_CONV true (conv1,conv2)
and pure = GEN_REAL_ARITH REAL_VECTOR_PROVER in
fun tm -> let th = init tm in EQ_MP (SYM th) (pure(rand(concl th)));;
let NORM_ARITH_TAC = CONV_TAC NORM_ARITH;;
let ASM_NORM_ARITH_TAC =
REPEAT(FIRST_X_ASSUM(MP_TAC o check (not o is_forall o concl))) THEN
NORM_ARITH_TAC;;
(* ------------------------------------------------------------------------- *)
(* Dot product in terms of the norm rather than conversely. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Equality of vectors in terms of dot products. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Hence more metric properties. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Sums of vectors. *)
(* ------------------------------------------------------------------------- *)
let vsum = new_definition
`(vsum:(A->bool)->(A->real^N)->real^N) s f = lambda i. sum s (\x. f(x)$i)`;;
let VSUM_DIFFS = prove
(`!m n.
vsum(m..n) (\k. f(k) - f(k + 1)) =
if m <= n then f(m) - f(n + 1) else
vec 0`,
GEN_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[
VSUM_CLAUSES_NUMSEG;
LE] THEN
ASM_CASES_TAC `m = SUC n` THEN
ASM_REWRITE_TAC[ARITH_RULE `~(SUC n <= n)`;
VECTOR_ADD_LID] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[GSYM
ADD1] THEN VECTOR_ARITH_TAC);;
let VSUM_NORM_ALLSUBSETS_BOUND = prove
(`!f:A->real^N p e.
FINITE p /\
(!q. q
SUBSET p ==>
norm(
vsum q f) <= e)
==>
sum p (\x.
norm(f x)) <= &2 * &(
dimindex(:N)) * e`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC
`
sum p (\x:A.
sum (1..dimindex(:N)) (\i. abs((f x:real^N)$i)))` THEN
CONJ_TAC THENL
[MATCH_MP_TAC
SUM_LE THEN ASM_SIMP_TAC[
NORM_LE_L1]; ALL_TAC] THEN
W(MP_TAC o PART_MATCH (lhand o rand)
SUM_SWAP o lhand o snd) THEN
ASM_REWRITE_TAC[
FINITE_NUMSEG] THEN DISCH_THEN SUBST1_TAC THEN
ONCE_REWRITE_TAC[REAL_ARITH `&2 * &n * e = &n * &2 * e`] THEN
GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV)
[GSYM
CARD_NUMSEG_1] THEN
MATCH_MP_TAC
SUM_BOUND THEN REWRITE_TAC[
FINITE_NUMSEG;
IN_NUMSEG] THEN
X_GEN_TAC `k:num` THEN STRIP_TAC THEN MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `
sum {x:A | x
IN p /\ &0 <= (f x:real^N)$k} (\x. abs((f x)$k)) +
sum {x | x
IN p /\ (f x)$k < &0} (\x. abs((f x)$k))` THEN
CONJ_TAC THENL
[MATCH_MP_TAC(REAL_ARITH `a = b ==> b <= a`) THEN
MATCH_MP_TAC
SUM_UNION_EQ THEN
ASM_SIMP_TAC[
EXTENSION;
NOT_IN_EMPTY;
IN_INTER;
IN_UNION;
IN_ELIM_THM] THEN
CONJ_TAC THEN X_GEN_TAC `x:A` THEN ASM_CASES_TAC `(x:A)
IN p` THEN
ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC(REAL_ARITH `x <= e /\ y <= e ==> x + y <= &2 * e`) THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [GSYM
REAL_ABS_NEG] THEN
CONJ_TAC THEN MATCH_MP_TAC(REAL_ARITH
`!g.
sum s g =
sum s f /\
sum s g <= e ==>
sum s f <= e`)
THENL
[EXISTS_TAC `\x. ((f:A->real^N) x)$k`;
EXISTS_TAC `\x. --(((f:A->real^N) x)$k)`] THEN
(CONJ_TAC THENL
[MATCH_MP_TAC
SUM_EQ THEN REWRITE_TAC[
IN_ELIM_THM] THEN REAL_ARITH_TAC;
ALL_TAC]) THEN
ASM_SIMP_TAC[GSYM
VSUM_COMPONENT;
SUM_NEG;
FINITE_RESTRICT] THEN
MATCH_MP_TAC(REAL_ARITH `abs(x) <= e ==> x <= e`) THEN
REWRITE_TAC[
REAL_ABS_NEG] THEN
MATCH_MP_TAC(REAL_ARITH
`abs((
vsum q f)$k) <=
norm(
vsum q f) /\
norm(
vsum q f) <= e
==> abs((
vsum q f)$k) <= e`) THEN
ASM_SIMP_TAC[
COMPONENT_LE_NORM] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN SET_TAC[]);;
let VSUM_PARTIAL_SUC = prove
(`!f g:num->real^N m n.
vsum (m..n) (\k. f(k) % (g(k + 1) - g(k))) =
if m <= n then f(n + 1) % g(n + 1) - f(m) % g(m) -
vsum (m..n) (\k. (f(k + 1) - f(k)) % g(k + 1))
else
vec 0`,
GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
COND_CASES_TAC THEN ASM_SIMP_TAC[
VSUM_TRIV_NUMSEG; GSYM
NOT_LE] THEN
ASM_REWRITE_TAC[
VSUM_CLAUSES_NUMSEG] THENL
[COND_CASES_TAC THEN ASM_SIMP_TAC[ARITH] THENL
[VECTOR_ARITH_TAC; ASM_ARITH_TAC];
ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
LE]) THEN
DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
ASM_SIMP_TAC[GSYM
NOT_LT;
VSUM_TRIV_NUMSEG; ARITH_RULE `n < SUC n`] THEN
ASM_SIMP_TAC[GSYM
ADD1;
ADD_CLAUSES] THEN VECTOR_ARITH_TAC);;
let VSUM_PARTIAL_PRE = prove
(`!f g:num->real^N m n.
vsum (m..n) (\k. f(k) % (g(k) - g(k - 1))) =
if m <= n then f(n + 1) % g(n) - f(m) % g(m - 1) -
vsum (m..n) (\k. (f(k + 1) - f(k)) % g(k))
else
vec 0`,
REPEAT GEN_TAC THEN
MP_TAC(ISPECL [`f:num->
real`; `\k. (g:num->real^N)(k - 1)`;
`m:num`; `n:num`]
VSUM_PARTIAL_SUC) THEN
REWRITE_TAC[
ADD_SUB] THEN DISCH_THEN SUBST1_TAC THEN
COND_CASES_TAC THEN REWRITE_TAC[]);;
let VSUM_PAIR_0 = prove
(`!f:num->real^N n.
vsum(0..2*n+1) f =
vsum(0..n) (\i. f(2*i) + f(2*i+1))`,
REPEAT GEN_TAC THEN
MP_TAC(ISPECL [`f:num->real^N`; `0`; `n:num`]
VSUM_PAIR) THEN
ASM_REWRITE_TAC[ARITH]);;
(* ------------------------------------------------------------------------- *)
(* Add useful congruences to the simplifier. *)
(* ------------------------------------------------------------------------- *)
let th = prove
(`(!f g s. (!x. x
IN s ==> f(x) = g(x))
==>
vsum s (\i. f(i)) =
vsum s g) /\
(!f g a b. (!i. a <= i /\ i <= b ==> f(i) = g(i))
==>
vsum(a..b) (\i. f(i)) =
vsum(a..b) g) /\
(!f g p. (!x. p x ==> f x = g x)
==>
vsum {y | p y} (\i. f(i)) =
vsum {y | p y} g)`,
(* ------------------------------------------------------------------------- *)
(* A conversion for evaluation of `vsum(m..n) f` for numerals m and n. *)
(* ------------------------------------------------------------------------- *)
let EXPAND_VSUM_CONV =
let pth_0,pth_1 = (CONJ_PAIR o prove)
(`vsum(0..0) (f:num->real^N) = f(0) /\
vsum(0..SUC n) f = vsum(0..n) f + f(SUC n)`,
REWRITE_TAC[VSUM_CLAUSES_NUMSEG; LE_0; VECTOR_ADD_AC]) in
let conv_0 = REWR_CONV pth_0 and conv_1 = REWR_CONV pth_1 in
let rec conv tm =
try (LAND_CONV(RAND_CONV num_CONV) THENC conv_1 THENC
NUM_REDUCE_CONV THENC LAND_CONV conv) tm
with Failure _ -> conv_0 tm in
conv THENC
(REDEPTH_CONV BETA_CONV) THENC
GEN_REWRITE_CONV TOP_DEPTH_CONV [GSYM VECTOR_ADD_ASSOC];;
(* ------------------------------------------------------------------------- *)
(* Basis vectors in coordinate directions. *)
(* ------------------------------------------------------------------------- *)
let VECTOR_CHOOSE_DIST = prove
(`!x e. &0 <= e ==> ?y:real^N.
dist(x,y) = e`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `?c:real^N.
norm(c) = e` CHOOSE_TAC THENL
[ASM_SIMP_TAC[
VECTOR_CHOOSE_SIZE]; ALL_TAC] THEN
EXISTS_TAC `x - c:real^N` THEN REWRITE_TAC[
dist] THEN
ASM_REWRITE_TAC[VECTOR_ARITH `x - (x - c) = c:real^N`]);;
(* ------------------------------------------------------------------------- *)
(* Orthogonality. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Explicit vector construction from lists. *)
(* ------------------------------------------------------------------------- *)
let FORALL_VECTOR_1 = prove
(`(!v:A^1. P v) <=> !x. P(
vector[x])`,
EQ_TAC THEN SIMP_TAC[] THEN REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `(v:A^1)$1`) THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
REWRITE_TAC[
CART_EQ;
FORALL_1;
VECTOR_1; DIMINDEX_1]);;
let FORALL_VECTOR_2 = prove
(`(!v:A^2. P v) <=> !x y. P(
vector[x;y])`,
EQ_TAC THEN SIMP_TAC[] THEN REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`(v:A^2)$1`; `(v:A^2)$2`]) THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
REWRITE_TAC[
CART_EQ;
FORALL_2;
VECTOR_2; DIMINDEX_2]);;
let FORALL_VECTOR_3 = prove
(`(!v:A^3. P v) <=> !x y z. P(
vector[x;y;z])`,
EQ_TAC THEN SIMP_TAC[] THEN REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`(v:A^3)$1`; `(v:A^3)$2`; `(v:A^3)$3`]) THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
REWRITE_TAC[
CART_EQ;
FORALL_3;
VECTOR_3; DIMINDEX_3]);;
let FORALL_VECTOR_4 = prove
(`(!v:A^4. P v) <=> !w x y z. P(
vector[w;x;y;z])`,
EQ_TAC THEN SIMP_TAC[] THEN REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`(v:A^4)$1`; `(v:A^4)$2`; `(v:A^4)$3`; `(v:A^4)$4`]) THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
REWRITE_TAC[
CART_EQ;
FORALL_4;
VECTOR_4; DIMINDEX_4]);;
(* ------------------------------------------------------------------------- *)
(* Linear functions. *)
(* ------------------------------------------------------------------------- *)
let linear = new_definition
`linear (f:real^M->real^N) <=>
(!x y. f(x + y) = f(x) + f(y)) /\
(!c x. f(c % x) = c % f(x))`;;
let LINEAR_BOUNDED_POS = prove
(`!f:real^M->real^N.
linear f ==> ?B. &0 < B /\ !x.
norm(f x) <= B *
norm(x)`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(X_CHOOSE_TAC `B:real` o MATCH_MP
LINEAR_BOUNDED) THEN
EXISTS_TAC `abs(B) + &1` THEN CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
POP_ASSUM MP_TAC THEN MATCH_MP_TAC
MONO_FORALL THEN GEN_TAC THEN
MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
MATCH_MP_TAC
REAL_LE_RMUL THEN REWRITE_TAC[
NORM_POS_LE] THEN
REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Bilinear functions. *)
(* ------------------------------------------------------------------------- *)
let BILINEAR_VSUM_PARTIAL_PRE = prove
(`!f g h:real^M->real^N->real^P m n.
bilinear h
==>
vsum (m..n) (\k. h (f k) (g(k) - g(k - 1))) =
if m <= n then h (f(n + 1)) (g(n)) - h (f m) (g(m - 1)) -
vsum (m..n) (\k. h (f(k + 1) - f(k)) (g(k)))
else
vec 0`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o ISPECL [`f:num->real^M`; `\k. (g:num->real^N)(k - 1)`;
`m:num`; `n:num`] o MATCH_MP
BILINEAR_VSUM_PARTIAL_SUC) THEN
REWRITE_TAC[
ADD_SUB] THEN DISCH_THEN SUBST1_TAC THEN
COND_CASES_TAC THEN REWRITE_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Adjoints. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Matrix notation. NB: an MxN matrix is of type real^N^M, not real^M^N. *)
(* We could define a special type if we're going to use them a lot. *)
(* ------------------------------------------------------------------------- *)
overload_interface ("--",`(matrix_neg):real^N^M->real^N^M`);;
overload_interface ("+",`(matrix_add):real^N^M->real^N^M->real^N^M`);;
overload_interface ("-",`(matrix_sub):real^N^M->real^N^M->real^N^M`);;
make_overloadable "**" `:A->B->C`;;
overload_interface ("**",`(matrix_mul):real^N^M->real^P^N->real^P^M`);;
overload_interface ("**",`(matrix_vector_mul):real^N^M->real^N->real^M`);;
overload_interface ("**",`(vector_matrix_mul):real^M->real^N^M->real^N`);;
parse_as_infix("%%",(21,"right"));;
prioritize_real();;
let matrix_mul = new_definition
`!A:real^N^M B:real^P^N.
A ** B =
lambda i j. sum(1..dimindex(:N)) (\k. A$i$k * B$k$j)`;;
let mat = new_definition
`(mat:num->real^N^M) k = lambda i j. if i = j then &k else &0`;;
let transp = new_definition
`(transp:real^N^M->real^M^N) A = lambda i j. A$j$i`;;
let row = new_definition
`(row:num->real^N^M->real^N) i A = lambda j. A$i$j`;;
let column = new_definition
`(column:num->real^N^M->real^M) j A = lambda i. A$i$j`;;
let MATRIX_ADD_AC = prove
(`(A:real^N^M) + B = B + A /\
(A + B) + C = A + (B + C) /\
A + (B + C) = B + (A + C)`,
(* ------------------------------------------------------------------------- *)
(* Two sometimes fruitful ways of looking at matrix-vector multiplication. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Slightly gruesome lemmas: better to define sums over vectors really... *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Inverse matrices (not necessarily square, but it's vacuous otherwise). *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Correspondence between matrices and linear operators. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Operator norm. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* It's handy to "lift" from R to R^1 and "drop" from R^1 to R. *)
(* ------------------------------------------------------------------------- *)
let lift = new_definition
`(lift:real->real^1) x = lambda i. x`;;
let drop = new_definition
`(drop:real^1->real) x = x$1`;;
let FORALL_LIFT_FUN = prove
(`!P:(A->real^1)->bool. (!f. P f) <=> (!f. P(
lift o f))`,
GEN_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN DISCH_TAC THEN
X_GEN_TAC `f:A->real^1` THEN
FIRST_X_ASSUM(MP_TAC o SPEC `
drop o (f:A->real^1)`) THEN
REWRITE_TAC[
o_DEF;
LIFT_DROP; ETA_AX]);;
(* ------------------------------------------------------------------------- *)
(* Pasting vectors. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* A bit of linear algebra. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Closure properties of subspaces. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Lemmas. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Individual closure properties. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Mapping under linear image. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* The key breakdown property. *)
(* ------------------------------------------------------------------------- *)
let SPAN_3 = prove
(`!a b c. span {a,b,c} =
{u % a + v % b + w % c | u
IN (:real) /\ v
IN (:real) /\ w
IN (:real)}`,
(* ------------------------------------------------------------------------- *)
(* Hence some "reversal" results. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Transitivity property. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* An explicit expansion is sometimes needed. *)
(* ------------------------------------------------------------------------- *)
let DEPENDENT_FINITE = prove
(`!s:real^N->bool.
FINITE s
==> (
dependent s <=> ?u. (?v. v
IN s /\ ~(u v = &0)) /\
vsum s (\v. u(v) % v) =
vec 0)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[
DEPENDENT_EXPLICIT] THEN EQ_TAC THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THENL
[MAP_EVERY X_GEN_TAC [`t:real^N->bool`; `u:real^N->
real`] THEN
DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
EXISTS_TAC `\v:real^N. if v
IN t then u(v) else &0` THEN
REWRITE_TAC[] THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
ONCE_REWRITE_TAC[
COND_RAND] THEN ONCE_REWRITE_TAC[
COND_RATOR] THEN
ASM_SIMP_TAC[
VECTOR_MUL_LZERO; GSYM
VSUM_RESTRICT_SET] THEN
ASM_SIMP_TAC[SET_RULE `t
SUBSET s ==> {x | x
IN s /\ x
IN t} = t`];
GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
MAP_EVERY EXISTS_TAC [`s:real^N->bool`; `u:real^N->
real`] THEN
ASM_REWRITE_TAC[
SUBSET_REFL]]);;
(* ------------------------------------------------------------------------- *)
(* Standard bases are a spanning set, and obviously finite. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* This is useful for building a basis step-by-step. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* The degenerate case of the Exchange Lemma. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* The general case of the Exchange Lemma, the key to what follows. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* This implies corresponding size bounds. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Explicit formulation of independence. *)
(* ------------------------------------------------------------------------- *)
let DEPENDENT_3 = prove
(`!a b c:real^N.
~(a = b) /\ ~(a = c) /\ ~(b = c)
==> (
dependent {a,b,c} <=>
?x y z. x % a + y % b + z % c =
vec 0 /\
~(x = &0 /\ y = &0 /\ z = &0))`,
(* ------------------------------------------------------------------------- *)
(* Hence we can create a maximal independent subset. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* A kind of closed graph property for linearity. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Notion of dimension. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Consequences of independence or spanning for cardinality. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* More lemmas about dimension. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Converses to those. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* More general size bound lemmas. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some stepping theorems. *)
(* ------------------------------------------------------------------------- *)
let DIM_EQ_0 = prove
(`!s:real^N->bool.
dim s = 0 <=> s
SUBSET {
vec 0}`,
REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THENL
[MATCH_MP_TAC(SET_RULE
`~(?b. ~(b = a) /\ {b}
SUBSET s) ==> s
SUBSET {a}`) THEN
STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP
DIM_SUBSET);
MATCH_MP_TAC(ARITH_RULE `!m. m = 0 /\ n <= m ==> n = 0`) THEN
EXISTS_TAC `
dim{
vec 0:real^N}` THEN ASM_SIMP_TAC[
DIM_SUBSET]] THEN
ASM_REWRITE_TAC[
DIM_SING; ARITH]);;
(* ------------------------------------------------------------------------- *)
(* Choosing a subspace of a given dimension. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Relation between bases and injectivity/surjectivity of map. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Picking an orthogonal replacement for a spanning set. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* We can extend a linear basis-basis injection to the whole set. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* We can extend a linear mapping from basis. *)
(* ------------------------------------------------------------------------- *)
let LINEAR_INDEPENDENT_EXTEND_LEMMA = prove
(`!f b. FINITE b
==>
independent b
==> ?g:real^M->real^N.
(!x y. x
IN span b /\ y
IN span b
==> (g(x + y) = g(x) + g(y))) /\
(!x c. x
IN span b ==> (g(c % x) = c % g(x))) /\
(!x. x
IN b ==> (g x = f x))`,
GEN_TAC THEN MATCH_MP_TAC
FINITE_INDUCT_STRONG THEN
REWRITE_TAC[
NOT_IN_EMPTY;
INDEPENDENT_INSERT] THEN CONJ_TAC THENL
[REPEAT STRIP_TAC THEN EXISTS_TAC `(\x.
vec 0):real^M->real^N` THEN
SIMP_TAC[
SPAN_EMPTY] THEN REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC;
ALL_TAC] THEN
SIMP_TAC[] THEN MAP_EVERY X_GEN_TAC [`a:real^M`; `b:real^M->bool`] THEN
DISCH_THEN(fun
th -> STRIP_TAC THEN MP_TAC
th) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `g:real^M->real^N` STRIP_ASSUME_TAC) THEN
ABBREV_TAC `h = \z:real^M. @k. (z - k % a)
IN span b` THEN
SUBGOAL_THEN `!z:real^M. z
IN span(a
INSERT b)
==> (z - h(z) % a)
IN span(b) /\
!k. (z - k % a)
IN span(b) ==> (k = h(z))`
MP_TAC THENL
[GEN_TAC THEN DISCH_TAC THEN
MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
[EXPAND_TAC "h" THEN CONV_TAC SELECT_CONV THEN
ASM_MESON_TAC[
SPAN_BREAKDOWN_EQ];
ALL_TAC] THEN
REWRITE_TAC[
RIGHT_IMP_FORALL_THM; IMP_IMP] THEN GEN_TAC THEN
DISCH_THEN(MP_TAC o MATCH_MP
SPAN_SUB) THEN
REWRITE_TAC[VECTOR_ARITH `(z - a % v) - (z - b % v) = (b - a) % v`] THEN
ASM_CASES_TAC `k = (h:real^M->
real) z` THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o SPEC `inv(k - (h:real^M->
real) z)` o
MATCH_MP
SPAN_MUL) THEN
ASM_SIMP_TAC[REAL_MUL_LINV;
VECTOR_MUL_ASSOC;
REAL_SUB_0] THEN
ASM_REWRITE_TAC[
VECTOR_MUL_LID];
ALL_TAC] THEN
REWRITE_TAC[TAUT `(a ==> b /\ c) <=> (a ==> b) /\ (a ==> c)`] THEN
REWRITE_TAC[
RIGHT_IMP_FORALL_THM; IMP_IMP] THEN
GEN_REWRITE_TAC LAND_CONV [
FORALL_AND_THM] THEN STRIP_TAC THEN
EXISTS_TAC `\z:real^M. h(z) % (f:real^M->real^N)(a) + g(z - h(z) % a)` THEN
REPEAT CONJ_TAC THENL
[MAP_EVERY X_GEN_TAC [`x:real^M`; `y:real^M`] THEN STRIP_TAC THEN
SUBGOAL_THEN `(h:real^M->
real)(x + y) = h(x) + h(y)` ASSUME_TAC THENL
[CONV_TAC SYM_CONV THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[VECTOR_ARITH
`(x + y) - (k + l) % a = (x - k % a) + (y - l % a)`] THEN
CONJ_TAC THEN MATCH_MP_TAC
SPAN_ADD THEN ASM_REWRITE_TAC[] THEN
ASM_SIMP_TAC[];
ALL_TAC] THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`(x + y) - (k + l) % a = (x - k % a) + (y - l % a)`] THEN
ASM_SIMP_TAC[] THEN VECTOR_ARITH_TAC;
MAP_EVERY X_GEN_TAC [`x:real^M`; `c:real`] THEN STRIP_TAC THEN
SUBGOAL_THEN `(h:real^M->
real)(c % x) = c * h(x)` ASSUME_TAC THENL
[CONV_TAC SYM_CONV THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[VECTOR_ARITH
`c % x - (c * k) % a = c % (x - k % a)`] THEN
CONJ_TAC THEN MATCH_MP_TAC
SPAN_MUL THEN ASM_REWRITE_TAC[] THEN
ASM_SIMP_TAC[];
ALL_TAC] THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`c % x - (c * k) % a = c % (x - k % a)`] THEN
ASM_SIMP_TAC[] THEN VECTOR_ARITH_TAC;
ALL_TAC] THEN
X_GEN_TAC `x:real^M` THEN REWRITE_TAC[
IN_INSERT] THEN
DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC ASSUME_TAC) THENL
[SUBGOAL_THEN `&1 = h(a:real^M)` (SUBST1_TAC o SYM) THENL
[FIRST_X_ASSUM MATCH_MP_TAC; ALL_TAC] THEN
REWRITE_TAC[VECTOR_ARITH `a - &1 % a =
vec 0`;
SPAN_0] THENL
[ASM_MESON_TAC[
SPAN_SUPERSET;
SUBSET;
IN_INSERT]; ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`
vec 0:real^M`; `
vec 0:real^M`]) THEN
REWRITE_TAC[
SPAN_0;
VECTOR_ADD_LID] THEN
REWRITE_TAC[VECTOR_ARITH `(a = a + a) <=> (a =
vec 0)`] THEN
DISCH_THEN SUBST1_TAC THEN VECTOR_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `&0 = h(x:real^M)` (SUBST1_TAC o SYM) THENL
[FIRST_X_ASSUM MATCH_MP_TAC; ALL_TAC] THEN
REWRITE_TAC[
VECTOR_ADD_LID;
VECTOR_MUL_LZERO;
VECTOR_SUB_RZERO] THEN
ASM_MESON_TAC[
SUBSET;
IN_INSERT;
SPAN_SUPERSET]);;
(* ------------------------------------------------------------------------- *)
(* Linear functions are equal on a subspace if they are on a spanning set. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Similar results for bilinear functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Detailed theorems about left and right invertibility in general case. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* An injective map real^N->real^N is also surjective. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* And vice versa. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Hence either is enough for isomorphism. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Left and right inverses are the same for R^N->R^N. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Moreover, a one-sided inverse is automatically linear. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Without (ostensible) constraints on types, though dimensions must match. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* The same result in terms of square matrices. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Invertibility of matrices and corresponding linear functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Left-invertible linear transformation has a lower bound. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Preservation of dimension by injective map. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Considering an n-element vector as an n-by-1 or 1-by-n matrix. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Rank of a matrix. Equivalence of row and column rank is taken from *)
(* George Mackiw's paper, Mathematics Magazine 1995, p. 285. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Basic lemmas about hyperplanes and halfspaces. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* A non-injective linear function maps into a hyperplane. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Orthogonal bases, Gram-Schmidt process, and related theorems. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Analogous theorems for existence of orthonormal basis for a subspace. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Decomposing a vector into parts in orthogonal subspaces. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Existence of isometry between subspaces of same dimension. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Properties of special hyperplanes. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* More theorems about dimensions of different subspaces. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* More about product spaces. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* More about rank from the rank/nullspace formula. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Infinity norm. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Prove that it differs only up to a bound from Euclidean norm. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Equality in Cauchy-Schwarz and triangle inequalities. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Collinearity. *)
(* ------------------------------------------------------------------------- *)
let COLLINEAR_2 = prove
(`!x y:real^N.
collinear {x,y}`,
REPEAT GEN_TAC THEN REWRITE_TAC[
collinear;
IN_INSERT;
NOT_IN_EMPTY] THEN
EXISTS_TAC `x - y:real^N` THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
[EXISTS_TAC `&0`; EXISTS_TAC `&1`; EXISTS_TAC `-- &1`; EXISTS_TAC `&0`] THEN
VECTOR_ARITH_TAC);;
let COLLINEAR_LEMMA = prove
(`!x y:real^N.
collinear {
vec 0,x,y} <=>
x =
vec 0 \/ y =
vec 0 \/ ?c. y = c % x`,
REPEAT GEN_TAC THEN
MAP_EVERY ASM_CASES_TAC [`x:real^N =
vec 0`; `y:real^N =
vec 0`] THEN
TRY(ASM_REWRITE_TAC[
INSERT_AC;
COLLINEAR_SING;
COLLINEAR_2] THEN NO_TAC) THEN
ASM_REWRITE_TAC[
collinear] THEN EQ_TAC THENL
[DISCH_THEN(X_CHOOSE_THEN `u:real^N`
(fun
th -> MP_TAC(SPECL [`x:real^N`; `
vec 0:real^N`]
th) THEN
MP_TAC(SPECL [`y:real^N`; `
vec 0:real^N`]
th))) THEN
REWRITE_TAC[
IN_INSERT;
VECTOR_SUB_RZERO] THEN
DISCH_THEN(X_CHOOSE_THEN `e:real` SUBST_ALL_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` SUBST_ALL_TAC) THEN
EXISTS_TAC `e / d` THEN REWRITE_TAC[
VECTOR_MUL_ASSOC] THEN
RULE_ASSUM_TAC(REWRITE_RULE[
VECTOR_MUL_EQ_0; DE_MORGAN_THM]) THEN
ASM_SIMP_TAC[
REAL_DIV_RMUL];
STRIP_TAC THEN EXISTS_TAC `x:real^N` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
IN_INSERT;
NOT_IN_EMPTY] THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[] THENL
[EXISTS_TAC `&0`; EXISTS_TAC `-- &1`; EXISTS_TAC `--c`;
EXISTS_TAC `&1`; EXISTS_TAC `&0`; EXISTS_TAC `&1 - c`;
EXISTS_TAC `c:real`; EXISTS_TAC `c - &1`; EXISTS_TAC `&0`] THEN
VECTOR_ARITH_TAC]);;
let COLLINEAR_3_EXPAND = prove
(`!a b c:real^N.
collinear{a,b,c} <=> a = c \/ ?u. b = u % a + (&1 - u) % c`,
REPEAT GEN_TAC THEN
ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN
ONCE_REWRITE_TAC[
COLLINEAR_3] THEN
REWRITE_TAC[
COLLINEAR_LEMMA;
VECTOR_SUB_EQ] THEN
ASM_CASES_TAC `a:real^N = c` THEN ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `b:real^N = c` THEN
ASM_REWRITE_TAC[VECTOR_ARITH `u % c + (&1 - u) % c = c`] THENL
[EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC;
AP_TERM_TAC THEN ABS_TAC THEN VECTOR_ARITH_TAC]);;
let COLLINEAR_TRIPLES = prove
(`!s a b:real^N.
~(a = b)
==> (
collinear(a
INSERT b
INSERT s) <=>
!x. x
IN s ==>
collinear{a,b,x})`,
REPEAT STRIP_TAC THEN EQ_TAC THENL
[REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
(REWRITE_RULE[
IMP_CONJ]
COLLINEAR_SUBSET)) THEN
ASM SET_TAC[];
ONCE_REWRITE_TAC[SET_RULE `{a,b,x} = {a,x,b}`] THEN
ASM_REWRITE_TAC[
COLLINEAR_3_EXPAND] THEN DISCH_TAC THEN
SUBGOAL_THEN
`!x:real^N. x
IN (a
INSERT b
INSERT s) ==> ?u. x = u % a + (&1 - u) % b`
MP_TAC THENL
[ASM_REWRITE_TAC[
FORALL_IN_INSERT] THEN CONJ_TAC THENL
[EXISTS_TAC `&1` THEN VECTOR_ARITH_TAC;
EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC];
POP_ASSUM_LIST(K ALL_TAC) THEN DISCH_TAC THEN
REWRITE_TAC[
collinear] THEN EXISTS_TAC `b - a:real^N` THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
FIRST_X_ASSUM(fun
th -> MP_TAC(SPEC `x:real^N`
th) THEN MP_TAC(SPEC
`y:real^N`
th)) THEN
ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`(u % a + (&1 - u) % b) - (v % a + (&1 - v) % b):real^N =
(v - u) % (b - a)`] THEN
MESON_TAC[]]]);;
let COLLINEAR_3_TRANS = prove
(`!a b c d:real^N.
collinear{a,b,c} /\
collinear{b,c,d} /\ ~(b = c) ==>
collinear{a,b,d}`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC
COLLINEAR_SUBSET THEN
EXISTS_TAC `{b:real^N,c,a,d}` THEN ASM_SIMP_TAC[
COLLINEAR_4_3] THEN
CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN
REPEAT(POP_ASSUM MP_TAC) THEN SIMP_TAC[
INSERT_AC]);;
(* ------------------------------------------------------------------------- *)
(* Between-ness. *)
(* ------------------------------------------------------------------------- *)
let COLLINEAR_BETWEEN_CASES = prove
(`!a b c:real^N.
collinear {a,b,c} <=>
between a (b,c) \/
between b (c,a) \/
between c (a,b)`,
REPEAT STRIP_TAC THEN EQ_TAC THENL
[REWRITE_TAC[
COLLINEAR_3_EXPAND] THEN
ASM_CASES_TAC `c:real^N = a` THEN ASM_REWRITE_TAC[
BETWEEN_REFL] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[
between;
dist] THEN
REWRITE_TAC[VECTOR_ARITH `(u % a + (&1 - u) % c) - c = --u % (c - a)`;
VECTOR_ARITH `(u % a + (&1 - u) % c) - a = (&1 - u) % (c - a)`;
VECTOR_ARITH `c - (u % a + (&1 - u) % c) = u % (c - a)`;
VECTOR_ARITH `a - (u % a + (&1 - u) % c) = (u - &1) % (c - a)`] THEN
REWRITE_TAC[
NORM_MUL] THEN
SUBST1_TAC(NORM_ARITH `
norm(a - c:real^N) =
norm(c - a)`) THEN
REWRITE_TAC[REAL_ARITH `a * c + c = (a + &1) * c`; GSYM
REAL_ADD_RDISTRIB;
REAL_ARITH `c + a * c = (a + &1) * c`] THEN
ASM_REWRITE_TAC[
REAL_EQ_MUL_RCANCEL;
REAL_RING `n = x * n <=> n = &0 \/ x = &1`] THEN
ASM_REWRITE_TAC[
NORM_EQ_0;
VECTOR_SUB_EQ] THEN REAL_ARITH_TAC;
DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN (MP_TAC o MATCH_MP
BETWEEN_IMP_COLLINEAR)) THEN
REWRITE_TAC[
INSERT_AC]]);;
(* ------------------------------------------------------------------------- *)
(* Midpoint between two points. *)
(* ------------------------------------------------------------------------- *)
let DIST_MIDPOINT = prove
(`!a b.
dist(a,
midpoint(a,b)) =
dist(a,b) / &2 /\
dist(b,
midpoint(a,b)) =
dist(a,b) / &2 /\
dist(
midpoint(a,b),a) =
dist(a,b) / &2 /\
dist(
midpoint(a,b),b) =
dist(a,b) / &2`,
REWRITE_TAC[
midpoint] THEN NORM_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* General "one way" lemma for properties preserved by injective map. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Inference rule to apply it conveniently. *)
(* *)
(* |- !f s. P s /\ linear f ==> P(IMAGE f s) [or /\ commuted] *)
(* --------------------------------------------------------------- *)
(* |- !f s. linear f /\ (!x y. f x = f y ==> x = y) *)
(* ==> (Q(IMAGE f s) <=> P s) *)
(* ------------------------------------------------------------------------- *)
let LINEAR_INVARIANT_RULE th =
let [f;s] = fst(strip_forall(concl th)) in
let (rm,rn) = dest_fun_ty (type_of f) in
let m = last(snd(dest_type rm)) and n = last(snd(dest_type rn)) in
let th' = INST_TYPE [m,n; n,m] th in
let th0 = CONJ th th' in
let th1 = try MATCH_MP WLOG_LINEAR_INJECTIVE_IMAGE_2 th0
with Failure _ ->
MATCH_MP WLOG_LINEAR_INJECTIVE_IMAGE_2
(GEN_REWRITE_RULE (BINOP_CONV o ONCE_DEPTH_CONV) [CONJ_SYM] th0) in
GEN_REWRITE_RULE BINDER_CONV [RIGHT_IMP_FORALL_THM] th1;;
(* ------------------------------------------------------------------------- *)
(* Immediate application. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Storage of useful "invariance under linear map / translation" theorems. *)
(* ------------------------------------------------------------------------- *)
let invariant_under_linear = ref([]:thm list);;
let invariant_under_translation = ref([]:thm list);;
let scaling_theorems = ref([]:thm list);;
(* ------------------------------------------------------------------------- *)
(* Scaling theorems and derivation from linear invariance. *)
(* ------------------------------------------------------------------------- *)
let INJECTIVE_SCALING = prove
(`!c. (!x y:real^N. c % x = c % y ==> x = y) <=> ~(c = &0)`,
GEN_TAC THEN REWRITE_TAC[
VECTOR_MUL_LCANCEL] THEN
ASM_CASES_TAC `c:real = &0` THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o SPECL [`
vec 0:real^N`; `
vec 1:real^N`]) THEN
REWRITE_TAC[
VEC_EQ; ARITH]);;
let SCALING_INVARIANT =
let pths = (CONJUNCTS o UNDISCH o prove)
(`&0 < c
==> linear(\x:real^N. c % x) /\
(!x y:real^N. c % x = c % y ==> x = y) /\
(!y:real^N. ?x. c % x = y)`,
SIMP_TAC[REAL_LT_IMP_NZ; LINEAR_SCALING;
INJECTIVE_SCALING; SURJECTIVE_SCALING])
and sc_tm = `\x:real^N. c % x`
and sa_tm = `&0:real < c`
and c_tm = `c:real` in
fun th ->
let ith = BETA_RULE(ISPEC sc_tm th) in
let avs,bod = strip_forall(concl ith) in
let cjs = conjuncts(lhand bod) in
let cths = map (fun t -> find(fun th -> aconv (concl th) t) pths) cjs in
let oth = MP (SPECL avs ith) (end_itlist CONJ cths) in
GEN c_tm (DISCH sa_tm (GENL avs oth));;
let scaling_theorems = ref([]:thm list);;
(* ------------------------------------------------------------------------- *)
(* Augmentation of the lists. The "add_linear_invariants" also updates *)
(* the scaling theorems automatically, so only a few of those will need *)
(* to be added explicitly. *)
(* ------------------------------------------------------------------------- *)
let add_scaling_theorems thl =
(scaling_theorems := (!scaling_theorems) @ thl);;
let add_linear_invariants thl =
ignore(mapfilter (fun th -> add_scaling_theorems[SCALING_INVARIANT th]) thl);
(invariant_under_linear := (!invariant_under_linear) @ thl);;
let add_translation_invariants thl =
(invariant_under_translation := (!invariant_under_translation) @ thl);;
(* ------------------------------------------------------------------------- *)
(* Start with some basic set equivalences. *)
(* We give them all an injectivity hypothesis even if it's not necessary. *)
(* For just the intersection theorem we add surjectivity (more manageable *)
(* than assuming that the set isn't empty). *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Now add arithmetical equivalences. *)
(* ------------------------------------------------------------------------- *)
add_linear_invariants
[GSYM LINEAR_ADD;
GSYM LINEAR_CMUL;
GSYM LINEAR_SUB;
GSYM LINEAR_NEG;
MIDPOINT_LINEAR_IMAGE;
MESON[] `!f:real^M->real^N x.
(!x. norm(f x) = norm x) ==> norm(f x) = norm x`;
PRESERVES_NORM_PRESERVES_DOT;
MESON[dist; LINEAR_SUB]
`!f:real^M->real^N x y.
linear f /\ (!x. norm(f x) = norm x)
==> dist(f x,f y) = dist(x,y)`;
MESON[] `!f:real^M->real^N x y.
(!x y. f x = f y ==> x = y) ==> (f x = f y <=> x = y)`;
SUBSPACE_LINEAR_IMAGE_EQ;
ORTHOGONAL_LINEAR_IMAGE_EQ;
SPAN_LINEAR_IMAGE;
DEPENDENT_LINEAR_IMAGE_EQ;
INDEPENDENT_LINEAR_IMAGE_EQ;
DIM_INJECTIVE_LINEAR_IMAGE];;
add_translation_invariants
[VECTOR_ARITH `!a x y. a + x:real^N = a + y <=> x = y`;
NORM_ARITH `!a x y. dist(a + x,a + y) = dist(x,y)`;
VECTOR_ARITH `!a x y. &1 / &2 % ((a + x) + (a + y)) = a + &1 / &2 % (x + y)`;
VECTOR_ARITH `!a x y. inv(&2) % ((a + x) + (a + y)) = a + inv(&2) % (x + y)`;
VECTOR_ARITH `!a x y. (a + x) - (a + y):real^N = x - y`;
(EQT_ELIM o (REWRITE_CONV[midpoint] THENC(EQT_INTRO o NORM_ARITH)))
`!a x y. midpoint(a + x,a + y) = a + midpoint(x,y)`;
(EQT_ELIM o (REWRITE_CONV[between] THENC(EQT_INTRO o NORM_ARITH)))
`!a x y z. between (a + x) (a + y,a + z) <=> between x (y,z)`];;
let th = prove
(`!a s b c:real^N. (a + b) + c
IN IMAGE (\x. a + x) s <=> (b + c)
IN s`,
REWRITE_TAC[
IN_IMAGE; VECTOR_ARITH
`(a + b) + c:real^N = a + x <=> x = b + c`] THEN
MESON_TAC[]) in
add_translation_invariants [
th];;
(* ------------------------------------------------------------------------- *)
(* A few for lists. *)
(* ------------------------------------------------------------------------- *)
add_translation_invariants [MEM_TRANSLATION];;
add_linear_invariants [MEM_LINEAR_IMAGE];;
(* ------------------------------------------------------------------------- *)
(* A few scaling theorems that don't come from invariance theorems. Most are *)
(* artificially weak with 0 < c hypotheses, so we don't bind them to names. *)
(* ------------------------------------------------------------------------- *)
add_scaling_theorems
[REAL_ARITH `!c. &0 < c ==> !a b. a * c * b = c * a * b`;
REAL_ARITH `!c. &0 < c ==> !a b. c * a + c * b = c * (a + b)`;
REAL_ARITH `!c. &0 < c ==> !a b. c * a - c * b = c * (a - b)`;
REAL_FIELD `!c. &0 < c ==> !a b. c * a = c * b <=> a = b`;
MESON[REAL_LT_LMUL_EQ] `!c. &0 < c ==> !a b. c * a < c * b <=> a < b`;
MESON[REAL_LE_LMUL_EQ] `!c. &0 < c ==> !a b. c * a <= c * b <=> a <= b`;
MESON[REAL_LT_LMUL_EQ; real_gt]
`!c. &0 < c ==> !a b. c * a > c * b <=> a > b`;
MESON[REAL_LE_LMUL_EQ; real_ge]
`!c. &0 < c ==> !a b. c * a >= c * b <=> a >= b`;
MESON[REAL_POW_MUL]
`!c. &0 < c ==> !a n. (c * a) pow n = c pow n * a pow n`;
REAL_ARITH `!c. &0 < c ==> !a b n. a * c pow n * b = c pow n * a * b`;
REAL_ARITH
`!c. &0 < c ==> !a b n. c pow n * a + c pow n * b = c pow n * (a + b)`;
REAL_ARITH
`!c. &0 < c ==> !a b n. c pow n * a - c pow n * b = c pow n * (a - b)`;
MESON[REAL_POW_LT; REAL_EQ_LCANCEL_IMP; REAL_LT_IMP_NZ]
`!c. &0 < c ==> !a b n. c pow n * a = c pow n * b <=> a = b`;
MESON[REAL_LT_LMUL_EQ; REAL_POW_LT]
`!c. &0 < c ==> !a b n. c pow n * a < c pow n * b <=> a < b`;
MESON[REAL_LE_LMUL_EQ; REAL_POW_LT]
`!c. &0 < c ==> !a b n. c pow n * a <= c pow n * b <=> a <= b`;
MESON[REAL_LT_LMUL_EQ; real_gt; REAL_POW_LT]
`!c. &0 < c ==> !a b n. c pow n * a > c pow n * b <=> a > b`;
MESON[REAL_LE_LMUL_EQ; real_ge; REAL_POW_LT]
`!c. &0 < c ==> !a b n. c pow n * a >= c pow n * b <=> a >= b`];;
(* ------------------------------------------------------------------------- *)
(* Theorem deducing quantifier mappings from surjectivity. *)
(* ------------------------------------------------------------------------- *)
let QUANTIFY_SURJECTION_THM = prove
(`!f:A->B.
(!y. ?x. f x = y)
==> ((!P. (!x. P x) <=> (!x. P (f x))) /\
(!P. (?x. P x) <=> (?x. P (f x))) /\
(!Q. (!s. Q s) <=> (!s. Q(
IMAGE f s))) /\
(!Q. (?s. Q s) <=> (?s. Q(
IMAGE f s)))) /\
(!P. {x | P x} =
IMAGE f {x | P(f x)})`,
GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [
SURJECTIVE_RIGHT_INVERSE] THEN
DISCH_THEN(X_CHOOSE_TAC `g:B->A`) THEN
SUBGOAL_THEN `!s.
IMAGE (f:A->B) (
IMAGE g s) = s` ASSUME_TAC THENL
[ASM SET_TAC[]; CONJ_TAC THENL [ASM MESON_TAC[]; ASM SET_TAC[]]]);;
let QUANTIFY_SURJECTION_HIGHER_THM = prove
(`!f:A->B.
(!y. ?x. f x = y)
==> ((!P. (!x. P x) <=> (!x. P (f x))) /\
(!P. (?x. P x) <=> (?x. P (f x))) /\
(!Q. (!s. Q s) <=> (!s. Q(
IMAGE f s))) /\
(!Q. (?s. Q s) <=> (?s. Q(
IMAGE f s))) /\
(!Q. (!s. Q s) <=> (!s. Q(
IMAGE (
IMAGE f) s))) /\
(!Q. (?s. Q s) <=> (?s. Q(
IMAGE (
IMAGE f) s))) /\
(!P. (!g:real^1->B. P g) <=> (!g. P(f o g))) /\
(!P. (?g:real^1->B. P g) <=> (?g. P(f o g))) /\
(!P. (!g:num->B. P g) <=> (!g. P(f o g))) /\
(!P. (?g:num->B. P g) <=> (?g. P(f o g))) /\
(!Q. (!l. Q l) <=> (!l. Q(
MAP f l))) /\
(!Q. (?l. Q l) <=> (?l. Q(
MAP f l)))) /\
((!P. {x | P x} =
IMAGE f {x | P(f x)}) /\
(!Q. {s | Q s} =
IMAGE (
IMAGE f) {s | Q(
IMAGE f s)}) /\
(!R. {l | R l} =
IMAGE (
MAP f) {l | R(
MAP f l)}))`,
(* ------------------------------------------------------------------------- *)
(* Apply such quantifier and set expansions once per level at depth. *)
(* In the PARTIAL version, avoid expanding named variables in list. *)
(* ------------------------------------------------------------------------- *)
let PARTIAL_EXPAND_QUANTS_CONV avoid th =
let ath,sth = CONJ_PAIR th in
let conv1 = GEN_REWRITE_CONV I [ath]
and conv2 = GEN_REWRITE_CONV I [sth] in
let conv1' tm =
let th = conv1 tm in
if mem (fst(dest_var(fst(dest_abs(rand tm))))) avoid
then failwith "Not going to expand this variable" else th in
let rec conv tm =
((conv1' THENC BINDER_CONV conv) ORELSEC
(conv2 THENC
RAND_CONV(RAND_CONV(ABS_CONV(BINDER_CONV(LAND_CONV conv))))) ORELSEC
SUB_CONV conv) tm in
conv;;
let EXPAND_QUANTS_CONV = PARTIAL_EXPAND_QUANTS_CONV [];;