I want to prove "If a point lies on the interior of an angle, that angle is the sum of two smaller angles with legs that go through the given point"
Binyameen, don't know the answers to your questions, although it sounded like John did, but let me add some mathematical comments. 1) This is a hard result in axiomatic geometry, one that Euclid could not prove. I discuss how Hilbert's axioms handle this in my paper http://www.math.northwestern.edu/~richter/hilbert.pdf Just defining the interior of an angle requires serious Hilbert theory, and this is not done by Euclid or high school geometry texts. So this is a fine problem for you to be having. 2) Your ANGLES_ADD_BETWEEN come from hol_light/Multivariate/geom.ml: John Harrison said that Multivariate is about using geometry in the coordinate plane. So you should first ask how you would prove this in the plane. Do the math first and then worry about proof assistants. 3) My hol_light/Multivariate/geom.ml, obtained by subversion, says let ANGLES_ADD_BETWEEN = prove (`!A B C D:real^N. between C (A,B) /\ ~(D = A) /\ ~(D = B) ==> angle(A,D,C) + angle(C,D,B) = angle(A,D,B)`, I don't know where between is defined, but this result makes pretty good sense to me. It's similar to what in my paper is called the converse of the crossbal theorem. Start with a triangle ADB, and suppose that C lies in the open interval (A, B) of points between A and B. Then C is in the interior of angle ADB, so the measures should add up: mu(angle ADB) = mu(angle ADC) + mu(angle CDB). 4) You should think about how angle(A,D,B) is even defined. It must be something like this. Let D = (0,0), and A = (1,0), so B = (x, y) is essentially (cos theta, sin theta). Then angle(A,D,B) = theta, right? Let's simplify by saying that B is in the first quadrant, with theta in (0, pi/2). Well, tan theta = y/x, so theta = tan^{-1} (y/x) So John's definition is quite possibly angle((1,0),(0,0),(x,y)) = tan^{-1} (y/x) for x, y > 0. If you're willing to talk about directed angles, as Birkhoff did, then you can use this formula for x > 0, and the angle will be negative for y < 0. -- Best, Bill ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
