I made my Hilbert axiomatic geometry code more readable, but code that
ran in 1:07 minutes now runs in 2:15 minutes. I sure enjoyed myself!
Perhaps this is an interface issue of the sort Mark & Felix raised.
I'd like to be able to write != or <> to mean "not equal" and have it
work fine, so that e.g. miz3 would know that ~(x = y) is the same as x
<> y, and if my thesis is
(x = y) \/ alpha
I could prove it by first making the assumption
x <> y
and then proving alpha. I tried this for IN, defining NOTIN by
let NOTIN = new_definition
`!a:A l:A->bool. a NOTIN l <=> ~(a IN l)`;;
I had to make massive changes to get away with this, and it was fun,
as I improved some sub-optimal old proofs, but I don't like this:
let Interval2sides2aLineHelp_THM = thm `;
let A B C X be point;
let l be point_set;
assume ¬(A = B) ∧ ¬(A = C) ∧ ¬(A = X) ∧ ¬(B = C) ∧ ¬(B = X) ∧ ¬(C = X)
[H1];
assume Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l ∧ X ∈ l [H2];
assume B ∈ open (A,C) [H3];
thus X ∉ open (A,B) ∨ X ∉ open (B,C)
proof
assume ¬(X ∉ open (A,B));
X ∈ open (A,B) [X_AB] by -, ∉;
Collinear X B C [XBCcol] by H2, Collinear_DEF;
ordered A X B C [AXBC] by X_AB, H3, TransitivityBetweennessVariant_THM;
B ∈ open (X,C) [B_XC] by AXBC, Ordered_DEF;
X ∉ open (C,B) by H1, XBCcol, B_XC, B3', ∉;
qed by -, B1', ∉`;;
It would be nice to replace the first two lines of my proof with
assume X ∈ open (A,B) [X_AB];
As another interface issue, I find my concrete syntax here, which
Emacs pre-processes (turning ∉ to NOTIN), to be improve readability.
Anyway, I'm happy, I've basically formalized the first 6 sections of
my paper, and so I only have one left to formalize, the hardest, which
treats Hartshorne's book, and I'm over 2700 lines of code!
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
--
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
