(* ========================================================================= *)
(* Geometric "without loss of generality" tactics to pick convenient coords. *)
(* ========================================================================= *)
needs "Multivariate/determinants.ml";;
needs "Multivariate/convex.ml";;
(* ------------------------------------------------------------------------- *)
(* Flyspeck definition of plane, and its invariance theorems. *)
(* ------------------------------------------------------------------------- *)
add_translation_invariants [PLANE_TRANSLATION_EQ];;
let PLANE_LINEAR_IMAGE_EQ = prove
(`!f:real^M->real^N p.
linear f /\ (!x y. f x = f y ==> x = y)
==> (plane(
IMAGE f p) <=> plane p)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[plane] THEN
MATCH_MP_TAC
EQ_TRANS THEN EXISTS_TAC
`?u. u
IN IMAGE f (:real^M) /\
?v. v
IN IMAGE f (:real^M) /\
?w. w
IN IMAGE (f:real^M->real^N) (:real^M) /\
~collinear {u, v, w} /\
IMAGE f p = affine hull {u, v, w}` THEN
CONJ_TAC THENL
[REWRITE_TAC[
RIGHT_AND_EXISTS_THM;
IN_IMAGE;
IN_UNIV] THEN
REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `{u,v,w}
SUBSET IMAGE (f:real^M->real^N) p` MP_TAC THENL
[ASM_REWRITE_TAC[
HULL_SUBSET]; SET_TAC[]];
REWRITE_TAC[
EXISTS_IN_IMAGE;
IN_UNIV] THEN
REWRITE_TAC[SET_RULE `{f a,f b,f c} =
IMAGE f {a,b,c}`] THEN
ASM_SIMP_TAC[
AFFINE_HULL_LINEAR_IMAGE] THEN
REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN BINOP_TAC THENL
[ASM_MESON_TAC[
COLLINEAR_LINEAR_IMAGE_EQ]; ASM SET_TAC[]]]);;
let ROTATION_PLANE_HORIZONTAL = prove
(`!s. plane s
==> ?a f.
orthogonal_transformation f /\ det(matrix f) = &1 /\
IMAGE f (
IMAGE (\x. a + x) s) = {z:real^3 | z$3 = &0}`,
let lemma = prove
(`span {z:real^3 | z$3 = &0} = {z:real^3 | z$3 = &0}`,
REWRITE_TAC[SPAN_EQ_SELF; subspace; IN_ELIM_THM] THEN
SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VEC_COMPONENT;
DIMINDEX_3; ARITH] THEN REAL_ARITH_TAC) in
REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [plane]) THEN
REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`a:real^3`; `b:real^3`; `c:real^3`] THEN
MAP_EVERY (fun t ->
ASM_CASES_TAC t THENL [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC];
ALL_TAC])
[`a:real^3 = b`; `a:real^3 = c`; `b:real^3 = c`] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC) THEN
ASM_SIMP_TAC[AFFINE_HULL_INSERT_SPAN; IN_INSERT; NOT_IN_EMPTY] THEN
EXISTS_TAC `--a:real^3` THEN
REWRITE_TAC[SET_RULE `IMAGE (\x:real^3. --a + x) {a + x | x | x IN s} =
IMAGE (\x. --a + a + x) s`] THEN
REWRITE_TAC[VECTOR_ARITH `--a + a + x:real^3 = x`; IMAGE_ID] THEN
REWRITE_TAC[SET_RULE `{x - a:real^x | x = b \/ x = c} = {b - a,c - a}`] THEN
MP_TAC(ISPEC `span{b - a:real^3,c - a}`
ROTATION_LOWDIM_HORIZONTAL) THEN
REWRITE_TAC[DIMINDEX_3] THEN ANTS_TAC THENL
[MATCH_MP_TAC LET_TRANS THEN
EXISTS_TAC `CARD{b - a:real^3,c - a}` THEN
SIMP_TAC[DIM_SPAN; DIM_LE_CARD; FINITE_RULES] THEN
SIMP_TAC[CARD_CLAUSES; FINITE_RULES] THEN ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `f:real^3->real^3` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP ORTHOGONAL_TRANSFORMATION_LINEAR) THEN
ASM_SIMP_TAC[GSYM SPAN_LINEAR_IMAGE] THEN
GEN_REWRITE_TAC RAND_CONV [GSYM lemma] THEN
MATCH_MP_TAC DIM_EQ_SPAN THEN CONJ_TAC THENL
[ASM_MESON_TAC[IMAGE_SUBSET; SPAN_INC; SUBSET_TRANS]; ALL_TAC] THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2` THEN CONJ_TAC THENL
[MP_TAC(ISPECL [`{z:real^3 | z$3 = &0}`; `(:real^3)`] DIM_EQ_SPAN) THEN
REWRITE_TAC[SUBSET_UNIV; DIM_UNIV; DIMINDEX_3; lemma] THEN
MATCH_MP_TAC(TAUT `~r /\ (~p ==> q) ==> (q ==> r) ==> p`) THEN
REWRITE_TAC[ARITH_RULE `~(x <= 2) <=> 3 <= x`] THEN
REWRITE_TAC[EXTENSION; SPAN_UNIV; IN_ELIM_THM] THEN
DISCH_THEN(MP_TAC o SPEC `vector[&0;&0;&1]:real^3`) THEN
REWRITE_TAC[IN_UNIV; VECTOR_3] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `dim {b - a:real^3,c - a}` THEN
CONJ_TAC THENL
[ALL_TAC; ASM_MESON_TAC[LE_REFL; DIM_INJECTIVE_LINEAR_IMAGE;
ORTHOGONAL_TRANSFORMATION_INJECTIVE]] THEN
MP_TAC(ISPEC `{b - a:real^3,c - a}` INDEPENDENT_BOUND_GENERAL) THEN
SIMP_TAC[CARD_CLAUSES; FINITE_RULES; IN_SING; NOT_IN_EMPTY] THEN
ASM_REWRITE_TAC[VECTOR_ARITH `b - a:real^3 = c - a <=> b = c`; ARITH] THEN
DISCH_THEN MATCH_MP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE (RAND_CONV o RAND_CONV)
[SET_RULE `{a,b,c} = {b,a,c}`]) THEN
REWRITE_TAC[] THEN ONCE_REWRITE_TAC[COLLINEAR_3] THEN
REWRITE_TAC[independent; CONTRAPOS_THM; dependent] THEN
REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; RIGHT_OR_DISTRIB] THEN
REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM2] THEN
ASM_SIMP_TAC[SET_RULE `~(a = b) ==> {a,b} DELETE b = {a}`;
SET_RULE `~(a = b) ==> {a,b} DELETE a = {b}`;
VECTOR_ARITH `b - a:real^3 = c - a <=> b = c`] THEN
REWRITE_TAC[SPAN_BREAKDOWN_EQ; SPAN_EMPTY; IN_SING] THEN
ONCE_REWRITE_TAC[VECTOR_SUB_EQ] THEN MESON_TAC[COLLINEAR_LEMMA; INSERT_AC]);;
let FORALL_PAD2D3D_THM = prove
(`!P. (!y:real^3. y$3 = &0 ==> P y) <=> (!x. P(pad2d3d x))`,
GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
[FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[pad2d3d] THEN
SIMP_TAC[
LAMBDA_BETA; DIMINDEX_3; ARITH;
LT_REFL];
FIRST_X_ASSUM(MP_TAC o SPEC `(lambda i. (y:real^3)$i):real^2`) THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
SIMP_TAC[
CART_EQ; pad2d3d; DIMINDEX_3; ARITH;
LAMBDA_BETA; DIMINDEX_2;
ARITH_RULE `i < 3 <=> i <= 2`] THEN
REWRITE_TAC[ARITH_RULE `i <= 3 <=> i <= 2 \/ i = 3`] THEN
ASM_MESON_TAC[]]);;
let QUANTIFY_PAD2D3D_THM = prove
(`(!P. (!y:real^3. y$3 = &0 ==> P y) <=> (!x. P(pad2d3d x))) /\
(!P. (?y:real^3. y$3 = &0 /\ P y) <=> (?x. P(pad2d3d x)))`,
REWRITE_TAC[MESON[] `(?y. P y) <=> ~(!x. ~P x)`] THEN
REWRITE_TAC[GSYM
FORALL_PAD2D3D_THM] THEN MESON_TAC[]);;
let INJECTIVE_PAD2D3D = prove
(`!x y. pad2d3d x = pad2d3d y ==> x = y`,
SIMP_TAC[
CART_EQ; pad2d3d;
LAMBDA_BETA; DIMINDEX_3; DIMINDEX_2] THEN
REWRITE_TAC[ARITH_RULE `i < 3 <=> i <= 2`] THEN
MESON_TAC[ARITH_RULE `i <= 2 ==> i <= 3`]);;
let pth = prove
(`!f.
orthogonal_transformation (f:real^N->real^N)
==> (vec 0 = f(vec 0) /\ {} =
IMAGE f {}) /\
((!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)})`,
REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[
IMAGE_CLAUSES] THEN
CONJ_TAC THENL
[FIRST_X_ASSUM(MP_TAC o MATCH_MP
ORTHOGONAL_TRANSFORMATION_LINEAR) THEN
MESON_TAC[
LINEAR_0];
MATCH_MP_TAC
QUANTIFY_SURJECTION_THM THEN
ASM_MESON_TAC[
ORTHOGONAL_TRANSFORMATION_SURJECTIVE]])
and oth =
prove
(`!f:real^N->real^N.
orthogonal_transformation f /\ det(matrix f) = &1
==> linear f /\
(!x y. f x = f y ==> x = y) /\
(!y. ?x. f x = y) /\
(!x. norm(f x) = norm x) /\
(2 <= dimindex(:N) ==> det(matrix f) = &1)`,
GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
[ASM_SIMP_TAC[
ORTHOGONAL_TRANSFORMATION_LINEAR];
ASM_MESON_TAC[
ORTHOGONAL_TRANSFORMATION_INJECTIVE];
ASM_MESON_TAC[
ORTHOGONAL_TRANSFORMATION_SURJECTIVE];
ASM_MESON_TAC[
ORTHOGONAL_TRANSFORMATION]])
and sth =
prove
(`((!k. 1 < k /\ k <= dimindex(:2) ==> b$k = &0) <=> b$2 = &0) /\
((!k. 1 < k /\ k <= dimindex(:3) ==> b$k = &0) <=> b$2 = &0 /\ b$3 = &0)`,
REWRITE_TAC[DIMINDEX_2; DIMINDEX_3;
ARITH_RULE `k <= 3 <=> k = 3 \/ k <= 2`;
ARITH_RULE `k <= 2 <=> k = 2 \/ ~(1 < k)`] THEN
MESON_TAC[ARITH_RULE `1 < 2 /\ 1 < 3`]) in
let sfn = GEN_REWRITE_RULE ONCE_DEPTH_CONV [sth] in
fun tm ->
let x,bod = dest_forall tm in
let th1 = EXISTS_GENVAR_RULE
(sfn(ISPEC x
ROTATION_HORIZONTAL_LINE)) in
let [a;f],tm1 = strip_exists(concl th1) in
let th_orth,th2 = CONJ_PAIR(ASSUME tm1) in
let th_det,th2a = CONJ_PAIR th2 in
let th_works,th_zero = CONJ_PAIR th2a in
let thc,thq = CONJ_PAIR(PROVE_HYP th2 (UNDISCH(ISPEC f pth))) in
let th3 = CONV_RULE(RAND_CONV(SUBS_CONV(GSYM th_works::CONJUNCTS thc)))
(EXPAND_QUANTS_CONV(ASSUME(concl thq)) bod) in
let th4 = PROVE_HYP thq th3 in
let thps = CONJUNCTS(MATCH_MP oth (CONJ th_orth th_det)) in
let th5 = LINEAR_INVARIANTS f thps in
let th6 = PROVE_HYP th_orth
(GEN_REWRITE_RULE (RAND_CONV o REDEPTH_CONV) [th5] th4) in
let ntm = mk_forall(a,mk_imp(concl th_zero,rand(concl th6))) in
let th7 = MP(SPEC a (ASSUME ntm)) th_zero in
let th8 = DISCH ntm (EQ_MP (SYM th6) th7) in
if intersect (frees(concl th8)) [a;f] = [] then
let th9 = PROVE_HYP th1 (itlist SIMPLE_CHOOSE [a;f] th8) in
let th10 = DISCH ntm (GEN x (UNDISCH th9)) in
CONV_RULE(LAND_CONV (GEN_ALPHA_CONV x)) th10
else
let mtm = list_mk_forall([a;f],mk_imp(hd(hyp th8),rand(concl th6))) in
let th9 = EQ_MP (SYM th6) (UNDISCH(SPECL [a;f] (ASSUME mtm))) in
let th10 = itlist SIMPLE_CHOOSE [a;f] (DISCH mtm th9) in
let th11 = GEN x (PROVE_HYP th1 th10) in
MATCH_MP
MONO_FORALL th11;;