Freek, your advice about exec GOAL_TAC; p();; helped me solve a
skeleton error that was really bugging me (fixed code below), and I
think you taught me something really valuable about variable scope.
I thought we could rebind variables (with consider) in the body of a
proof environment, and I realized we can't. So my proof worked fine
after I changed the conflicting variable names. Look at this snippet:
consider a' b' such that
O IN a' /\ A IN a' /\ O IN b' /\B IN b' /\
~(D IN a') /\ ~(D IN b') /\
D,B same_side a' /\ D,A same_side b' [existsa'b'] by H2, InteriorAngle_DEF;
a' = a /\ b' = b by Distinct, a_OA, b_OB, existsa'b', I1;
[...]
~(D int_angle B,O,A') [notD_BOA']
proof
assume D int_angle B,O,A';
consider a' b' such that
O IN a' /\ A' IN a' /\ O IN b' /\B IN b' /\
~(D IN a') /\ ~(D IN b') /\
D,B same_side a' /\ D,A' same_side b' [X1] by -, InteriorAngle_DEF;
exec GOAL_TAC;
b' = b by Distinct, b_OB, X1, I1;
~(D IN b) /\ D,A' same_side b by -, X1;
qed by -;
I got a skeleton error on the line before exec GOAL_TAC;.
You can see the problem right off, but I realize it after
p();;
1 [`D int_angle A,O,B`] (H2)
2 [`Between (A,O,A')`] (H3)
3 [`~(A = O) /\ ~(A = B) /\ ~(O = B)`] (Distinct)
4 [`O IN a /\ A IN a`] (a_OA)
5 [`O IN b /\ B IN b`] (b_OB)
6 [`~(A IN b)`] (notAb)
7 [`~(B IN a)`] (notBa)
8 [`~(a = b)`]
9 [`b INTER a = {O}`] (ab_O)
10 [`A' IN a`] (A'a)
11 [`A' IN a DELETE O`]
12 [`~(A' IN b)`] (notA'b)
13 [`~(A,A' same_side b)`] (Ansim_bA')
14 [`O IN a' /\
A IN a' /\
O IN b' /\
B IN b' /\
~(D IN a') /\
~(D IN b') /\
D,B same_side a' /\
D,A same_side b'`] (existsa'b')
15 [`a' = a /\ b' = b`]
16 [`~(D IN a) /\ ~(D IN b) /\ D,B same_side a /\ D,A same_side b`] (DintAOB)
17 [`~(D,A' same_side b)`]
18 [`D int_angle B,O,A'`]
`F`
I thought wait a minute, why are a' & b' bindings still active???
So I changed the variables to alpha & beta, and now I get
18 [`D int_angle B,O,A'`]
19 [`O IN alpha /\
A' IN alpha /\
O IN beta /\
B IN beta /\
~(D IN alpha) /\
~(D IN beta) /\
D,B same_side alpha /\
D,A' same_side beta`] (X1)
Thanks for the tip!!!
Now I proved my theorem
InteriorReflectionInterior_THM : thm =
|- !A O B D A'.
~Collinear (A,O,B)
==> D int_angle A,O,B
==> Between (A,O,A')
==> B int_angle D,O,A'
with the code below, which you can paste after my code yesterday.
--
Best,
Bill
let InteriorReflectionInterior_THM = thm `;
let A O B D A' be point;
assume ~Collinear(A, O, B) [H1];
assume D int_angle A,O,B [H2];
assume Between(A, O, A') [H3];
thus B int_angle D,O,A'
proof
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1,
NonCollinearImpliesDistinct_THM;
consider a such that
O IN a /\ A IN a [a_OA] by Distinct, I1;
consider b such that
O IN b /\ B IN b [b_OB] by Distinct, I1;
~(A IN b) [notAb] by b_OB, H1, Collinear_DEF;
~(B IN a) [notBa] by a_OA, H1, Collinear_DEF;
~(a = b) by -, b_OB;
b INTER a = {O} [ab_O] by -, a_OA, b_OB, Line01infinity_THM;
A' IN a [A'a] by H3, B1, Collinear_DEF, a_OA, Distinct, CollinearLinear_THM;
A' IN a DELETE O by A'a, H3, B1, IN_DELETE;
~(A' IN b) [notA'b] by ab_O, -, EquivIntersectionHelp_THM;
~(A,A' same_side b) [Ansim_bA'] by b_OB, H3, same_side_DEF ;
consider a' b' such that
O IN a' /\ A IN a' /\ O IN b' /\B IN b' /\
~(D IN a') /\ ~(D IN b') /\
D,B same_side a' /\ D,A same_side b' [existsa'b'] by H2, InteriorAngle_DEF;
a' = a /\ b' = b by Distinct, a_OA, b_OB, existsa'b', I1;
~(D IN a) /\ ~(D IN b) /\
D,B same_side a /\ D,A same_side b [DintAOB] by -, existsa'b';
:: ~(D = A') [notDA'] by DintAOB, A'a;
~(D,A' same_side b) [Dnsim_bA']
proof
assume D,A' same_side b;
A',D same_side b by DintAOB, notA'b, -, SameSideSymmetricRelation_THM,
Symmetric_relation_DEF;
A',A same_side b by DintAOB, notA'b, notAb, -,
SameSideTransitiveRelation_THM, Transitive_relation_DEF;
A,A' same_side b by notA'b, notAb, -, SameSideSymmetricRelation_THM,
Symmetric_relation_DEF;
F by -, Ansim_bA';
qed by -;
~(D int_angle B,O,A') [notD_BOA']
proof
assume D int_angle B,O,A';
consider beta such that
O IN beta /\B IN beta /\ D,A' same_side beta [exists_beta] by -,
InteriorAngle_DEF;
beta = b by Distinct, b_OB, exists_beta, I1;
D,A' same_side b [D_BOA'] by -, exists_beta;
F by -, Dnsim_bA';
qed by -;
~Collinear (D,O,B) [DOB_noncol] by Distinct, b_OB, I1, DintAOB,
Collinear_DEF;
~(O = A') by H3, B1;
B int_angle D,O,A' by -, a_OA, A'a, DintAOB, notBa, DOB_noncol, notD_BOA',
AngleOrdering_THM;
qed by -`;;
------------------------------------------------------------------------------
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
