100/ceva.ml

   1 (* ========================================================================= *)
   2 (* #61: Ceva's theorem.                                                      *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/convex.ml";;
   6 needs "Examples/sos.ml";;
   7
   8 prioritize_real();;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* We use the notion of "betweenness".                                       *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let BETWEEN_THM = prove
  15  (`between x (a,b) <=>
  16        ?u. &0 <= u /\ u <= &1 /\ x = u % a + (&1 - u) % b`,
  17   REWRITE_TAC[BETWEEN_IN_CONVEX_HULL] THEN
  18   ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN
  19   REWRITE_TAC[CONVEX_HULL_2_ALT; IN_ELIM_THM] THEN
  20   AP_TERM_TAC THEN ABS_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
  21   AP_TERM_TAC THEN VECTOR_ARITH_TAC);;
  22
  23 (* ------------------------------------------------------------------------- *)
  24 (* Lemmas to reduce geometric concepts to more convenient forms.             *)
  25 (* ------------------------------------------------------------------------- *)
  26
  27 let NORM_CROSS = prove
  28  (`norm(a) * norm(b) * norm(c) = norm(d) * norm(e) * norm(f) <=>
  29    (a dot a) * (b dot b) * (c dot c) = (d dot d) * (e dot e) * (f dot f)`,
  30   let lemma = prove
  31    (`!x y. &0 <= x /\ &0 <= y ==> (x pow 2 = y pow 2 <=> x = y)`,
  32     REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[REAL_POW_2] THEN
  33     REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
  34      (SPECL [`x:real`; `y:real`] REAL_LT_TOTAL) THEN
  35     ASM_MESON_TAC[REAL_LT_MUL2; REAL_LT_REFL]) in
  36   REWRITE_TAC[GSYM NORM_POW_2; GSYM REAL_POW_MUL] THEN
  37   MATCH_MP_TAC(GSYM lemma) THEN SIMP_TAC[NORM_POS_LE; REAL_LE_MUL]);;
  38
  39 let COLLINEAR = prove
  40  (`!a b c:real^2.
  41         collinear {a:real^2,b,c} <=>
  42         ((a$1 - b$1) * (b$2 - c$2) = (a$2 - b$2) * (b$1 - c$1))`,
  43   let lemma = prove
  44    (`~(y1 = &0) /\ x2 * y1 = x1 * y2 ==> ?c. x1 = c * y1 /\ x2 = c * y2`,
  45     STRIP_TAC THEN EXISTS_TAC `x1 / y1` THEN
  46     REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD) in
  47   REPEAT GEN_TAC THEN ASM_CASES_TAC `a:real^2 = b` THENL
  48    [ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_RZERO; REAL_MUL_LZERO] THEN
  49     REWRITE_TAC[COLLINEAR_SING; COLLINEAR_2; INSERT_AC];
  50     ALL_TAC] THEN
  51   REWRITE_TAC[collinear] THEN EQ_TAC THENL
  52    [DISCH_THEN(CHOOSE_THEN (fun th ->
  53         MP_TAC(SPECL [`a:real^2`; `b:real^2`] th) THEN
  54         MP_TAC(SPECL [`b:real^2`; `c:real^2`] th))) THEN
  55     REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN REPEAT STRIP_TAC THEN
  56     ASM_SIMP_TAC[GSYM VECTOR_SUB_COMPONENT; DIMINDEX_2; ARITH] THEN
  57     SIMP_TAC[VECTOR_MUL_COMPONENT; DIMINDEX_2; ARITH] THEN
  58     REAL_ARITH_TAC;
  59     ALL_TAC] THEN
  60   DISCH_TAC THEN EXISTS_TAC `a - b:real^2` THEN
  61   REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
  62   REPEAT GEN_TAC THEN DISCH_TAC THEN
  63   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [CART_EQ]) THEN
  64   REWRITE_TAC[DIMINDEX_2; FORALL_2; ARITH; DE_MORGAN_THM] THEN STRIP_TAC THEN
  65   SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; VECTOR_MUL_COMPONENT;
  66            VECTOR_SUB_COMPONENT; ARITH]
  67   THENL [ALL_TAC; ONCE_REWRITE_TAC[CONJ_SYM]] THEN
  68   FIRST_X_ASSUM(CONJUNCTS_THEN(REPEAT_TCL STRIP_THM_THEN SUBST1_TAC)) THEN
  69   MATCH_MP_TAC lemma THEN REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD);;
  70
  71 (* ------------------------------------------------------------------------- *)
  72 (* More or less automatic proof of the main direction.                       *)
  73 (* ------------------------------------------------------------------------- *)
  74
  75 let CEVA_WEAK = prove
  76  (`!A B C X Y Z P:real^2.
  77         ~(collinear {A,B,C}) /\
  78         between X (B,C) /\ between Y (A,C) /\ between Z (A,B) /\
  79         between P (A,X) /\ between P (B,Y) /\ between P (C,Z)
  80         ==> dist(B,X) * dist(C,Y) * dist(A,Z) =
  81             dist(X,C) * dist(Y,A) * dist(Z,B)`,
  82   REPEAT GEN_TAC THEN
  83   REWRITE_TAC[dist; NORM_CROSS; COLLINEAR; BETWEEN_THM] THEN STRIP_TAC THEN
  84   REPEAT(FIRST_X_ASSUM(SUBST_ALL_TAC o check (is_var o lhs o concl))) THEN
  85   REPEAT(FIRST_X_ASSUM(MP_TAC o SYM)) THEN
  86   SIMP_TAC[dot; SUM_2; VECTOR_SUB_COMPONENT; DIMINDEX_2; VECTOR_ADD_COMPONENT;
  87            CART_EQ; FORALL_2; VECTOR_MUL_COMPONENT; ARITH] THEN
  88   FIRST_X_ASSUM(MP_TAC o check(is_neg o concl)) THEN
  89   CONV_TAC REAL_RING);;
  90
  91 (* ------------------------------------------------------------------------- *)
  92 (* More laborious proof of equivalence.                                      *)
  93 (* ------------------------------------------------------------------------- *)
  94
  95 let CEVA = prove
  96  (`!A B C X Y Z:real^2.
  97         ~(collinear {A,B,C}) /\
  98         between X (B,C) /\ between Y (C,A) /\ between Z (A,B)
  99         ==> (dist(B,X) * dist(C,Y) * dist(A,Z) =
 100              dist(X,C) * dist(Y,A) * dist(Z,B) <=>
 101              (?P. between P (A,X) /\ between P (B,Y) /\ between P (C,Z)))`,
 102   REPEAT GEN_TAC THEN
 103   MAP_EVERY ASM_CASES_TAC [`A:real^2 = B`; `A:real^2 = C`; `B:real^2 = C`] THEN
 104   ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_SING; COLLINEAR_2] THEN
 105   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[BETWEEN_THM] THEN
 106   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `x:real`) MP_TAC) THEN
 107   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `y:real`)
 108     (X_CHOOSE_TAC `z:real`)) THEN
 109   REPEAT(FIRST_X_ASSUM(CONJUNCTS_THEN STRIP_ASSUME_TAC)) THEN
 110   REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN REWRITE_TAC[dist] THEN
 111   REWRITE_TAC[VECTOR_ARITH `B - (x % B + (&1 - x) % C) = (&1 - x) % (B - C)`;
 112               VECTOR_ARITH `(x % B + (&1 - x) % C) - C = x % (B - C)`] THEN
 113   REWRITE_TAC[NORM_MUL] THEN
 114   REWRITE_TAC[REAL_ARITH `(a * a') * (b * b') * (c * c') =
 115                           (a * b * c) * (a' * b' * c')`] THEN
 116   REWRITE_TAC[REAL_MUL_ASSOC; REAL_EQ_MUL_RCANCEL; REAL_ENTIRE] THEN
 117   ASM_REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN
 118   ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - x <=> x <= &1`; real_abs] THEN
 119   EQ_TAC THENL
 120    [ALL_TAC;
 121     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [COLLINEAR]) THEN
 122     SIMP_TAC[dot; SUM_2; VECTOR_SUB_COMPONENT; DIMINDEX_2; FORALL_2;
 123             VECTOR_ADD_COMPONENT; CART_EQ; VECTOR_MUL_COMPONENT; ARITH] THEN
 124     CONV_TAC REAL_RING] THEN
 125   DISCH_TAC THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
 126   SUBGOAL_THEN
 127    `?u v w. w = (&1 - u) * (&1 - x) /\
 128             v = (&1 - u) * x /\
 129             u = (&1 - v) * (&1 - y) /\
 130             u = (&1 - w) * z /\
 131             v = (&1 - w) * (&1 - z) /\
 132             w = (&1 - v) * y /\
 133             &0 <= u /\ u <= &1 /\ &0 <= v /\ v <= &1 /\ &0 <= w /\ w <= &1`
 134   (STRIP_ASSUME_TAC o GSYM) THENL
 135    [ALL_TAC;
 136     EXISTS_TAC `u % A + v % B + w % C:real^2` THEN REPEAT CONJ_TAC THENL
 137      [EXISTS_TAC `u:real`; EXISTS_TAC `v:real`; EXISTS_TAC `w:real`] THEN
 138     ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC] THEN
 139   REWRITE_TAC[UNWIND_THM2] THEN
 140   MATCH_MP_TAC(MESON[]
 141    `(!x. p x /\ q x ==> r x) /\ (?x. p x /\ q x)
 142     ==> (?x. p x /\ q x /\ r x)`) THEN
 143   CONJ_TAC THENL
 144    [GEN_TAC THEN
 145     REPEAT(FIRST_X_ASSUM(MP_TAC o check (not o is_neg o concl))) THEN
 146     REWRITE_TAC[IMP_IMP] THEN
 147     REPEAT(MATCH_MP_TAC(TAUT `(a ==> b /\ c) /\ (a /\ b /\ c ==> d)
 148                               ==> a ==> b /\ c /\ d`) THEN
 149            CONJ_TAC THENL
 150             [CONV_TAC REAL_RING ORELSE CONV_TAC REAL_SOS; ALL_TAC]) THEN
 151     CONV_TAC REAL_SOS;
 152     ALL_TAC] THEN
 153   RULE_ASSUM_TAC(REWRITE_RULE[COLLINEAR]) THEN
 154   ASM_CASES_TAC `x = &0` THENL
 155    [EXISTS_TAC `&1 - y / (&1 - x + x * y)` THEN
 156     REPEAT(FIRST_X_ASSUM(MP_TAC o check (not o is_neg o concl))) THEN
 157     CONV_TAC REAL_FIELD; ALL_TAC] THEN
 158   EXISTS_TAC `&1 - (&1 - z) / (x + (&1 - x) * (&1 - z))` THEN
 159   SUBGOAL_THEN `~(x + (&1 - x) * (&1 - z) = &0)` MP_TAC THENL
 160    [ALL_TAC;
 161     REPEAT(FIRST_X_ASSUM(MP_TAC o check (not o is_neg o concl))) THEN
 162     CONV_TAC REAL_FIELD] THEN
 163   MATCH_MP_TAC(REAL_ARITH
 164    `z * (&1 - x) < &1 ==> ~(x + (&1 - x) * (&1 - z) = &0)`) THEN
 165   ASM_CASES_TAC `z = &0` THEN ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_LT_01] THEN
 166   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&1 * (&1 - x)` THEN
 167   ASM_SIMP_TAC[REAL_LE_RMUL; REAL_ARITH `x <= &1 ==> &0 <= &1 - x`] THEN
 168   ASM_REAL_ARITH_TAC);;
 169
 170 (* ------------------------------------------------------------------------- *)
 171 (* Just for geometric intuition, verify metrical version of "between".       *)
 172 (* This isn't actually needed in the proof. Moreover, this is now actually   *)
 173 (* the definition of "between" so this is all a relic.                       *)
 174 (* ------------------------------------------------------------------------- *)
 175
 176 let BETWEEN_SYM = prove
 177  (`!u v w. between v (u,w) <=> between v (w,u)`,
 178   REPEAT GEN_TAC THEN REWRITE_TAC[BETWEEN_THM] THEN EQ_TAC THEN
 179   DISCH_THEN(X_CHOOSE_TAC `u:real`) THEN EXISTS_TAC `&1 - u` THEN
 180   ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN TRY VECTOR_ARITH_TAC THEN
 181   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
 182
 183 let BETWEEN_METRICAL = prove
 184  (`!u v w:real^N. between v (u,w) <=> dist(u,v) + dist(v,w) = dist(u,w)`,
 185   REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
 186   ONCE_REWRITE_TAC[BETWEEN_SYM] THEN REWRITE_TAC[BETWEEN_THM; dist] THEN
 187   REWRITE_TAC[VECTOR_ARITH `x % u + (&1 - x) % v = v + x % (u - v)`] THEN
 188   SUBST1_TAC(VECTOR_ARITH `u - w:real^N = (u - v) + (v - w)`) THEN
 189   CONV_TAC(LAND_CONV SYM_CONV) THEN REWRITE_TAC[NORM_TRIANGLE_EQ] THEN
 190   EQ_TAC THENL
 191    [ALL_TAC;
 192     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 193     REWRITE_TAC[VECTOR_ARITH `u - (u + x):real^N = --x`; NORM_NEG;
 194                 VECTOR_ARITH `(u + c % (w - u)) - w = (&1 - c) % (u - w)`] THEN
 195     REWRITE_TAC[VECTOR_ARITH `a % --(c % (x - y)) = (a * c) % (y - x)`] THEN
 196     REWRITE_TAC[VECTOR_MUL_ASSOC; NORM_MUL] THEN
 197     ASM_SIMP_TAC[REAL_ARITH `c <= &1 ==> abs(&1 - c) = &1 - c`;
 198                  REAL_ARITH `&0 <= c ==> abs c = c`] THEN
 199     REWRITE_TAC[NORM_SUB; REAL_MUL_AC]] THEN
 200   DISCH_TAC THEN ASM_CASES_TAC `&0 < norm(u - v:real^N) + norm(v - w)` THENL
 201    [ALL_TAC;
 202     FIRST_X_ASSUM(MP_TAC o MATCH_MP (REAL_ARITH
 203      `~(&0 < x + y) ==> &0 <= x /\ &0 <= y ==> x = &0 /\ y = &0`)) THEN
 204     REWRITE_TAC[NORM_POS_LE; NORM_EQ_0; VECTOR_SUB_EQ] THEN
 205     STRIP_TAC THEN EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[REAL_POS] THEN
 206     VECTOR_ARITH_TAC] THEN
 207   EXISTS_TAC `norm(u - v:real^N) / (norm(u - v) + norm(v - w))` THEN
 208   ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ; REAL_MUL_LZERO;
 209                REAL_MUL_LID; REAL_LE_ADDR; NORM_POS_LE] THEN
 210   MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP THEN
 211   EXISTS_TAC `norm(u - v:real^N) + norm(v - w)` THEN
 212   ASM_SIMP_TAC[REAL_LT_IMP_NZ] THEN
 213   REWRITE_TAC[VECTOR_ARITH `x % (y + z % v) = x % y + (x * z) % v`] THEN
 214   ASM_SIMP_TAC[REAL_LT_IMP_NZ; REAL_DIV_LMUL] THEN
 215   FIRST_X_ASSUM(MP_TAC o SYM) THEN VECTOR_ARITH_TAC);;