## Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

 Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light From: John Harrison - 2012-05-07 16:12:13 ```Hi Bill, | John, thanks for writing the R^2 = Tarski-model code! I could not | have done it. You're the boss, so I'll use your new code. OK, sounds good. For now, there would be no problem just replacing the first part with axioms, since that would be faster to load and wouldn't require the latest HOL Light. See below for this version. I know I discouraged you from using axioms before, but now it's clear from the model that they are consistent and you can replace the axioms by the derivation at any point without needing to make any changes to your proofs. | BTW did you see that I proved your equation responding to Josef? | (x1^2 + x2^2 + x3^2 + x4^2) (y1^2 + y2^2 + y3^2 + y4^2) Well yes, that looks reasonable, though I wouldn't quite characterize it as an axiomatic proof, since there are some implicit assumptions that are not boiled down to axioms. BTW, this (or to be more precise its counterpart over the integers) comes from a proof that every nonnegative integer is the sum of 4 integer squares. This identity lets you reduce it to primes. | Your other code works quite well, and I ported Bqaa, but I'm stuck on | C1. I assumed you had a typo | loadt "miz3/make.ml";; | and changed it to loadt "miz3/miz3.ml";; Yes, sorry, this "make.ml" was something I added to Freek's package now that I actually distribute miz3 with HOL Light. Which I do, by the way: it's now there in revision 135. | So I paste in 3 commands | hol_light> ocaml | #use "hol.ml";; | #load "unix.cma";; So far so good... | and then paste in the file below, JohnTarski.ml (I couldn't figure out | how to #use it), and everything compiles, where I got the C1 error The problem just arises from the use of "then", which isn't in the miz3 grammar. Although miz3 sticks pretty close to Mizar, you don't use "then" to link to the previous fact. Instead you can use "-" in a justification list to refer to it explicitly, or rely on a settable "horizon" of facts that are automatically used. For more details, see Freek's paper, in particular the list of differences with Mizar on page 17: http://arxiv.org/abs/1201.3601 Anyway, if you delete those two instances of "then" it works fine for me. But anyway, I'd still recommend working in the cleaner world without the modularity, as in the fragment I append below. John. (* ========================================================================= *) (* Model for Tarski axioms and port of Bill Richter's geometry proofs. *) (* ========================================================================= *) new_type("point",0);; parse_as_infix("===",(12, "right"));; parse_as_infix("cong",(12, "right"));; new_constant("===",`:point#point->point#point->bool`);; new_constant("Between",`:point#point#point->bool`);; let cong_DEF = new_definition `a,b,c cong x,y,z <=> a,b === x,y /\ a,c === x,z /\ b,c === y,z`;; (* ------------------------------------------------------------------------- *) (* The axioms. *) (* ------------------------------------------------------------------------- *) let A1 = new_axiom `!a b. a,b === b,a`;; let A2 = new_axiom `!a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s`;; let A3 = new_axiom `!a b c. a,b === c,c ==> a = b`;; let A4 = new_axiom `!a q b c. ?x. Between(q,a,x) /\ a,x === b,c`;; let A5 = new_axiom `!a b c x a' b' c' x'. ~(a = b) /\ a,b,c cong a',b',c' /\ Between(a,b,x) /\ Between(a',b',x') /\ b,x === b',x' ==> c,x === c',x'`;; let A6 = new_axiom `!a b. Between(a,b,a) ==> a = b`;; let A7 = new_axiom `!a b p q z. Between(a,p,z) /\ Between(b,q,z) ==> ?x. Between(p,x,b) /\ Between(q,x,a)`;; (* ------------------------------------------------------------------------- *) (* Now Mizarlight versions of the actual proofs. *) (* ------------------------------------------------------------------------- *) #load "unix.cma";; loadt "miz3/miz3.ml";; let EquivReflexive = thm `; !a b. a,b === a,b proof let a b be point; b,a === a,b by A1; thus a,b === a,b by A2; end`;; let EquivSymmetric = thm `; !a b c d. a,b === c,d ==> c,d === a,b proof let a b c d be point; assume a,b === c,d [1]; a,b === a,b by EquivReflexive; thus c,d === a,b by 1, A2; end`;; let EquivTransitive = thm `; !a b p q r s : point. a,b === p,q /\ p,q === r,s ==> a,b === r,s proof let a b p q r s be point; assume a,b === p,q [1]; assume p,q === r,s [2]; p,q === a,b by 1, EquivSymmetric; thus a,b === r,s by 2, A2; end`;; let Baaa_THM = thm `; !a b. Between (a,a,a) /\ a,a === b,b proof let a b be point; ?x. Between (a,a,x) /\ a,x === b,b by A4; consider x such that Between (a,a,x) /\ a,x === b,b [1]; a = x by 1, A3; thus Between (a,a,a) /\ a,a === b,b by 1; end`;; let Bqaa_THM = thm `; !a q. Between(q,a,a) proof let a q be point; ? x : point . Between(q,a,x) /\ a,x === a,a by A4; consider x such that Between(q,a,x) /\ a,x === a,a [1]; a = x by 1, A3; thus Between(q,a,a) by 1; end`;; ```