Thanks for thinking about my Tarski geometry code problems, John! That would be great to use less than full Mizar mode. Let me stress that Mizar does more automation than is allowed in 2-column proofs.
BTW can we use fancy characters like ∧⇒∀∃ in HOL Light? It sure makes the code more readable. I wrote Emacs code so I could do it in Mizar. I suppose that most geometric problems are purely universally quantified so the extra structuring steps are not as important. I don't know. Is this theorem and definition universally quantified? theorem RhombusDiagBisect: ∀ S, b, c, d, c', d' . S Tarski-model holds Between b,c,d' ∧ Between b,d,c' ∧ c,d' ≡ c,d ∧ d,c' ≡ c,d ∧ d',c' ≡ c,d ⇒ ∃ e . Between c,e,c' ∧ Between d,e,d' ∧ c,e ≡ c',e ∧ d,e ≡ d',e definition let S, a, b, x, y; pred a,b equal_line x,y means :DefLineEq: ¬(a = b) ∧ ¬(x = y) ∧ ∀ c holds c on_line a,b ⇔ c on_line x,y; end; That's the weirdest my Mizar code gets with quantifiers. Thanks for the encouragement to modify code! I suppose I'd have to learn the HOL Light mechanics pretty well first. I think I'm a pretty good Scheme programmer, and ML can't be that different. But, uh, I was really hoping you guys would write it :) Right now we're not having an interface problem, but a design problem: how do you stack definitions and axioms into something like an Isabelle locale, and then cite that locale portably? Yes, [Phil] is really making use of programming to fill in tricky gaps in the incidence reasoning and so on, which is indeed more ambitious. It will be interesting to see whether you encounter similar issues in your own formalization from the Tarski axioms, with some of the steps becoming painful by hand and motivating more ambitious automation. Julien Narboux, who used Coq to prove Tarksi theorems, said something like that, and I just don't understand. It took me 300 lines to (porting Julien) prove Gupta's amazing theorem that 2 points determine a line. I found it exhilarating, not painful. My problem is math: I don't know how to prove the rest of Hilbert's axioms. I don't know how to prove the full Pasch axiom (Tarski's axiom is 1/3 of that). -- 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
