Freek, you're running a very interesting discussion with Mark, Felix, Chris etc. I'd like to know why Mark can't do his interface improvements on HOL Light. Responding to your points:
Maybe you _would_ experience those steps very fleetingly, but you wouldn't focus at them in the way a proof assistant forces you to. Yes, I've been forced to focus in my 2600+ lines of miz3 code http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz formalizing my Hilbert axiomatic geometry paper http://www.math.northwestern.edu/~richter/hilbert.pdf Often I've found that I hadn't done a good job on those those steps I experience very fleetingly. My latest example involves the supplement of angle, which sounds really easy, right? And a right angle is one whose supplement is congruent to itself. My Lemma 6.6 from my paper reads Supplements of congruent angles are congruent. An angle congruent to a right angle is a right angle. All right angles are congruent. Proof. Greenberg proves the first statement [7, Prop. 3.14]. This implies the second statement, by axiom C5. The third statement, due to Hilbert, is [7, Prop. 3.23]. How hard can that be to formalize? It took me over 200 lines! The problem was that I wasn't thinking about an angle (a subset of the plane, a union of two rays) but instead 3 points. Possibly my experts Hartshorne and Greenberg thought the same way. Straightening that out took work, and I include below all the thm & defs I use for supplements and right angles, partly to shed light on And when you prove something you will need to decide on a name for your new lemma. That's something that's particularly difficult. Yes! I have a 775 line long file thmFontHilbertAxiom.ml which contains all my defs and thms, and I'd be lost without it. I'm constantly searching through it for something to cut & paste and then make variable substitutions with Emacs query-replace. I definitely worried about the names of my thms & defs. But I think the interface issues that Mark, Felix & Chris bring up are also important. The miz3 error messages don't confuse me at all any more. Maybe I'm coding better. But I'll need to explain to my geometry audience what miz3 does. Thanks for comparing it privately to Mizar. It will take me a while to understand what you said. If John's HOLBY prover turns out to be weaker than Mizar, as you suggested, I don't necessary think that's bad. I need to understand the proof assistant, and whether it's a little too strong or a little too weak isn't as important. So why can't we understand John's HOLBY? -- Best, Bill Ray_DEF : thm = |- ∀ A B X. ray A B X ⇔ ¬(A = B) ∧ Collinear A B X ∧ ¬(A ∈ open (X,B)) Angle_DEF : thm = |- ∀ A O B. angle A O B = ray O A ∪ ray O B ANGLE : thm = |- ∀α. Angle α ⇔ (∃ A O B. α = angle A O B ∧ ¬Collinear A O B) RAY : thm = |- ∀ r. Ray r ⇔ (∃O A. ¬(O = A) ∧ r = ray O A) SupplementaryAngles_DEF : thm = |- ∀α β. α Suppl β ⇔ (∃ A O B A'. ¬Collinear A O B ∧ O ∈ open (A,A') ∧ α = angle A O B ∧ β = angle B O A') RightAngle_DEF : thm = |- ∀α. Right α ⇔ Angle α ∧ (∃ β. α Suppl β ∧ α ≡ β) SupplementExists_THM : thm = |- ∀ α. Angle α ⇒ (∃ α'. α Suppl α') SupplementImpliesAngle_THM : thm = |- ∀α β. α Suppl β ⇒ Angle α ∧ Angle β SupplementSymmetry_THM : thm = |- ∀α β. α Suppl β ⇒ β Suppl α SupplementsCongAnglesCong_THM : thm = |- ∀α β α' β'. α Suppl α' ∧ β Suppl β' ∧ α ≡ β ⇒ α' ≡ β' SupplementUnique_THM : thm = |- ∀ α β β'. α Suppl β ∧ α Suppl β' ⇒ β ≡ β' CongRightImpliesRight_THM : thm = |- ∀ α β. Angle α ∧ Angle β ∧ Right α ∧ α ≡ β ⇒ Right β RightAnglesCongruentHelp_THM : thm = |- ∀A O B A' P a. ¬Collinear A O B ∧ O ∈ open (A,A') ⇒ Line a ∧ O ∈ a ∧ A ∈ a ⇒ ¬(P ∈ a) ∧ P,B same_side a ⇒ Right (angle A O B) ∧ Right (angle A O P) ⇒ ¬(P ∈ int_angle A O B) CongRightImpliesRight_THM : thm = |- ∀α β. Angle α ∧ Angle β ∧ Right α ∧ β ≡ α ⇒ Right β RightAnglesCongruent_THM : thm = |- ∀α β. Right α ∧ Right β ⇒ α ≡ β OppositeRightAnglesLinear_THM : thm = |- ∀ A B O H h. ¬Collinear A O H ∧ ¬Collinear H O B ⇒ Right (angle A O H) ∧ Right (angle H O B) ⇒ Line h ∧ O ∈ h ∧ H ∈ h ⇒ ¬(A,B same_side h) ⇒ O ∈ open (A,B) ------------------------------------------------------------------------------ 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
