Hi Bill,
| Thanks for the responses! Can someone look at the code I posted
| http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar
| and tell me how to turn it into nice HOL code? Or post a different
| axiom-proof example? There's no relevant example in the HOL dox.
There are two different issues, I suppose: first setting up the
axiomatic basis, and secondly actually doing the proofs. I'll comment
a bit more on setting up the axioms below. For the proofs, you already
have scripts in Mizar, and this style seems better suited to the
domain, so you may want to consider using one of the "Mizar Light"
like systems within HOL Light (see reply from Freek in the other
thread). There is already lots of interesting work going on in
Edinburgh on formalizing geometry using HOL Light, which indeed uses
Mizar Light. I'll leave those involved to tell you more details, but
you can find the following recent papers online by Phil Scott and
Jacques Fleuriot:
"An Investigation of Hilbert's Implicit Reasoning Through
Proof Discovery in Idle Time" (ADG 2010)
"Composable Discovery Engines for Interactive Theorem Proving"
(ITP 2011)
| Lorenzo, I'd be delighted to see your Tarski geometry code, but if you
| could explain how to do it on the group, that might be even better.
I didn't see this email, but it sounds interesting.
| Roger, if there's ``some cultural aversion to the use of axioms in the
| HOL community,'' then maybe HOL isn't the right proof-checker to use
| in high school geometry classes. Does anyone think there is a better
| proof-checker? My guess is that this is just an interface problem
| that HOL could easily solve, and I'm willing to work on it myself.
It's not so much that HOL prevents you from reasoning axiomatically if
you want to, merely that the "house style" is to build up everything
definitionally. In fact, this was one of the features that
distinguished HOL from its LCF-like predecessors.
As Makarius suggested, one approach is to make all your theorems
hypothetical with the "axioms" as the antecedent of an implication.
This could be done, but since HOL Light doesn't have any built-in
module or sectioning mechanism, you would need to set up a bit of
machinery yourself to avoid seeing these assumptions pop up in a few
places.
Another approach, which would work more smoothly in HOL Light at
least, is to set up a new type isomorphic to some specific model, but
then merely derive the axioms and thereafter reason from them alone,
never looking back at the respresentation. (Rather as one might
consider real numbers as being Dedekind cuts but then never look back
at the definitions once the complete ordered field axioms are
derived.) This is not unlike what you have done in Mizar already, as
noted in this comment:
:: In Mizar it isn't possible to define such a type (or model) without
:: proving that some model exist
It would be pretty easy to prove most of the axioms for real^2 based
on the theory already there in the "Multivariate/..." theories. Then
the process of setting up a new type corresponding to it is a little
bit technical but basically straightforward. For example, here is a
possible start:
(* ----------------------------------------------------------------------- *)
(* Define a new type "Plane" in bijection with real^2. *)
(* ----------------------------------------------------------------------- *)
needs "Multivariate/determinants.ml";;
let Plane_TYBIJ =
let th = prove(`?x:real^2. T`,REWRITE_TAC[]) in
let def = new_type_definition "Plane" ("planify","coords") th in
REWRITE_RULE[] def;;
(* ----------------------------------------------------------------------- *)
(* Define notions of congruence and between-ness as Euclidean equivalents. *)
(* ----------------------------------------------------------------------- *)
parse_as_infix("===",(12, "right"));;
let Congruent_DEF = new_definition
`a,b === c,d <=> dist(coords a,coords b) = dist(coords c,coords d)`;;
let Between_DEF = new_definition
`Between (a,b,c) <=> between (coords b) (coords a,coords c)`;;
(* ----------------------------------------------------------------------- *)
(* Simple tactic to switch variables from "Plane" to "real^2". *)
(* ----------------------------------------------------------------------- *)
let PLANE_COORD_TAC =
let PLANE_QUANT_THM = MESON[Plane_TYBIJ]
`((!x. P x) <=> (!x. P(planify x))) /\
((?x. P x) <=> (?x. P(planify x)))`
and PLANE_EQ_THM = MESON[Plane_TYBIJ] `planify x = planify y <=> x = y` in
REWRITE_TAC[PLANE_QUANT_THM; Congruent_DEF; Between_DEF; PLANE_EQ_THM;
Plane_TYBIJ];;
(* ----------------------------------------------------------------------- *)
(* Derivation of the axioms. *)
(* ----------------------------------------------------------------------- *)
let AXIOM_1 = prove
(`!a b. a,b === b,a`,
PLANE_COORD_TAC THEN NORM_ARITH_TAC);;
let AXIOM_2 = prove
(`!a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s`,
PLANE_COORD_TAC THEN NORM_ARITH_TAC);;
let AXIOM_3 = prove
(`!a b c. a,b === c,c ==> a = b`,
PLANE_COORD_TAC THEN NORM_ARITH_TAC);;
let AXIOM_4 = prove
(`!a q b c. ?x. Between(q,a,x) /\ a,x === b,c`,
PLANE_COORD_TAC THEN GEOM_ORIGIN_TAC `a:real^2` THEN REPEAT GEN_TAC THEN
REWRITE_TAC[DIST_0] THEN ASM_CASES_TAC `q:real^2 = vec 0` THENL
[ASM_SIMP_TAC[BETWEEN_REFL; VECTOR_CHOOSE_SIZE; DIST_POS_LE];
EXISTS_TAC `--(dist(b:real^2,c) / norm(q) % q):real^2` THEN
REWRITE_TAC[between; DIST_0] THEN
REWRITE_TAC[dist; NORM_MUL; NORM_NEG; REAL_ABS_DIV; REAL_ABS_NORM;
VECTOR_ARITH `q - --(a % q) = (&1 + a) % q`] THEN
CONJ_TAC THENL
[MATCH_MP_TAC(REAL_RING `a = &1 + b ==> a * q = q + b * q`) THEN
SIMP_TAC[REAL_ABS_REFL; REAL_POS; REAL_LE_ADD; REAL_LE_DIV;
NORM_POS_LE];
ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0]]]);;
... etc.
| Most of what I know about HOL is that Tom Hales really fired me about
| in his Notices article. Have you read Tom's article
| www.math.pitt.edu/~thales/papers/turing.pdf
| His focus seems quite different from mine. I'd like to use
| proof-checkers to rigorize human proofs, starting with high school
| geometry.
This is an interesting and ambitious goal! There has been some use of
theorem proving technology in teaching at the graduate and even the
undergraduate level, e.g.
@INPROCEEDINGS{szczerba-mizar,
author = "Les{\l}aw W. Szczerba",
title = "The use of {M}izar {MSE} in a course in foundations
of geometry",
booktitle = "Initiatives in logic",
editor = "Jan Srzednicki",
publisher = "M. Nijhoff",
series = "Reason and argument series",
volume = 2,
year = 1989}
But I'm not aware of any similar activities at the high-school level.
Two somewhat related things I do know about that might be of some
interest are:
* Michael Beeson's MathXpert, which is a computer algebra system that
emphasizes rigorous proof, aimed at the education sector.
* Some experiments in Finland (e.g. by Ralph Back and Jockum von Wright)
on teaching high-school proofs in a more structured formal way.
| I've been appalled for some time at the lack of rigor in my
| subject, homotopy theory, and even got a paper published
|
http://www.ams.org/journals/proc/2009-137-07/S0002-9939-09-09763-9/S0002-9939-09-09763-9.pdf
| fixing a longstanding error, and my first paragraph reads
|
| We find this to be a serious pedagogical gap and give combinatorial
| proofs here.
Interesting! I don't have permission to actually view the paper online,
so I can't see the details right now, but I'll try to look it up later.
| I'd like proof-checkers like HOL to improve the rigor level of
| theorems that are much simpler that Tom's Kepler conjecture proof.
| Tom's focus instead seems to be realizing Turing's AI dreams, and he
| looks forward to the days of million page proofs churned out by the
| computer, about which we can only understand `fables' which maybe are
| churned out by the computer as well. Then he laments that cosmic rays
| may doom the enterprise. It's an awe inspiring vision, and he has
| lots of interesting example . Perhaps it doesn't jibe with my focus.
| Although using proof-checkers to debug software is a great idea.
I'm all in favour of the whole spectrum of applications. The really
huge collaborative efforts like Hales's Flyspeck project and
Gonthier's odd order theorem formalization are currently exceptional,
and most of us are going to be undertaking more modest endeavors. But
these large projects also stimulate a lot of development that is
useful in other areas. And it's exciting that Flyspeck, at least, is
trying to solve a problem for which the current mathematical review
process has demonstrably failed.
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
