(* ========================================================================= *) (* "Without loss of generality" reasoning. *) (* ========================================================================= *) prioritize_real();; (* ------------------------------------------------------------------------- *) (* Schur's inequality. *) (* ------------------------------------------------------------------------- *) g `!k a b c. &0 <= a /\ &0 <= b /\ &0 <= c ==> &0 <= a pow k * (a - b) * (a - c) + b pow k * (b - a) * (b - c) + c pow k * (c - a) * (c - b)`;; e GEN_TAC;; (* ------------------------------------------------------------------------- *) (* We want a "without loss of generality" theorem for 3 variables. *) (* ------------------------------------------------------------------------- *) REAL_WLOG_LE;; let REAL_WLOG_3_LE = prove (`(!x y z. P x y z ==> P y x z /\ P x z y) /\ (!x y z. x <= y /\ y <= z ==> P x y z) ==> !x y z. P x y z`, REPEAT STRIP_TAC THEN (STRIP_ASSUME_TAC o REAL_ARITH) `x <= y /\ y <= z \/ x <= z /\ z <= y \/ y <= x /\ x <= z \/ y <= z /\ z <= x \/ z <= x /\ x <= y \/ z <= y /\ y <= x` THEN ASM_MESON_TAC[]);; (* ------------------------------------------------------------------------- *) (* Now the proof of Schur. *) (* ------------------------------------------------------------------------- *) g `!k a b c. &0 <= a /\ &0 <= b /\ &0 <= c ==> &0 <= a pow k * (a - b) * (a - c) + b pow k * (b - a) * (b - c) + c pow k * (c - a) * (c - b)`;; e(GEN_TAC THEN MATCH_MP_TAC REAL_WLOG_3_LE);; e CONJ_TAC;; e(MESON_TAC[REAL_ADD_AC; REAL_MUL_AC]);; e(ONCE_REWRITE_TAC[REAL_ARITH `a pow k * (a - b) * (a - c) + b pow k * (b - a) * (b - c) + c pow k * (c - a) * (c - b) = (c - b) * (c pow k * (c - a) - b pow k * (b - a)) + a pow k * (c - a) * (b - a)`]);; e(REPEAT STRIP_TAC);; e(REPEAT (FIRST(map MATCH_MP_TAC [REAL_LE_ADD; REAL_LE_MUL; REAL_LE_MUL2]) THEN ASM_SIMP_TAC[REAL_POW_LE2; REAL_POW_LE; REAL_SUB_LE] THEN REPEAT CONJ_TAC));; e ASM_REAL_ARITH_TAC;; e ASM_REAL_ARITH_TAC;; let SCHUR = top_thm();; (* ------------------------------------------------------------------------- *) (* As a single script. *) (* ------------------------------------------------------------------------- *) let SCHUR = prove (`!k a b c. &0 <= a /\ &0 <= b /\ &0 <= c ==> &0 <= a pow k * (a - b) * (a - c) + b pow k * (b - a) * (b - c) + c pow k * (c - a) * (c - b)`, GEN_TAC THEN MATCH_MP_TAC REAL_WLOG_3_LE THEN CONJ_TAC THENL [MESON_TAC[REAL_ADD_AC; REAL_MUL_AC]; REPEAT STRIP_TAC] THEN ONCE_REWRITE_TAC[REAL_ARITH `a pow k * (a - b) * (a - c) + b pow k * (b - a) * (b - c) + c pow k * (c - a) * (c - b) = (c - b) * (c pow k * (c - a) - b pow k * (b - a)) + a pow k * (c - a) * (b - a)`] THEN REPEAT (FIRST(map MATCH_MP_TAC [REAL_LE_ADD; REAL_LE_MUL; REAL_LE_MUL2]) THEN ASM_SIMP_TAC[REAL_POW_LE2; REAL_POW_LE; REAL_SUB_LE] THEN REPEAT CONJ_TAC) THEN ASM_REAL_ARITH_TAC);; (* ------------------------------------------------------------------------- *) (* First attempt at such reasoning in geometry. *) (* ------------------------------------------------------------------------- *) needs "Multivariate/geom.ml";; prioritize_vector();; let WLOG_ORIGIN = prove (`(!a x. P(a + x) <=> P x) /\ P(vec 0) ==> (!x:real^N. P x)`, MESON_TAC[VECTOR_ADD_RID]);; g`!A B C:real^N. ~(A = B /\ B = C /\ A = C) ==> angle(B,A,C) + angle(A,B,C) + angle(B,C,A) = pi`;; e(MATCH_MP_TAC WLOG_ORIGIN THEN CONJ_TAC);; (* ------------------------------------------------------------------------- *) (* Justifying the similar transformation of the quantifiers. *) (* ------------------------------------------------------------------------- *) let QUANTIFY_SURJECTION_THM = SET_RULE `!f:A->B. (!y. ?x. f x = y) ==> (!P. (!x. P x) <=> (!x. P (f x))) /\ (!P. (?x. P x) <=> (?x. P (f x)))`;; (* ------------------------------------------------------------------------- *) (* We can do more "higher-order" transformations. *) (* ------------------------------------------------------------------------- *) let QUANTIFY_SURJECTION_THM = prove (`!f:A->B. (!y. ?x. f x = y) ==> (!P. (!x. P x) <=> (!x. P (f x))) /\ (!P. (?x. P x) <=> (?x. P (f x))) /\ (!Q. (!s. Q s) <=> (!s. Q(IMAGE f s))) /\ (!Q. (?s. Q s) <=> (?s. Q(IMAGE f s))) /\ (!P. {x | P x} = IMAGE f {x | P(f x)})`, GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [SURJECTIVE_RIGHT_INVERSE] THEN DISCH_THEN(X_CHOOSE_TAC `g:B->A`) THEN SUBGOAL_THEN `!s. IMAGE (f:A->B) (IMAGE g s) = s` ASSUME_TAC THEN ASM SET_TAC[]);; (* ------------------------------------------------------------------------- *) (* Some difficulties. *) (* ------------------------------------------------------------------------- *) g `!a x y z. angle(a + x,a + y,a + z) = angle(x,y,z)`;; e(REWRITE_TAC[angle]);; e(REWRITE_TAC[VECTOR_ARITH `(a + x) - (a + y):real^N = x - y`]);; (**** This is a bit more complicated ****) g `!a w x y z. azim (a + w) (a + x) (a + y) (a + z) = azim w x y z`;; e(REWRITE_TAC[azim_def]);; (* ------------------------------------------------------------------------- *) (* GEOM_ORIGIN_TAC examples. *) (* ------------------------------------------------------------------------- *) g `!A B C:real^N. ~(A = B /\ B = C /\ A = C) ==> angle(B,A,C) + angle(A,B,C) + angle(B,C,A) = pi`;; e(GEOM_ORIGIN_TAC `A:real^N`);; g `!z:real^3 r. &0 <= r ==> measure(cball(z,r)) = &4 / &3 * pi * r pow 3`;; e(GEOM_ORIGIN_TAC `z:real^3`);; g `!s a:real^N. closed s /\ ~(s = {}) ==> (?x. x IN s /\ (!y. y IN s ==> dist (a,x) <= dist (a,y)))`;; e(GEOM_ORIGIN_TAC `a:real^N`);; g `{y | ~collinear {v1, v2, y} /\ &0 < azim v1 v2 w1 y /\ azim v1 v2 w1 y < azim v1 v2 w1 w2} = (if collinear {v1, v2, w1} \/ collinear {v1, v2, w2} then {} else if w2 IN aff_ge {v1, v2} {w1} then {} else if w2 IN aff_lt {v1, v2} {w1} then aff_gt {v1, v2, w1} {v1 + (v2 - v1) cross (w1 - v1)} else if ((v2 - v1) cross (w1 - v1)) dot (w2 - v1) > &0 then aff_gt {v1, v2} {w1, w2} else (:real^3) DIFF aff_ge {v1, v2} {w1, w2})`;; e(GEOM_ORIGIN_TAC `v1:real^3`);; e(REWRITE_TAC[VECTOR_ADD_RID; TRANSLATION_INVARIANTS `v1:real^3`]);; (* ------------------------------------------------------------------------- *) (* The general situation. *) (* ------------------------------------------------------------------------- *) let WLOG_TRANSFORM_FORWARDS = prove (`!P. (!x. ?f. transform(f) /\ nice(f x)) /\ (!f x. transform f ==> (P(f x) <=> P x)) ==> ((!x. P x) <=> (!x. nice(x) ==> P(x)))`, MESON_TAC[]);; let WLOG_TRANSFORM_BACKWARDS = prove (`!P P'. (!x. ?f y. transform(f) /\ nice(y) /\ f y = x) /\ (!f x. transform f /\ nice x ==> (P(f x) <=> P' x)) ==> ((!x. P x) <=> (!y. nice(y) ==> P'(y)))`, MESON_TAC[]);; (* ------------------------------------------------------------------------- *) (* A more extended example. *) (* ------------------------------------------------------------------------- *) g `!u1:real^3 u2 p a b. ~(u1 = u2) /\ plane p /\ {u1,u2} SUBSET p /\ dist(u1,u2) <= a + b /\ abs(a - b) < dist(u1,u2) /\ &0 <= a /\ &0 <= b ==> (?d1 d2. {d1, d2} SUBSET p /\ ~(d1 = d2) /\ &1 / &2 % (d1 + d2) IN affine hull {u1, u2} /\ dist(d1,u1) = a /\ dist(d1,u2) = b /\ dist(d2,u1) = a /\ dist(d2,u2) = b)`;; (*** First, rotate the plane p to the special case z\$3 = &0 ***) e(GEOM_HORIZONTAL_PLANE_TAC `p:real^3->bool`);; (*** Now reshuffle the goal to have explicit restricted quantifiers ***) e(ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d ==> e <=> c /\ a /\ b /\ d ==> e`] THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM] THEN REWRITE_TAC[IN_ELIM_THM]);; (*** Now replace quantifiers over real^3 with those over real^2 ***) e(PAD2D3D_TAC);; (*** Tidy the goal a little ***) e(REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP; GSYM CONJ_ASSOC]);; (*** Choose u1 as the origin ***) e(GEOM_ORIGIN_TAC `u1:real^2`);; (*** Rotate the point u2 onto the x-axis ***) e(GEOM_BASIS_MULTIPLE_TAC 1 `u2:real^2`);; (*** Only now introduce coordinates ***)