Screenshot instructions:
Windows
Mac
Red Hat Linux
Ubuntu
Click URL instructions:
Rightclick on ad, choose "Copy Link", then paste here →
(This may not be possible with some types of ads)
From: John Harrison <John.Harrison@cl...>  20120530 03:29:25

Hi Binyameen,  g`!(A:real^2) (B:real^2). angle (A,D,B) <= pi / &2 /\ angle (C,D,B) => &0  ==> angle (A,D,B) = angle (A,D,C) + angle (C,D,B)`;;   If we replace A with basis 1 (xaxis) then the configuration is illustrated  by the attached figure. Now if i use the above mentioned theorem then the  condition "between C (A,B)" appears. How can i remove this restriction? One approach would be to argue that you can scale C by a suitable amount so that it is between A and B. Here's your initial goal: g`!(A:real^2) (B:real^2). angle (A,D,B) <= pi / &2 /\ angle (C,D,B) >= &0 ==> angle (A,D,B) = angle (A,D,C) + angle (C,D,B)`;; If we start off by assuming without loss of generality that D is the origin: # e(GEOM_ORIGIN_TAC `D:real^2`);; val it : goalstack = 1 subgoal (1 total) `!A B C. angle (A,vec 0,B) <= pi / &2 /\ angle (C,vec 0,B) >= &0 ==> angle (A,vec 0,B) = angle (A,vec 0,C) + angle (C,vec 0,B)` then we can collapse things to use the basic "angle between two vectors" function: # e(REWRITE_TAC[angle; VECTOR_SUB_RZERO]);; val it : goalstack = 1 subgoal (1 total) `!A B C. vector_angle A B <= pi / &2 /\ vector_angle C B >= &0 ==> vector_angle A B = vector_angle A C + vector_angle C B` Now it should be possible to argue that there is some scaled version of C, say a % C, such that a % C is between A and B, then use theorems like VECTOR_ANGLE_LMUL and VECTOR_ANGLE_RMUL. However your theorem is not going to be quite true as stated because "angle" gives just the symmetric angle between two lines, not some kind of oriented angle, so it is in fact always in the range [0,pi]. One would need to formulate the hypothesis you want (that in some sense if you sweep out the angle from A to B with a ray from D then you pass through C) in a somewhat different fashion. It may not seem very natural in the context of elementary geometry, but in some situations where I have wanted to talk about this sort of orientation concept, I've used the complex numbers and their "Arg" (argument) function. For example, Arg((B  D) / (A  D)) is a possible definition of an "anticlockwise" angle from A to B about the point D, and there is a theorem VECTOR_ANGLE_ARG that relates the angle between two vectors w and z to the argument of the complex number z / w. Note that the nonnegativity of the imaginary part of z / w is one usable formulation of the kind of orientation property that you are after, and this controls how these two concepts relate to each other. The theorem ARG_LE_PI gives another formulation.  !w z. ~(w = Cx (&0)) /\ ~(z = Cx (&0)) ==> vector_angle w z = (if &0 <= Im (z / w) then Arg (z / w) else &2 * pi  Arg (z / w))) And then there are theorems like REAL_ADD_ARG that would allow you to figure out the compositions expressed in that way. So here would be one way of formulating and proving your theorem, hiding the complex numbers in an additional notion "anticlockwise", let anticlockwise = new_definition `anticlockwise D (A,B) <=> &0 <= Im((B  D) / (A  D))`;; let lemma = prove (`!(A:real^2) (B:real^2). ~collinear{A,D,B} /\ ~(C = D) /\ anticlockwise D (A,C) /\ anticlockwise D (C,B) /\ anticlockwise D (A,B) ==> angle (A,D,B) = angle (A,D,C) + angle (C,D,B)`, REWRITE_TAC[anticlockwise] THEN GEOM_ORIGIN_TAC `D:real^2` THEN REWRITE_TAC[angle; VECTOR_SUB_RZERO] THEN REPEAT GEN_TAC THEN ASM_CASES_TAC `A:real^2 = vec 0` THENL [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN ASM_CASES_TAC `B:real^2 = vec 0` THENL [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[COMPLEX_VEC_0] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[VECTOR_ANGLE_ARG] THEN SUBGOAL_THEN `B / A = (C / A) * (B / C)` SUBST1_TAC THENL [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD; ALL_TAC] THEN ASM_SIMP_TAC[ARG_MUL; COMPLEX_FIELD `~(w = Cx(&0)) /\ ~(z = Cx(&0)) ==> ~(w / z = Cx(&0))`] THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[GSYM ARG_LE_PI]) THEN FIRST_ASSUM(MP_TAC o MATCH_MP (REAL_ARITH `~(a + b < &2 * pi) ==> &0 <= a /\ &0 <= b /\ a <= pi /\ b <= pi ==> a = pi /\ b = pi`)) THEN ASM_REWRITE_TAC[ARG; ARG_EQ_PI] THEN DISCH_THEN(MP_TAC o MATCH_MP (TAUT `(a /\ b) /\ (c /\ d) ==> a /\ c`)) THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_MUL) THEN ASM_SIMP_TAC[REAL_EXISTS; COMPLEX_FIELD `~(A = Cx(&0)) /\ ~(C = Cx(&0)) ==> (C / A * B / C = z <=> B = z * A)`] THEN DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC) THEN ASM_MESON_TAC[INSERT_AC; COLLINEAR_LEMMA; COMPLEX_CMUL; COMPLEX_VEC_0]);; This isn't necessarily the definitively right way to formulate things, but it might give you some ideas to try out. John. 
From: John Harrison <John.Harrison@cl...>  20120530 17:06:10

Hi Bill,  I don't know where between is defined, but this result makes pretty good  sense to me. The definition of "between" can be found in "Multivariate/vectors.ml". There are several equivalent formulations, the first of which is the actual definition (bound to the OCaml name "between") between =  !a x b. between x (a,b) <=> dist(a,b) = dist(a,x) + dist(x,b) BETWEEN_IN_SEGMENT =  !x a b. between x (a,b) <=> x IN segment[a,b] BETWEEN_IN_CONVEX_HULL =  !x a b. between x (a,b) <=> x IN convex hull {a, b}  4) You should think about how angle(A,D,B) is even defined. Yes, this is arguably the problem. The "angle" function is defined (via "vector_angle" in the file "Multivariate/geom.ml") in a symmetrical way to be whichever of the two angles between two vectors is nonreflex, with degenerate cases mapped to pi/2.  vector_angle x y = if x = vec 0 \/ y = vec 0 then pi / &2 else acs((x dot y) / (norm x * norm y)))  angle(a,b,c) = vector_angle (a  b) (c  b) For some purposes, it would be more useful or natural to use directed angles. There isn't much infrastructure set up so far about directed angles, though there are two possible ways of getting them via complex functions, either the argument function with 0 <= Arg(z) < 2 pi or the imaginary part of the complex logarithm with pi <= Im(clog z) < pi. These would be angles w.r.t. the positive xaxis, but then you can get the angle between two vectors w and z by considering the complex quotient w/z or z/w. John. 
From: Bill Richter <richter@ma...>  20120531 03:38:43

Thanks, John! I'll just add that this is Birkhoff's definition between =  !a x b. between x (a,b) <=> dist(a,b) = dist(a,x) + dist(x,b) used in Moise's & Venema's geometry books, and The "angle" function is defined (via "vector_angle" in the file "Multivariate/geom.ml") in a symmetrical way to be whichever of the two angles between two vectors is nonreflex This is Hilbert's definition, also used by Moise & Venema, and For some purposes, it would be more useful or natural to use directed angles. Only Birkhoff did this, and his directed angle caused him a lot of trouble. Birkhoff's 1932 Annals paper used an axiom saying some function is continuous in order to deal with a directed angle problem (the triangle angles are either all clock or all counterclockwise), and it took an erratum and a paper by MacLane 20 years later to prove this. So I think you have the right definition.  Best, Bill 