(* ========================================================================= *)
(* 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_CONVEX_HULLS = prove
(`!f s:real^N->bool.
FINITE s /\ f
SUBSET s /\
DISJOINT (affine hull f) (convex hull (s
DIFF f))
==> (convex hull f)
face_of (convex hull s)`,
let lemma = prove
(`!s x y:real^N.
affine s /\ ~(k = &0) /\ ~(k = &1) /\ x IN s /\ inv(&1 - k) % y IN s
==> inv(k) % (x - y) IN s`,
REWRITE_TAC[AFFINE_ALT] THEN REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`inv(k) % (x - y):real^N = (&1 - inv k) % inv(&1 - k) % y + inv(k) % x`
(fun th -> ASM_SIMP_TAC[th]) THEN
REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_ARITH
`k % (x - y):real^N = a % b % y + k % x <=> (a * b + k) % y = vec 0`] THEN
DISJ1_TAC THEN MAP_EVERY UNDISCH_TAC [`~(k = &0)`; `~(k = &1)`] THEN
CONV_TAC REAL_FIELD) in
REPEAT STRIP_TAC THEN REWRITE_TAC[face_of] THEN
SUBGOAL_THEN `FINITE(f:real^N->bool)` ASSUME_TAC THENL
[ASM_MESON_TAC[FINITE_SUBSET]; ALL_TAC] THEN
FIRST_ASSUM(ASSUME_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
ASM_SIMP_TAC[HULL_MONO; CONVEX_CONVEX_HULL] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`; `w:real^N`] THEN
STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_SEGMENT]) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
(X_CHOOSE_THEN `u:real` STRIP_ASSUME_TAC)) THEN
SUBGOAL_THEN `(w:real^N) IN affine hull f` ASSUME_TAC THENL
[ASM_MESON_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL; SUBSET]; ALL_TAC] THEN
MAP_EVERY UNDISCH_TAC
[`(y:real^N) IN convex hull s`; `(x:real^N) IN convex hull s`] THEN
REWRITE_TAC[CONVEX_HULL_FINITE; IN_ELIM_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `a:real^N->real` STRIP_ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `b:real^N->real` STRIP_ASSUME_TAC) THEN
ABBREV_TAC `(c:real^N->real) = \x. (&1 - u) * a x + u * b x` THEN
SUBGOAL_THEN `!x:real^N. x IN s ==> &0 <= c x` ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN EXPAND_TAC "c" THEN REWRITE_TAC[] THEN
MATCH_MP_TAC REAL_LE_ADD THEN CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN
ASM_SIMP_TAC[] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
ASM_CASES_TAC `sum (s DIFF f:real^N->bool) c = &0` THENL
[SUBGOAL_THEN `!x:real^N. x IN (s DIFF f) ==> c x = &0` MP_TAC THENL
[MATCH_MP_TAC SUM_POS_EQ_0 THEN ASM_MESON_TAC[FINITE_DIFF; IN_DIFF];
ALL_TAC] THEN
EXPAND_TAC "c" THEN
ASM_SIMP_TAC[IN_DIFF; REAL_LE_MUL; REAL_LT_IMP_LE; REAL_SUB_LT;
REAL_ARITH `&0 <= x /\ &0 <= y ==> (x + y = &0 <=> x = &0 /\ y = &0)`;
REAL_ENTIRE; REAL_SUB_0; REAL_LT_IMP_NE] THEN
STRIP_TAC THEN CONJ_TAC THENL
[EXISTS_TAC `a:real^N->real`; EXISTS_TAC `b:real^N->real`] THEN
ASM_SIMP_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM(fun th g ->
(GEN_REWRITE_TAC RAND_CONV [GSYM th] THEN CONV_TAC SYM_CONV THEN
(MATCH_MP_TAC SUM_SUPERSET ORELSE MATCH_MP_TAC VSUM_SUPERSET)) g) THEN
ASM_SIMP_TAC[VECTOR_MUL_LZERO];
ALL_TAC] THEN
ABBREV_TAC `k = sum (s DIFF f:real^N->bool) c` THEN
SUBGOAL_THEN `&0 < k` ASSUME_TAC THENL
[ASM_REWRITE_TAC[REAL_LT_LE] THEN EXPAND_TAC "k" THEN
MATCH_MP_TAC SUM_POS_LE THEN ASM_SIMP_TAC[FINITE_DIFF; IN_DIFF];
ALL_TAC] THEN
ASM_CASES_TAC `k = &1` THENL
[FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_DISJOINT]) THEN
MATCH_MP_TAC(TAUT `b ==> ~b ==> c`) THEN
EXISTS_TAC `w:real^N` THEN
ASM_REWRITE_TAC[CONVEX_HULL_FINITE; IN_ELIM_THM] THEN
EXISTS_TAC `c:real^N->real` THEN
ASM_SIMP_TAC[IN_DIFF; SUM_DIFF; VSUM_DIFF] THEN
SUBGOAL_THEN `vsum f (\x:real^N. c x % x) = vec 0` SUBST1_TAC THENL
[ALL_TAC;
EXPAND_TAC "c" THEN REWRITE_TAC[VECTOR_ADD_RDISTRIB] THEN
ASM_SIMP_TAC[VSUM_ADD; GSYM VECTOR_MUL_ASSOC; VSUM_LMUL] THEN
REWRITE_TAC[VECTOR_SUB_RZERO]] THEN
SUBGOAL_THEN `sum(s DIFF f) c = sum s c - sum f (c:real^N->real)`
MP_TAC THENL [ASM_MESON_TAC[SUM_DIFF]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `sum s (c:real^N->real) = &1` SUBST1_TAC THENL
[EXPAND_TAC "c" THEN REWRITE_TAC[VECTOR_ADD_RDISTRIB] THEN
ASM_SIMP_TAC[SUM_ADD; GSYM REAL_MUL_ASSOC; SUM_LMUL] THEN
REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[REAL_ARITH `&1 = &1 - x <=> x = &0`] THEN DISCH_TAC THEN
MP_TAC(ISPECL [`c:real^N->real`;`f:real^N->bool`] SUM_POS_EQ_0) THEN
ANTS_TAC THENL [ASM_MESON_TAC[FINITE_SUBSET; SUBSET]; ALL_TAC] THEN
SIMP_TAC[VECTOR_MUL_LZERO; VSUM_0];
ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_DISJOINT]) THEN
MATCH_MP_TAC(TAUT `b ==> ~b ==> c`) THEN
EXISTS_TAC `inv(k) % (w - vsum f (\x:real^N. c x % x))` THEN CONJ_TAC THENL
[ALL_TAC;
SUBGOAL_THEN `w = vsum f (\x:real^N. c x % x) +
vsum (s DIFF f) (\x:real^N. c x % x)`
SUBST1_TAC THENL
[ASM_SIMP_TAC[VSUM_DIFF; VECTOR_ARITH `a + b - a:real^N = b`] THEN
EXPAND_TAC "c" THEN REWRITE_TAC[VECTOR_ADD_RDISTRIB] THEN
ASM_SIMP_TAC[VSUM_ADD; GSYM VECTOR_MUL_ASSOC; VSUM_LMUL];
REWRITE_TAC[VECTOR_ADD_SUB]] THEN
ASM_SIMP_TAC[GSYM VSUM_LMUL; FINITE_DIFF] THEN
REWRITE_TAC[CONVEX_HULL_FINITE; IN_ELIM_THM] THEN
EXISTS_TAC `\x. inv k * (c:real^N->real) x` THEN
ASM_REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
ASM_SIMP_TAC[IN_DIFF; REAL_LE_MUL; REAL_LE_INV_EQ; REAL_LT_IMP_LE] THEN
ASM_SIMP_TAC[SUM_LMUL; ETA_AX; REAL_MUL_LINV]] THEN
MATCH_MP_TAC lemma THEN REPEAT CONJ_TAC THENL
[REWRITE_TAC[AFFINE_AFFINE_HULL];
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[];
ASM_MESON_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL; SUBSET];
ALL_TAC] THEN
ASM_SIMP_TAC[GSYM VSUM_LMUL; AFFINE_HULL_FINITE; IN_ELIM_THM] THEN
EXISTS_TAC `(\x. inv(&1 - k) * c x):real^N->real` THEN
REWRITE_TAC[VECTOR_MUL_ASSOC; SUM_LMUL] THEN
MATCH_MP_TAC(REAL_FIELD
`~(k = &1) /\ f = &1 - k ==> inv(&1 - k) * f = &1`) THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `sum(s DIFF f) c = sum s c - sum f (c:real^N->real)`
MP_TAC THENL [ASM_MESON_TAC[SUM_DIFF]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `sum s (c:real^N->real) = &1` SUBST1_TAC THENL
[EXPAND_TAC "c" THEN REWRITE_TAC[VECTOR_ADD_RDISTRIB] THEN
ASM_SIMP_TAC[SUM_ADD; GSYM REAL_MUL_ASSOC; SUM_LMUL];
ALL_TAC] THEN
REAL_ARITH_TAC);;
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. *)
(* ------------------------------------------------------------------------- *)
let FACE_OF_CONVEX_HULL_INSERT_EQ = prove
(`!f s a:real^N.
FINITE s /\ ~(a
IN affine hull s)
==> (f
face_of (convex hull (a
INSERT s)) <=>
f
face_of (convex hull s) \/
?f'. f'
face_of (convex hull s) /\
f = convex hull (a
INSERT f'))`,
let lemma = prove
(`!a b c p:real^N u v w x.
x % p = u % a + v % b + w % c
==> !s. u + v + w = x /\ ~(x = &0) /\ affine s /\
a IN s /\ b IN s /\ c IN s
==> p IN s`,
REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o AP_TERM `(%) (inv x):real^N->real^N`) THEN
ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
DISCH_THEN SUBST1_TAC THEN
REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
MATCH_MP_TAC(SET_RULE `!t. x IN t /\ t SUBSET s ==> x IN s`) THEN
EXISTS_TAC `affine hull {a:real^N,b,c}` THEN
ASM_SIMP_TAC[HULL_MINIMAL; INSERT_SUBSET; EMPTY_SUBSET] THEN
REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN MAP_EVERY EXISTS_TAC
[`inv x * u:real`; `inv x * v:real`; `inv x * w:real`] THEN
REWRITE_TAC[] THEN UNDISCH_TAC `u + v + w:real = x` THEN
UNDISCH_TAC `~(x = &0)` THEN CONV_TAC REAL_FIELD) in
REPEAT STRIP_TAC THEN EQ_TAC THENL
[DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
FACE_OF_CONVEX_HULL_SUBSET)) THEN
ASM_SIMP_TAC[COMPACT_INSERT; FINITE_IMP_COMPACT] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM SUBST_ALL_TAC THEN ASM_CASES_TAC `(a:real^N) IN t` THENL
[ALL_TAC;
DISJ1_TAC THEN MATCH_MP_TAC FACE_OF_SUBSET THEN
EXISTS_TAC `convex hull ((a:real^N) INSERT s)` THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THEN MATCH_MP_TAC HULL_MONO THEN
ASM SET_TAC[]] THEN
DISJ2_TAC THEN
EXISTS_TAC `(convex hull t) INTER (convex hull s):real^N->bool` THEN
CONJ_TAC THENL
[MATCH_MP_TAC FACE_OF_SUBSET THEN
EXISTS_TAC `convex hull ((a:real^N) INSERT s)` THEN
SIMP_TAC[INTER_SUBSET; HULL_MONO; SET_RULE `s SUBSET (a INSERT s)`] THEN
MATCH_MP_TAC FACE_OF_INTER THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC FACE_OF_CONVEX_HULL_INSERT THEN
ASM_REWRITE_TAC[FACE_OF_REFL_EQ; CONVEX_CONVEX_HULL];
MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THEN
MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_CONVEX_HULL] THEN
ASM_SIMP_TAC[INSERT_SUBSET; HULL_INC; INTER_SUBSET] THEN
REWRITE_TAC[SUBSET] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC HULL_INC THEN
ASM_CASES_TAC `x:real^N = a` THEN ASM_REWRITE_TAC[IN_INSERT] THEN
REWRITE_TAC[IN_INTER] THEN CONJ_TAC THEN MATCH_MP_TAC HULL_INC THEN
ASM SET_TAC[]];
ALL_TAC] THEN
DISCH_THEN(DISJ_CASES_THEN ASSUME_TAC) THENL
[MATCH_MP_TAC FACE_OF_CONVEX_HULL_INSERT THEN ASM_REWRITE_TAC[];
FIRST_X_ASSUM(X_CHOOSE_THEN `f':real^N->bool` MP_TAC)] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC SUBST1_TAC) THEN
SPEC_TAC(`f':real^N->bool`,`f:real^N->bool`) THEN REPEAT STRIP_TAC THEN
ASM_CASES_TAC `s:real^N->bool = {}` THENL
[UNDISCH_TAC `(f:real^N->bool) face_of convex hull s` THEN
ASM_SIMP_TAC[FACE_OF_EMPTY; CONVEX_HULL_EMPTY; FACE_OF_REFL_EQ] THEN
REWRITE_TAC[CONVEX_CONVEX_HULL];
ALL_TAC] THEN
ASM_CASES_TAC `f:real^N->bool = {}` THENL
[ASM_REWRITE_TAC[CONVEX_HULL_SING; FACE_OF_SING] THEN
MATCH_MP_TAC EXTREME_POINT_OF_CONVEX_HULL_INSERT THEN
ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL; SUBSET];
ALL_TAC] THEN
REWRITE_TAC[face_of; CONVEX_CONVEX_HULL] THEN CONJ_TAC THENL
[MATCH_MP_TAC HULL_MINIMAL THEN
SIMP_TAC[INSERT_SUBSET; HULL_INC; IN_INSERT; CONVEX_CONVEX_HULL] THEN
MATCH_MP_TAC SUBSET_TRANS THEN
EXISTS_TAC `convex hull s:real^N->bool` THEN
ASM_SIMP_TAC[HULL_MONO; SET_RULE `s SUBSET (a INSERT s)`] THEN
ASM_MESON_TAC[FACE_OF_IMP_SUBSET];
ALL_TAC] THEN
ASM_REWRITE_TAC[CONVEX_HULL_INSERT_ALT] THEN
REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_GSPEC] THEN
REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC] THEN
X_GEN_TAC `ub:real` THEN STRIP_TAC THEN
X_GEN_TAC `b:real^N` THEN STRIP_TAC THEN
X_GEN_TAC `uc:real` THEN STRIP_TAC THEN
X_GEN_TAC `c:real^N` THEN STRIP_TAC THEN
X_GEN_TAC `ux:real` THEN STRIP_TAC THEN
X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
FIRST_X_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [face_of]) THEN
SUBGOAL_THEN `convex hull f:real^N->bool = f` SUBST_ALL_TAC THENL
[ASM_MESON_TAC[CONVEX_HULL_EQ]; ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_SEGMENT]) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_THEN `v:real` MP_TAC)) THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
REWRITE_TAC[VECTOR_ARITH
`(&1 - ux) % a + ux % x:real^N =
(&1 - v) % ((&1 - ub) % a + ub % b) + v % ((&1 - uc) % a + uc % c) <=>
((&1 - ux) - ((&1 - v) * (&1 - ub) + v * (&1 - uc))) % a +
(ux % x - (((&1 - v) * ub) % b + (v * uc) % c)) = vec 0`] THEN
ASM_CASES_TAC `&1 - ux - ((&1 - v) * (&1 - ub) + v * (&1 - uc)) = &0` THENL
[ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP (REAL_RING
`(&1 - ux) - ((&1 - v) * (&1 - ub) + v * (&1 - uc)) = &0
==> (&1 - v) * ub + v * uc = ux`)) THEN
ASM_CASES_TAC `uc = &0` THENL
[UNDISCH_THEN `uc = &0` SUBST_ALL_TAC THEN
FIRST_X_ASSUM(SUBST_ALL_TAC o MATCH_MP (REAL_ARITH
`a + v * &0 = b ==> b = a`)) THEN
REWRITE_TAC[REAL_MUL_RZERO; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
REWRITE_TAC[VECTOR_SUB_EQ; VECTOR_MUL_LCANCEL; REAL_ENTIRE] THEN
STRIP_TAC THENL
[ASM_REAL_ARITH_TAC;
ASM_MESON_TAC[VECTOR_MUL_LZERO];
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[IN_ELIM_THM] THEN
MAP_EVERY EXISTS_TAC [`&0`; `x:real^N`] THEN
ASM_REWRITE_TAC[] THEN CONV_TAC VECTOR_ARITH];
ALL_TAC] THEN
ASM_CASES_TAC `ub = &0` THENL
[UNDISCH_THEN `ub = &0` SUBST_ALL_TAC THEN
FIRST_X_ASSUM(SUBST_ALL_TAC o MATCH_MP (REAL_ARITH
`v * &0 + a = b ==> b = a`)) THEN
REWRITE_TAC[REAL_MUL_RZERO; VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
REWRITE_TAC[VECTOR_SUB_EQ; VECTOR_MUL_LCANCEL; REAL_ENTIRE] THEN
STRIP_TAC THENL
[ASM_REAL_ARITH_TAC;
ASM_MESON_TAC[VECTOR_MUL_LZERO];
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
REWRITE_TAC[IN_ELIM_THM] THEN
MAP_EVERY EXISTS_TAC [`&0`; `x:real^N`] THEN
ASM_REWRITE_TAC[] THEN CONV_TAC VECTOR_ARITH];
ALL_TAC] THEN
DISCH_THEN(fun th ->
SUBGOAL_THEN
`(b:real^N) IN f /\ (c:real^N) IN f`
MP_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN MP_TAC th) THEN
ASM_CASES_TAC `ux = &0` THENL
[DISCH_THEN(K ALL_TAC) THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
EXISTS_TAC `x:real^N` THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MP_TAC o MATCH_MP (REAL_ARITH
`&1 - ux - a = &0 ==> ux = &0 ==> ~(a < &1)`)) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT `p ==> ~p ==> q`) THEN
MATCH_MP_TAC REAL_LTE_TRANS THEN
EXISTS_TAC `(&1 - v) * &1 + v * &1` THEN
CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
MATCH_MP_TAC(REAL_ARITH
`x <= y /\ w <= z /\ ~(x = y /\ w = z) ==> x + w < y + z`) THEN
ASM_SIMP_TAC[REAL_LE_LMUL_EQ; REAL_SUB_LT; REAL_EQ_MUL_LCANCEL] THEN
REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
ASM_SIMP_TAC[REAL_SUB_0; REAL_LT_IMP_NE] THEN
REWRITE_TAC[REAL_ARITH `&1 - x = &1 <=> x = &0`] THEN
DISCH_THEN(CONJUNCTS_THEN SUBST_ALL_TAC) THEN
ASM_MESON_TAC[VECTOR_MUL_LZERO];
ALL_TAC] THEN
REWRITE_TAC[VECTOR_SUB_EQ] THEN ASM_CASES_TAC `c:real^N = b` THENL
[ASM_REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; VECTOR_MUL_LCANCEL] THEN
ASM_MESON_TAC[];
ALL_TAC] THEN
DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
EXISTS_TAC `x:real^N` THEN ASM_REWRITE_TAC[IN_SEGMENT] THEN
EXISTS_TAC `(v * uc) / ux:real` THEN
ASM_SIMP_TAC[REAL_LT_RDIV_EQ; REAL_LT_LDIV_EQ; REAL_ARITH
`&0 <= x /\ ~(x = &0) ==> &0 < x`] THEN
REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_LID] THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC REAL_LT_MUL THEN ASM_REAL_ARITH_TAC;
EXPAND_TAC "ux" THEN REWRITE_TAC[REAL_ARITH `b < a + b <=> &0 < a`] THEN
MATCH_MP_TAC REAL_LT_MUL THEN ASM_REAL_ARITH_TAC;
FIRST_X_ASSUM(MP_TAC o AP_TERM `(%) (inv ux) :real^N->real^N`) THEN
ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV] THEN
REWRITE_TAC[VECTOR_MUL_LID] THEN DISCH_THEN SUBST1_TAC THEN
REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
BINOP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
REWRITE_TAC[REAL_ARITH `inv u * v * uc:real = (v * uc) / u`] THEN
UNDISCH_TAC `(&1 - v) * ub + v * uc = ux` THEN
UNDISCH_TAC `~(ux = &0)` THEN CONV_TAC REAL_FIELD];
DISCH_THEN(MP_TAC o MATCH_MP (VECTOR_ARITH
`a + (b - c):real^N = vec 0 ==> a = c + --b`)) THEN
REWRITE_TAC[GSYM VECTOR_ADD_ASSOC; GSYM VECTOR_MUL_LNEG] THEN
DISCH_THEN(MP_TAC o SPEC `affine hull s:real^N->bool` o
MATCH_MP lemma) THEN
ASM_REWRITE_TAC[AFFINE_AFFINE_HULL] THEN
MATCH_MP_TAC(TAUT `p ==> ~p ==> q`) THEN
CONJ_TAC THENL [CONV_TAC REAL_RING; REPEAT CONJ_TAC] THEN
MATCH_MP_TAC(REWRITE_RULE[SUBSET] CONVEX_HULL_SUBSET_AFFINE_HULL) THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[]]);;
(* ------------------------------------------------------------------------- *)
(* 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[]);;
let POLYTOPE_SUMS = prove
(`!s t:real^N->bool.
polytope s /\ polytope t ==> polytope {x + y | x
IN s /\ y
IN t}`,
REPEAT GEN_TAC THEN REWRITE_TAC[polytope] THEN DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_THEN `u:real^N->bool` STRIP_ASSUME_TAC)
(X_CHOOSE_THEN `v:real^N->bool` STRIP_ASSUME_TAC)) THEN
EXISTS_TAC `{x + y:real^N | x
IN u /\ y
IN v}` THEN
ASM_SIMP_TAC[
FINITE_PRODUCT_DEPENDENT;
CONVEX_HULL_SUMS]);;
(* ------------------------------------------------------------------------- *)
(* Approximation of bounded convex sets by polytopes. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Polyhedra. *)
(* ------------------------------------------------------------------------- *)
let POLYHEDRON_INTER = prove
(`!s t:real^N->bool.
polyhedron s /\ polyhedron t ==> polyhedron (s
INTER t)`,
REPEAT GEN_TAC THEN REWRITE_TAC[polyhedron] THEN
DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_TAC `f:(real^N->bool)->bool`)
(X_CHOOSE_TAC `g:(real^N->bool)->bool`)) THEN
EXISTS_TAC `f
UNION g:(real^N->bool)->bool` THEN
ASM_REWRITE_TAC[SET_RULE `
INTERS(f
UNION g) =
INTERS f
INTER INTERS g`] THEN
REWRITE_TAC[
FINITE_UNION;
IN_UNION] THEN
REPEAT STRIP_TAC THEN ASM_SIMP_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Canonical polyedron representation making facial structure explicit. *)
(* ------------------------------------------------------------------------- *)
let POLYHEDRON_INTER_AFFINE_PARALLEL = prove
(`!s:real^N->bool.
polyhedron s <=>
?f.
FINITE f /\
s = (affine hull s)
INTER (
INTERS f) /\
(!h. h
IN f
==> ?a b. ~(a = vec 0) /\ h = {x:real^N | a dot x <= b} /\
(!x. x
IN affine hull s
==> (x + a)
IN affine hull s))`,
GEN_TAC THEN REWRITE_TAC[
POLYHEDRON_INTER_AFFINE] THEN EQ_TAC THENL
[ALL_TAC; MATCH_MP_TAC
MONO_EXISTS THEN MESON_TAC[]] THEN
DISCH_THEN(X_CHOOSE_THEN `f:(real^N->bool)->bool` MP_TAC) THEN
ASM_CASES_TAC `s:real^N->bool = {}` THENL
[DISCH_THEN(K ALL_TAC) THEN EXISTS_TAC `{}:(real^N->bool)->bool` THEN
ASM_SIMP_TAC[
AFFINE_HULL_EMPTY;
INTER_EMPTY;
NOT_IN_EMPTY;
FINITE_EMPTY];
ALL_TAC] THEN
ASM_CASES_TAC `f:(real^N->bool)->bool = {}` THENL
[ASM_REWRITE_TAC[
NOT_IN_EMPTY;
INTERS_0;
INTER_UNIV] THEN
DISCH_THEN(ASSUME_TAC o SYM o CONJUNCT2) THEN
EXISTS_TAC `{}:(real^N->bool)->bool` THEN
ASM_REWRITE_TAC[
NOT_IN_EMPTY;
INTERS_0;
INTER_UNIV;
FINITE_EMPTY];
ALL_TAC] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o GSYM) MP_TAC)) THEN
GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)
[
RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM;
SKOLEM_THM] THEN
MAP_EVERY X_GEN_TAC
[`a:(real^N->bool)->real^N`; `b:(real^N->bool)->real`] THEN
DISCH_THEN(ASSUME_TAC o GSYM) THEN
SUBGOAL_THEN
`!h. h
IN f /\ ~(affine hull s
SUBSET h)
==> ?a' b'. ~(a' = vec 0) /\
affine hull s
INTER {x:real^N | a' dot x <= b'} =
affine hull s
INTER h /\
!w. w
IN affine hull s ==> (w + a')
IN affine hull s`
MP_TAC THENL
[GEN_TAC THEN STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN
REWRITE_TAC[ASSUME `(h:real^N->bool)
IN f`] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC o GSYM) THEN
MP_TAC(ISPECL [`affine hull s:real^N->bool`;
`(a:(real^N->bool)->real^N) h`;
`(b:(real^N->bool)->real) h`]
AFFINE_PARALLEL_SLICE) THEN
REWRITE_TAC[
AFFINE_AFFINE_HULL] THEN MATCH_MP_TAC(TAUT
`~p /\ ~q /\ (r ==> r') ==> (p \/ q \/ r ==> r')`) THEN
ASM_SIMP_TAC[] THEN CONJ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
DISCH_TAC THEN
UNDISCH_TAC `~(s:real^N->bool = {})` THEN
EXPAND_TAC "s" THEN REWRITE_TAC[GSYM
INTERS_INSERT] THEN
MATCH_MP_TAC(SET_RULE
`!t. t
SUBSET s /\
INTERS t = {} ==>
INTERS s = {}`) THEN
EXISTS_TAC `{affine hull s,h:real^N->bool}` THEN
ASM_REWRITE_TAC[
INTERS_2] THEN ASM SET_TAC[];
ALL_TAC] THEN
GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV) [
RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[
SKOLEM_THM;
LEFT_IMP_EXISTS_THM] THEN
FIRST_X_ASSUM(K ALL_TAC o SPEC `{}:real^N->bool`) THEN
MAP_EVERY X_GEN_TAC
[`a:(real^N->bool)->real^N`; `b:(real^N->bool)->real`] THEN
DISCH_TAC THEN
EXISTS_TAC `
IMAGE (\h:real^N->bool. {x:real^N | a h dot x <= b h})
{h | h
IN f /\ ~(affine hull s
SUBSET h)}` THEN
ASM_SIMP_TAC[
FINITE_IMAGE;
FINITE_RESTRICT;
FORALL_IN_IMAGE] THEN
REWRITE_TAC[
FORALL_IN_GSPEC] THEN CONJ_TAC THENL
[ALL_TAC;
X_GEN_TAC `h:real^N->bool` THEN STRIP_TAC THEN
MAP_EVERY EXISTS_TAC
[`(a:(real^N->bool)->real^N) h`; `(b:(real^N->bool)->real) h`] THEN
ASM_MESON_TAC[]] THEN
FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [GSYM th]) THEN
GEN_REWRITE_TAC I [
EXTENSION] THEN X_GEN_TAC `x:real^N` THEN
REWRITE_TAC[
INTERS_IMAGE;
IN_INTER;
IN_ELIM_THM] THEN
ASM_CASES_TAC `(x:real^N)
IN affine hull s` THEN
ASM_REWRITE_TAC[
IN_INTERS] THEN AP_TERM_TAC THEN ABS_TAC THEN
ASM SET_TAC[]);;
let POLYHEDRON_INTER_AFFINE_PARALLEL_MINIMAL = prove
(`!s. polyhedron s <=>
?f.
FINITE f /\
s = (affine hull s)
INTER (
INTERS f) /\
(!h. h
IN f
==> ?a b. ~(a = vec 0) /\ h = {x:real^N | a dot x <= b} /\
(!x. x
IN affine hull s
==> (x + a)
IN affine hull s)) /\
!f'. f'
PSUBSET f ==> s
PSUBSET (affine hull s)
INTER (
INTERS f')`,
GEN_TAC THEN REWRITE_TAC[
POLYHEDRON_INTER_AFFINE_PARALLEL] THEN
EQ_TAC THENL [ALL_TAC; MATCH_MP_TAC
MONO_EXISTS THEN MESON_TAC[]] THEN
GEN_REWRITE_TAC LAND_CONV
[MESON[
HAS_SIZE]
`(?f.
FINITE f /\ P f) <=> (?n f. f
HAS_SIZE n /\ P f)`] THEN
GEN_REWRITE_TAC LAND_CONV [
num_WOP] THEN
DISCH_THEN(X_CHOOSE_THEN `n:num` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
MATCH_MP_TAC
MONO_EXISTS THEN REWRITE_TAC[
HAS_SIZE] THEN
X_GEN_TAC `f:(real^N->bool)->bool` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
CONJ_TAC THENL [FIRST_ASSUM ACCEPT_TAC; ALL_TAC] THEN
X_GEN_TAC `f':(real^N->bool)->bool` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `
CARD(f':(real^N->bool)->bool)`) THEN
ANTS_TAC THENL [ASM_MESON_TAC[
CARD_PSUBSET]; ALL_TAC] THEN
REWRITE_TAC[
NOT_EXISTS_THM;
HAS_SIZE] THEN
DISCH_THEN(MP_TAC o SPEC `f':(real^N->bool)->bool`) THEN
MATCH_MP_TAC(TAUT `a /\ c /\ (~b ==> d) ==> ~(a /\ b /\ c) ==> d`) THEN
CONJ_TAC THENL [ASM_MESON_TAC[
PSUBSET;
FINITE_SUBSET]; ALL_TAC] THEN
CONJ_TAC THENL
[REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[];
MATCH_MP_TAC(SET_RULE `s
SUBSET t ==> ~(s = t) ==> s
PSUBSET t`) THEN
FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN
ASM SET_TAC[]]);;
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. *)
(* ------------------------------------------------------------------------- *)
let FACET_OF_POLYHEDRON = prove
(`!s:real^N->bool c.
polyhedron s /\ c
facet_of s
==> ?a b. ~(a = vec 0) /\
s
SUBSET {x | a dot x <= b} /\
c = s
INTER {x | a dot x = b}`,
REPEAT STRIP_TAC THEN FIRST_ASSUM
(MP_TAC o GEN_REWRITE_RULE I [
POLYHEDRON_INTER_AFFINE_MINIMAL]) THEN
GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)
[
RIGHT_IMP_EXISTS_THM;
SKOLEM_THM] THEN
SIMP_TAC[
LEFT_IMP_EXISTS_THM;
RIGHT_AND_EXISTS_THM;
LEFT_AND_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
STRIP_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`]
FACET_OF_POLYHEDRON_EXPLICIT) THEN
ANTS_TAC THENL [ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(MP_TAC o SPEC `c:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `i:real^N->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `(a:(real^N->bool)->real^N) i` THEN
EXISTS_TAC `(b:(real^N->bool)->real) i` THEN ASM_SIMP_TAC[] THEN
FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN
MATCH_MP_TAC(SET_RULE `t
SUBSET u ==> (s
INTER t)
SUBSET u`) THEN
MATCH_MP_TAC(SET_RULE `t
IN f ==>
INTERS f
SUBSET t`) THEN ASM_MESON_TAC[]);;
let FACE_OF_POLYHEDRON = prove
(`!s:real^N->bool c.
polyhedron s /\ c
face_of s /\ ~(c = {}) /\ ~(c = s)
==> c =
INTERS {f | f
facet_of s /\ c
SUBSET f}`,
REPEAT STRIP_TAC THEN FIRST_ASSUM
(MP_TAC o GEN_REWRITE_RULE I [
POLYHEDRON_INTER_AFFINE_MINIMAL]) THEN
REWRITE_TAC[
RIGHT_IMP_EXISTS_THM;
SKOLEM_THM] THEN
SIMP_TAC[
LEFT_IMP_EXISTS_THM;
RIGHT_AND_EXISTS_THM;
LEFT_AND_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
STRIP_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`]
FACET_OF_POLYHEDRON_EXPLICIT) THEN
ANTS_TAC THENL [ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
MP_TAC(ISPECL [`s:real^N->bool`; `f:(real^N->bool)->bool`;
`a:(real^N->bool)->real^N`; `b:(real^N->bool)->real`]
FACE_OF_POLYHEDRON_EXPLICIT) THEN
ANTS_TAC THENL [ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(MP_TAC o SPEC `c:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [
EXTENSION] THEN
X_GEN_TAC `h:real^N->bool` THEN REWRITE_TAC[
IN_ELIM_THM] THEN MESON_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* 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. *)
(* ------------------------------------------------------------------------- *)
let FARKAS_LEMMA = prove
(`!A:real^N^M b.
(?x:real^N.
A ** x = b /\
(!i. 1 <= i /\ i <= dimindex(:N) ==> &0 <= x$i)) <=>
~(?y:real^M.
b dot y < &0 /\
(!i. 1 <= i /\ i <= dimindex(:N) ==> &0 <= (transp A ** y)$i))`,
let FARKAS_LEMMA_ALT = prove
(`!A:real^N^M b.
(?x:real^N.
(!i. 1 <= i /\ i <= dimindex(:M) ==> (A ** x)$i <= b$i)) <=>
~(?y:real^M.
(!i. 1 <= i /\ i <= dimindex(:M) ==> &0 <= y$i) /\
y ** A = vec 0 /\ b dot y < &0)`,
(* ------------------------------------------------------------------------- *)
(* 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). *)
(* ------------------------------------------------------------------------- *)