(* ========================================================================= *)
(* 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`]);;
let SUM_4 = prove
(`!t. sum(1..4) t = t(1) + t(2) + t(3) + t(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`;;
let vector_neg = new_definition
`(vector_neg:real^N->real^N) x = lambda i. --(x$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"));;
let vector_mul = new_definition
`((%):real->real^N->real^N) c x = lambda i. c * x$i`;;
(* ------------------------------------------------------------------------- *)
(* Vectors corresponding to small naturals. Perhaps should overload "&"? *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Dot products. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("dot",(20,"right"));;
let DOT_1 = prove
(`(x:real^1) dot (y:real^1) = x$1 * y$1`,
REWRITE_TAC[dot; DIMINDEX_1;
SUM_1]);;
let DOT_2 = prove
(`(x:real^2) dot (y:real^2) = x$1 * y$1 + x$2 * y$2`,
REWRITE_TAC[dot; DIMINDEX_2;
SUM_2]);;
let DOT_3 = prove
(`(x:real^3) dot (y:real^3) = x$1 * y$1 + x$2 * y$2 + x$3 * y$3`,
REWRITE_TAC[dot; DIMINDEX_3;
SUM_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`,
REWRITE_TAC[dot; DIMINDEX_4;
SUM_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. *)
(* ------------------------------------------------------------------------- *)
let DOT_SYM = VECTOR_ARITH `!x y. x dot y = y dot x`;;
let DOT_LADD = VECTOR_ARITH `!x y z. (x + y) dot z = (x dot z) + (y dot z)`;;
let DOT_RADD = VECTOR_ARITH `!x y z. x dot (y + z) = (x dot y) + (x dot z)`;;
let DOT_LSUB = VECTOR_ARITH `!x y z. (x - y) dot z = (x dot z) - (y dot z)`;;
let DOT_RSUB = VECTOR_ARITH `!x y z. x dot (y - z) = (x dot y) - (x dot z)`;;
let DOT_LMUL = VECTOR_ARITH `!c x y. (c % x) dot y = c * (x dot y)`;;
let DOT_RMUL = VECTOR_ARITH `!c x y. x dot (c % y) = c * (x dot y)`;;
let DOT_LNEG = VECTOR_ARITH `!x y. (--x) dot y = --(x dot y)`;;
let DOT_RNEG = VECTOR_ARITH `!x y. x dot (--y) = --(x dot y)`;;
(* ------------------------------------------------------------------------- *)
(* 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! *)
(* ------------------------------------------------------------------------- *)
let SQRT_MUL = prove
(`!x y. &0 <= x /\ &0 <= y
==> (sqrt(x * y) = sqrt x * sqrt y)`,
let SQRT_DIV = prove
(`!x y. &0 <= x /\ &0 <= y ==> (sqrt (x / y) = sqrt x / sqrt y)`,
let SQRT_INJ = prove
(`!x y. &0 <= x /\ &0 <= y ==> ((sqrt(x) = sqrt(y)) <=> (x = y))`,
(* ------------------------------------------------------------------------- *)
(* Hence derive more interesting properties of the norm. *)
(* ------------------------------------------------------------------------- *)
let NORM_EQ = prove
(`!x y. (norm x = norm y) <=> (x dot x = y dot y)`,
REWRITE_TAC[GSYM REAL_LE_ANTISYM;
NORM_LE]);;
let L1_LE_NORM = prove
(`!x:real^N.
sum(1..dimindex(:N)) (\i. abs(x$i)) <= sqrt(&(dimindex(:N))) * norm x`,
(* ------------------------------------------------------------------------- *)
(* Squaring equations and inequalities involving norms. *)
(* ------------------------------------------------------------------------- *)
let NORM_EQ_SQUARE = prove
(`!x:real^N. norm(x) = a <=> &0 <= a /\ x dot x = a pow 2`,
REWRITE_TAC[
DOT_SQUARE_NORM] THEN
ONCE_REWRITE_TAC[REAL_RING `x pow 2 = a pow 2 <=> x = a \/ x + a = &0`] THEN
GEN_TAC THEN MP_TAC(ISPEC `x:real^N`
NORM_POS_LE) THEN REAL_ARITH_TAC);;
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. *)
(* ------------------------------------------------------------------------- *)
let DOT_NORM = prove
(`!x y. x dot y = (norm(x + y) pow 2 - norm(x) pow 2 - norm(y) pow 2) / &2`,
let DOT_NORM_NEG = prove
(`!x y. x dot y = ((norm(x) pow 2 + norm(y) pow 2) - norm(x - y) pow 2) / &2`,
let DOT_NORM_SUB = prove
(`!x y. x dot y = ((norm(x) pow 2 + norm(y) pow 2) - norm(x - y) pow 2) / &2`,
(* ------------------------------------------------------------------------- *)
(* Equality of vectors in terms of dot products. *)
(* ------------------------------------------------------------------------- *)
let VECTOR_EQ = prove
(`!x y. (x = y) <=> (x dot x = x dot y) /\ (y dot y = x dot x)`,
(* ------------------------------------------------------------------------- *)
(* Hence more metric properties. *)
(* ------------------------------------------------------------------------- *)
let DIST_NZ = prove
(`!x y. ~(x = y) <=> &0 < dist(x,y)`,
NORM_ARITH_TAC);;
let DIST_EQ = prove
(`!w x y z. dist(w,x) = dist(y,z) <=> dist(w,x) pow 2 = dist(y,z) pow 2`,
let DIST_0 = prove
(`!x. dist(x,vec 0) = norm(x) /\ dist(vec 0,x) = norm(x)`,
NORM_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Sums of vectors. *)
(* ------------------------------------------------------------------------- *)
let NEUTRAL_VECTOR_ADD = prove
(`neutral(+) = vec 0:real^N`,
REWRITE_TAC[neutral] THEN MATCH_MP_TAC
SELECT_UNIQUE THEN
REWRITE_TAC[VECTOR_ARITH `x + y = y <=> x = vec 0`;
VECTOR_ARITH `x + y = x <=> y = vec 0`]);;
let VSUM_COMPONENT = prove
(`!s f i. 1 <= i /\ i <= dimindex(:N)
==> ((vsum s (f:A->real^N))$i = sum s (\x. f(x)$i))`,
let VSUM_EQ = prove
(`!f g s. (!x. x
IN s ==> (f x = g x)) ==> (vsum s f = vsum s g)`,
let VSUM_CASES = prove
(`!s P f g.
FINITE s
==> vsum s (\x:A. if P x then (f x):real^N else g x) =
vsum {x | x
IN s /\ P x} f + vsum {x | x
IN s /\ ~P x} g`,
let VSUM_CLAUSES_NUMSEG = prove
(`(!m. vsum(m..0) f = if m = 0 then f(0) else vec 0) /\
(!m n. vsum(m..SUC n) f = if m <= SUC n then vsum(m..n) f + f(SUC n)
else vsum(m..n) f)`,
let VSUM_EQ_NUMSEG = prove
(`!f g m n.
(!x. m <= x /\ x <= n ==> (f x = g x))
==> (vsum(m .. n) f = vsum(m .. n) g)`,
let VSUM_DELTA = prove
(`!s a. vsum s (\x. if x = a then b else vec 0) =
if a
IN s then b else vec 0`,
let VSUM_ADD_SPLIT = prove
(`!f m n p.
m <= n + 1 ==> vsum(m..n + p) f = vsum(m..n) f + vsum(n + 1..n + p) f`,
let VSUM_IMAGE_NONZERO = prove
(`!d:B->real^N i:A->B s.
FINITE s /\
(!x y. x
IN s /\ y
IN s /\ ~(x = y) /\ i x = i y ==> d(i x) = vec 0)
==> vsum (
IMAGE i s) d = vsum s (d o i)`,
GEN_TAC THEN GEN_TAC THEN ONCE_REWRITE_TAC[
IMP_CONJ] THEN
MATCH_MP_TAC
FINITE_INDUCT_STRONG THEN
SIMP_TAC[
IMAGE_CLAUSES;
VSUM_CLAUSES;
FINITE_IMAGE] THEN
MAP_EVERY X_GEN_TAC [`a:A`; `s:A->bool`] THEN
REWRITE_TAC[
IN_INSERT] THEN REPEAT STRIP_TAC THEN
SUBGOAL_THEN `vsum s ((d:B->real^N) o (i:A->B)) = vsum (
IMAGE i s) d`
SUBST1_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
o_THM] THEN
REWRITE_TAC[VECTOR_ARITH `a = x + a <=> x = vec 0`] THEN
ASM_MESON_TAC[
IN_IMAGE]);;
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_DIFFS_ALT = prove
(`!m n. vsum(m..n) (\k. f(k + 1) - f(k)) =
if m <= n then f(n + 1) - f(m) else vec 0`,
let VSUM_EQ_GENERAL = prove
(`!s:A->bool t:B->bool (f:A->real^N) g h.
(!y. y
IN t ==> ?!x. x
IN s /\ h x = y) /\
(!x. x
IN s ==> h x
IN t /\ g(h x) = f x)
==> vsum s f = vsum t g`,
let VSUM_EQ_GENERAL_INVERSES = prove
(`!s t (f:A->real^N) (g:B->real^N) h k.
(!y. y
IN t ==> k y
IN s /\ h (k y) = y) /\
(!x. x
IN s ==> h x
IN t /\ k (h x) = x /\ g (h x) = f x)
==> vsum s f = vsum t g`,
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_BIJECTION = prove
(`!f:A->real^N p s:A->bool.
(!x. x
IN s ==> p(x)
IN s) /\
(!y. y
IN s ==> ?!x. x
IN s /\ p(x) = y)
==> vsum s f = vsum s (f o p)`,
REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN
MATCH_MP_TAC
VSUM_EQ_GENERAL THEN EXISTS_TAC `p:A->A` THEN
ASM_REWRITE_TAC[
o_THM]);;
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_COMBINE_L = prove
(`!f m n p.
0 < n /\ m <= n /\ n <= p + 1
==> vsum(m..n - 1) f + vsum(n..p) f = vsum(m..p) f`,
let VSUM_COMBINE_R = prove
(`!f m n p.
m <= n + 1 /\ n <= p
==> vsum(m..n) f + vsum(n + 1..p) f = vsum(m..p) f`,
let VSUM_SWAP_NUMSEG = prove
(`!a b c d f.
vsum (a..b) (\i. vsum (c..d) (f i)) =
vsum (c..d) (\j. vsum (a..b) (\i. f i j))`,
let VSUM_PAIR = prove
(`!f:num->real^N m n.
vsum(2*m..2*n+1) f = vsum(m..n) (\i. f(2*i) + f(2*i+1))`,
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)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC
VSUM_EQ THEN
ASM_SIMP_TAC[
IN_ELIM_THM;
IN_NUMSEG]) in
extend_basic_congs (map SPEC_ALL (CONJUNCTS th));;
(* ------------------------------------------------------------------------- *)
(* 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 NORM_BASIS = prove
(`!k. 1 <= k /\ k <= dimindex(:N)
==> (norm(basis k :real^N) = &1)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[basis; dot;
vector_norm] THEN
GEN_REWRITE_TAC RAND_CONV [GSYM
SQRT_1] THEN AP_TERM_TAC THEN
MATCH_MP_TAC
EQ_TRANS THEN EXISTS_TAC
`sum (1..dimindex(:N)) (\i. if i = k then &1 else &0)` THEN
CONJ_TAC THENL
[MATCH_MP_TAC
SUM_EQ_NUMSEG THEN
ASM_SIMP_TAC[
LAMBDA_BETA;
IN_NUMSEG;
EQ_SYM_EQ] THEN
REPEAT STRIP_TAC THEN COND_CASES_TAC THEN REAL_ARITH_TAC;
ASM_REWRITE_TAC[
SUM_DELTA;
IN_NUMSEG]]);;
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`]);;
let BASIS_INJ = prove
(`!i j. 1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N) /\
(basis i :real^N = basis j)
==> (i = j)`,
SIMP_TAC[basis;
CART_EQ;
LAMBDA_BETA] THEN REPEAT GEN_TAC THEN
REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
ASM_SIMP_TAC[REAL_OF_NUM_EQ;
ARITH_EQ]);;
let BASIS_INJ_EQ = prove
(`!i j. 1 <= i /\ i <= dimindex(:N) /\ 1 <= j /\ j <= dimindex(:N)
==> (basis i:real^N = basis j <=> i = j)`,
let BASIS_NE = prove
(`!i j. 1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N) /\
~(i = j)
==> ~(basis i :real^N = basis j)`,
let BASIS_COMPONENT = prove
(`!k i. 1 <= i /\ i <= dimindex(:N)
==> ((basis k :real^N)$i = if i = k then &1 else &0)`,
let BASIS_EXPANSION_UNIQUE = prove
(`!f x:real^N. (vsum(1..dimindex(:N)) (\i. f(i) % basis i) = x) <=>
(!i. 1 <= i /\ i <= dimindex(:N) ==> f(i) = x$i)`,
let DOT_BASIS = prove
(`!x:real^N i.
1 <= i /\ i <= dimindex(:N)
==> ((basis i) dot x = x$i) /\ (x dot (basis i) = x$i)`,
let DOT_BASIS_BASIS = prove
(`!i j. 1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N)
==> (basis i:real^N) dot (basis j) = if i = j then &1 else &0`,
(* ------------------------------------------------------------------------- *)
(* Orthogonality. *)
(* ------------------------------------------------------------------------- *)
let ORTHOGONAL_MUL = prove
(`(!a x y:real^N. orthogonal (a % x) y <=> a = &0 \/ orthogonal x y) /\
(!a x y:real^N. orthogonal x (a % y) <=> a = &0 \/ orthogonal x y)`,
let ORTHOGONAL_BASIS_BASIS = prove
(`!i j. 1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N)
==> (orthogonal (basis i :real^N) (basis j) <=> ~(i = j))`,
let ORTHOGONAL_CLAUSES = prove
(`(!a. orthogonal a (vec 0)) /\
(!a x c. orthogonal a x ==> orthogonal a (c % x)) /\
(!a x. orthogonal a x ==> orthogonal a (--x)) /\
(!a x y. orthogonal a x /\ orthogonal a y ==> orthogonal a (x + y)) /\
(!a x y. orthogonal a x /\ orthogonal a y ==> orthogonal a (x - y)) /\
(!a. orthogonal (vec 0) a) /\
(!a x c. orthogonal x a ==> orthogonal (c % x) a) /\
(!a x. orthogonal x a ==> orthogonal (--x) a) /\
(!a x y. orthogonal x a /\ orthogonal y a ==> orthogonal (x + y) a) /\
(!a x y. orthogonal x a /\ orthogonal y a ==> orthogonal (x - y) a)`,
(* ------------------------------------------------------------------------- *)
(* Explicit vector construction from lists. *)
(* ------------------------------------------------------------------------- *)
let VECTOR_3 = prove
(`(vector[x;y;z]:A^3)$1 = x /\
(vector[x;y;z]:A^3)$2 = y /\
(vector[x;y;z]:A^3)$3 = z`,
let VECTOR_4 = prove
(`(vector[w;x;y;z]:A^4)$1 = w /\
(vector[w;x;y;z]:A^4)$2 = x /\
(vector[w;x;y;z]:A^4)$3 = y /\
(vector[w;x;y;z]:A^4)$4 = z`,
SIMP_TAC[vector;
LAMBDA_BETA; DIMINDEX_4; ARITH;
LENGTH;
EL] THEN
REWRITE_TAC[num_CONV `3`; num_CONV `2`; num_CONV `1`;
HD;
TL;
EL]);;
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_COMPOSE_CMUL = prove
(`!f c. linear f ==> linear (\x. c % f(x))`,
SIMP_TAC[linear] THEN REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC);;
let LINEAR_COMPOSE_NEG = prove
(`!f. linear f ==> linear (\x. --(f(x)))`,
SIMP_TAC[linear] THEN REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC);;
let LINEAR_COMPOSE_ADD = prove
(`!f g. linear f /\ linear g ==> linear (\x. f(x) + g(x))`,
SIMP_TAC[linear] THEN REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC);;
let LINEAR_COMPOSE_SUB = prove
(`!f g. linear f /\ linear g ==> linear (\x. f(x) - g(x))`,
SIMP_TAC[linear] THEN REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC);;
let LINEAR_ZERO = prove
(`linear (\x. vec 0)`,
REWRITE_TAC[linear] THEN CONJ_TAC THEN VECTOR_ARITH_TAC);;
let LINEAR_ADD = prove
(`!f x y. linear f ==> (f(x + y) = f(x) + f(y))`,
SIMP_TAC[linear]);;
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_LADD = prove
(`!h x y z. bilinear h ==> h (x + y) z = (h x z) + (h y z)`,
SIMP_TAC[bilinear; linear]);;
let BILINEAR_RADD = prove
(`!h x y z. bilinear h ==> h x (y + z) = (h x y) + (h x z)`,
SIMP_TAC[bilinear; linear]);;
let BILINEAR_LMUL = prove
(`!h c x y. bilinear h ==> h (c % x) y = c % (h x y)`,
SIMP_TAC[bilinear; linear]);;
let BILINEAR_RMUL = prove
(`!h c x y. bilinear h ==> h x (c % y) = c % (h x y)`,
SIMP_TAC[bilinear; linear]);;
let BILINEAR_VSUM = prove
(`!h:real^M->real^N->real^P.
bilinear h /\
FINITE s /\
FINITE t
==> h (vsum s f) (vsum t g) = vsum (s
CROSS t) (\(i,j). h (f i) (g j))`,
REPEAT GEN_TAC THEN SIMP_TAC[bilinear; ETA_AX] THEN
ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c /\ d <=> (a /\ d) /\ (b /\ c)`] THEN
DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
ONCE_REWRITE_TAC[
LEFT_AND_FORALL_THM] THEN DISCH_TAC THEN
FIRST_ASSUM(MP_TAC o GEN_ALL o MATCH_MP
LINEAR_VSUM o SPEC_ALL) THEN
SIMP_TAC[] THEN ASM_SIMP_TAC[
LINEAR_VSUM;
o_DEF;
VSUM_VSUM_PRODUCT] THEN
REWRITE_TAC[GSYM
CROSS]);;
let BILINEAR_BOUNDED = prove
(`!h:real^M->real^N->real^P.
bilinear h ==> ?B. !x y. norm(h x y) <= B * norm(x) * norm(y)`,
let BILINEAR_BOUNDED_POS = prove
(`!h. bilinear h
==> ?B. &0 < B /\ !x y. norm(h x y) <= B * norm(x) * norm(y)`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(X_CHOOSE_TAC `B:real` o MATCH_MP
BILINEAR_BOUNDED) THEN
EXISTS_TAC `abs(B) + &1` THEN CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
POP_ASSUM MP_TAC THEN REPEAT(MATCH_MP_TAC
MONO_FORALL THEN GEN_TAC) THEN
MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
REPEAT(MATCH_MP_TAC
REAL_LE_RMUL THEN
SIMP_TAC[
NORM_POS_LE;
REAL_LE_MUL]) THEN
REAL_ARITH_TAC);;
let BILINEAR_VSUM_PARTIAL_SUC = prove
(`!f g h:real^M->real^N->real^P m n.
bilinear h
==> vsum (m..n) (\k. h (f k) (g(k + 1) - g(k))) =
if m <= n then h (f(n + 1)) (g(n + 1)) - h (f m) (g m) -
vsum (m..n) (\k. h (f(k + 1) - f(k)) (g(k + 1)))
else vec 0`,
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. *)
(* ------------------------------------------------------------------------- *)
let ADJOINT_CLAUSES = prove
(`!f:real^M->real^N.
linear f ==> (!x y. x dot (adjoint f)(y) = f(x) dot y) /\
(!x y. (adjoint f)(y) dot x = y dot f(x))`,
let ADJOINT_COMPOSE = prove
(`!f g:real^N->real^N.
linear f /\ linear g ==> adjoint(f o g) = adjoint g o adjoint f`,
let SELF_ADJOINT_COMPOSE = prove
(`!f g:real^N->real^N.
linear f /\ linear g /\ adjoint f = f /\ adjoint g = g
==> (adjoint(f o g) = f o g <=> f o g = g o f)`,
(* ------------------------------------------------------------------------- *)
(* 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_cmul = new_definition
`((%%):real->real^N^M->real^N^M) c A = lambda i j. c * A$i$j`;;
let matrix_neg = new_definition
`!A:real^N^M. --A = lambda i j. --(A$i$j)`;;
let matrix_add = new_definition
`!A:real^N^M B:real^N^M. A + B = lambda i j. A$i$j + B$i$j`;;
let matrix_sub = new_definition
`!A:real^N^M B:real^N^M. A - B = lambda i j. A$i$j - B$i$j`;;
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 matrix_vector_mul = new_definition
`!A:real^N^M x:real^N.
A ** x = lambda i. sum(1..dimindex(:N)) (\j. A$i$j * x$j)`;;
let vector_matrix_mul = new_definition
`!A:real^N^M x:real^M.
x ** A = lambda j. sum(1..dimindex(:M)) (\i. A$i$j * x$i)`;;
let TRANSP_COMPONENT = prove
(`!A:real^N^M i j. (transp A)$i$j = A$j$i`,
REPEAT GEN_TAC THEN
SUBGOAL_THEN `?k. 1 <= k /\ k <= dimindex(:N) /\
(!A:real^M^N. A$i = A$k) /\ (!z:real^N. z$i = z$k)`
CHOOSE_TAC THENL [REWRITE_TAC[
FINITE_INDEX_INRANGE_2]; ALL_TAC] THEN
SUBGOAL_THEN `?l. 1 <= l /\ l <= dimindex(:M) /\
(!A:real^N^M. A$j = A$l) /\ (!z:real^M. z$j = z$l)`
CHOOSE_TAC THENL [REWRITE_TAC[
FINITE_INDEX_INRANGE_2]; ALL_TAC] THEN
ASM_SIMP_TAC[transp;
LAMBDA_BETA]);;
let MAT_COMPONENT = prove
(`!n i j.
1 <= i /\ i <= dimindex(:M) /\
1 <= j /\ j <= dimindex(:N)
==> (mat n:real^N^M)$i$j = if i = j then &n else &0`,
let MATRIX_ADD_AC = prove
(`(A:real^N^M) + B = B + A /\
(A + B) + C = A + (B + C) /\
A + (B + C) = B + (A + C)`,
let ROW_TRANSP = prove
(`!A:real^N^M i.
1 <= i /\ i <= dimindex(:N) ==> row i (transp A) = column i A`,
let COLUMN_TRANSP = prove
(`!A:real^N^M i.
1 <= i /\ i <= dimindex(:M) ==> column i (transp A) = row i A`,
(* ------------------------------------------------------------------------- *)
(* Two sometimes fruitful ways of looking at matrix-vector multiplication. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Slightly gruesome lemmas: better to define sums over vectors really... *)
(* ------------------------------------------------------------------------- *)
let LINEAR_COMPONENTWISE_EXPANSION = prove
(`!f:real^M->real^N.
linear(f)
==> !x j. 1 <= j /\ j <= dimindex(:N)
==> (f x $j =
sum(1..dimindex(:M)) (\i. x$i * f(basis i)$j))`,
REWRITE_TAC[linear] THEN REPEAT STRIP_TAC THEN
GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o RAND_CONV)
[
VECTOR_COMPONENTWISE] THEN
SPEC_TAC(`dimindex(:M)`,`n:num`) THEN
INDUCT_TAC THEN REWRITE_TAC[
SUM_CLAUSES_NUMSEG; ARITH] THENL
[REWRITE_TAC[GSYM vec] THEN
GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o RAND_CONV)
[GSYM
VECTOR_MUL_LZERO] THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[
VECTOR_MUL_LZERO] THEN
ASM_SIMP_TAC[vec;
LAMBDA_BETA];
REWRITE_TAC[ARITH_RULE `1 <= SUC n`] THEN
ASSUM_LIST(fun thl -> REWRITE_TAC(map GSYM thl)) THEN
SIMP_TAC[GSYM
VECTOR_MUL_COMPONENT;
ASSUME `1 <= j`; ASSUME `j <= dimindex(:N)`] THEN
ASSUM_LIST(fun thl -> REWRITE_TAC(map GSYM thl)) THEN
SIMP_TAC[GSYM
VECTOR_ADD_COMPONENT;
ASSUME `1 <= j`; ASSUME `j <= dimindex(:N)`] THEN
ASSUM_LIST(fun thl -> REWRITE_TAC(map GSYM thl)) THEN
AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
ASM_SIMP_TAC[
CART_EQ;
VECTOR_ADD_COMPONENT;
LAMBDA_BETA] THEN
SIMP_TAC[
VECTOR_MUL_COMPONENT]]);;
(* ------------------------------------------------------------------------- *)
(* Inverse matrices (not necessarily square, but it's vacuous otherwise). *)
(* ------------------------------------------------------------------------- *)
let MATRIX_INV = prove
(`!A:real^N^M.
invertible A ==> A **
matrix_inv A = mat 1 /\
matrix_inv A ** A = mat 1`,
GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[
matrix_inv; invertible] THEN
CONV_TAC SELECT_CONV THEN ASM_REWRITE_TAC[GSYM invertible]);;
(* ------------------------------------------------------------------------- *)
(* Correspondence between matrices and linear operators. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Operator norm. *)
(* ------------------------------------------------------------------------- *)
let NORM_BOUND_GENERALIZE = prove
(`!f:real^M->real^N b.
linear f
==> ((!x. (norm(x) = &1) ==> norm(f x) <= b) <=>
(!x. norm(f x) <= b * norm(x)))`,
let ONORM = prove
(`!f:real^M->real^N.
linear f
==> (!x. norm(f x) <= onorm f * norm(x)) /\
(!b. (!x. norm(f x) <= b * norm(x)) ==> onorm f <= b)`,
let ONORM_EQ_0 = prove
(`!f:real^M->real^N. linear f ==> ((onorm f = &0) <=> (!x. f x = vec 0))`,
let ONORM_NEG = prove
(`!f:real^M->real^N. linear f ==> (onorm(\x. --(f x)) = onorm f)`,
let ONORM_TRIANGLE = prove
(`!f:real^M->real^N g.
linear f /\ linear g ==> onorm(\x. f x + g x) <= onorm f + onorm g`,
let ONORM_ID = prove
(`onorm(\x:real^N. x) = &1`,
REWRITE_TAC[onorm] THEN
SUBGOAL_THEN `{norm(x:real^N) | norm x = &1} = {&1}`
(fun th -> REWRITE_TAC[th;
SUP_SING]) THEN
SUBGOAL_THEN `norm(basis 1:real^N) = &1` MP_TAC THENL
[SIMP_TAC[
NORM_BASIS;
DIMINDEX_GE_1;
LE_REFL]; SET_TAC[]]);;
(* ------------------------------------------------------------------------- *)
(* It's handy to "lift" from R to R^1 and "drop" from R^1 to R. *)
(* ------------------------------------------------------------------------- *)
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]);;
let DROP_WLOG_LE = prove
(`(!x y. P x y <=> P y x) /\ (!x y. drop x <= drop y ==> P x y)
==> (!x y. P x y)`,
(* ------------------------------------------------------------------------- *)
(* Pasting vectors. *)
(* ------------------------------------------------------------------------- *)
let FSTCART_ADD = prove
(`!x:real^(M,N)finite_sum y. fstcart(x + y) = fstcart(x) + fstcart(y)`,
let FSTCART_NEG = prove
(`!x:real^(M,N)finite_sum. --(fstcart x) = fstcart(--x)`,
ONCE_REWRITE_TAC[VECTOR_ARITH `--x = --(&1) % x`] THEN
REWRITE_TAC[
FSTCART_CMUL]);;
let FSTCART_SUB = prove
(`!x:real^(M,N)finite_sum y. fstcart(x - y) = fstcart(x) - fstcart(y)`,
let SNDCART_ADD = prove
(`!x:real^(M,N)finite_sum y. sndcart(x + y) = sndcart(x) + sndcart(y)`,
let SNDCART_NEG = prove
(`!x:real^(M,N)finite_sum. --(sndcart x) = sndcart(--x)`,
ONCE_REWRITE_TAC[VECTOR_ARITH `--x = --(&1) % x`] THEN
REWRITE_TAC[
SNDCART_CMUL]);;
let SNDCART_SUB = prove
(`!x:real^(M,N)finite_sum y. sndcart(x - y) = sndcart(x) - sndcart(y)`,
let PASTECART_ADD = prove
(`!x1 y1 x2:real^M y2:real^N.
pastecart x1 y1 + pastecart x2 y2 = pastecart (x1 + x2) (y1 + y2)`,
let PASTECART_NEG = prove
(`!x:real^M y:real^N. pastecart (--x) (--y) = --(pastecart x y)`,
ONCE_REWRITE_TAC[VECTOR_ARITH `--x = --(&1) % x`] THEN
REWRITE_TAC[
PASTECART_CMUL]);;
let PASTECART_SUB = prove
(`!x1 y1 x2:real^M y2:real^N.
pastecart x1 y1 - pastecart x2 y2 = pastecart (x1 - x2) (y1 - y2)`,
let DOT_PASTECART = prove
(`!x1 x2 y1 y2. (pastecart x1 x2) dot (pastecart y1 y2) =
x1 dot y1 + x2 dot y2`,
let DIST_PASTECART_CANCEL = prove
(`(!x x' y. dist(pastecart x y,pastecart x' y) = dist(x,x')) /\
(!x y y'. dist(pastecart x y,pastecart x y') = dist(y,y'))`,
let LINEAR_PASTECART = prove
(`!f:real^M->real^N g:real^M->real^P.
linear f /\ linear g ==> linear (\x. pastecart (f x) (g x))`,
(* ------------------------------------------------------------------------- *)
(* A bit of linear algebra. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Closure properties of subspaces. *)
(* ------------------------------------------------------------------------- *)
let SUBSPACE_UNION_CHAIN = prove
(`!s t:real^N->bool.
subspace s /\ subspace t /\ subspace(s
UNION t)
==> s
SUBSET t \/ t
SUBSET s`,
REPEAT STRIP_TAC THEN REWRITE_TAC[SET_RULE
`s
SUBSET t \/ t
SUBSET s <=>
~(?x y. x
IN s /\ ~(x
IN t) /\ y
IN t /\ ~(y
IN s))`] THEN
STRIP_TAC THEN SUBGOAL_THEN `(x + y:real^N)
IN s
UNION t` MP_TAC THENL
[MATCH_MP_TAC
SUBSPACE_ADD THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
REWRITE_TAC[
IN_UNION; DE_MORGAN_THM] THEN
ASM_MESON_TAC[
SUBSPACE_SUB; VECTOR_ARITH
`(x + y) - x:real^N = y /\ (x + y) - y = x`]]);;
(* ------------------------------------------------------------------------- *)
(* Lemmas. *)
(* ------------------------------------------------------------------------- *)
let SPAN_CLAUSES = prove
(`(!a s. a
IN s ==> a
IN span s) /\
(vec(0)
IN span s) /\
(!x y s. x
IN span s /\ y
IN span s ==> (x + y)
IN span s) /\
(!x c s. x
IN span s ==> (c % x)
IN span s)`,
(* ------------------------------------------------------------------------- *)
(* Individual closure properties. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Mapping under linear image. *)
(* ------------------------------------------------------------------------- *)
let DEPENDENT_LINEAR_IMAGE_EQ = prove
(`!f:real^M->real^N s.
linear f /\ (!x y. f x = f y ==> x = y)
==> (dependent(
IMAGE f s) <=> dependent s)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[dependent;
EXISTS_IN_IMAGE] THEN
AP_TERM_TAC THEN REWRITE_TAC[
FUN_EQ_THM] THEN X_GEN_TAC `a:real^M` THEN
ASM_CASES_TAC `(a:real^M)
IN s` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
EQ_TRANS THEN
EXISTS_TAC `(f:real^M->real^N) a
IN span(
IMAGE f (s
DELETE a))` THEN
CONJ_TAC THENL
[AP_TERM_TAC THEN AP_TERM_TAC THEN ASM SET_TAC[];
ASM_SIMP_TAC[
SPAN_LINEAR_IMAGE] THEN ASM SET_TAC[]]);;
(* ------------------------------------------------------------------------- *)
(* The key breakdown property. *)
(* ------------------------------------------------------------------------- *)
let SPAN_BREAKDOWN = prove
(`!b s a:real^N.
b
IN s /\ a
IN span s ==> ?k. (a - k % b)
IN span(s
DELETE b)`,
REWRITE_TAC[
IMP_CONJ;
RIGHT_FORALL_IMP_THM] THEN
REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC
SPAN_INDUCT THEN
REWRITE_TAC[subspace;
IN_ELIM_THM] THEN CONJ_TAC THENL
[GEN_TAC THEN DISCH_TAC THEN ASM_CASES_TAC `a:real^N = b`; ALL_TAC] THEN
ASM_MESON_TAC[
SPAN_CLAUSES;
IN_DELETE; VECTOR_ARITH
`(a - &1 % a = vec 0) /\ (a - &0 % b = a) /\
((x + y) - (k1 + k2) % b = (x - k1 % b) + (y - k2 % b)) /\
(c % x - (c * k) % y = c % (x - k % y))`]);;
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_2 = prove
(`!a b:real^N.
dependent {a,b} <=>
if a = b then a = vec 0
else ?x y. x % a + y % b = vec 0 /\ ~(x = &0 /\ y = &0)`,
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))`,
let INDEPENDENT_2 = prove
(`!a b:real^N x y.
independent{a,b} /\ ~(a = b)
==> (x % a + y % b = vec 0 <=> x = &0 /\ y = &0)`,
let INDEPENDENT_3 = prove
(`!a b c:real^N x y z.
independent{a,b,c} /\ ~(a = b) /\ ~(a = c) /\ ~(b = c)
==> (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. *)
(* ------------------------------------------------------------------------- *)
let INDEPENDENT_INJECTIVE_IMAGE_GEN = prove
(`!f:real^M->real^N s.
independent s /\ linear f /\
(!x y. x
IN span s /\ y
IN span s /\ f(x) = f(y) ==> x = y)
==> independent (
IMAGE f s)`,
REPEAT GEN_TAC THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
REWRITE_TAC[independent;
DEPENDENT_EXPLICIT] THEN
REWRITE_TAC[
CONJ_ASSOC;
FINITE_SUBSET_IMAGE] THEN
REWRITE_TAC[MESON[]
`(?s u. ((?t. p t /\ s = f t) /\ q s u) /\ r s u) <=>
(?t u. p t /\ q (f t) u /\ r (f t) u)`] THEN
REWRITE_TAC[
EXISTS_IN_IMAGE;
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`t:real^M->bool`; `u:real^N->real`] THEN
DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
MAP_EVERY EXISTS_TAC
[`t:real^M->bool`; `(u:real^N->real) o (f:real^M->real^N)`] THEN
ASM_REWRITE_TAC[
o_THM] THEN
FIRST_ASSUM MATCH_MP_TAC THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC
SPAN_VSUM THEN ASM_REWRITE_TAC[] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC
SPAN_MUL THEN
MATCH_MP_TAC
SPAN_SUPERSET THEN ASM SET_TAC[];
REWRITE_TAC[
SPAN_0];
ASM_SIMP_TAC[
LINEAR_VSUM] THEN
FIRST_ASSUM(SUBST1_TAC o MATCH_MP
LINEAR_0) THEN
FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN CONV_TAC SYM_CONV THEN
W(MP_TAC o PART_MATCH (lhs o rand)
VSUM_IMAGE o lhand o snd) THEN
ASM_SIMP_TAC[
o_DEF;
LINEAR_CMUL] THEN DISCH_THEN MATCH_MP_TAC THEN
ASM_MESON_TAC[
SPAN_SUPERSET;
SUBSET]]);;
(* ------------------------------------------------------------------------- *)
(* 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. *)
(* ------------------------------------------------------------------------- *)
let LINEAR_EQ_0_SPAN = prove
(`!f:real^M->real^N b.
linear f /\ (!x. x
IN b ==> f(x) = vec 0)
==> !x. x
IN span(b) ==> f(x) = vec 0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN
RULE_ASSUM_TAC(REWRITE_RULE[
IN]) THEN
MATCH_MP_TAC
SPAN_INDUCT THEN ASM_REWRITE_TAC[
IN] THEN
MP_TAC(ISPEC `f:real^M->real^N`
SUBSPACE_KERNEL) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN
AP_TERM_TAC THEN REWRITE_TAC[
EXTENSION;
IN_ELIM_THM]);;
let LINEAR_EQ = prove
(`!f g b s. linear f /\ linear g /\ s
SUBSET (span b) /\
(!x. x
IN b ==> f(x) = g(x))
==> !x. x
IN s ==> f(x) = g(x)`,
let LINEAR_EQ_STDBASIS = prove
(`!f:real^M->real^N g.
linear f /\ linear g /\
(!i. 1 <= i /\ i <= dimindex(:M)
==> f(basis i) = g(basis i))
==> f = g`,
(* ------------------------------------------------------------------------- *)
(* Similar results for bilinear functions. *)
(* ------------------------------------------------------------------------- *)
let BILINEAR_EQ = prove
(`!f:real^M->real^N->real^P g b c s.
bilinear f /\ bilinear g /\
s
SUBSET (span b) /\ t
SUBSET (span c) /\
(!x y. x
IN b /\ y
IN c ==> f x y = g x y)
==> !x y. x
IN s /\ y
IN t ==> f x y = g x y`,
let BILINEAR_EQ_STDBASIS = prove
(`!f:real^M->real^N->real^P g.
bilinear f /\ bilinear g /\
(!i j. 1 <= i /\ i <= dimindex(:M) /\ 1 <= j /\ j <= dimindex(:N)
==> f (basis i) (basis j) = g (basis i) (basis j))
==> f = g`,
REPEAT STRIP_TAC THEN SUBGOAL_THEN
`!x y. x
IN UNIV /\ y
IN UNIV ==> (f:real^M->real^N->real^P) x y = g x y`
(fun th -> MP_TAC th THEN REWRITE_TAC[
FUN_EQ_THM;
IN_UNIV]) THEN
MATCH_MP_TAC
BILINEAR_EQ THEN
EXISTS_TAC `{basis i :real^M | 1 <= i /\ i <= dimindex(:M)}` THEN
EXISTS_TAC `{basis i :real^N | 1 <= i /\ i <= dimindex(:N)}` THEN
ASM_REWRITE_TAC[
SPAN_STDBASIS;
SUBSET_REFL;
IN_ELIM_THM] THEN
ASM_MESON_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* 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. *)
(* ------------------------------------------------------------------------- *)
let LINEAR_INVERSE_LEFT = prove
(`!f:real^N->real^N f'.
linear f /\ linear f' ==> ((f o f' = I) <=> (f' o f = I))`,
SUBGOAL_THEN
`!f:real^N->real^N f'.
linear f /\ linear f' /\ (f o f' = I) ==> (f' o f = I)`
(fun th -> MESON_TAC[th]) THEN
REWRITE_TAC[
FUN_EQ_THM;
o_THM;
I_THM] THEN REPEAT STRIP_TAC THEN
MP_TAC(ISPEC `f:real^N->real^N`
LINEAR_SURJECTIVE_ISOMORPHISM) THEN
ASM_MESON_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Moreover, a one-sided inverse is automatically linear. *)
(* ------------------------------------------------------------------------- *)
let LEFT_INVERSE_LINEAR = prove
(`!f g:real^N->real^N. linear f /\ (g o f = I) ==> linear g`,
REPEAT GEN_TAC THEN REWRITE_TAC[
FUN_EQ_THM;
o_THM;
I_THM] THEN
STRIP_TAC THEN SUBGOAL_THEN
`?h:real^N->real^N. linear h /\ (!x. h(f x) = x) /\ (!x. f(h x) = x)`
CHOOSE_TAC THENL
[MATCH_MP_TAC
LINEAR_INJECTIVE_ISOMORPHISM THEN ASM_MESON_TAC[];
SUBGOAL_THEN `g:real^N->real^N = h` (fun th -> ASM_REWRITE_TAC[th]) THEN
REWRITE_TAC[
FUN_EQ_THM] THEN ASM_MESON_TAC[]]);;
let RIGHT_INVERSE_LINEAR = prove
(`!f g:real^N->real^N. linear f /\ (f o g = I) ==> linear g`,
REPEAT GEN_TAC THEN REWRITE_TAC[
FUN_EQ_THM;
o_THM;
I_THM] THEN
STRIP_TAC THEN SUBGOAL_THEN
`?h:real^N->real^N. linear h /\ (!x. h(f x) = x) /\ (!x. f(h x) = x)`
CHOOSE_TAC THENL [ASM_MESON_TAC[
LINEAR_SURJECTIVE_ISOMORPHISM]; ALL_TAC] THEN
SUBGOAL_THEN `g:real^N->real^N = h` (fun th -> ASM_REWRITE_TAC[th]) THEN
REWRITE_TAC[
FUN_EQ_THM] THEN ASM_MESON_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Without (ostensible) constraints on types, though dimensions must match. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* The same result in terms of square matrices. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Invertibility of matrices and corresponding linear functions. *)
(* ------------------------------------------------------------------------- *)
let MATRIX_INVERTIBLE = prove
(`!f:real^N->real^N.
linear f
==> (invertible(matrix f) <=>
?g. linear g /\ f o g = I /\ g o f = I)`,
(* ------------------------------------------------------------------------- *)
(* Left-invertible linear transformation has a lower bound. *)
(* ------------------------------------------------------------------------- *)
let LINEAR_INVERTIBLE_BOUNDED_BELOW_POS = prove
(`!f:real^M->real^N g.
linear f /\ linear g /\ (g o f = I)
==> ?B. &0 < B /\ !x. B * norm(x) <= norm(f x)`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPEC `g:real^N->real^M`
LINEAR_BOUNDED_POS) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `inv B:real` THEN ASM_REWRITE_TAC[
REAL_LT_INV_EQ] THEN
X_GEN_TAC `x:real^M` THEN MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `inv(B) * norm(((g:real^N->real^M) o (f:real^M->real^N)) x)` THEN
CONJ_TAC THENL [ASM_SIMP_TAC[
I_THM;
REAL_LE_REFL]; ALL_TAC] THEN
REWRITE_TAC[REAL_ARITH `inv B * x = x / B`] THEN
ASM_SIMP_TAC[
o_THM;
REAL_LE_LDIV_EQ] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_REWRITE_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Preservation of dimension by injective map. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Considering an n-element vector as an n-by-1 or 1-by-n matrix. *)
(* ------------------------------------------------------------------------- *)
let DOT_MATRIX_VECTOR_MUL = prove
(`!A:real^N^N B:real^N^N x:real^N y:real^N.
(A ** x) dot (B ** y) =
((rowvector x) ** (transp(A) ** B) ** (columnvector y))$1$1`,
(* ------------------------------------------------------------------------- *)
(* 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. *)
(* ------------------------------------------------------------------------- *)
let ADJOINT_INJECTIVE = prove
(`!f:real^M->real^N.
linear f
==> ((!x y. adjoint f x = adjoint f y ==> x = y) <=>
(!y. ?x. f x = y))`,
(* ------------------------------------------------------------------------- *)
(* Orthogonal bases, Gram-Schmidt process, and related theorems. *)
(* ------------------------------------------------------------------------- *)
let GRAM_SCHMIDT_STEP = prove
(`!s a x.
pairwise orthogonal s /\ x
IN span s
==> orthogonal x (a - vsum s (\b:real^N. (b dot a) / (b dot b) % b))`,
let ORTHOGONAL_EXTENSION_STRONG = prove
(`!s t:real^N->bool.
pairwise orthogonal s
==> ?u.
DISJOINT u (vec 0
INSERT s) /\
pairwise orthogonal (s
UNION u) /\
span (s
UNION u) = span (s
UNION t)`,
REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o
SPEC `t:real^N->bool` o MATCH_MP
ORTHOGONAL_EXTENSION) THEN
DISCH_THEN(X_CHOOSE_THEN `u:real^N->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `u
DIFF ((vec 0:real^N)
INSERT s)` THEN REPEAT CONJ_TAC THENL
[SET_TAC[];
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
PAIRWISE_MONO)) THEN SET_TAC[];
FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
GEN_REWRITE_TAC BINOP_CONV [GSYM
SPAN_DELETE_0] THEN
AP_TERM_TAC THEN SET_TAC[]]);;
let VECTOR_IN_ORTHOGONAL_BASIS = prove
(`!a. ~(a = vec 0)
==> ?s. a
IN s /\ ~(vec 0
IN s) /\
pairwise orthogonal s /\
independent s /\
s
HAS_SIZE (dimindex(:N)) /\
span s = (:real^N)`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPEC `a:real^N`
VECTOR_IN_ORTHOGONAL_SPANNINGSET) THEN
DISCH_THEN(X_CHOOSE_THEN `s:real^N->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `s
DELETE (vec 0:real^N)` THEN ASM_REWRITE_TAC[
IN_DELETE] THEN
MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
[RULE_ASSUM_TAC(REWRITE_RULE[pairwise]) THEN
ASM_SIMP_TAC[pairwise;
IN_DELETE];
DISCH_TAC] THEN
MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
[MATCH_MP_TAC
PAIRWISE_ORTHOGONAL_INDEPENDENT THEN ASM_SIMP_TAC[
IN_DELETE];
DISCH_TAC] THEN
MATCH_MP_TAC(TAUT `b /\ (b ==> a) ==> a /\ b`) THEN CONJ_TAC THENL
[ASM_MESON_TAC[
SPAN_DELETE_0];
DISCH_TAC THEN ASM_SIMP_TAC[
BASIS_HAS_SIZE_UNIV]]);;
let BESSEL_INEQUALITY = prove
(`!s x:real^N.
pairwise orthogonal s /\ (!x. x
IN s ==> norm x = &1)
==> sum s (\e. (e dot x) pow 2) <= norm(x) pow 2`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
PAIRWISE_ORTHOGONAL_IMP_FINITE) THEN
MP_TAC(ISPEC `x - vsum s (\e. (e dot x) % e):real^N`
DOT_POS_LE) THEN
REWRITE_TAC[
NORM_POW_2; VECTOR_ARITH
`(a - b:real^N) dot (a - b) = a dot a + b dot b - &2 * b dot a`] THEN
ASM_SIMP_TAC[
DOT_LSUM; REAL_POW_2;
DOT_LMUL] THEN
MATCH_MP_TAC(REAL_ARITH `t = s ==> &0 <= x + t - &2 * s ==> s <= x`) THEN
MATCH_MP_TAC
SUM_EQ THEN X_GEN_TAC `e:real^N` THEN DISCH_TAC THEN
ASM_SIMP_TAC[
DOT_RSUM] THEN AP_TERM_TAC THEN
MATCH_MP_TAC
EQ_TRANS THEN
EXISTS_TAC `sum s (\k:real^N. if k = e then e dot x else &0)` THEN
CONJ_TAC THENL [ALL_TAC; ASM_SIMP_TAC[
SUM_DELTA]] THEN
MATCH_MP_TAC
SUM_EQ THEN X_GEN_TAC `k:real^N` THEN DISCH_TAC THEN
REWRITE_TAC[
DOT_RMUL] THEN COND_CASES_TAC THENL
[ASM_REWRITE_TAC[REAL_RING `a * x = a <=> a = &0 \/ x = &1`] THEN
DISJ2_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `e:real^N`) THEN
ASM_REWRITE_TAC[
NORM_EQ_SQUARE] THEN REAL_ARITH_TAC;
RULE_ASSUM_TAC(REWRITE_RULE[pairwise; orthogonal]) THEN
ASM_SIMP_TAC[
REAL_ENTIRE]]);;
(* ------------------------------------------------------------------------- *)
(* Analogous theorems for existence of orthonormal basis for a subspace. *)
(* ------------------------------------------------------------------------- *)
let ORTHOGONAL_SPANNINGSET_SUBSPACE = prove
(`!s:real^N->bool.
subspace s
==> ?b. b
SUBSET s /\ pairwise orthogonal b /\ span b = s`,
REPEAT STRIP_TAC THEN MP_TAC(ISPEC `s:real^N->bool`
BASIS_EXISTS) THEN
DISCH_THEN(X_CHOOSE_THEN `b:real^N->bool` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPECL[`{}:real^N->bool`; `b:real^N->bool`]
ORTHOGONAL_EXTENSION) THEN
REWRITE_TAC[
PAIRWISE_EMPTY;
UNION_EMPTY] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `c:real^N->bool` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(TAUT `b /\ (b ==> a) ==> a /\ b`) THEN CONJ_TAC THENL
[MATCH_MP_TAC
SPAN_SUBSPACE THEN ASM_REWRITE_TAC[];
DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_MESON_TAC[
SPAN_INC]]);;
let ORTHOGONAL_BASIS_SUBSPACE = prove
(`!s:real^N->bool.
subspace s
==> ?b. ~(vec 0
IN b) /\
b
SUBSET s /\
pairwise orthogonal b /\
independent b /\
b
HAS_SIZE (dim s) /\
span b = s`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o MATCH_MP
ORTHOGONAL_SPANNINGSET_SUBSPACE) THEN
DISCH_THEN(X_CHOOSE_THEN `b:real^N->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `b
DELETE (vec 0:real^N)` THEN ASM_REWRITE_TAC[
IN_DELETE] THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
[RULE_ASSUM_TAC(REWRITE_RULE[pairwise]) THEN
ASM_SIMP_TAC[pairwise;
IN_DELETE];
DISCH_TAC] THEN
MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
[MATCH_MP_TAC
PAIRWISE_ORTHOGONAL_INDEPENDENT THEN ASM_SIMP_TAC[
IN_DELETE];
DISCH_TAC] THEN
MATCH_MP_TAC(TAUT `b /\ (b ==> a) ==> a /\ b`) THEN CONJ_TAC THENL
[ASM_MESON_TAC[
SPAN_DELETE_0];
DISCH_TAC THEN ASM_SIMP_TAC[
BASIS_HAS_SIZE_DIM]]);;
let ORTHOGONAL_TO_SUBSPACE_EXISTS_GEN = prove
(`!s t:real^N->bool.
span s
PSUBSET span t
==> ?x. ~(x = vec 0) /\ x
IN span t /\
(!y. y
IN span s ==> orthogonal x y)`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPEC `span s:real^N->bool`
ORTHOGONAL_BASIS_SUBSPACE) THEN
REWRITE_TAC[
SUBSPACE_SPAN] THEN
DISCH_THEN(X_CHOOSE_THEN `b:real^N->bool` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
PSUBSET_ALT]) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
(X_CHOOSE_THEN `u:real^N` STRIP_ASSUME_TAC)) THEN
MP_TAC(ISPECL [`b:real^N->bool`; `{u:real^N}`]
ORTHOGONAL_EXTENSION) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `ns:real^N->bool` MP_TAC) THEN
ASM_CASES_TAC `ns
SUBSET (vec 0:real^N)
INSERT b` THENL
[DISCH_THEN(MP_TAC o AP_TERM `(
IN) (u:real^N)` o CONJUNCT2) THEN
SIMP_TAC[
SPAN_SUPERSET;
IN_UNION;
IN_SING] THEN
MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
SUBGOAL_THEN `~(u
IN span (b
UNION {vec 0:real^N}))` MP_TAC THENL
[ASM_REWRITE_TAC[SET_RULE `s
UNION {a} = a
INSERT s`;
SPAN_INSERT_0];
MATCH_MP_TAC(SET_RULE `s
SUBSET t ==> ~(x
IN t) ==> ~(x
IN s)`) THEN
MATCH_MP_TAC
SPAN_MONO THEN ASM SET_TAC[]];
ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o MATCH_MP (SET_RULE
`~(s
SUBSET t) ==> ?z. z
IN s /\ ~(z
IN t)`)) THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM;
IN_INSERT; DE_MORGAN_THM] THEN
X_GEN_TAC `n:real^N` THEN STRIP_TAC THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
REWRITE_TAC[pairwise;
IMP_CONJ;
RIGHT_FORALL_IMP_THM] THEN
DISCH_THEN(MP_TAC o SPEC `n:real^N`) THEN ASM_REWRITE_TAC[
IN_UNION] THEN
REWRITE_TAC[IMP_IMP] THEN DISCH_TAC THEN EXISTS_TAC `n:real^N` THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[SUBGOAL_THEN `(n:real^N)
IN span (b
UNION ns)` MP_TAC THENL
[MATCH_MP_TAC
SPAN_SUPERSET THEN ASM SET_TAC[];
ASM_REWRITE_TAC[] THEN SPEC_TAC(`n:real^N`,`n:real^N`) THEN
REWRITE_TAC[GSYM
SUBSET] THEN
MATCH_MP_TAC
SPAN_SUBSET_SUBSPACE THEN REWRITE_TAC[
SUBSPACE_SPAN] THEN
ASM_REWRITE_TAC[SET_RULE
`s
UNION {a}
SUBSET t <=> s
SUBSET t /\ a
IN t`] THEN
ASM_MESON_TAC[
SPAN_INC;
SUBSET_TRANS]];
MATCH_MP_TAC
SPAN_INDUCT THEN
REWRITE_TAC[SET_RULE `(\y. orthogonal n y) = {y | orthogonal n y}`] THEN
REWRITE_TAC[
SUBSPACE_ORTHOGONAL_TO_VECTOR] THEN ASM SET_TAC[]]);;
(* ------------------------------------------------------------------------- *)
(* Decomposing a vector into parts in orthogonal subspaces. *)
(* ------------------------------------------------------------------------- *)
let ORTHOGONAL_SUBSPACE_DECOMP_UNIQUE = prove
(`!s t x y x' y':real^N.
(!a b. a
IN s /\ b
IN t ==> orthogonal a b) /\
x
IN span s /\ x'
IN span s /\ y
IN span t /\ y'
IN span t /\
x + y = x' + y'
==> x = x' /\ y = y'`,
REWRITE_TAC[VECTOR_ARITH `x + y:real^N = x' + y' <=> x - x' = y' - y`] THEN
ONCE_REWRITE_TAC[GSYM
ORTHOGONAL_TO_SPANS_EQ] THEN
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[VECTOR_ARITH
`x:real^N = x' /\ y:real^N = y' <=> x - x' = vec 0 /\ y' - y = vec 0`] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[GSYM
ORTHOGONAL_REFL] THEN
FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
ASM_MESON_TAC[
ORTHOGONAL_CLAUSES;
ORTHOGONAL_SYM]);;
(* ------------------------------------------------------------------------- *)
(* Existence of isometry between subspaces of same dimension. *)
(* ------------------------------------------------------------------------- *)
let ISOMETRIES_SUBSPACES = prove
(`!s:real^M->bool t:real^N->bool.
subspace s /\ subspace t /\ dim s = dim t
==> ?f g. linear f /\ linear g /\
IMAGE f s = t /\
IMAGE g t = s /\
(!x. x
IN s ==> norm(f x) = norm x) /\
(!y. y
IN t ==> norm(g y) = norm y) /\
(!x. x
IN s ==> g(f x) = x) /\
(!y. y
IN t ==> f(g y) = y)`,
REPEAT STRIP_TAC THEN ABBREV_TAC `n = dim(t:real^N->bool)` THEN
MP_TAC(ISPEC `t:real^N->bool`
ORTHONORMAL_BASIS_SUBSPACE) THEN
MP_TAC(ISPEC `s:real^M->bool`
ORTHONORMAL_BASIS_SUBSPACE) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `b:real^M->bool` STRIP_ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `c:real^N->bool` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPECL [`b:real^M->bool`; `c:real^N->bool`]
CARD_EQ_BIJECTIONS) THEN
RULE_ASSUM_TAC(REWRITE_RULE[
HAS_SIZE]) THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`fb:real^M->real^N`; `gb:real^N->real^M`] THEN
STRIP_TAC THEN
MP_TAC(ISPECL [`gb:real^N->real^M`; `c:real^N->bool`]
LINEAR_INDEPENDENT_EXTEND) THEN
MP_TAC(ISPECL [`fb:real^M->real^N`; `b:real^M->bool`]
LINEAR_INDEPENDENT_EXTEND) THEN
ASM_REWRITE_TAC[IMP_IMP;
LEFT_AND_EXISTS_THM] THEN
REWRITE_TAC[
RIGHT_AND_EXISTS_THM] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `f:real^M->real^N` THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `g:real^N->real^M` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
[REWRITE_TAC[SYM(ASSUME `span b:real^M->bool = s`)] THEN
ASM_SIMP_TAC[GSYM
SPAN_LINEAR_IMAGE] THEN
REWRITE_TAC[SYM(ASSUME `span c:real^N->bool = t`)] THEN
AP_TERM_TAC THEN ASM SET_TAC[];
REWRITE_TAC[SYM(ASSUME `span c:real^N->bool = t`)] THEN
ASM_SIMP_TAC[GSYM
SPAN_LINEAR_IMAGE] THEN
REWRITE_TAC[SYM(ASSUME `span b:real^M->bool = s`)] THEN
AP_TERM_TAC THEN ASM SET_TAC[];
UNDISCH_THEN `span b:real^M->bool = s` (SUBST1_TAC o SYM) THEN
ASM_SIMP_TAC[
SPAN_FINITE] THEN
REWRITE_TAC[
IN_ELIM_THM;
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`z:real^M`; `u:real^M->real`] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_SIMP_TAC[
LINEAR_VSUM] THEN
REWRITE_TAC[
o_DEF;
NORM_EQ_SQUARE;
NORM_POS_LE; GSYM
NORM_POW_2] THEN
ASM_SIMP_TAC[
LINEAR_CMUL] THEN
W(MP_TAC o PART_MATCH (lhand o rand)
NORM_VSUM_PYTHAGOREAN o rand o snd) THEN
W(MP_TAC o PART_MATCH (lhand o rand)
NORM_VSUM_PYTHAGOREAN o lhand o rand o snd) THEN
RULE_ASSUM_TAC(REWRITE_RULE[pairwise]) THEN
ASM_SIMP_TAC[pairwise;
ORTHOGONAL_CLAUSES] THEN ANTS_TAC THENL
[REPEAT STRIP_TAC THEN REWRITE_TAC[
ORTHOGONAL_MUL] THEN ASM SET_TAC[];
REPEAT(DISCH_THEN SUBST1_TAC) THEN
ASM_SIMP_TAC[
NORM_MUL]];
UNDISCH_THEN `span c:real^N->bool = t` (SUBST1_TAC o SYM) THEN
ASM_SIMP_TAC[
SPAN_FINITE] THEN
REWRITE_TAC[
IN_ELIM_THM;
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`z:real^N`; `u:real^N->real`] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_SIMP_TAC[
LINEAR_VSUM] THEN
REWRITE_TAC[
o_DEF;
NORM_EQ_SQUARE;
NORM_POS_LE; GSYM
NORM_POW_2] THEN
ASM_SIMP_TAC[
LINEAR_CMUL] THEN
W(MP_TAC o PART_MATCH (lhand o rand)
NORM_VSUM_PYTHAGOREAN o rand o snd) THEN
W(MP_TAC o PART_MATCH (lhand o rand)
NORM_VSUM_PYTHAGOREAN o lhand o rand o snd) THEN
RULE_ASSUM_TAC(REWRITE_RULE[pairwise]) THEN
ASM_SIMP_TAC[pairwise;
ORTHOGONAL_CLAUSES] THEN ANTS_TAC THENL
[REPEAT STRIP_TAC THEN REWRITE_TAC[
ORTHOGONAL_MUL] THEN ASM SET_TAC[];
REPEAT(DISCH_THEN SUBST1_TAC) THEN
ASM_SIMP_TAC[
NORM_MUL]];
REWRITE_TAC[SYM(ASSUME `span b:real^M->bool = s`)] THEN
MATCH_MP_TAC
SPAN_INDUCT THEN
CONJ_TAC THENL [ASM_MESON_TAC[
SUBSET;
IN]; ALL_TAC] THEN
REWRITE_TAC[subspace;
IN] THEN ASM_MESON_TAC[linear;
LINEAR_0];
REWRITE_TAC[SYM(ASSUME `span c:real^N->bool = t`)] THEN
MATCH_MP_TAC
SPAN_INDUCT THEN
CONJ_TAC THENL [ASM_MESON_TAC[
SUBSET;
IN]; ALL_TAC] THEN
REWRITE_TAC[subspace;
IN] THEN ASM_MESON_TAC[linear;
LINEAR_0]]);;
let ISOMETRY_SUBSPACES = prove
(`!s:real^M->bool t:real^N->bool.
subspace s /\ subspace t /\ dim s = dim t
==> ?f:real^M->real^N. linear f /\
IMAGE f s = t /\
(!x. x
IN s ==> norm(f x) = norm(x))`,
let SUBSPACE_ISOMORPHISM = prove
(`!s t. subspace s /\ subspace t /\ dim(s) = dim(t)
==> ?f:real^M->real^N.
linear f /\ (
IMAGE f s = t) /\
(!x y. x
IN s /\ y
IN s /\ f x = f y ==> (x = y))`,
let ISOMORPHISMS_UNIV_UNIV = prove
(`dimindex(:M) = dimindex(:N)
==> ?f:real^M->real^N g.
linear f /\ linear g /\
(!x. norm(f x) = norm x) /\ (!y. norm(g y) = norm y) /\
(!x. g(f x) = x) /\ (!y. f(g y) = y)`,
(* ------------------------------------------------------------------------- *)
(* Properties of special hyperplanes. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* More theorems about dimensions of different subspaces. *)
(* ------------------------------------------------------------------------- *)
let DIM_KERNEL_COMPOSE = prove
(`!f:real^M->real^N g:real^N->real^P.
linear f /\ linear g
==> dim {x | (g o f) x = vec 0} <=
dim {x | f(x) = vec 0} +
dim {y | g(y) = vec 0}`,
(* ------------------------------------------------------------------------- *)
(* More about product spaces. *)
(* ------------------------------------------------------------------------- *)
let SPAN_SUMS = prove
(`!s t:real^N->bool.
~(s = {}) /\ ~(t = {}) /\ vec 0
IN (s
UNION t)
==> span {x + y | x
IN s /\ y
IN t} =
{x + y | x
IN span s /\ y
IN span t}`,
(* ------------------------------------------------------------------------- *)
(* More about rank from the rank/nullspace formula. *)
(* ------------------------------------------------------------------------- *)
let RANK_SYLVESTER = prove
(`!A:real^N^M B:real^P^N.
rank(A) + rank(B) <= rank(A ** B) + dimindex(:N)`,
REPEAT GEN_TAC THEN MATCH_MP_TAC(ARITH_RULE
`!ia ib iab p:num.
ra + ia = n /\
rb + ib = p /\
rab + iab = p /\
iab <= ia + ib
==> ra + rb <= rab + n`) THEN
MAP_EVERY EXISTS_TAC
[`dim {x | (A:real^N^M) ** x = vec 0}`;
`dim {x | (B:real^P^N) ** x = vec 0}`;
`dim {x | ((A:real^N^M) ** (B:real^P^N)) ** x = vec 0}`;
`dimindex(:P)`] THEN
REWRITE_TAC[
RANK_NULLSPACE] THEN
REWRITE_TAC[GSYM
MATRIX_VECTOR_MUL_ASSOC] THEN
ONCE_REWRITE_TAC[
ADD_SYM] THEN
MATCH_MP_TAC(REWRITE_RULE[
o_DEF]
DIM_KERNEL_COMPOSE) THEN
CONJ_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM ETA_AX] THEN
REWRITE_TAC[
MATRIX_VECTOR_MUL_LINEAR]);;
(* ------------------------------------------------------------------------- *)
(* Infinity norm. *)
(* ------------------------------------------------------------------------- *)
let INFNORM_SET_IMAGE = prove
(`{abs(x$i) | 1 <= i /\ i <= dimindex(:N)} =
IMAGE (\i. abs(x$i)) (1..dimindex(:N))`,
REWRITE_TAC[numseg] THEN SET_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Prove that it differs only up to a bound from Euclidean norm. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Equality in Cauchy-Schwarz and triangle inequalities. *)
(* ------------------------------------------------------------------------- *)
let NORM_TRIANGLE_EQ = prove
(`!x y:real^N. norm(x + y) = norm(x) + norm(y) <=> norm(x) % y = norm(y) % x`,
REPEAT GEN_TAC THEN REWRITE_TAC[GSYM
NORM_CAUCHY_SCHWARZ_EQ] THEN
MATCH_MP_TAC
EQ_TRANS THEN
EXISTS_TAC `norm(x + y:real^N) pow 2 = (norm(x) + norm(y)) pow 2` THEN
CONJ_TAC THENL
[REWRITE_TAC[REAL_RING `x pow 2 = y pow 2 <=> x = y \/ x + y = &0`] THEN
MAP_EVERY (MP_TAC o C ISPEC
NORM_POS_LE)
[`x + y:real^N`; `x:real^N`; `y:real^N`] THEN
REAL_ARITH_TAC;
REWRITE_TAC[
NORM_POW_2;
DOT_LADD;
DOT_RADD; REAL_ARITH
`(x + y) pow 2 = x pow 2 + y pow 2 + &2 * x * y`] THEN
REWRITE_TAC[
DOT_SYM] THEN REAL_ARITH_TAC]);;
let DIST_TRIANGLE_EQ = prove
(`!x y z. dist(x,z) = dist(x,y) + dist(y,z) <=>
norm (x - y) % (y - z) = norm (y - z) % (x - y)`,
(* ------------------------------------------------------------------------- *)
(* 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_4_3 = prove
(`!a b c d:real^N.
~(a = b)
==> (collinear {a,b,c,d} <=> collinear{a,b,c} /\ collinear{a,b,d})`,
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]);;
let COLLINEAR_3_2D = prove
(`!x y z:real^2. collinear{x,y,z} <=>
(z$1 - x$1) * (y$2 - x$2) = (y$1 - x$1) * (z$2 - x$2)`,
(* ------------------------------------------------------------------------- *)
(* Between-ness. *)
(* ------------------------------------------------------------------------- *)
let BETWEEN_REFL = prove
(`!a b. between a (a,b) /\ between b (a,b) /\ between a (a,a)`,
REWRITE_TAC[between] THEN NORM_ARITH_TAC);;
let BETWEEN_SYM = prove
(`!a b x. between x (a,b) <=> between x (b,a)`,
REWRITE_TAC[between] THEN NORM_ARITH_TAC);;
let BETWEEN_TRANS = prove
(`!a b c d. between a (b,c) /\ between d (a,c) ==> between d (b,c)`,
REWRITE_TAC[between;
DIST_SYM] THEN NORM_ARITH_TAC);;
let BETWEEN_NORM = prove
(`!a b x:real^N.
between x (a,b) <=> norm(x - a) % (b - x) = norm(b - x) % (x - a)`,
let BETWEEN_DOT = prove
(`!a b x:real^N.
between x (a,b) <=> (x - a) dot (b - x) = norm(x - a) * norm(b - x)`,
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);;
let MIDPOINT_EQ_ENDPOINT = prove
(`!a b. (midpoint(a,b) = a <=> a = b) /\
(midpoint(a,b) = b <=> a = b) /\
(a = midpoint(a,b) <=> a = b) /\
(b = midpoint(a,b) <=> a = b)`,
REWRITE_TAC[midpoint] THEN NORM_ARITH_TAC);;
let BETWEEN_MIDPOINT = prove
(`!a b. between (midpoint(a,b)) (a,b) /\ between (midpoint(a,b)) (b,a)`,
REWRITE_TAC[between; midpoint] THEN NORM_ARITH_TAC);;
let MIDPOINT_COLLINEAR = prove
(`!a b c:real^N.
~(a = c)
==> (b = midpoint(a,c) <=> collinear{a,b,c} /\ dist(a,b) = dist(b,c))`,
REPEAT STRIP_TAC THEN
MATCH_MP_TAC(TAUT `(a ==> b) /\ (b ==> (a <=> c)) ==> (a <=> b /\ c)`) THEN
SIMP_TAC[
COLLINEAR_MIDPOINT] THEN ASM_REWRITE_TAC[
COLLINEAR_3_EXPAND] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[midpoint; dist] THEN
REWRITE_TAC
[VECTOR_ARITH `a - (u % a + (&1 - u) % c) = (&1 - u) % (a - c)`;
VECTOR_ARITH `(u % a + (&1 - u) % c) - c = u % (a - c)`;
VECTOR_ARITH `u % a + (&1 - u) % c = inv (&2) % (a + c) <=>
(u - &1 / &2) % (a - c) = vec 0`] THEN
ASM_SIMP_TAC[
NORM_MUL;
REAL_EQ_MUL_RCANCEL;
NORM_EQ_0;
VECTOR_SUB_EQ;
VECTOR_MUL_EQ_0] THEN
REAL_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 [];;