On Thu, Jul 5, 2012 at 3:17 AM, Bill Richter
<[email protected]>wrote:
> Thanks to all the help I got here, I'm doing fine formalizing my paper
> http://www.math.northwestern.edu/~richter/hilbert.pdf
>
> http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
> I've formalized 12 of my 18 pages on Hilbert plane geometry, and got
> past the hard part, formalizing the set theory involved in segments
> and angles, both subsets of the Hilbert plane. In particular I proved
> the SAS, ASA and Angle Subtraction theorems, stated below together
> with the definitions and congruence axioms needed.
>
> I'd like to discuss how HOL Light and miz3 actually checking my
> proofs, as I want my formalization to be a selling point for my paper.
>
This question is actually easy.
HOL Light, in the tradition of so-called "LCF-style" proof assistants,
checks proofs by using an abstract datatype for theorems whose only
constructors are inference rules.
You can see this in the file "fusion.ml", which, being the only ML code one
needs to trust (presuming you trust your ML environment) to believe that
HOL Light thms are theorems of higher order logic, is relatively
well-written and easy to read.
In particular, notice that in the module signature the type thm is abstract
(it doesn't say "type thm = something", just "type thm") and the only
functions that return thms (at the bottom) are inference rules (REFL,
TRANS, etc.), definitional rules (new_basic_definition, etc.) and axioms
(new_axiom).
Since OCaml modules are "closed", when the module type signature ends and
there's nothing else to generate thms, we know those are the only ways thms
will ever be generated.
Thus, no matter how clever the code you use to generate your proofs (be it
miz3, normal HOL Light tactics, or something else), ultimately, if that
code generates any thms, what it has to do is steer the so-called "kernel"
in fusion.ml by calling the inference/definition rules and new_axiom,
possibly using existing theorems and existing derived rules (which do the
same thing), in clever ways to construct the desired thms. The kernel is
designed so that doing so is equivalent to running line-by-line down a
proof in higher order logic.
In the implementation of the rules you can check that they do what they
ought to.
In particular, new_axiom records any axioms in the list !the_axioms, so
you can check axioms() to be sure you nobody added unsound axioms to prove
your theorems. the_axioms itself is in the module and not the signature, so
the only access to it outside of fusion.ml is read-only via axioms (which
is in the signature), thus the list can only grow, and axioms used along
the way can't be removed and hidden.
As you may have inferred, while thms are OCaml objects that you can store
and play with, and we have a story for why they can only be created in ways
guaranteeing that they have proofs, the proofs themselves are dynamic and
ephemeral. If you want to see/keep the (ultra low level) proofs as well,
you could use Joe Hurd's fork of HOL Light (
http://src.gilith.com/hol-light.html) which records the proofs and enables
export in OpenTheory Article format (
http://www.gilith.com/research/opentheory/article.html).
This is why sometimes people let LCF-style proofs become "unreadable": no
matter whether you write readable (maybe even declarative) programs for
constructing thms or whether you write totally unreadable (but possibly
efficient, or smart, or good for exploration and automation) code for
constructing thms, there will always be this (ephemeral) ultra low level
proof that is the "real" proof of your theorem in the formal sense. There
are arguments on both sides for prioritising readability of the programs or
not.
> John's HOL Light documentation doesn't seem to explain the proof
> mechanism, but http://hol.sourceforge.net/documentation.html, looks
> good, and I think I need to read the HOL Logic manual.
>
> I'm not good enough at HOL Light to read the miz3.ml code, and even
> HOL Light experts would have trouble, because miz3 is a very ambitious
> project to combine declarative (all I'm using) and procedural proofs.
>
> John's purple FOL book explains how to implement a Mizar style proof
> assistant in FOL. John even suggested that his purple book code is
> all I need. Freek explained that I'm getting heavy miz3 use out of
> MESON, but I see that John's code
> http://www.cl.cam.ac.uk/~jrh13/atp/index.html includes
> meson.ml: MESON-type model elimination
> Could I really switch to John's purple FOL code? Maybe more
> reasonably, could one implement John's purple book Mizar code
> tactics.ml: Tactics and Mizar-style proofs
> in HOL Light? I'm not of course looking for an improvement in speed
> or durability, but only in understanding.
>
> --
> Best,
> Bill
>
> SAS_THM : thm =
> |- ∀ A B C A' B' C'.
> ¬Collinear A B C ∧ ¬Collinear A' B' C'
> ⇒ seg A B ≡ seg A' B' ∧ seg A C ≡ seg A' C'
> ⇒ angle B A C ≡ angle B' A' C'
> ⇒ A,B,C ≅ A',B',C'
>
> ASA_THM : thm =
> |- ∀ A B C A' B' C'.
> ¬Collinear A B C ∧ ¬Collinear A' B' C'
> ⇒ seg B C ≡ seg B' C'
> ⇒ angle A B C ≡ angle A' B' C'
> ⇒ angle B C A ≡ angle B' C' A'
> ⇒ A,B,C ≅ A',B',C'
>
> AngleSubtraction_THM : thm =
> |- ∀ A O B A' O' B' G G'.
> ¬Collinear A O B ∧ ¬Collinear A' O' B'
> ⇒ G ∈ int_angle A O B ∧ G' ∈ int_angle A' O' B'
> ⇒ angle A O B ≡ angle A' O' B'
> ⇒ angle A O G ≡ angle A' O' G'
> ⇒ angle B O G ≡ angle B' O' G'
>
> Segment_DEF : thm = |- ∀ A B. seg A B = {A, B} ∪ open (A,B)
>
> SEGMENT : thm = |- ∀ s. Segment s ⇔ (∃ A B. s = seg A B ∧ ¬(A = B))
>
> SegmentOrdering_DEF : thm =
> |- ∀ t s.
> s seg_less t ⇔
> Segment s ∧
> Segment t ∧
> (∃ C D X. t = seg C D ∧ X ∈ open (C,D) ∧ s ≡ seg C X)
>
> Angle_DEF : thm = |- ∀ A O B. angle A O B = ray O A ∪ ray O B
>
> ANGLE : thm =
> |- ∀alpha. Angle alpha ⇔
> (∃ A O B. alpha = angle A O B ∧ ¬Collinear A O B)
>
> TriangleCong_DEF : thm =
> |- ∀ A B C A' B' C'.
> A,B,C ≅ 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'
>
> C1 : thm =
> |- ∀ s O Z.
> Segment s ∧ ¬(O = Z)
> ⇒ (∃! P. P ∈ ray O Z ━ O ∧ seg O P ≡ s)
>
> C2Reflexive : thm = |- Segment s ⇒ s ≡ s
>
> C2Symmetric : thm = |- Segment s ∧ Segment t ∧ s ≡ t ⇒ t ≡ s
>
> C2Transitive : thm =
> |- Segment s ∧ Segment t ∧ Segment u ∧ s ≡ t ∧ t ≡ u ⇒ s ≡ u
>
> C3 : thm =
> |- ∀ A B C A' B' C'.
> B ∈ open (A,C) ∧
> B' ∈ open (A',C') ∧
> seg A B ≡ seg A' B' ∧
> seg B C ≡ seg B' C'
> ⇒ seg A C ≡ seg A' C'
>
> C4 : thm =
> |- ∀alpha O A l Y.
> Angle alpha ∧ ¬(O = A) ∧ Line l ∧ O ∈ l ∧ A ∈ l ∧ ¬(Y ∈ l)
> ⇒ (∃! r. Ray r ∧ (∃B. ¬(O = B) ∧ r = ray O B ∧
> ¬(B ∈ l) ∧ B,Y same_side l ∧ angle A O B ≡ alpha))
>
> C5Reflexive : thm = |- Angle alpha ⇒ alpha ≡ alpha
>
> C5Symmetric : thm =
> |- Angle alpha ∧ Angle beta ∧ alpha ≡ beta ⇒ beta ≡ alpha
>
> C5Transitive : thm =
> |- Angle alpha ∧ Angle beta ∧
> Angle gamma ∧ alpha ≡ beta ∧ beta ≡ gamma
> ⇒ alpha ≡ gamma
>
> C6 : thm =
> |- ∀A B C A' B' C'.
> ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
> seg A B ≡ seg A' B' ∧ seg A C ≡ seg A' C' ∧
> angle B A C ≡ angle B' A' C'
> ⇒ angle A B C ≡ angle A' B' C'
>
>
> ------------------------------------------------------------------------------
> 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
>
------------------------------------------------------------------------------
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
