What if you quote H1, H2 and all of the theorems that you
ultimately quoted in the final proof as arguments to "by"? Does
miz3 "by" then get it in one step? That's the true test.
Michael, here's my best example of passing your test. Miz3 verified this
1-line proof
let Line01infinity2_THM = thm `;
let X be point;
let l m be point_set;
assume Line l /\ Line m [H0];
assume ~(l = m) [H1];
assume X IN l /\ X IN m [H2];
thus l INTER m = {X}
by H0, H1, H2, IN_INTER, BiggerThanSingleton_THM, I1`;;
with timeout = 8000 and a MESON `solved at' number of 175 million. I'm having
trouble believing that, so let me paste the output from my ocaml/Hol-Light/miz3
window:
0..0..2..4..12..22..36..61..86..113..245..443..836..1561..3024..6996..15441..39903..102450..283181..757604..2266961..6222938..18678485..53548684..160275297..solved
at 175311305
val Line01infinity2_THM : thm =
|- !X l m.
Line l /\ Line m
==> ~(l = m)
==> X IN l /\ X IN m
==> l INTER m = {X}
I'm working on a Dell Linux box with a 2.4GHz Intel Xeon CPU and almost 4Gb of
RAM (isn't that what MemTotal: 3920424 kB in /proc/meminfo means?) and
it took almost 3 hours. I do not know how to run a background Hol-Light job
that prints data to a file. If anyone wants to replicate my experiment on a
faster machine, that would be nice. Below is my file of my first 26 theorems
with 1-line proofs, all of which miz3 verified.
Australia's favourite bat-and-ball game is cricket...
I like the cricket scene at the end of the movie "Bend it like Beckham", but I
don't know much about the game. Can I conclude that, like in baseball, you
want to hit the ball on the sweet spot of the bat? My son, who understands my
Hilbert code, was a good fastball hitter in 4th grade, and one time he hit a
double over the outfielders' heads, suprising the heck out of me. Another dad
said that's what happens when you hit the sweet spot.
--
Best,
Bill
horizon := 0;;
timeout := 8000;;
new_type("point",0);;
new_type_abbrev("point_set",`:point->bool`);;
new_constant("Between",`:point->point->point->bool`);;
new_constant("Line",`:point_set->bool`);;
new_constant("===",`:(point->bool)->(point->bool)->bool`);;
parse_as_infix("cong",(12, "right"));;
parse_as_infix("same_side",(12, "right"));;
parse_as_infix("===",(12, "right"));;
parse_as_infix("<_seg",(12, "right"));;
parse_as_infix("<_ang",(12, "right"));;
parse_as_infix("Suppl",(12, "right"));;
parse_as_infix("NOTIN",(11, "right"));;
let NOTIN = new_definition
`!a:A l:A->bool. a NOTIN l <=> ~(a IN l)`;;
let Interval_DEF = new_definition
`! A B X. open (A,B) X <=> Between A X B`;;
let Collinear_DEF = new_definition
`Collinear A B C <=>
? l. Line l /\ A IN l /\ B IN l /\ C IN l`;;
let SameSide_DEF = new_definition
`A,B same_side l <=>
Line l /\ ~(? X. (X IN l) /\ X IN open (A,B))`;;
let Ray_DEF = new_definition
`! A B X. ray A B X <=> ~(A = B) /\ Collinear A B X /\ A NOTIN open (X,B)`;;
let Ordered_DEF = new_definition
`ordered A B C D <=>
B IN open (A,C) /\ B IN open (A,D) /\ C IN open (A,D) /\ C IN open (B,D)`;;
let InteriorAngle_DEF = new_definition
`! A O B P.
int_angle A O B P <=> ~Collinear A O B /\ ? a b.
Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\
P NOTIN a /\ P NOTIN b /\ P,B same_side a /\ P,A same_side b`;;
let InteriorTriangle_DEF = new_definition
`! A B C P.
int_triangle A B C P <=>
P IN int_angle A B C /\ P IN int_angle B C A /\ P IN int_angle C A B`;;
let Tetralateral_DEF = new_definition
`Tetralateral A B C D <=>
~(A = B) /\ ~(A = C) /\ ~(A = D) /\ ~(B = C) /\ ~(B = D) /\ ~(C = D) /\
~Collinear A B C /\ ~Collinear B C D /\ ~Collinear C D A /\ ~Collinear D A
B`;;
let Quadrilateral_DEF = new_definition
`Quadrilateral A B C D <=>
Tetralateral A B C D /\
open (A,B) INTER open (C,D) = {} /\
open (B,C) INTER open (D,A) = {} `;;
let ConvexQuad_DEF = new_definition
`ConvexQuadrilateral A B C D <=>
Quadrilateral A B C D /\
A IN int_angle B C D /\ B IN int_angle C D A /\ C IN int_angle D A B /\ D IN
int_angle A B C `;;
let Segment_DEF = new_definition
`seg A B = {A, B} UNION open (A,B)`;;
let SEGMENT = new_definition
`Segment s <=> ? A B. s = seg A B /\ ~(A = B)`;;
let SegmentOrdering_DEF = new_definition
`s <_seg t <=>
Segment s /\
? C D X. t = seg C D /\ X IN open (C,D) /\ s === seg C X`;;
let Angle_DEF = new_definition
` angle A O B = ray O A UNION ray O B `;;
let ANGLE = new_definition
`Angle alpha <=> ? A O B. alpha = angle A O B /\ ~Collinear A O B`;;
let AngleOrdering_DEF = new_definition
`alpha <_ang beta <=>
Angle alpha /\
? A O B G. ~Collinear A O B /\ beta = angle A O B /\
G IN int_angle A O B /\ alpha === angle A O G`;;
let RAY = new_definition
`Ray r <=> ? O A. ~(O = A) /\ r = ray O A`;;
let TriangleCong_DEF = new_definition
`! A B C A' B' C' :point. (A, B, C) cong (A', B', C') <=>
~Collinear A B C /\ ~Collinear A' B' C' /\
seg A B === seg A' B' /\ seg A C === seg A' C' /\ seg B C === seg B' C' /\
angle A B C === angle A' B' C' /\
angle B C A === angle B' C' A' /\
angle C A B === angle C' A' B'`;;
let SupplementaryAngles_DEF = new_definition
`! alpha beta. alpha Suppl beta <=>
? A O B A'. ~Collinear A O B /\ O IN open (A,A') /\ alpha = angle A O B
/\ beta = angle B O A'`;;
let RightAngle_DEF = new_definition
`! alpha. Right alpha <=> Angle alpha /\
? beta. alpha Suppl beta /\ alpha === beta`;;
let PlaneComplement_DEF = new_definition
`! A:point alpha:point_set. complement alpha P <=> P NOTIN alpha`;;
let CONVEX = new_definition
`Convex alpha <=> ! A B. A IN alpha /\ B IN alpha ==> open (A,B) SUBSET
alpha`;;
(* ----------------------------------------------------------------- *)
(* The axioms. *)
(* ----------------------------------------------------------------- *)
let I1 = new_axiom
`! A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;;
let I2 = new_axiom
`! l. ? A B. Line l /\ A IN l /\ B IN l /\ ~(A = B)`;;
let I3 = new_axiom
`? A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
~Collinear A B C`;;
let B1 = new_axiom
`! A B C. Between A B C ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
Between C B A /\ Collinear A B C`;;
let B2 = new_axiom
`! A B. ~(A = B) ==> ? C. Between A B C`;;
let B3 = new_axiom
`! A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear A B C
==> (Between A B C \/ Between B C A \/ Between C A B) /\
~(Between A B C /\ Between B C A) /\
~(Between A B C /\ Between C A B) /\
~(Between B C A /\ Between C A B)`;;
let B4 = new_axiom
`! l A B C. Line l /\ ~Collinear A B C /\
A NOTIN l /\ B NOTIN l /\ C NOTIN l /\
(? X. X IN l /\ Between A X C) ==>
(? Y. Y IN l /\ Between A Y B) \/ (? Y. Y IN l /\ Between B Y C)`;;
let C1 = new_axiom
`! s O Z. Segment s /\ ~(O = Z) ==>
?! P. P IN ray O Z DELETE O /\ seg O P === s`;;
let C2Reflexive = new_axiom
`Segment s ==> s === s`;;
let C2Symmetric = new_axiom
`Segment s /\ Segment t /\ s === t ==> t === s`;;
let C2Transitive = new_axiom
`Segment s /\ Segment t /\ Segment u /\
s === t /\ t === u ==> s === u`;;
let C3 = new_axiom
`! A B C A' B' C'. B IN open (A,C) /\ B' IN open (A',C') /\
seg A B === seg A' B' /\ seg B C === seg B' C' ==>
seg A C === seg A' C'`;;
let C4 = new_axiom
`! alpha O A l Y. Angle alpha /\ ~(O = A) /\ Line l /\ O IN l /\ A IN l /\
Y NOTIN l ==>
?! r. Ray r /\ ? B. ~(O = B) /\ r = ray O B /\ B NOTIN l /\ B,Y same_side l
/\
angle A O B === alpha`;;
let C5Reflexive = new_axiom
`Angle alpha ==> alpha === alpha`;;
let C5Symmetric = new_axiom
`Angle alpha /\ Angle beta /\ alpha === beta ==> beta === alpha`;;
let C5Transitive = new_axiom
`Angle alpha /\ Angle beta /\ Angle gamma /\
alpha === beta /\ beta === gamma ==> alpha === gamma`;;
let C6 = new_axiom
`! A B C A' B' C'. ~Collinear A B C /\ ~Collinear A' B' C' /\
seg B A === seg B' A' /\ seg B C === seg B' C' /\ angle A B C === angle A'
B' C'
==> angle B C A === angle B' C' A'`;;
(* ----------------------------------------------------------------- *)
(* Theorems. *)
(* ----------------------------------------------------------------- *)
let B1' = thm `;
! A B C. B IN open (A,C) ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
B IN open (C,A) /\ Collinear A B C
by IN, Interval_DEF, B1`;;
let B2' = thm `;
! A B. ~(A = B) ==> ? C. B IN open (A,C)
by IN, Interval_DEF, B2`;;
let B3' = thm `;
! A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear A B C
==> (B IN open (A,C) \/ C IN open (B,A) \/ A IN open (C,B)) /\
~(B IN open (A,C) /\ C IN open (B,A)) /\
~(B IN open (A,C) /\ A IN open (C,B)) /\
~(C IN open (B,A) /\ A IN open (C,B))
by IN, Interval_DEF, B3`;;
let B4' = thm `;
! l A B C. Line l /\ ~Collinear A B C /\
A NOTIN l /\ B NOTIN l /\ C NOTIN l /\
(? X. X IN l /\ X IN open (A,C)) ==>
(? Y. Y IN l /\ Y IN open (A,B)) \/ (? Y. Y IN l /\ Y IN open (B,C))
by B4, IN, Interval_DEF`;;
let B4'' = thm `;
let l be point_set;
let A B C be point;
assume Line l [H0];
assume ~Collinear A B C /\ A NOTIN l /\ B NOTIN l /\ C NOTIN l [H1];
assume A,B same_side l /\ B,C same_side l [H2];
thus A,C same_side l
by H0, H1, H2, B4', IN, SameSide_DEF`;;
let BiggerThanSingleton_THM = thm `;
let p be A->bool;
let x be A;
assume x IN p [H1];
assume ~(p = {x}) [H2];
thus ? a . a IN p /\ ~(a = x)
by H1, H2, SING_SUBSET, SUBSET_ANTISYM, SUBSET, NOTIN, IN_SING`;;
let DisjointOneNotOther_THM = thm `;
let x be A;
let l m be A->bool;
assume l INTER m = {} [H1];
assume x IN m [H2];
thus x NOTIN l
proof
qed by H1, H2, NOTIN, IN_INTER, NOT_IN_EMPTY`;;
let IntersectionSingletonOneNotOther_THM = thm `;
let e x be A;
let l m be A->bool;
assume l INTER m = {x} [H1];
assume e IN l [H2];
assume ~(e = x) [H3];
thus e NOTIN m
by H1, H2, H3, NOTIN, IN_INTER, IN_SING`;;
let EquivIntersectionHelp_THM = thm `;
let e x be A;
let l m be A->bool;
assume l INTER m = {x} [H1];
assume e IN m DELETE x [H2];
thus e NOTIN l
by H1, H2, NOTIN, IN_DELETE, IntersectionSingletonOneNotOther_THM`;;
let SubsetTensor_THM = thm `;
let a b s be A->bool;
assume a SUBSET b [H1];
thus a INTER s SUBSET b INTER s /\ s INTER a SUBSET s INTER b
by H1, INTER_SUBSET, SUBSET_TRANS, SUBSET_INTER`;;
let NonemptySubsetSing_THM = thm `;
let a be A;
let l be A->bool;
assume ~(l = {}) [H1];
assume l SUBSET {a} [H2];
thus a IN l
by H1, H2, MEMBER_NOT_EMPTY, SUBSET, IN_SING`;;
let CollinearSymmetry_THM = thm `;
let A B C be point;
assume Collinear A B C [H1];
thus Collinear A C B /\ Collinear B A C /\ Collinear B C A /\
Collinear C A B /\ Collinear C B A
by H1, Collinear_DEF`;;
let OnePointImpliesAnother_THM = thm `;
let P be point;
thus ? Q:point. ~(Q = P)
by I3`;;
let ExistsPointOffLine_THM = thm `;
let l be point_set;
assume Line l [H1];
thus ? Q:point. Q NOTIN l
by H1, I3, NOTIN, Collinear_DEF`;;
let BetweenLinear_THM = thm `; ::solved at 849,716
let A B C be point;
let m be point_set;
assume Line m /\ A IN m /\ C IN m [H1];
assume B IN open (A,C) \/ C IN open (B,A) \/ A IN open (C,B) [H2];
thus B IN m
by H1, H2, B1', Collinear_DEF, I1`;;
let CollinearLinear_THM = thm `;
let A B C be point;
let m be point_set;
assume Line m /\ A IN m /\ C IN m [H1];
assume Collinear A B C \/ Collinear B C A \/ Collinear C A B [H2];
assume ~(A = C) [H3];
thus B IN m
by H1, H2, H3, Collinear_DEF, I1`;;
let SameSideDisjointIntersection_THM = thm `;
! l A B. Line l ==>
(A,B same_side l <=> open (A,B) INTER l = {})
by IN_INTER, SameSide_DEF, MEMBER_NOT_EMPTY`;;
let NonCollinearImpliesDistinct_THM = thm `; ::solved at 1,050,293
let A B C be point;
assume ~Collinear A B C [H1];
thus ~(A = B) /\ ~(A = C) /\ ~(B = C)
by H1, OnePointImpliesAnother_THM, I1, Collinear_DEF`;;
let OpenIntervalSubsetLine_THM = thm `;
let A B be point;
let l be point_set;
assume Line l /\ A IN l /\ B IN l [H1];
thus open (A,B) SUBSET l
by H1, BetweenLinear_THM, SUBSET`;;
let SameSideDisjointLines_THM = thm `;
let l m be point_set;
let A B be point;
assume Line m /\ A IN m /\ B IN m [m_line];
assume Line l [l_line];
assume m INTER l = {} [Disjoint];
thus A NOTIN l /\ B NOTIN l /\ A,B same_side l
by m_line, l_line, Disjoint, IN_INTER, MEMBER_NOT_EMPTY, NOTIN,
OpenIntervalSubsetLine_THM, SubsetTensor_THM, SUBSET_EMPTY,
SameSideDisjointIntersection_THM`;;
let Reverse4Order_THM = thm `;
let A B C D be point;
assume ordered A B C D [H1];
thus ordered D C B A
by H1, Ordered_DEF, B1'`;;
let OriginInRay_THM = thm `;
let O Q be point;
assume ~(Q = O) [H1];
thus O IN ray O Q
by H1, B1', NOTIN, I1, Collinear_DEF, IN, Ray_DEF`;;
let EndpointInRay_THM = thm `;
let O Q be point;
assume ~(Q = O) [H1];
thus Q IN ray O Q
by H1, B1', NOTIN, I1, Collinear_DEF, IN, Ray_DEF`;;
let Line01infinity2_THM = thm `;
let X be point;
let l m be point_set;
assume Line l /\ Line m [H0];
assume ~(l = m) [H1];
assume X IN l /\ X IN m [H2];
thus l INTER m = {X}
by H0, H1, H2, IN_INTER, BiggerThanSingleton_THM, I1`;;
let SameSideLinesIntersect1Point_THM = thm `; :: #2 timeout at 26,338,897
on a slow machine
let A B X be point;
let l m be point_set;
assume Line l /\ Line m [H0];
assume l INTER m = {X} [H1];
assume A IN m DELETE X /\ B IN m DELETE X [H2];
assume ~(A,B same_side l) [H3];
thus A NOTIN l /\ B NOTIN l /\ X IN open (A,B)
:: proof
:: A NOTIN l /\ B NOTIN l [notABl] by H1, H2, EquivIntersectionHelp_THM;
:: A IN m /\ B IN m /\ ~(A = X) /\ ~(B = X) [H2'] by H2, IN_DELETE;
:: ~(open (A,B) INTER l = {}) [nonempty] by H0, H3,
SameSideDisjointIntersection_THM;
:: open (A,B) SUBSET m [ABm] by H0, H2', OpenIntervalSubsetLine_THM;
:: open (A,B) INTER l SUBSET {X} by -, SubsetTensor_THM, H1, INTER_COMM;
:: X IN open (A,B) INTER l by nonempty, -, NonemptySubsetSing_THM;
:: qed by notABl, -, IN_INTER
by H0, H1, H2, H3, EquivIntersectionHelp_THM, IN_DELETE,
SameSideDisjointIntersection_THM, OpenIntervalSubsetLine_THM, SubsetTensor_THM,
INTER_COMM, NonemptySubsetSing_THM, IN_INTER`;;
------------------------------------------------------------------------------
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
