John, I'm finally responding to your Aug 31 post. I lifted a bold, clever
proof of TRIANGLE_ANGLE_SUM in Multivariate/geom.ml, although your actual proof
may be simpler. I ran your code below, and saw the goalstacks, but they didn't
help much, because it's really TRIANGLE_ANGLE_SUM_LEMMA I want. Below I'll
discuss the proof of that:
Even if you don't learn how to write procedural proofs, it wouldn't
be too hard for you to step through existing ones
step-by-step. [...] You can see the sequence of goals that gets
generated.
needs "Multivariate/geom.ml";;
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(REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
[`A:real^N = B`; `B:real^N = C`; `A:real^N = C`] THEN
ASM_SIMP_TAC[ANGLE_REFL_MID; ANGLE_REFL; REAL_HALF; REAL_ADD_RID] THEN
REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN
REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[REAL_ADD_LID; REAL_HALF]);;
e(REPEAT STRIP_TAC THEN MATCH_MP_TAC COS_MINUS1_LEMMA);;
e(ASM_SIMP_TAC[TRIANGLE_ANGLE_SUM_LEMMA; REAL_LE_ADD; ANGLE_RANGE]);;
e(MATCH_MP_TAC(REAL_ARITH
`&0 <= x /\ x <= p /\ &0 <= y /\ y <= p /\ &0 <= z /\ z <= p /\
~(x = p /\ y = p /\ z = p)
==> x + y + z < &3 * p`));;
e(ASM_SIMP_TAC[ANGLE_RANGE] THEN REPEAT STRIP_TAC);;
e(REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ANGLE_EQ_PI_DIST])));;
e(REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
[GSYM VECTOR_SUB_EQ])));;
e(REWRITE_TAC[GSYM NORM_EQ_0; dist; NORM_SUB] THEN REAL_ARITH_TAC);;
I worked out a proof using the theorems you cited in the proof of
TRIANGLE_ANGLE_SUM_LEMMA, but it occured to me afterwards that this may be
quite different from your proof. Anyway, I was shocked that this worked:
Let a, b & c be the three angles of a triangle. We want a + b + c = pi, and
that will follow from
cos(a + b + c) = - 1
I never would have tried to prove that, but using these results
COS_ADD : thm = |- !x y. cos (x + y) = cos x * cos y - sin x * sin y
SIN_ADD : thm = |- !x y. sin (x + y) = sin x * cos y + cos x * sin y
from transcendentals.ml, we have
cos(a + b + c) = cos(a) * cos(b + c) - sin(a) * sin(b + c)
=
cos(a) * cos(b) * cos(c) -
(cos(a) * sin(b) * sin(c) + sin(a) * cos(b) * sin(c) + sin(a) * sin(b) * cos(c))
Let x, y & z be the opposite sides of the angles a, b & c. Then by
LAW_OF_SINES,
sin(b) = y * sin(a) / x
sin(c) = z * sin(a) / x
cos(a) * sin(b) * sin(c) + sin(a) * cos(b) * sin(c) + sin(a) * sin(b) * cos(c)
=
sin^2(a) * (cos(a) * y * z / x^2 + cos(b) * z / x + cos(c) * y / x)
Now by SIN_CIRCLE
cos(a + b + c) = cos(a) * cos(b) * cos(c) -
(1 - cos^2(a)) / x^2 * (cos(a) * y * z + cos(b) * x * z + cos(c) * x * y)
Now we have a shot, because we only have cosines, and we can use vector
definition of angles,
ANGLE : thm =
|- !A B C.
(A - C) dot (B - C) = dist (A,C) * dist (B,C) * cos (angle (A,C,B))
Let's say the points are A, B and C next to the angles a, b and c. Then
cos(a) = (B - A) dot (C - A) / (y * z)
cos(b) = (A - B) dot (C - B) / (x * z)
cos(c) = (B - C) dot (A - C) / (x * y)
1 - cos^2(a) = (y^2 * z^2 - ((B - A) dot (C - A))^2) / (y^2 * z^2)
cos(a) * y * z = (B - A) dot (C - A)
cos(b) * x * z = (A - B) dot (C - B)
cos(c) * x * y = (B - C) dot (A - C)
(x^2 * y^2 * z^2) * cos(a + b + c)
=
(B - A) dot (C - A) * (A - B) dot (C - B) * (B - C) dot (A - C) -
(y^2 * z^2 - ((B - A) dot (C - A))^2) *
((B - A) dot (C - A) + (A - B) dot (C - B) + (B - C) dot (A - C))
By translating, we can make the simplification A = 0. Call d = B dot C. Then
B dot B = z^2
C dot C = y^2
x^2 = (C - B) dot (C - B) = y^2 + z^2 - 2 * d
Then we have
(x^2 * y^2 * z^2) * cos(a + b + c)
=
d * (z^2 - d) * (y^2 - d) - (y^2 * z^2 - d^2) * (d + z^2 - d + y^2 - d)
=
d * (z^2 - d) * (y^2 - d) + (d^2 - y^2 * z^2) * (y^2 + z^2 - d)
=
- y^2 * z^2 * (y^2 + z^2) + d * 2 * y^2 * z^2
=
- y^2 * z^2 * (y^2 + z^2 - 2 * d) = - y^2 * z^2 * x^2.
Thus cos(a + b + c) = -1, and this proves your TRIANGLE_ANGLE_SUM!!! I tried
your g & e stunts on TRIANGLE_ANGLE_SUM
g `!A B C:real^N. ~(A = B) /\ ~(A = C) /\ ~(B = C)
==> cos(angle(B,A,C) + angle(A,B,C) + angle(B,C,A)) = -- &1`;;
val it : goalstack = 1 subgoal (1 total)
`!A B C.
~(A = B) /\ ~(A = C) /\ ~(B = C)
==> cos (angle (B,A,C) + angle (A,B,C) + angle (B,C,A)) = -- &1`
e(REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
REWRITE_TAC[GSYM NORM_EQ_0] THEN
MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] LAW_OF_COSINES) THEN
MP_TAC(ISPECL [`B:real^N`; `A:real^N`; `C:real^N`] LAW_OF_COSINES) THEN
MP_TAC(ISPECL [`C:real^N`; `B:real^N`; `A:real^N`] LAW_OF_COSINES) THEN
MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] LAW_OF_SINES) THEN
MP_TAC(ISPECL [`B:real^N`; `A:real^N`; `C:real^N`] LAW_OF_SINES) THEN
MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `A:real^N`] LAW_OF_SINES) THEN
REWRITE_TAC[COS_ADD; SIN_ADD; dist; NORM_SUB]);;
`sin (angle (B,C,A)) * norm (A - C) = sin (angle (C,B,A)) * norm (A - B)
==> sin (angle (B,A,C)) * norm (A - C) = sin (angle (A,B,C)) * norm (B - C)
==> sin (angle (A,B,C)) * norm (B - C) = sin (angle (B,A,C)) * norm (A - C)
==> norm (A - B) pow 2 =
(norm (B - C) pow 2 + norm (A - C) pow 2) -
&2 * norm (B - C) * norm (A - C) * cos (angle (B,C,A))
==> norm (A - C) pow 2 =
(norm (A - B) pow 2 + norm (B - C) pow 2) -
&2 * norm (A - B) * norm (B - C) * cos (angle (A,B,C))
==> norm (B - C) pow 2 =
(norm (A - B) pow 2 + norm (A - C) pow 2) -
&2 * norm (A - B) * norm (A - C) * cos (angle (B,A,C))
==> ~(norm (A - B) = &0) /\ ~(norm (A - C) = &0) /\ ~(norm (B - C) = &0)
==> cos (angle (B,A,C)) *
(cos (angle (A,B,C)) * cos (angle (B,C,A)) -
sin (angle (A,B,C)) * sin (angle (B,C,A))) -
sin (angle (B,A,C)) *
(sin (angle (A,B,C)) * cos (angle (B,C,A)) +
cos (angle (A,B,C)) * sin (angle (B,C,A))) =
-- &1`
I can't see how to keep going with e, but I definitely see some similarity
between the e-output and my proof above. And some difference! I never used
the LAW_OF_COSINES! OK, I have to go think about this. So you may have a
simpler proof than mine. I still want to understand whether the Hilbert
betweenness of my proof is secretly appearing in your proof. I see that you
define sin & cos by complex power series, which is great, and that immediately
implies the COS_ADD and SIN_ADD, but not necessarily LAW_OF_SINES and
LAW_OF_COSINES...
I could not find where you defined REAL_ADD_LID. Here's my effort, plus a
similar effort that worked, which showed that REAL_ADD_RID is defined in
calc_int.ml, to be
REAL_ADD_RID : thm = |- !x. x + &0 = x
(poisson)hol_light> find . -name \*.ml -exec grep "REAL_ADD_LID = " {} \;
-print |m
let TREAL_ADD_LID = prove
./realax.ml
(poisson)hol_light> find . -name \*.ml -exec grep "REAL_ADD_RID = " {} \;
-print |m
let REAL_ADD_RID = prove
./calc_int.ml
let HREAL_ADD_RID = prove
./realax.ml
--
Best,
Bill
------------------------------------------------------------------------------
LogMeIn Central: Instant, anywhere, Remote PC access and management.
Stay in control, update software, and manage PCs from one command center
Diagnose problems and improve visibility into emerging IT issues
Automate, monitor and manage. Do more in less time with Central
http://p.sf.net/sfu/logmein12331_d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
