(* ========================================================================= *)
(* Faces, extreme points, polytopes, polyhedra etc. *)
(* ========================================================================= *)
needs "Multivariate/paths.ml";;
(* ------------------------------------------------------------------------- *)
(* Faces of a (usually convex) set. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("face_of",(12,"right"));;
add_translation_invariants [FACE_OF_TRANSLATION_EQ];;
add_linear_invariants [FACE_OF_LINEAR_IMAGE];;
let FACE_OF_AFFINE_TRIVIAL = prove
(`!s f:real^N->bool.
affine s /\ f
face_of s ==> f = {} \/ f = s`,
REPEAT STRIP_TAC THEN
ASM_CASES_TAC `f:real^N->bool = {}` THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
DISCH_THEN(X_CHOOSE_TAC `a:real^N`) THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
FACE_OF_IMP_SUBSET) THEN
MATCH_MP_TAC
SUBSET_ANTISYM THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
SUBSET] THEN X_GEN_TAC `b:real^N` THEN DISCH_TAC THEN
ASM_CASES_TAC `(b:real^N)
IN f` THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
face_of]) THEN
DISCH_THEN(MP_TAC o SPECL [`&2 % a - b:real^N`; `b:real^N`; `a:real^N`] o
CONJUNCT2 o CONJUNCT2) THEN
SUBGOAL_THEN `~(a:real^N = b)` ASSUME_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_SIMP_TAC[
IN_SEGMENT; VECTOR_ARITH `&2 % a - b:real^N = b <=> a = b`] THEN
CONJ_TAC THENL
[REWRITE_TAC[VECTOR_ARITH `&2 % a - b:real^N = a + &1 % (a - b)`] THEN
MATCH_MP_TAC
IN_AFFINE_ADD_MUL_DIFF THEN ASM SET_TAC[];
EXISTS_TAC `&1 / &2` THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
VECTOR_ARITH_TAC]);;
let INTERS_FACES_FINITE_BOUND = prove
(`!s f:(real^N->bool)->bool.
convex s /\ (!c. c
IN f ==> c
face_of s)
==> ?f'. FINITE f' /\ f'
SUBSET f /\
CARD f' <=
dimindex(:N) + 1 /\
INTERS f' =
INTERS f`,
SUBGOAL_THEN
`!s f:(real^N->bool)->bool.
convex s /\ (!c. c
IN f ==> c
face_of s /\ ~(c = s))
==> ?f'. FINITE f' /\ f'
SUBSET f /\
CARD f' <=
dimindex(:N) + 1 /\
INTERS f' =
INTERS f`
ASSUME_TAC THENL
[ALL_TAC;
REPEAT STRIP_TAC THEN
ASM_CASES_TAC `(s:real^N->bool)
IN f` THENL
[ALL_TAC; FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[]] THEN
FIRST_ASSUM(DISJ_CASES_THEN2 SUBST1_TAC MP_TAC o MATCH_MP (SET_RULE
`s
IN f ==> f = {s} \/ ?t. ~(t = s) /\ t
IN f`)) THENL
[EXISTS_TAC `{s:real^N->bool}` THEN
SIMP_TAC[
FINITE_INSERT;
FINITE_EMPTY;
SUBSET_REFL;
CARD_CLAUSES] THEN
ARITH_TAC;
DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool` STRIP_ASSUME_TAC)] THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`s:real^N->bool`; `f
DELETE
(s:real^N->bool)`]) THEN
ASM_SIMP_TAC[
IN_DELETE;
SUBSET_DELETE] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `f':(real^N->bool)->bool` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `f = (s:real^N->bool)
INSERT (f
DELETE s)` MP_TAC THENL
[ASM SET_TAC[];
DISCH_THEN(fun
th -> GEN_REWRITE_TAC (funpow 2 RAND_CONV) [
th])] THEN
REWRITE_TAC[
INTERS_INSERT] THEN
MATCH_MP_TAC(SET_RULE `t
SUBSET s ==> t = s
INTER t`) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `t:real^N->bool`) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(ASSUME_TAC o MATCH_MP
FACE_OF_IMP_SUBSET) THEN
MATCH_MP_TAC
SUBSET_TRANS THEN EXISTS_TAC `t:real^N->bool` THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[
SUBSET;
IN_INTERS;
IN_DELETE] THEN
ASM SET_TAC[]] THEN
REPEAT STRIP_TAC THEN ASM_CASES_TAC
`!f':(real^N->bool)->bool.
FINITE f' /\ f'
SUBSET f /\
CARD f' <=
dimindex(:N) + 1
==> ?c. c
IN f /\ c
INTER (
INTERS f')
PSUBSET (
INTERS f')`
THENL
[ALL_TAC;
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
NOT_FORALL_THM]) THEN
MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC THEN
SIMP_TAC[NOT_IMP; GSYM
CONJ_ASSOC] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
ASM_REWRITE_TAC[
PSUBSET;
INTER_SUBSET] THEN ASM SET_TAC[]] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE BINDER_CONV
[
RIGHT_IMP_EXISTS_THM]) THEN
REWRITE_TAC[
SKOLEM_THM;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `c:((real^N->bool)->bool)->real^N->bool` THEN DISCH_TAC THEN
CHOOSE_TAC(prove_recursive_functions_exist num_RECURSION
`d 0 = {c {} :real^N->bool} /\ !n. d(SUC n) = c(d n)
INSERT d n`) THEN
SUBGOAL_THEN `!n:num. ~(d n:(real^N->bool)->bool = {})` ASSUME_TAC THENL
[INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN
`!n. n <=
dimindex(:N) + 1
==> (d n)
SUBSET (f:(real^N->bool)->bool) /\
FINITE(d n) /\
CARD(d n) <= n + 1`
ASSUME_TAC THENL
[INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_SIMP_TAC[
INSERT_SUBSET;
CARD_CLAUSES;
FINITE_INSERT;
FINITE_EMPTY;
EMPTY_SUBSET; ARITH_RULE `SUC n <= m + 1 ==> n <= m + 1`] THEN
REPEAT STRIP_TAC THEN TRY ASM_ARITH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `(d:num->(real^N->bool)->bool) n`) THEN
FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN
ANTS_TAC THENL [ASM_ARITH_TAC; STRIP_TAC] THEN ASM_REWRITE_TAC[] THEN
ANTS_TAC THENL [ASM_ARITH_TAC; SIMP_TAC[]];
ALL_TAC] THEN
SUBGOAL_THEN
`!n. n <=
dimindex(:N)
==> (
INTERS(d(SUC n)):real^N->bool)
PSUBSET INTERS(d n)`
ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[
INTERS_INSERT] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `(d:num->(real^N->bool)->bool) n`) THEN
ANTS_TAC THENL [ALL_TAC; SIMP_TAC[]] THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `n:num`)) THEN
ASM_SIMP_TAC[ARITH_RULE `n <= N ==> n <= N + 1`] THEN
ASM_ARITH_TAC;
ALL_TAC] THEN
FIRST_X_ASSUM(CONJUNCTS_THEN(K ALL_TAC)) THEN
SUBGOAL_THEN
`!n. n <=
dimindex(:N) + 1
==>
aff_dim(
INTERS(d n):real^N->bool) < &(
dimindex(:N)) - &n`
MP_TAC THENL
[INDUCT_TAC THENL
[DISCH_TAC THEN REWRITE_TAC[
INT_SUB_RZERO] THEN
MATCH_MP_TAC
INT_LTE_TRANS THEN
EXISTS_TAC `
aff_dim(s:real^N->bool)` THEN
REWRITE_TAC[
AFF_DIM_LE_UNIV] THEN
MATCH_MP_TAC
FACE_OF_AFF_DIM_LT THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[MATCH_MP_TAC
FACE_OF_INTERS THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY] o
SPEC `0`) THEN
DISCH_THEN(X_CHOOSE_TAC `e:real^N->bool`) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `e:real^N->bool`) THEN
ANTS_TAC THENL [ASM SET_TAC[]; STRIP_TAC] THEN
MATCH_MP_TAC(SET_RULE
`!t. t
PSUBSET s /\ u
SUBSET t ==> ~(u = s)`) THEN
EXISTS_TAC `e:real^N->bool` THEN
FIRST_X_ASSUM(ASSUME_TAC o MATCH_MP
FACE_OF_IMP_SUBSET) THEN
ASM SET_TAC[]];
DISCH_TAC THEN REWRITE_TAC[GSYM
INT_OF_NUM_SUC] THEN
MATCH_MP_TAC(INT_ARITH
`!d':int. d < d' /\ d' < m - n ==> d < m - (n + &1)`) THEN
EXISTS_TAC `
aff_dim(
INTERS(d(n:num)):real^N->bool)` THEN
ASM_SIMP_TAC[ARITH_RULE `SUC n <= k + 1 ==> n <= k + 1`] THEN
MATCH_MP_TAC
FACE_OF_AFF_DIM_LT THEN
ASM_SIMP_TAC[ARITH_RULE `SUC n <= m + 1 ==> n <= m`;
SET_RULE `s
PSUBSET t ==> ~(s = t)`] THEN
CONJ_TAC THENL
[MATCH_MP_TAC
CONVEX_INTERS THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC
FACE_OF_IMP_CONVEX THEN
EXISTS_TAC `s:real^N->bool` THEN
ASM_MESON_TAC[
SUBSET; ARITH_RULE `SUC n <= m + 1 ==> n <= m + 1`];
ALL_TAC] THEN
MP_TAC(ISPECL [`
INTERS(d(SUC n)):real^N->bool`;`s:real^N->bool`;
`
INTERS(d(n:num)):real^N->bool`]
FACE_OF_FACE) THEN
ASM_SIMP_TAC[SET_RULE `s
PSUBSET t ==> s
SUBSET t`;
ARITH_RULE `SUC n <= m + 1 ==> n <= m`] THEN
MATCH_MP_TAC(TAUT `a /\ b ==> (a ==> (c <=> b)) ==> c`) THEN
CONJ_TAC THEN MATCH_MP_TAC
FACE_OF_INTERS THEN ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[
SUBSET; ARITH_RULE `SUC n <= m + 1 ==> n <= m + 1`]];
ALL_TAC] THEN
DISCH_THEN(MP_TAC o SPEC `
dimindex(:N) + 1`) THEN REWRITE_TAC[
LE_REFL] THEN
MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN REWRITE_TAC[
INT_NOT_LT] THEN
REWRITE_TAC[GSYM
INT_OF_NUM_ADD; INT_ARITH `d - (d + &1):int = -- &1`] THEN
REWRITE_TAC[
AFF_DIM_GE]);;
let INTERS_FACES_FINITE_ALTBOUND = prove
(`!s f:(real^N->bool)->bool.
(!c. c
IN f ==> c
face_of s)
==> ?f'. FINITE f' /\ f'
SUBSET f /\
CARD f' <=
dimindex(:N) + 2 /\
INTERS f' =
INTERS f`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC
`!f':(real^N->bool)->bool.
FINITE f' /\ f'
SUBSET f /\
CARD f' <=
dimindex(:N) + 2
==> ?c. c
IN f /\ c
INTER (
INTERS f')
PSUBSET (
INTERS f')`
THENL
[ALL_TAC;
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
NOT_FORALL_THM]) THEN
MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC THEN
SIMP_TAC[NOT_IMP; GSYM
CONJ_ASSOC] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
ASM_REWRITE_TAC[
PSUBSET;
INTER_SUBSET] THEN ASM SET_TAC[]] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE BINDER_CONV
[
RIGHT_IMP_EXISTS_THM]) THEN
REWRITE_TAC[
SKOLEM_THM;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `c:((real^N->bool)->bool)->real^N->bool` THEN DISCH_TAC THEN
CHOOSE_TAC(prove_recursive_functions_exist num_RECURSION
`d 0 = {c {} :real^N->bool} /\ !n. d(SUC n) = c(d n)
INSERT d n`) THEN
SUBGOAL_THEN `!n:num. ~(d n:(real^N->bool)->bool = {})` ASSUME_TAC THENL
[INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN
`!n. n <=
dimindex(:N) + 2
==> (d n)
SUBSET (f:(real^N->bool)->bool) /\
FINITE(d n) /\
CARD(d n) <= n + 1`
ASSUME_TAC THENL
[INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_SIMP_TAC[
INSERT_SUBSET;
CARD_CLAUSES;
FINITE_INSERT;
FINITE_EMPTY;
EMPTY_SUBSET; ARITH_RULE `SUC n <= m + 2 ==> n <= m + 2`] THEN
REPEAT STRIP_TAC THEN TRY ASM_ARITH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `(d:num->(real^N->bool)->bool) n`) THEN
FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN
ANTS_TAC THENL [ASM_ARITH_TAC; STRIP_TAC] THEN ASM_REWRITE_TAC[] THEN
ANTS_TAC THENL [ASM_ARITH_TAC; SIMP_TAC[]];
ALL_TAC] THEN
SUBGOAL_THEN
`!n. n <=
dimindex(:N) + 1
==> (
INTERS(d(SUC n)):real^N->bool)
PSUBSET INTERS(d n)`
ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[
INTERS_INSERT] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `(d:num->(real^N->bool)->bool) n`) THEN
ANTS_TAC THENL [ALL_TAC; SIMP_TAC[]] THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `n:num`)) THEN
ASM_SIMP_TAC[ARITH_RULE `n <= N + 1 ==> n <= N + 2`] THEN
ASM_ARITH_TAC;
ALL_TAC] THEN
FIRST_X_ASSUM(CONJUNCTS_THEN(K ALL_TAC)) THEN
SUBGOAL_THEN
`!n. n <=
dimindex(:N) + 2
==>
aff_dim(
INTERS(d n):real^N->bool) <= &(
dimindex(:N)) - &n`
MP_TAC THENL
[INDUCT_TAC THEN REWRITE_TAC[
INT_SUB_RZERO;
AFF_DIM_LE_UNIV] THEN
DISCH_TAC THEN REWRITE_TAC[GSYM
INT_OF_NUM_SUC] THEN
MATCH_MP_TAC(INT_ARITH
`!d':int. d < d' /\ d' <= m - n ==> d <= m - (n + &1)`) THEN
EXISTS_TAC `
aff_dim(
INTERS(d(n:num)):real^N->bool)` THEN
ASM_SIMP_TAC[ARITH_RULE `SUC n <= k + 2 ==> n <= k + 2`] THEN
MATCH_MP_TAC
FACE_OF_AFF_DIM_LT THEN
ASM_SIMP_TAC[ARITH_RULE `SUC n <= m + 2 ==> n <= m + 1`;
SET_RULE `s
PSUBSET t ==> ~(s = t)`] THEN
CONJ_TAC THENL
[MATCH_MP_TAC
CONVEX_INTERS THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC
FACE_OF_IMP_CONVEX THEN
EXISTS_TAC `s:real^N->bool` THEN
ASM_MESON_TAC[
SUBSET; ARITH_RULE `SUC n <= m + 2 ==> n <= m + 2`];
ALL_TAC] THEN
MP_TAC(ISPECL [`
INTERS(d(SUC n)):real^N->bool`;`s:real^N->bool`;
`
INTERS(d(n:num)):real^N->bool`]
FACE_OF_FACE) THEN
ASM_SIMP_TAC[SET_RULE `s
PSUBSET t ==> s
SUBSET t`;
ARITH_RULE `SUC n <= m + 2 ==> n <= m + 1`] THEN
MATCH_MP_TAC(TAUT `a /\ b ==> (a ==> (c <=> b)) ==> c`) THEN
CONJ_TAC THEN MATCH_MP_TAC
FACE_OF_INTERS THEN ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[
SUBSET; ARITH_RULE `SUC n <= m + 2 ==> n <= m + 2`];
ALL_TAC] THEN
DISCH_THEN(MP_TAC o SPEC `
dimindex(:N) + 2`) THEN REWRITE_TAC[
LE_REFL] THEN
MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN REWRITE_TAC[
INT_NOT_LE] THEN
REWRITE_TAC[GSYM
INT_OF_NUM_ADD; INT_ARITH
`d - (d + &2):int < i <=> -- &1 <= i`] THEN
REWRITE_TAC[
AFF_DIM_GE]);;
let FACE_OF_CONIC = prove
(`!s f:real^N->bool.
conic s /\ f
face_of s ==>
conic f`,
REPEAT GEN_TAC THEN REWRITE_TAC[
face_of;
conic] THEN STRIP_TAC THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `c:real`] THEN STRIP_TAC THEN
ASM_CASES_TAC `x:real^N =
vec 0` THENL
[ASM_MESON_TAC[
VECTOR_MUL_RZERO]; ALL_TAC] THEN
ASM_CASES_TAC `c = &1` THENL
[ASM_MESON_TAC[
VECTOR_MUL_LID]; ALL_TAC] THEN
SUBGOAL_THEN `?d e. &0 <= d /\ &0 <= e /\ d < &1 /\ &1 < e /\ d < e /\
(d = c \/ e = c)`
MP_TAC THENL
[FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH
`~(c = &1) ==> c < &1 \/ &1 < c`))
THENL
[MAP_EVERY EXISTS_TAC [`c:real`; `&2`] THEN ASM_REAL_ARITH_TAC;
MAP_EVERY EXISTS_TAC [`&1 / &2`; `c:real`] THEN ASM_REAL_ARITH_TAC];
DISCH_THEN(REPEAT_TCL CHOOSE_THEN
(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC)) THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`d % x :real^N`; `e % x:real^N`; `x:real^N`]) THEN
ANTS_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
SUBGOAL_THEN `(x:real^N)
IN s` ASSUME_TAC THENL
[ASM SET_TAC[]; ASM_SIMP_TAC[
IN_SEGMENT]] THEN
ASM_SIMP_TAC[
VECTOR_MUL_RCANCEL;
REAL_LT_IMP_NE] THEN
EXISTS_TAC `(&1 - d) / (e - d)` THEN
ASM_SIMP_TAC[
REAL_LT_LDIV_EQ;
REAL_LT_RDIV_EQ;
REAL_SUB_LT] THEN
REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
REWRITE_TAC[
VECTOR_MUL_ASSOC; GSYM
VECTOR_ADD_RDISTRIB] THEN
REWRITE_TAC[VECTOR_ARITH `x:real^N = a % x <=> (a - &1) % x =
vec 0`] THEN
ASM_REWRITE_TAC[
VECTOR_MUL_EQ_0] THEN
UNDISCH_TAC `d:real < e` THEN CONV_TAC REAL_FIELD]);;
(* ------------------------------------------------------------------------- *)
(* Exposed faces (faces that are intersection with supporting hyperplane). *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("exposed_face_of",(12,"right"));;
let EXPOSED_FACE_OF_TRANSLATION_EQ = prove
(`!a f s:real^N->bool.
(
IMAGE (\x. a + x) f)
exposed_face_of (
IMAGE (\x. a + x) s) <=>
f
exposed_face_of s`,
REPEAT GEN_TAC THEN REWRITE_TAC[
exposed_face_of;
FACE_OF_TRANSLATION_EQ] THEN
MP_TAC(ISPEC `\x:real^N. a + x`
QUANTIFY_SURJECTION_THM) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL
[MESON_TAC[VECTOR_ARITH `y + (x - y):real^N = x`]; ALL_TAC] THEN
DISCH_THEN(fun
th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
[last(CONJUNCTS
th)]) THEN
REWRITE_TAC[end_itlist CONJ (!invariant_under_translation)] THEN
REWRITE_TAC[
DOT_RADD] THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
REWRITE_TAC[GSYM
REAL_LE_SUB_LADD; GSYM
REAL_EQ_SUB_LADD] THEN
AP_TERM_TAC THEN AP_TERM_TAC THEN GEN_REWRITE_TAC I [
FUN_EQ_THM] THEN
X_GEN_TAC `c:real^N` THEN REWRITE_TAC[] THEN
EQ_TAC THEN DISCH_THEN(X_CHOOSE_THEN `b:real` STRIP_ASSUME_TAC) THENL
[EXISTS_TAC `b - (c:real^N)
dot a`;
EXISTS_TAC `b + (c:real^N)
dot a`] THEN
ASM_REWRITE_TAC[REAL_ARITH `(x + y) - y:real = x`]);;
add_translation_invariants [EXPOSED_FACE_OF_TRANSLATION_EQ];;
let EXPOSED_FACE_OF_INTERS = prove
(`!P s:real^N->bool.
~(P = {}) /\ (!t. t
IN P ==> t
exposed_face_of s)
==>
INTERS P
exposed_face_of s`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL [`s:real^N->bool`; `P:(real^N->bool)->bool`]
INTERS_FACES_FINITE_ALTBOUND) THEN
ANTS_TAC THENL [ASM_MESON_TAC[
exposed_face_of]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `Q:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SYM) THEN
ASM_CASES_TAC `Q:(real^N->bool)->bool = {}` THENL
[ASM_SIMP_TAC[
INTERS_0] THEN
REWRITE_TAC[SET_RULE `
INTERS s =
UNIV <=> !t. t
IN s ==> t =
UNIV`] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
ASM_MESON_TAC[];
DISCH_THEN SUBST1_TAC THEN
FIRST_X_ASSUM(MP_TAC o check (is_neg o concl)) THEN
SUBGOAL_THEN `!t:real^N->bool. t
IN Q ==> t
exposed_face_of s` MP_TAC THENL
[ASM SET_TAC[]; UNDISCH_TAC `FINITE(Q:(real^N->bool)->bool)`] THEN
SPEC_TAC(`Q:(real^N->bool)->bool`,`Q:(real^N->bool)->bool`) THEN
POP_ASSUM_LIST(K ALL_TAC) THEN
MATCH_MP_TAC
FINITE_INDUCT_STRONG THEN REWRITE_TAC[
FORALL_IN_INSERT] THEN
MAP_EVERY X_GEN_TAC [`t:real^N->bool`; `P:(real^N->bool)->bool`] THEN
DISCH_THEN(fun
th -> STRIP_TAC THEN MP_TAC
th) THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
INTERS_INSERT] THEN
ASM_CASES_TAC `P:(real^N->bool)->bool = {}` THEN
ASM_SIMP_TAC[
INTERS_0;
INTER_UNIV;
EXPOSED_FACE_OF_INTER]]);;
(* ------------------------------------------------------------------------- *)
(* Extreme points of a set, which are its singleton faces. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("extreme_point_of",(12,"right"));;
let EXTREME_POINT_OF_MIDPOINT = prove
(`!s x:real^N.
convex s
==> (x
extreme_point_of s <=>
x
IN s /\
!a b. a
IN s /\ b
IN s /\ x =
midpoint(a,b) ==> x = a /\ x = b)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[
extreme_point_of] THEN
AP_TERM_TAC THEN EQ_TAC THEN
DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN
DISCH_TAC THENL
[FIRST_X_ASSUM(MP_TAC o SPECL [`a:real^N`; `b:real^N`]) THEN
ASM_SIMP_TAC[
MIDPOINT_IN_SEGMENT;
MIDPOINT_REFL];
ALL_TAC] THEN
REWRITE_TAC[
IN_SEGMENT] THEN DISCH_THEN(CONJUNCTS_THEN2
ASSUME_TAC (X_CHOOSE_THEN `u:real` STRIP_ASSUME_TAC)) THEN
ABBREV_TAC `d = min (&1 - u) u` THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`x - d / &2 % (b - a):real^N`; `x + d / &2 % (b - a):real^N`]) THEN
REWRITE_TAC[NOT_IMP] THEN REPEAT CONJ_TAC THENL
[FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
CONVEX_ALT]) THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`((&1 - u) % a + u % b) - d / &2 % (b - a):real^N =
(&1 - (u - d / &2)) % a + (u - d / &2) % b`] THEN
DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
CONVEX_ALT]) THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`((&1 - u) % a + u % b) + d / &2 % (b - a):real^N =
(&1 - (u + d / &2)) % a + (u + d / &2) % b`] THEN
DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
REWRITE_TAC[
midpoint] THEN VECTOR_ARITH_TAC;
REWRITE_TAC[VECTOR_ARITH `x:real^N = x - d <=> d =
vec 0`;
VECTOR_ARITH `x:real^N = x + d <=> d =
vec 0`] THEN
ASM_REWRITE_TAC[
VECTOR_MUL_EQ_0;
VECTOR_SUB_EQ] THEN ASM_REAL_ARITH_TAC]);;
add_translation_invariants [EXTREME_POINT_OF_TRANSLATION_EQ];;
add_linear_invariants [EXTREME_POINT_OF_LINEAR_IMAGE];;
(* ------------------------------------------------------------------------- *)
(* Facets. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("facet_of",(12, "right"));;
add_translation_invariants [FACET_OF_TRANSLATION_EQ];;
add_linear_invariants [FACET_OF_LINEAR_IMAGE];;
(* ------------------------------------------------------------------------- *)
(* Edges, i.e. faces of affine dimension 1. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("edge_of",(12, "right"));;
add_translation_invariants [EDGE_OF_TRANSLATION_EQ];;
add_linear_invariants [EDGE_OF_LINEAR_IMAGE];;
(* ------------------------------------------------------------------------- *)
(* Existence of extreme points. *)
(* ------------------------------------------------------------------------- *)
let DIFFERENT_NORM_3_COLLINEAR_POINTS = prove
(`!a b x:real^N.
~(x
IN segment(a,b) /\
norm(a) =
norm(b) /\
norm(x) =
norm(b))`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `a:real^N = b` THEN
ASM_SIMP_TAC[
SEGMENT_REFL;
NOT_IN_EMPTY;
OPEN_SEGMENT_ALT] THEN
REWRITE_TAC[
IN_ELIM_THM] THEN DISCH_THEN
(CONJUNCTS_THEN2 (X_CHOOSE_THEN `u:real` STRIP_ASSUME_TAC) MP_TAC) THEN
ASM_REWRITE_TAC[
NORM_EQ] THEN REWRITE_TAC[VECTOR_ARITH
`(x + y:real^N)
dot (x + y) = x
dot x + &2 * x
dot y + y
dot y`] THEN
REWRITE_TAC[
DOT_LMUL;
DOT_RMUL] THEN
DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) MP_TAC) THEN
UNDISCH_TAC `~(a:real^N = b)` THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM
VECTOR_SUB_EQ] THEN
REWRITE_TAC[GSYM
DOT_EQ_0; VECTOR_ARITH
`(a - b:real^N)
dot (a - b) = a
dot a + b
dot b - &2 * a
dot b`] THEN
ASM_REWRITE_TAC[REAL_RING `a + a - &2 * ab = &0 <=> ab = a`] THEN
SIMP_TAC[REAL_RING
`(&1 - u) * (&1 - u) * a + &2 * (&1 - u) * u * x + u * u * a = a <=>
x = a \/ u = &0 \/ u = &1`] THEN
ASM_REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Krein-Milman, the weaker form as in more general spaces first. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Now the sharper form. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Applying it to convex hulls of explicitly indicated finite sets. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Polytopes. *)
(* ------------------------------------------------------------------------- *)
add_translation_invariants [POLYTOPE_TRANSLATION_EQ];;
let POLYTOPE_LINEAR_IMAGE_EQ = prove
(`!f:real^M->real^N s.
linear f /\ (!x y. f x = f y ==> x = y) /\ (!y. ?x. f x = y)
==> (
polytope (
IMAGE f s) <=>
polytope s)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[
polytope] THEN
MP_TAC(ISPEC `f:real^M->real^N`
QUANTIFY_SURJECTION_THM) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(fun
th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)[
th]) THEN
MP_TAC(end_itlist CONJ
(mapfilter (ISPEC `f:real^M->real^N`) (!invariant_under_linear))) THEN
ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Polyhedra. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Canonical polyedron representation making facial structure explicit. *)
(* ------------------------------------------------------------------------- *)
let FACET_OF_POLYHEDRON_EXPLICIT = prove
(`!s:real^N->bool f a b.
FINITE f /\
s =
affine hull s
INTER INTERS f /\
(!h. h
IN f ==> ~(a h =
vec 0) /\ h = {x | a h
dot x <= b h}) /\
(!f'. f'
PSUBSET f ==> s
PSUBSET affine hull s
INTER INTERS f')
==> !c. c
facet_of s <=>
?h. h
IN f /\ c = s
INTER {x | a h
dot x = b h}`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `s:real^N->bool = {}` THENL
[ASM_REWRITE_TAC[
INTER_EMPTY;
AFFINE_HULL_EMPTY; SET_RULE `~(s
PSUBSET s)`;
FACET_OF_EMPTY] THEN
ASM_CASES_TAC `f:(real^N->bool)->bool = {}` THEN
ASM_REWRITE_TAC[
NOT_IN_EMPTY] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
DISCH_THEN(X_CHOOSE_TAC `h:real^N->bool`) THEN DISCH_THEN
(MP_TAC o SPEC `f
DELETE (h:real^N->bool)` o last o CONJUNCTS) THEN
ASM SET_TAC[];
STRIP_TAC] THEN
SUBGOAL_THEN `
polyhedron(s:real^N->bool)` ASSUME_TAC THENL
[REWRITE_TAC[
POLYHEDRON_INTER_AFFINE] THEN
REWRITE_TAC[
RIGHT_IMP_EXISTS_THM;
SKOLEM_THM] THEN ASM_MESON_TAC[];
ALL_TAC] THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
POLYHEDRON_IMP_CONVEX) THEN
SUBGOAL_THEN
`!h:real^N->bool.
h
IN f ==> (s
INTER {x:real^N | a h
dot x = b h})
facet_of s`
(LABEL_TAC "face") THENL
[REPEAT STRIP_TAC THEN REWRITE_TAC[
facet_of] THEN CONJ_TAC THENL
[MATCH_MP_TAC
FACE_OF_INTER_SUPPORTING_HYPERPLANE_LE THEN
CONJ_TAC THENL
[MATCH_MP_TAC
POLYHEDRON_IMP_CONVEX THEN
REWRITE_TAC[
POLYHEDRON_INTER_AFFINE] THEN
REWRITE_TAC[
RIGHT_IMP_EXISTS_THM;
SKOLEM_THM] THEN ASM_MESON_TAC[];
X_GEN_TAC `x:real^N` THEN FIRST_X_ASSUM SUBST1_TAC THEN
REWRITE_TAC[
IN_INTER;
IN_INTERS] THEN
DISCH_THEN(MP_TAC o SPEC `h:real^N->bool` o CONJUNCT2) THEN
ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[]];
ALL_TAC] THEN
MP_TAC(ISPEC `s:real^N->bool`
RELATIVE_INTERIOR_EQ_EMPTY) THEN
ASM_SIMP_TAC[] THEN REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY] THEN
DISCH_THEN(X_CHOOSE_TAC `x:real^N`) THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
IN_RELATIVE_INTERIOR]) THEN
DISCH_TAC THEN
FIRST_ASSUM(MP_TAC o SPEC `f
DELETE (h:real^N->bool)`) THEN
ANTS_TAC THENL
[ASM SET_TAC[];
REWRITE_TAC[
PSUBSET_ALT;
IN_INTER;
IN_INTERS;
IN_DELETE]] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `z:real^N` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `(a:(real^N->bool)->real^N) h
dot z > b h` ASSUME_TAC THENL
[UNDISCH_TAC `~((z:real^N)
IN s)` THEN
FIRST_ASSUM(SUBST1_TAC o SYM) THEN
REWRITE_TAC[
IN_INTER;
IN_INTERS] THEN
ASM_REWRITE_TAC[REAL_ARITH `a:real > b <=> ~(a <= b)`] THEN
ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `~(z:real^N = x)` ASSUME_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
MP_TAC(ISPECL [`s:real^N->bool`; `f:(real^N->bool)->bool`;
`a:(real^N->bool)->real^N`; `b:(real^N->bool)->
real`]
RELATIVE_INTERIOR_POLYHEDRON_EXPLICIT) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[FIRST_ASSUM ACCEPT_TAC; ALL_TAC] THEN
GEN_REWRITE_TAC LAND_CONV [
EXTENSION] THEN
DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN
ASM_REWRITE_TAC[
IN_ELIM_THM] THEN
DISCH_THEN(fun
th ->
MP_TAC(SPEC `h:real^N->bool`
th) THEN ASM_REWRITE_TAC[] THEN
DISCH_TAC THEN ASSUME_TAC
th) THEN
SUBGOAL_THEN `(a:(real^N->bool)->real^N) h
dot x < a h
dot z`
ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
ABBREV_TAC `l = (b h - (a:(real^N->bool)->real^N) h
dot x) /
(a h
dot z - a h
dot x)` THEN
SUBGOAL_THEN `&0 < l /\ l < &1` STRIP_ASSUME_TAC THENL
[EXPAND_TAC "l" THEN
ASM_SIMP_TAC[
REAL_LT_LDIV_EQ;
REAL_LT_RDIV_EQ;
REAL_SUB_LT] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
ABBREV_TAC `w:real^N = (&1 - l) % x + l % z:real^N` THEN
SUBGOAL_THEN
`!i. i
IN f /\ ~(i = h) ==> (a:(real^N->bool)->real^N) i
dot w < b i`
ASSUME_TAC THENL
[X_GEN_TAC `i:real^N->bool` THEN STRIP_TAC THEN EXPAND_TAC "w" THEN
REWRITE_TAC[
DOT_RADD;
DOT_RMUL] THEN
MATCH_MP_TAC(REAL_ARITH
`(&1 - l) * x < (&1 - l) * z /\ l * y <= l * z
==> (&1 - l) * x + l * y < z`) THEN
ASM_SIMP_TAC[
REAL_LE_LMUL_EQ;
REAL_LT_IMP_LE;
REAL_LT_LMUL_EQ;
REAL_SUB_LT] THEN
UNDISCH_TAC `!t:real^N->bool. t
IN f /\ ~(t = h) ==> z
IN t` THEN
DISCH_THEN(MP_TAC o SPEC `i:real^N->bool`) THEN ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `(a:(real^N->bool)->real^N) h
dot w = b h` ASSUME_TAC THENL
[EXPAND_TAC "w" THEN REWRITE_TAC[VECTOR_ARITH
`(&1 - l) % x + l % z:real^N = x + l % (z - x)`] THEN
EXPAND_TAC "l" THEN REWRITE_TAC[
DOT_RADD;
DOT_RSUB;
DOT_RMUL] THEN
ASM_SIMP_TAC[
REAL_DIV_RMUL;
REAL_LT_IMP_NE;
REAL_SUB_0] THEN
REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `(w:real^N)
IN s` ASSUME_TAC THENL
[FIRST_ASSUM(fun
th -> GEN_REWRITE_TAC RAND_CONV [
th]) THEN
REWRITE_TAC[
IN_INTER;
IN_INTERS] THEN CONJ_TAC THENL
[EXPAND_TAC "w" THEN
MATCH_MP_TAC(REWRITE_RULE[
AFFINE_ALT]
AFFINE_AFFINE_HULL) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
HULL_INC THEN
ASM_MESON_TAC[
RELATIVE_INTERIOR_SUBSET;
SUBSET];
ALL_TAC] THEN
X_GEN_TAC `i:real^N->bool` THEN DISCH_TAC THEN
ASM_CASES_TAC `i:real^N->bool = h` THENL
[ASM SET_TAC[
REAL_LE_REFL]; ALL_TAC] THEN
SUBGOAL_THEN `
convex(i:real^N->bool)` MP_TAC THENL
[REPEAT(FIRST_X_ASSUM(MP_TAC o C MATCH_MP
(ASSUME `(i:real^N->bool)
IN f`))) THEN
REPEAT(DISCH_THEN(fun
th -> ONCE_REWRITE_TAC[
th])) THEN
REWRITE_TAC[
CONVEX_HALFSPACE_LE];
ALL_TAC] THEN
REWRITE_TAC[
CONVEX_ALT] THEN EXPAND_TAC "w" THEN
DISCH_THEN MATCH_MP_TAC THEN
ASM_SIMP_TAC[] THEN FIRST_X_ASSUM(MP_TAC o CONJUNCT1) THEN
FIRST_ASSUM(fun t -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [t]) THEN
REWRITE_TAC[
IN_INTER;
IN_INTERS] THEN ASM_SIMP_TAC[
REAL_LT_IMP_LE];
ALL_TAC] THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
ONCE_REWRITE_TAC[GSYM
AFF_DIM_AFFINE_HULL] THEN
SUBGOAL_THEN
`
affine hull (s
INTER {x | (a:(real^N->bool)->real^N) h
dot x = b h}) =
(
affine hull s)
INTER {x | a h
dot x = b h}`
SUBST1_TAC THENL
[ALL_TAC;
SIMP_TAC[
AFF_DIM_AFFINE_INTER_HYPERPLANE;
AFFINE_AFFINE_HULL] THEN
COND_CASES_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
COND_CASES_TAC THENL [ASM SET_TAC[
REAL_LT_REFL]; REFL_TAC]] THEN
MATCH_MP_TAC
SUBSET_ANTISYM THEN REWRITE_TAC[
SUBSET_INTER] THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC
HULL_MONO THEN SET_TAC[];
MATCH_MP_TAC(SET_RULE
`s
SUBSET affine hull t /\
affine hull t = t ==> s
SUBSET t`) THEN
REWRITE_TAC[
AFFINE_HULL_EQ;
AFFINE_HYPERPLANE] THEN
MATCH_MP_TAC
HULL_MONO THEN SET_TAC[];
ALL_TAC] THEN
REWRITE_TAC[
SUBSET;
IN_INTER;
IN_ELIM_THM] THEN
X_GEN_TAC `y:real^N` THEN STRIP_TAC THEN
SUBGOAL_THEN
`?t. &0 < t /\
!j. j
IN f /\ ~(j:real^N->bool = h)
==> t * (a j
dot y - a j
dot w) <= b j - a j
dot (w:real^N)`
STRIP_ASSUME_TAC THENL
[ASM_CASES_TAC `f
DELETE (h:real^N->bool) = {}` THENL
[ASM_REWRITE_TAC[GSYM
IN_DELETE;
NOT_IN_EMPTY] THEN
EXISTS_TAC `&1` THEN REWRITE_TAC[
REAL_LT_01];
ALL_TAC] THEN
EXISTS_TAC `
inf (
IMAGE
(\j. if &0 < a j
dot y - a j
dot (w:real^N)
then (b j - a j
dot w) / (a j
dot y - a j
dot w)
else &1) (f
DELETE (h:real^N->bool)))` THEN
MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
[ASM_SIMP_TAC[
REAL_LT_INF_FINITE;
FINITE_IMAGE;
FINITE_DELETE;
IMAGE_EQ_EMPTY;
FORALL_IN_IMAGE;
IN_DELETE] THEN
ONCE_REWRITE_TAC[
COND_RAND] THEN ONCE_REWRITE_TAC[
COND_RATOR] THEN
ASM_SIMP_TAC[
REAL_LT_DIV;
REAL_SUB_LT;
REAL_LT_01;
COND_ID];
REWRITE_TAC[
REAL_SUB_LT] THEN DISCH_TAC] THEN
X_GEN_TAC `j:real^N->bool` THEN STRIP_TAC THEN
ASM_CASES_TAC `a j
dot (w:real^N) < a(j:real^N->bool)
dot y` THENL
[ASM_SIMP_TAC[GSYM
REAL_LE_RDIV_EQ;
REAL_INF_LE_FINITE;
REAL_SUB_LT;
FINITE_IMAGE;
FINITE_DELETE;
IMAGE_EQ_EMPTY] THEN
REWRITE_TAC[
EXISTS_IN_IMAGE] THEN EXISTS_TAC `j:real^N->bool` THEN
ASM_REWRITE_TAC[
IN_DELETE;
REAL_LE_REFL];
MATCH_MP_TAC(REAL_ARITH `&0 <= --x /\ &0 < y ==> x <= y`) THEN
ASM_SIMP_TAC[
REAL_SUB_LT; GSYM
REAL_MUL_RNEG;
REAL_LE_MUL_EQ] THEN
ASM_REAL_ARITH_TAC];
ALL_TAC] THEN
ABBREV_TAC `c:real^N = (&1 - t) % w + t % y` THEN
SUBGOAL_THEN `y:real^N = (&1 - inv t) % w + inv(t) % c` SUBST1_TAC THENL
[EXPAND_TAC "c" THEN
REWRITE_TAC[
VECTOR_ADD_LDISTRIB;
VECTOR_MUL_ASSOC] THEN
ASM_SIMP_TAC[REAL_MUL_LINV;
REAL_LT_IMP_NZ;
REAL_FIELD `&0 < x ==> inv x * (&1 - x) = inv x - &1`] THEN
VECTOR_ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC(REWRITE_RULE[
AFFINE_ALT]
AFFINE_AFFINE_HULL) THEN
CONJ_TAC THEN MATCH_MP_TAC
HULL_INC THEN
ASM_REWRITE_TAC[
IN_INTER;
IN_ELIM_THM] THEN
MATCH_MP_TAC(TAUT `b /\ (b ==> a) ==> a /\ b`) THEN CONJ_TAC THENL
[EXPAND_TAC "c" THEN REWRITE_TAC[
DOT_RADD;
DOT_RMUL] THEN
ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RING;
DISCH_TAC] THEN
FIRST_ASSUM(fun t -> GEN_REWRITE_TAC RAND_CONV [t]) THEN
REWRITE_TAC[
IN_INTER;
IN_INTERS] THEN CONJ_TAC THENL
[EXPAND_TAC "c" THEN
MATCH_MP_TAC(REWRITE_RULE[
AFFINE_ALT]
AFFINE_AFFINE_HULL) THEN
ASM_SIMP_TAC[
HULL_INC];
ALL_TAC] THEN
X_GEN_TAC `j:real^N->bool` THEN DISCH_TAC THEN
FIRST_X_ASSUM(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC o C MATCH_MP
(ASSUME `(j:real^N->bool)
IN f`)) THEN
DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[
IN_ELIM_THM] THEN
ASM_CASES_TAC `j:real^N->bool = h` THEN ASM_SIMP_TAC[
REAL_EQ_IMP_LE] THEN
EXPAND_TAC "c" THEN REWRITE_TAC[
DOT_RADD;
DOT_RMUL] THEN
REWRITE_TAC[REAL_ARITH
`(&1 - t) * x + t * y <= z <=> t * (y - x) <= z - x`] THEN
ASM_SIMP_TAC[];
ALL_TAC] THEN
X_GEN_TAC `c:real^N->bool` THEN EQ_TAC THENL
[ALL_TAC; STRIP_TAC THEN ASM_SIMP_TAC[]] THEN
REWRITE_TAC[
facet_of] THEN STRIP_TAC THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
FACE_OF_IMP_CONVEX) THEN
SUBGOAL_THEN `~(
relative_interior(c:real^N->bool) = {})` MP_TAC THENL
[ASM_SIMP_TAC[
RELATIVE_INTERIOR_EQ_EMPTY]; ALL_TAC] THEN
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY] THEN
DISCH_THEN(X_CHOOSE_TAC `x:real^N`) THEN
MP_TAC(ISPECL [`s:real^N->bool`; `f:(real^N->bool)->bool`;
`a:(real^N->bool)->real^N`; `b:(real^N->bool)->
real`]
RELATIVE_INTERIOR_POLYHEDRON_EXPLICIT) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [FIRST_ASSUM ACCEPT_TAC; ALL_TAC] THEN
GEN_REWRITE_TAC LAND_CONV [
EXTENSION] THEN
DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[
IN_ELIM_THM] THEN
SUBGOAL_THEN `~(c:real^N->bool = s)` ASSUME_TAC THENL
[ASM_MESON_TAC[INT_ARITH`~(i:int = i - &1)`]; ALL_TAC] THEN
SUBGOAL_THEN `~((x:real^N)
IN relative_interior s)` ASSUME_TAC THENL
[UNDISCH_TAC `~(c:real^N->bool = s)` THEN REWRITE_TAC[CONTRAPOS_THM] THEN
DISCH_TAC THEN MATCH_MP_TAC
FACE_OF_EQ THEN
EXISTS_TAC `s:real^N->bool` THEN ASM_SIMP_TAC[
FACE_OF_REFL] THEN
ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `(x:real^N)
IN s` MP_TAC THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o REWRITE_RULE[
SUBSET] o MATCH_MP
FACE_OF_IMP_SUBSET) THEN
ASM_SIMP_TAC[REWRITE_RULE[
SUBSET]
RELATIVE_INTERIOR_SUBSET];
ALL_TAC] THEN
ASM_SIMP_TAC[] THEN DISCH_THEN(fun
th -> ASSUME_TAC
th THEN MP_TAC
th) THEN
FIRST_ASSUM(fun t -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [t]) THEN
REWRITE_TAC[
IN_INTER;
IN_INTERS] THEN STRIP_TAC THEN
REWRITE_TAC[
NOT_FORALL_THM] THEN MATCH_MP_TAC
MONO_EXISTS THEN
X_GEN_TAC `i:real^N->bool` THEN REWRITE_TAC[NOT_IMP] THEN STRIP_TAC THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `(a:(real^N->bool)->real^N) i
dot x = b i` ASSUME_TAC THENL
[MATCH_MP_TAC(REAL_ARITH `x <= y /\ ~(x < y) ==> x = y`) THEN
ASM_REWRITE_TAC[] THEN UNDISCH_THEN
`!t:real^N->bool. t
IN f ==> x
IN t` (MP_TAC o SPEC `i:real^N->bool`) THEN
ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(MP_TAC o CONJUNCT2 o C MATCH_MP
(ASSUME `(i:real^N->bool)
IN f`)) THEN SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `c
SUBSET (s
INTER {x:real^N | a(i:real^N->bool)
dot x = b i})`
ASSUME_TAC THENL
[MATCH_MP_TAC
SUBSET_OF_FACE_OF THEN EXISTS_TAC `s:real^N->bool` THEN
ASM_SIMP_TAC[
FACE_OF_IMP_SUBSET] THEN
RULE_ASSUM_TAC(REWRITE_RULE[
facet_of]) THEN ASM_SIMP_TAC[] THEN
REWRITE_TAC[
DISJOINT; GSYM
MEMBER_NOT_EMPTY] THEN
EXISTS_TAC `x:real^N` THEN ASM_REWRITE_TAC[
IN_INTER;
IN_ELIM_THM];
ALL_TAC] THEN
SUBGOAL_THEN `c
face_of (s
INTER {x:real^N | a(i:real^N->bool)
dot x = b i})`
ASSUME_TAC THENL
[MP_TAC(ISPECL [`c:real^N->bool`; `s:real^N->bool`;
`s
INTER {x:real^N | a(i:real^N->bool)
dot x = b i}`]
FACE_OF_FACE) THEN
RULE_ASSUM_TAC(REWRITE_RULE[
facet_of]) THEN ASM_SIMP_TAC[];
ALL_TAC] THEN
MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
SUBGOAL_THEN
`
aff_dim(c:real^N->bool) <
aff_dim(s
INTER {x:real^N | a(i:real^N->bool)
dot x = b i})`
MP_TAC THENL
[MATCH_MP_TAC
FACE_OF_AFF_DIM_LT THEN
ASM_SIMP_TAC[
CONVEX_INTER;
CONVEX_HYPERPLANE];
RULE_ASSUM_TAC(REWRITE_RULE[
facet_of]) THEN ASM_SIMP_TAC[
INT_LT_REFL]]);;
(* ------------------------------------------------------------------------- *)
(* More general corollaries from the explicit representation. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* A characterization of polyhedra as having finitely many faces. *)
(* ------------------------------------------------------------------------- *)
add_translation_invariants [POLYHEDRON_TRANSLATION_EQ];;
add_linear_invariants [POLYHEDRON_LINEAR_IMAGE_EQ];;
(* ------------------------------------------------------------------------- *)
(* Relation between polytopes and polyhedra. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Polytope is union of convex hulls of facets plus any point inside. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Finitely generated cone is polyhedral, and hence closed. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* And conversely, a polyhedral cone is finitely generated. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Decomposition of polyhedron into cone plus polytope and more corollaries. *)
(* ------------------------------------------------------------------------- *)
let POLYHEDRON_AS_CONE_PLUS_CONV = prove
(`!s:real^N->bool.
polyhedron s <=> ?t u. FINITE t /\ FINITE u /\
s = {x + y | x
IN convex_cone hull t /\
y
IN convex hull u}`,
REPEAT GEN_TAC THEN EQ_TAC THENL
[REWRITE_TAC[
polyhedron;
LEFT_IMP_EXISTS_THM];
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
POLYHEDRON_POLYTOPE_SUMS THEN
ASM_SIMP_TAC[
POLYTOPE_CONVEX_HULL;
POLYHEDRON_CONVEX_CONE_HULL]] THEN
REWRITE_TAC[
polyhedron;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `f:(real^N->bool)->bool` THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) MP_TAC) THEN
GEN_REWRITE_TAC (LAND_CONV o REDEPTH_CONV) [
RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[
SKOLEM_THM;
LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC
[`a:(real^N->bool)->real^N`; `b:(real^N->bool)->
real`] THEN
ONCE_REWRITE_TAC[MESON[] `h = {x | P x} <=> {x | P x} = h`] THEN
DISCH_TAC THEN
ABBREV_TAC
`s':real^(N,1)finite_sum->bool =
{x | &0 <=
drop(
sndcart x) /\
!h:real^N->bool.
h
IN f ==> a h
dot (
fstcart x) <= b h *
drop(
sndcart x)}` THEN
SUBGOAL_THEN
`?t u. FINITE t /\ FINITE u /\
(!y:real^(N,1)finite_sum. y
IN t ==>
drop(
sndcart y) = &0) /\
(!y. y
IN u ==>
drop(
sndcart y) = &1) /\
s' =
convex_cone hull (t
UNION u)`
STRIP_ASSUME_TAC THENL
[MP_TAC(ISPEC `s':real^(N,1)finite_sum->bool`
FINITELY_GENERATED_CONIC_POLYHEDRON) THEN
ANTS_TAC THENL
[EXPAND_TAC "s'" THEN REPEAT CONJ_TAC THENL
[REWRITE_TAC[
polyhedron] THEN
EXISTS_TAC
`{ x:real^(N,1)finite_sum |
pastecart (
vec 0) (--vec 1)
dot x <= &0}
INSERT
{ {x |
pastecart (a h) (--lift(b h))
dot x <= &0} |
(h:real^N->bool)
IN f}` THEN
REWRITE_TAC[
FINITE_INSERT;
INTERS_INSERT;
SIMPLE_IMAGE] THEN
ASM_SIMP_TAC[
FINITE_IMAGE;
FORALL_IN_INSERT;
FORALL_IN_IMAGE] THEN
REPEAT CONJ_TAC THENL
[EXPAND_TAC "s'" THEN
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM;
FORALL_PASTECART;
IN_INTER;
DOT_PASTECART;
INTERS_IMAGE;
FSTCART_PASTECART;
SNDCART_PASTECART;
DOT_1; GSYM
drop;
DROP_NEG;
LIFT_DROP] THEN
REWRITE_TAC[
DROP_VEC;
DOT_LZERO;
REAL_MUL_LNEG; GSYM
real_sub] THEN
REWRITE_TAC[REAL_MUL_LID; REAL_ARITH `x - y <= &0 <=> x <= y`];
EXISTS_TAC `
pastecart (
vec 0) (--vec 1):real^(N,1)finite_sum` THEN
EXISTS_TAC `&0` THEN
REWRITE_TAC[
PASTECART_EQ_VEC;
VECTOR_NEG_EQ_0;
VEC_EQ] THEN
ARITH_TAC;
X_GEN_TAC `h:real^N->bool` THEN DISCH_TAC THEN MAP_EVERY EXISTS_TAC
[`
pastecart (a(h:real^N->bool)) (--lift(b h)):real^(N,1)finite_sum`;
`&0`] THEN
ASM_SIMP_TAC[
PASTECART_EQ_VEC]];
REWRITE_TAC[
conic;
IN_ELIM_THM;
FSTCART_CMUL;
SNDCART_CMUL] THEN
SIMP_TAC[
DROP_CMUL;
DOT_RMUL;
REAL_LE_MUL] THEN
MESON_TAC[
REAL_LE_LMUL;
REAL_MUL_AC];
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY] THEN
EXISTS_TAC `
vec 0:real^(N,1)finite_sum` THEN
REWRITE_TAC[
IN_ELIM_THM;
FSTCART_VEC;
SNDCART_VEC] THEN
REWRITE_TAC[
DROP_VEC;
DOT_RZERO;
REAL_LE_REFL;
REAL_MUL_RZERO]];
DISCH_THEN(X_CHOOSE_THEN `c:real^(N,1)finite_sum->bool`
STRIP_ASSUME_TAC) THEN
MAP_EVERY EXISTS_TAC
[`{x:real^(N,1)finite_sum | x
IN c /\
drop(
sndcart x) = &0}`;
`
IMAGE (\x. inv(
drop(
sndcart x)) % x)
{x:real^(N,1)finite_sum | x
IN c /\ ~(
drop(
sndcart x) = &0)}`] THEN
ASM_SIMP_TAC[
FINITE_IMAGE;
FINITE_RESTRICT;
FORALL_IN_IMAGE] THEN
SIMP_TAC[
IN_ELIM_THM;
SNDCART_CMUL;
DROP_CMUL; REAL_MUL_LINV] THEN
SUBGOAL_THEN
`!x:real^(N,1)finite_sum. x
IN c ==> &0 <=
drop(
sndcart x)`
ASSUME_TAC THENL
[GEN_TAC THEN DISCH_TAC THEN
SUBGOAL_THEN `(x:real^(N,1)finite_sum)
IN s'` MP_TAC THENL
[ASM_MESON_TAC[
HULL_INC]; EXPAND_TAC "s'"] THEN
SIMP_TAC[
IN_ELIM_THM];
ALL_TAC] THEN
MATCH_MP_TAC
SUBSET_ANTISYM THEN CONJ_TAC THEN
MATCH_MP_TAC
HULL_MINIMAL THEN
REWRITE_TAC[
CONVEX_CONE_CONVEX_CONE_HULL;
UNION_SUBSET] THEN
SIMP_TAC[
SUBSET;
IN_ELIM_THM;
HULL_INC;
FORALL_IN_IMAGE] THEN
X_GEN_TAC `x:real^(N,1)finite_sum` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:real^(N,1)finite_sum`) THEN
ASM_SIMP_TAC[
CONVEX_CONE_HULL_MUL;
HULL_INC;
REAL_LE_INV_EQ] THEN
ASM_REWRITE_TAC[REAL_ARITH `&0 <= x <=> x = &0 \/ &0 < x`] THEN
STRIP_TAC THENL
[MATCH_MP_TAC
HULL_INC THEN ASM_REWRITE_TAC[
IN_UNION;
IN_ELIM_THM];
SUBGOAL_THEN
`x:real^(N,1)finite_sum =
drop(
sndcart x) % inv(
drop(
sndcart x)) % x`
SUBST1_TAC THENL
[ASM_SIMP_TAC[
VECTOR_MUL_ASSOC;
REAL_MUL_RINV;
REAL_LT_IMP_NZ] THEN
REWRITE_TAC[
VECTOR_MUL_LID];
MATCH_MP_TAC
CONVEX_CONE_HULL_MUL THEN
ASM_SIMP_TAC[
REAL_LT_IMP_LE] THEN MATCH_MP_TAC
HULL_INC THEN
REWRITE_TAC[
IN_UNION] THEN DISJ2_TAC THEN
REWRITE_TAC[
IN_IMAGE] THEN EXISTS_TAC `x:real^(N,1)finite_sum` THEN
ASM_SIMP_TAC[
IN_ELIM_THM;
REAL_LT_IMP_NZ]]]];
EXISTS_TAC `
IMAGE fstcart (t:real^(N,1)finite_sum->bool)` THEN
EXISTS_TAC `
IMAGE fstcart (u:real^(N,1)finite_sum->bool)` THEN
ASM_SIMP_TAC[
FINITE_IMAGE] THEN
SUBGOAL_THEN `s = {x:real^N |
pastecart x (
vec 1:real^1)
IN s'}`
SUBST1_TAC THENL
[MAP_EVERY EXPAND_TAC ["s";
"s'"] THEN
REWRITE_TAC[IN_ELIM_THM; SNDCART_PASTECART; DROP_VEC; REAL_POS] THEN
GEN_REWRITE_TAC I [EXTENSION] THEN
REWRITE_TAC[FSTCART_PASTECART; IN_ELIM_THM; IN_INTERS; REAL_MUL_RID] THEN
ASM SET_TAC[];
ASM_REWRITE_TAC[CONVEX_CONE_HULL_UNION]] THEN
REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN X_GEN_TAC `z:real^N` THEN
SIMP_TAC[CONVEX_CONE_HULL_LINEAR_IMAGE; CONVEX_HULL_LINEAR_IMAGE;
LINEAR_FSTCART] THEN
REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM] THEN
REWRITE_TAC[EXISTS_IN_IMAGE] THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
X_GEN_TAC `a:real^(N,1)finite_sum` THEN REWRITE_TAC[] THEN
MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`) THEN
DISCH_TAC THEN AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
X_GEN_TAC `b:real^(N,1)finite_sum` THEN REWRITE_TAC[PASTECART_EQ] THEN
REWRITE_TAC[FSTCART_PASTECART; SNDCART_PASTECART; FSTCART_ADD;
SNDCART_ADD] THEN
ASM_CASES_TAC `fstcart(a:real^(N,1)finite_sum) +
fstcart(b:real^(N,1)finite_sum) = z` THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `sndcart(a:real^(N,1)finite_sum) = vec 0` SUBST1_TAC THENL
[UNDISCH_TAC `(a:real^(N,1)finite_sum) IN convex_cone hull t` THEN
SPEC_TAC(`a:real^(N,1)finite_sum`,`a:real^(N,1)finite_sum`) THEN
MATCH_MP_TAC HULL_INDUCT THEN ASM_SIMP_TAC[GSYM DROP_EQ; DROP_VEC] THEN
REWRITE_TAC[convex_cone; convex; conic; IN_ELIM_THM] THEN
SIMP_TAC[SNDCART_ADD; SNDCART_CMUL; DROP_ADD; DROP_CMUL] THEN
REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_RID; GSYM MEMBER_NOT_EMPTY] THEN
EXISTS_TAC `vec 0:real^(N,1)finite_sum` THEN
REWRITE_TAC[IN_ELIM_THM; SNDCART_VEC; DROP_VEC];
REWRITE_TAC[VECTOR_ADD_LID]] THEN
ASM_CASES_TAC `u:real^(N,1)finite_sum->bool = {}` THENL
[ASM_REWRITE_TAC[CONVEX_CONE_HULL_EMPTY; CONVEX_HULL_EMPTY] THEN
REWRITE_TAC[IN_SING; NOT_IN_EMPTY] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
ASM_REWRITE_TAC[SNDCART_VEC; VEC_EQ] THEN ARITH_TAC;
ALL_TAC] THEN
ASM_SIMP_TAC[CONVEX_CONE_HULL_CONVEX_HULL_NONEMPTY; IN_ELIM_THM] THEN
SUBGOAL_THEN
`!y:real^(N,1)finite_sum. y IN convex hull u ==> sndcart y = vec 1`
(LABEL_TAC "*")
THENL
[MATCH_MP_TAC HULL_INDUCT THEN ASM_SIMP_TAC[GSYM DROP_EQ; DROP_VEC] THEN
REWRITE_TAC[convex; IN_ELIM_THM] THEN
SIMP_TAC[SNDCART_ADD; SNDCART_CMUL; DROP_ADD; DROP_CMUL] THEN
SIMP_TAC[REAL_MUL_RID];
ALL_TAC] THEN
EQ_TAC THEN REWRITE_TAC[LEFT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THENL
[MAP_EVERY X_GEN_TAC [`c:real`; `d:real^(N,1)finite_sum`] THEN
DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
ASM_SIMP_TAC[SNDCART_CMUL; VECTOR_MUL_EQ_0; VECTOR_ARITH
`x:real^N = c % x <=> (c - &1) % x = vec 0`] THEN
ASM_SIMP_TAC[REAL_SUB_0; VEC_EQ; ARITH_EQ; VECTOR_MUL_LID];
DISCH_TAC THEN ASM_SIMP_TAC[] THEN EXISTS_TAC `&1` THEN
ASM_REWRITE_TAC[REAL_POS; VECTOR_MUL_LID] THEN ASM_MESON_TAC[]]]);;
(* ------------------------------------------------------------------------- *)
(* Farkas's lemma (2 variants) and stronger separation for polyhedra. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Relative and absolute frontier of a polytope. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Special case of a triangle. *)
(* ------------------------------------------------------------------------- *)
let RELATIVE_BOUNDARY_OF_TRIANGLE = prove
(`!a b c:real^N.
~collinear {a,b,c}
==>
convex hull {a,b,c}
DIFF relative_interior(
convex hull {a,b,c}) =
segment[a,b]
UNION segment[b,c]
UNION segment[c,a]`,
(* ------------------------------------------------------------------------- *)
(* A ridge is the intersection of precisely two facets. *)
(* ------------------------------------------------------------------------- *)
let POLYHEDRON_RIDGE_TWO_FACETS = prove
(`!p:real^N->bool r.
polyhedron p /\ r
face_of p /\ ~(r = {}) /\
aff_dim r =
aff_dim p - &2
==> ?f1 f2. f1
face_of p /\
aff_dim f1 =
aff_dim p - &1 /\
f2
face_of p /\
aff_dim f2 =
aff_dim p - &1 /\
~(f1 = f2) /\ r
SUBSET f1 /\ r
SUBSET f2 /\ f1
INTER f2 = r /\
!f. f
face_of p /\
aff_dim f =
aff_dim p - &1 /\ r
SUBSET f
==> f = f1 \/ f = f2`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL [`p:real^N->bool`; `r:real^N->bool`]
FACE_OF_POLYHEDRON) THEN
ANTS_TAC THENL [ASM_MESON_TAC[INT_ARITH `~(p:int = p - &2)`]; ALL_TAC] THEN
SUBGOAL_THEN `&2 <=
aff_dim(p:real^N->bool)` ASSUME_TAC THENL
[MP_TAC(ISPEC `r:real^N->bool`
AFF_DIM_GE) THEN
MP_TAC(ISPEC `r:real^N->bool`
AFF_DIM_EQ_MINUS1) THEN
ASM_REWRITE_TAC[] THEN INT_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN
`{f:real^N->bool | f
facet_of p /\ r
SUBSET f} =
{f | f
face_of p /\
aff_dim f =
aff_dim p - &1 /\ r
SUBSET f}`
SUBST1_TAC THENL
[GEN_REWRITE_TAC I [
EXTENSION] THEN
ASM_REWRITE_TAC[
IN_ELIM_THM;
facet_of] THEN
X_GEN_TAC `f:real^N->bool` THEN
ASM_CASES_TAC `f:real^N->bool = {}` THEN
ASM_REWRITE_TAC[
AFF_DIM_EMPTY; GSYM
CONJ_ASSOC] THEN ASM_INT_ARITH_TAC;
DISCH_THEN(MP_TAC o SYM)] THEN
ASM_CASES_TAC
`{f:real^N->bool | f
face_of p /\
aff_dim f =
aff_dim p - &1 /\ r
SUBSET f}
= {}`
THENL
[ASM_REWRITE_TAC[
INTERS_0] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
UNDISCH_TAC `
aff_dim(r:real^N->bool) =
aff_dim(p:real^N->bool) - &2` THEN
ASM_REWRITE_TAC[
AFF_DIM_UNIV; DIMINDEX_3] THEN
MP_TAC(ISPEC `p:real^N->bool`
AFF_DIM_LE_UNIV) THEN INT_ARITH_TAC;
ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM;
IN_ELIM_THM] THEN
X_GEN_TAC `f1:real^N->bool` THEN STRIP_TAC THEN
ASM_CASES_TAC
`{f:real^N->bool | f
face_of p /\
aff_dim f =
aff_dim p - &1 /\ r
SUBSET f}
= {f1}`
THENL
[ASM_REWRITE_TAC[
INTERS_1] THEN
ASM_MESON_TAC[INT_ARITH `~(x - &2:int = x - &1)`];
ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o MATCH_MP (SET_RULE
`~(s = {a}) ==> a
IN s ==> ?b. ~(b = a) /\ b
IN s`)) THEN
ASM_REWRITE_TAC[
IN_ELIM_THM;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `f2:real^N->bool` THEN STRIP_TAC THEN
ASM_CASES_TAC
`{f:real^N->bool | f
face_of p /\
aff_dim f =
aff_dim p - &1 /\ r
SUBSET f}
= {f1,f2}`
THENL
[ASM_REWRITE_TAC[
INTERS_2] THEN DISCH_TAC THEN
MAP_EVERY EXISTS_TAC [`f1:real^N->bool`; `f2:real^N->bool`] THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o MATCH_MP (SET_RULE
`~(s = {a,b})
==> a
IN s /\ b
IN s ==> ?c. ~(c = a) /\ ~(c = b) /\ c
IN s`)) THEN
ASM_REWRITE_TAC[
IN_ELIM_THM;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `f3:real^N->bool` THEN STRIP_TAC THEN DISCH_TAC THEN
UNDISCH_TAC `
aff_dim(r:real^N->bool) =
aff_dim(p:real^N->bool) - &2` THEN
MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
MATCH_MP_TAC(INT_ARITH `~(p - &2:int <= x:int) ==> ~(x = p - &2)`) THEN
DISCH_TAC THEN SUBGOAL_THEN
`~(f1:real^N->bool = {}) /\
~(f2:real^N->bool = {}) /\
~(f3:real^N->bool = {})`
STRIP_ASSUME_TAC THENL
[REPEAT CONJ_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN
RULE_ASSUM_TAC(REWRITE_RULE[
AFF_DIM_EMPTY]) THEN ASM_INT_ARITH_TAC;
ALL_TAC] THEN
MP_TAC(ISPEC `p:real^N->bool`
POLYHEDRON_INTER_AFFINE_PARALLEL_MINIMAL) THEN
REWRITE_TAC[
RIGHT_IMP_EXISTS_THM;
SKOLEM_THM] THEN
REWRITE_TAC[
RIGHT_AND_EXISTS_THM;
LEFT_AND_EXISTS_THM] THEN
ASM_REWRITE_TAC[
NOT_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC
[`f:(real^N->bool)->bool`; `a:(real^N->bool)->real^N`;
`b:(real^N->bool)->
real`] THEN
ONCE_REWRITE_TAC[
EQ_SYM_EQ] THEN
REWRITE_TAC[VECTOR_ARITH `
vec 0:real^N = v <=> v =
vec 0`] THEN
STRIP_TAC THEN MP_TAC(ISPECL
[`p:real^N->bool`; `f:(real^N->bool)->bool`; `a:(real^N->bool)->real^N`;
`b:(real^N->bool)->
real`]
FACET_OF_POLYHEDRON_EXPLICIT) THEN
ASM_SIMP_TAC[] THEN DISCH_THEN(fun
th ->
MP_TAC(SPEC `f1:real^N->bool`
th) THEN
MP_TAC(SPEC `f2:real^N->bool`
th) THEN
MP_TAC(SPEC `f3:real^N->bool`
th)) THEN
ASM_REWRITE_TAC[
facet_of] THEN
DISCH_THEN(X_CHOOSE_THEN `h3:real^N->bool` (STRIP_ASSUME_TAC o GSYM)) THEN
DISCH_THEN(X_CHOOSE_THEN `h2:real^N->bool` (STRIP_ASSUME_TAC o GSYM)) THEN
DISCH_THEN(X_CHOOSE_THEN `h1:real^N->bool` (STRIP_ASSUME_TAC o GSYM)) THEN
SUBGOAL_THEN `~((a:(real^N->bool)->real^N) h1 = a h2) /\
~(a h2 = a h3) /\ ~(a h1 = a h3)`
STRIP_ASSUME_TAC THENL
[REPEAT CONJ_TAC THENL
[DISJ_CASES_TAC(REAL_ARITH
`b(h1:real^N->bool) <= b h2 \/ b h2 <= b h1`)
THENL
[FIRST_X_ASSUM(MP_TAC o SPEC `f
DELETE (h2:real^N->bool)`);
FIRST_X_ASSUM(MP_TAC o SPEC `f
DELETE (h1:real^N->bool)`)] THEN
(ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC(SET_RULE `(p ==> s = t) ==> s
PSUBSET t ==> ~p`) THEN
DISCH_TAC THEN
FIRST_X_ASSUM(fun
th -> GEN_REWRITE_TAC LAND_CONV [SYM
th]) THEN
AP_TERM_TAC)
THENL
[SUBGOAL_THEN `f
DELETE h2 = h1
INSERT (f
DIFF {h1,h2}) /\
f = (h2:real^N->bool)
INSERT h1
INSERT (f
DIFF {h1,h2})`
(fun
th -> ONCE_REWRITE_TAC[
th]) THENL [ASM SET_TAC[]; ALL_TAC];
SUBGOAL_THEN `f
DELETE h1 = h2
INSERT (f
DIFF {h1,h2}) /\
f = (h1:real^N->bool)
INSERT h2
INSERT (f
DIFF {h1,h2})`
(fun
th -> ONCE_REWRITE_TAC[
th]) THENL [ASM SET_TAC[]; ALL_TAC]] THEN
REWRITE_TAC[
INTERS_INSERT] THEN MATCH_MP_TAC(SET_RULE
`b
SUBSET a ==> a
INTER b
INTER s = b
INTER s`) THEN
FIRST_X_ASSUM(fun
th ->
MP_TAC(SPEC `h1:real^N->bool`
th) THEN
MP_TAC(SPEC `h2:real^N->bool`
th)) THEN
ASM_REWRITE_TAC[IMP_IMP] THEN
DISCH_THEN(fun
th -> ONCE_REWRITE_TAC[GSYM
th]) THEN
REWRITE_TAC[
SUBSET;
IN_ELIM_THM] THEN ASM_REAL_ARITH_TAC;
DISJ_CASES_TAC(REAL_ARITH
`b(h2:real^N->bool) <= b h3 \/ b h3 <= b h2`)
THENL
[FIRST_X_ASSUM(MP_TAC o SPEC `f
DELETE (h3:real^N->bool)`);
FIRST_X_ASSUM(MP_TAC o SPEC `f
DELETE (h2:real^N->bool)`)] THEN
(ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC(SET_RULE `(p ==> s = t) ==> s
PSUBSET t ==> ~p`) THEN
DISCH_TAC THEN
FIRST_X_ASSUM(fun
th -> GEN_REWRITE_TAC LAND_CONV [SYM
th]) THEN
AP_TERM_TAC)
THENL
[SUBGOAL_THEN `f
DELETE h3 = h2
INSERT (f
DIFF {h2,h3}) /\
f = (h3:real^N->bool)
INSERT h2
INSERT (f
DIFF {h2,h3})`
(fun
th -> ONCE_REWRITE_TAC[
th]) THENL [ASM SET_TAC[]; ALL_TAC];
SUBGOAL_THEN `f
DELETE h2 = h3
INSERT (f
DIFF {h2,h3}) /\
f = (h2:real^N->bool)
INSERT h3
INSERT (f
DIFF {h2,h3})`
(fun
th -> ONCE_REWRITE_TAC[
th]) THENL [ASM SET_TAC[]; ALL_TAC]] THEN
REWRITE_TAC[
INTERS_INSERT] THEN MATCH_MP_TAC(SET_RULE
`b
SUBSET a ==> a
INTER b
INTER s = b
INTER s`) THEN
FIRST_X_ASSUM(fun
th ->
MP_TAC(SPEC `h2:real^N->bool`
th) THEN
MP_TAC(SPEC `h3:real^N->bool`
th)) THEN
ASM_REWRITE_TAC[IMP_IMP] THEN
DISCH_THEN(fun
th -> ONCE_REWRITE_TAC[GSYM
th]) THEN
REWRITE_TAC[
SUBSET;
IN_ELIM_THM] THEN ASM_REAL_ARITH_TAC;
DISJ_CASES_TAC(REAL_ARITH
`b(h1:real^N->bool) <= b h3 \/ b h3 <= b h1`)
THENL
[FIRST_X_ASSUM(MP_TAC o SPEC `f
DELETE (h3:real^N->bool)`);
FIRST_X_ASSUM(MP_TAC o SPEC `f
DELETE (h1:real^N->bool)`)] THEN
(ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC(SET_RULE `(p ==> s = t) ==> s
PSUBSET t ==> ~p`) THEN
DISCH_TAC THEN
FIRST_X_ASSUM(fun
th -> GEN_REWRITE_TAC LAND_CONV [SYM
th]) THEN
AP_TERM_TAC)
THENL
[SUBGOAL_THEN `f
DELETE h3 = h1
INSERT (f
DIFF {h1,h3}) /\
f = (h3:real^N->bool)
INSERT h1
INSERT (f
DIFF {h1,h3})`
(fun
th -> ONCE_REWRITE_TAC[
th]) THENL [ASM SET_TAC[]; ALL_TAC];
SUBGOAL_THEN `f
DELETE h1 = h3
INSERT (f
DIFF {h1,h3}) /\
f = (h1:real^N->bool)
INSERT h3
INSERT (f
DIFF {h1,h3})`
(fun
th -> ONCE_REWRITE_TAC[
th]) THENL [ASM SET_TAC[]; ALL_TAC]] THEN
REWRITE_TAC[
INTERS_INSERT] THEN MATCH_MP_TAC(SET_RULE
`b
SUBSET a ==> a
INTER b
INTER s = b
INTER s`) THEN
FIRST_X_ASSUM(fun
th ->
MP_TAC(SPEC `h1:real^N->bool`
th) THEN
MP_TAC(SPEC `h3:real^N->bool`
th)) THEN
ASM_REWRITE_TAC[IMP_IMP] THEN
DISCH_THEN(fun
th -> ONCE_REWRITE_TAC[GSYM
th]) THEN
REWRITE_TAC[
SUBSET;
IN_ELIM_THM] THEN ASM_REAL_ARITH_TAC];
ALL_TAC] THEN
SUBGOAL_THEN
`~({x | a h1
dot x <= b h1}
INTER {x | a h2
dot x <= b h2}
SUBSET {x | a h3
dot x <= b h3}) /\
~({x | a h1
dot x <= b h1}
INTER {x | a h3
dot x <= b h3}
SUBSET {x | a h2
dot x <= b h2}) /\
~({x | a h2
dot x <= b h2}
INTER {x | a h3
dot x <= b h3}
SUBSET {x:real^N | a(h1:real^N->bool)
dot x <= b h1})`
MP_TAC THENL
[ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THENL
[FIRST_X_ASSUM(MP_TAC o SPEC `f
DELETE (h3:real^N->bool)`);
FIRST_X_ASSUM(MP_TAC o SPEC `f
DELETE (h2:real^N->bool)`);
FIRST_X_ASSUM(MP_TAC o SPEC `f
DELETE (h1:real^N->bool)`)] THEN
(ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
FIRST_X_ASSUM(fun
th -> GEN_REWRITE_TAC
(LAND_CONV o LAND_CONV) [SYM
th]) THEN
MATCH_MP_TAC(SET_RULE `s = t ==> s
PSUBSET t ==> F`) THEN
AP_TERM_TAC)
THENL
[SUBGOAL_THEN
`f
DELETE (h3:real^N->bool) = h1
INSERT h2
INSERT (f
DELETE h3) /\
f = h1
INSERT h2
INSERT h3
INSERT (f
DELETE h3)`
(fun
th -> ONCE_REWRITE_TAC[
th]) THENL [ASM SET_TAC[]; ALL_TAC];
SUBGOAL_THEN
`f
DELETE (h2:real^N->bool) = h1
INSERT h3
INSERT (f
DELETE h2) /\
f = h2
INSERT h1
INSERT h3
INSERT (f
DELETE h2)`
(fun
th -> ONCE_REWRITE_TAC[
th]) THENL [ASM SET_TAC[]; ALL_TAC];
SUBGOAL_THEN
`f
DELETE (h1:real^N->bool) = h2
INSERT h3
INSERT (f
DELETE h1) /\
f = h1
INSERT h2
INSERT h3
INSERT (f
DELETE h1)`
(fun
th -> ONCE_REWRITE_TAC[
th]) THENL [ASM SET_TAC[]; ALL_TAC]] THEN
REWRITE_TAC[
INTERS_INSERT] THEN REWRITE_TAC[GSYM
INTER_ASSOC] THEN
AP_THM_TAC THEN AP_TERM_TAC THEN ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`?w. (a:(real^N->bool)->real^N) h1
dot w < b h1 /\
a h2
dot w < b h2 /\ a h3
dot w < b h3`
(CHOOSE_THEN MP_TAC)
THENL
[SUBGOAL_THEN `~(
relative_interior p :real^N->bool = {})` MP_TAC THENL
[ASM_SIMP_TAC[
RELATIVE_INTERIOR_EQ_EMPTY;
POLYHEDRON_IMP_CONVEX] THEN
ASM SET_TAC[];
ALL_TAC] THEN
MP_TAC(ISPECL
[`p:real^N->bool`; `f:(real^N->bool)->bool`; `a:(real^N->bool)->real^N`;
`b:(real^N->bool)->
real`]
RELATIVE_INTERIOR_POLYHEDRON_EXPLICIT) THEN
ASM_SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC) THEN
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY;
IN_ELIM_THM] THEN
MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC THEN
DISCH_THEN(MP_TAC o CONJUNCT2) THEN ASM_SIMP_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`!x. x
IN r ==> (a h1)
dot (x:real^N) = b h1 /\
(a h2)
dot x = b h2 /\
(a (h3:real^N->bool))
dot x = b h3`
MP_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `?z:real^N. z
IN r` CHOOSE_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
MAP_EVERY UNDISCH_TAC
[`~((a:(real^N->bool)->real^N) h1 = a h2)`;
`~((a:(real^N->bool)->real^N) h1 = a h3)`;
`~((a:(real^N->bool)->real^N) h2 = a h3)`;
`
aff_dim(p:real^N->bool) - &2 <=
aff_dim(r:real^N->bool)`] THEN
MAP_EVERY (fun t ->
FIRST_X_ASSUM(fun
th -> MP_TAC(SPEC t
th) THEN ASM_REWRITE_TAC[] THEN
ASSUME_TAC
th) THEN
DISCH_THEN(MP_TAC o SPEC `z:real^N` o CONJUNCT2 o CONJUNCT2))
[`h1:real^N->bool`; `h2:real^N->bool`; `h3:real^N->bool`] THEN
SUBGOAL_THEN `(z:real^N)
IN (
affine hull p)` ASSUME_TAC THENL
[MATCH_MP_TAC
HULL_INC THEN ASM SET_TAC[];
ASM_REWRITE_TAC[]] THEN
UNDISCH_TAC `(z:real^N)
IN (
affine hull p)` THEN
SUBGOAL_THEN `(a h1)
dot (z:real^N) = b h1 /\
(a h2)
dot z = b h2 /\
(a (h3:real^N->bool))
dot z = b h3`
(REPEAT_TCL CONJUNCTS_THEN (SUBST1_TAC o SYM))
THENL [ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `(r:real^N->bool)
SUBSET affine hull p` MP_TAC THENL
[ASM_MESON_TAC[
FACE_OF_IMP_SUBSET;
HULL_SUBSET;
SUBSET_TRANS]; ALL_TAC] THEN
SUBGOAL_THEN
`~((a:(real^N->bool)->real^N) h1 =
vec 0) /\
~((a:(real^N->bool)->real^N) h2 =
vec 0) /\
~((a:(real^N->bool)->real^N) h3 =
vec 0)`
MP_TAC THENL [ASM_SIMP_TAC[]; ALL_TAC] THEN
UNDISCH_TAC `(z:real^N)
IN r` THEN POP_ASSUM_LIST(K ALL_TAC) THEN
MAP_EVERY SPEC_TAC
[`(a:(real^N->bool)->real^N) h1`,`a1:real^N`;
`(a:(real^N->bool)->real^N) h2`,`a2:real^N`;
`(a:(real^N->bool)->real^N) h3`,`a3:real^N`] THEN
REPEAT GEN_TAC THEN
GEN_GEOM_ORIGIN_TAC `z:real^N` ["a1";
"a2"; "a3"] THEN
REWRITE_TAC[VECTOR_ADD_RID; VECTOR_ADD_LID] THEN
REWRITE_TAC[DOT_RADD; IMAGE_CLAUSES;
REAL_ARITH `a + b:real <= a <=> b <= &0`;
REAL_ARITH `a + b:real < a <=> b < &0`;
REAL_ARITH `a + b:real = a <=> b = &0`] THEN
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `aff_dim(p:real^N->bool) = &(dim p)` SUBST_ALL_TAC THENL
[ASM_SIMP_TAC[AFF_DIM_DIM_0; HULL_INC]; ALL_TAC] THEN
SUBGOAL_THEN `aff_dim(r:real^N->bool) = &(dim r)` SUBST_ALL_TAC THENL
[ASM_SIMP_TAC[AFF_DIM_DIM_0; HULL_INC]; ALL_TAC] THEN
RULE_ASSUM_TAC(REWRITE_RULE[INT_OF_NUM_ADD; INT_OF_NUM_LE;
INT_ARITH `p - &2:int <= q <=> p <= q + &2`]) THEN
MP_TAC(ISPECL
[`{a1:real^N,a2,a3}`; `r:real^N->bool`] DIM_ORTHOGONAL_SUM) THEN
REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
ASM_SIMP_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
`p <= r + 2 ==> u <= p /\ 3 <= t ==> ~(u = t + r)`)) THEN
SUBGOAL_THEN `affine hull p :real^N->bool = span p` SUBST_ALL_TAC THENL
[ASM_MESON_TAC[AFFINE_HULL_EQ_SPAN]; ALL_TAC] THEN
CONJ_TAC THENL
[GEN_REWRITE_TAC RAND_CONV [GSYM DIM_SPAN] THEN
MATCH_MP_TAC DIM_SUBSET THEN ASM SET_TAC[];
ALL_TAC] THEN
MP_TAC(ISPEC `{a1:real^N,a2,a3}` DEPENDENT_BIGGERSET_GENERAL) THEN
SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY; ARITH] THEN
ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM CONTRAPOS_THM] THEN
REWRITE_TAC[ARITH_RULE `~(3 > x) <=> 3 <= x`] THEN
DISCH_THEN MATCH_MP_TAC THEN
REWRITE_TAC[dependent; EXISTS_IN_INSERT; NOT_IN_EMPTY] THEN
ASM_REWRITE_TAC[DELETE_INSERT; EMPTY_DELETE] THEN
REWRITE_TAC[SPAN_2; IN_ELIM_THM; IN_UNIV] THEN
POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o rev) THEN
W(fun (asl,w) -> let fv = frees w
and av = [`a1:real^N`; `a2:real^N`; `a3:real^N`] in
MAP_EVERY (fun t -> SPEC_TAC(t,t)) (subtract fv av @ av)) THEN
REWRITE_TAC[LEFT_FORALL_IMP_THM] THEN
MATCH_MP_TAC(MESON[]
`(!a1 a2 a3. P a1 a2 a3 ==> P a2 a1 a3 /\ P a3 a1 a2) /\
(!a1 a2 a3. Q a1 a2 a3 ==> ~(P a1 a2 a3))
==> !a3 a2 a1. P a1 a2 a3
==> ~(Q a1 a2 a3 \/ Q a2 a1 a3 \/ Q a3 a1 a2)`) THEN
CONJ_TAC THENL
[REPEAT GEN_TAC THEN MATCH_MP_TAC(TAUT
`(p ==> q) /\ (p ==> r) ==> p ==> q /\ r`) THEN
CONJ_TAC THEN REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
REWRITE_TAC[CONJ_ACI] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
ASM SET_TAC[];
ALL_TAC] THEN
REPEAT GEN_TAC THEN DISCH_THEN
(X_CHOOSE_THEN `u:real` (X_CHOOSE_TAC `v:real`)) THEN
REWRITE_TAC[NOT_EXISTS_THM] THEN REPEAT GEN_TAC THEN
ASM_CASES_TAC `u = &0` THENL
[ASM_REWRITE_TAC[VECTOR_ADD_LID; VECTOR_MUL_LZERO] THEN
REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (REAL_ARITH
`v = &0 \/ &0 < v \/ &0 < --v`)
THENL
[ASM_REWRITE_TAC[VECTOR_MUL_LZERO];
REWRITE_TAC[DOT_LMUL; REAL_ARITH `a * b <= &0 <=> &0 <= a * --b`] THEN
ASM_SIMP_TAC[REAL_LE_MUL_EQ] THEN
REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INTER] THEN REAL_ARITH_TAC;
REWRITE_TAC[DOT_LMUL; REAL_ARITH `a * b < &0 <=> &0 < --a * b`] THEN
ASM_SIMP_TAC[REAL_LT_MUL_EQ] THEN REAL_ARITH_TAC];
ALL_TAC] THEN
ASM_CASES_TAC `v = &0` THENL
[ASM_REWRITE_TAC[VECTOR_ADD_RID; VECTOR_MUL_LZERO] THEN
REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (REAL_ARITH
`u = &0 \/ &0 < u \/ &0 < --u`)
THENL
[ASM_REWRITE_TAC[VECTOR_MUL_LZERO];
REWRITE_TAC[DOT_LMUL; REAL_ARITH `a * b <= &0 <=> &0 <= a * --b`] THEN
ASM_SIMP_TAC[REAL_LE_MUL_EQ] THEN
REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INTER] THEN REAL_ARITH_TAC;
REWRITE_TAC[DOT_LMUL; REAL_ARITH `a * b < &0 <=> &0 < --a * b`] THEN
ASM_SIMP_TAC[REAL_LT_MUL_EQ] THEN REAL_ARITH_TAC];
ALL_TAC] THEN
STRIP_TAC THEN
SUBGOAL_THEN
`&0 < u /\ &0 < v \/ &0 < u /\ &0 < --v \/
&0 < --u /\ &0 < v \/ &0 < --u /\ &0 < --v`
STRIP_ASSUME_TAC THENL
[ASM_REAL_ARITH_TAC;
UNDISCH_TAC
`~({x | a2 dot x <= &0} INTER {x | a3 dot x <= &0} SUBSET
{x:real^N | a1 dot x <= &0})` THEN
ASM_REWRITE_TAC[SUBSET; IN_INTER; IN_ELIM_THM] THEN
REWRITE_TAC[DOT_LADD; DOT_LMUL] THEN
REWRITE_TAC[REAL_ARITH `x <= &0 <=> &0 <= --x`] THEN
REWRITE_TAC[REAL_NEG_ADD; GSYM REAL_MUL_RNEG] THEN
ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_ADD; REAL_LT_IMP_LE];
UNDISCH_TAC
`~({x | a1 dot x <= &0} INTER {x | a3 dot x <= &0} SUBSET
{x:real^N | a2 dot x <= &0})` THEN
ASM_REWRITE_TAC[SUBSET; IN_INTER; IN_ELIM_THM] THEN
GEN_TAC THEN REWRITE_TAC[DOT_LADD; DOT_LMUL] THEN
MATCH_MP_TAC(REAL_ARITH
`(&0 < u * a2 <=> &0 < a2) /\ (&0 < --v * a3 <=> &0 < a3)
==> u * a2 + v * a3 <= &0 /\ a3 <= &0 ==> a2 <= &0`) THEN
ASM_SIMP_TAC[REAL_LT_MUL_EQ];
UNDISCH_TAC
`~({x | a1 dot x <= &0} INTER {x | a2 dot x <= &0} SUBSET
{x:real^N | a3 dot x <= &0})` THEN
ASM_REWRITE_TAC[SUBSET; IN_INTER; IN_ELIM_THM] THEN
GEN_TAC THEN REWRITE_TAC[DOT_LADD; DOT_LMUL] THEN
MATCH_MP_TAC(REAL_ARITH
`(&0 < --u * a2 <=> &0 < a2) /\ (&0 < v * a3 <=> &0 < a3)
==> u * a2 + v * a3 <= &0 /\ a2 <= &0 ==> a3 <= &0`) THEN
ASM_SIMP_TAC[REAL_LT_MUL_EQ];
UNDISCH_TAC `(a1:real^N) dot w < &0` THEN
ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL] THEN
MATCH_MP_TAC(REAL_ARITH
`&0 < --u * --a /\ &0 < --v * --b ==> ~(u * a + v * b < &0)`) THEN
CONJ_TAC THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REAL_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Lower bounds on then number of 0 and n-1 dimensional faces. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* The notion of n-simplex where n is an integer >= -1. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("simplex",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Simplicial complexes and triangulations. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Subdividing a cell complex (not necessarily simplicial). *)
(* ------------------------------------------------------------------------- *)