On Thu, Jul 5, 2012 at 3:17 AM, Bill Richter <richter@math.northwestern.edu> 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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info