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 (x-axis) 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.
------------------------------------------------------------------------------
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
