John, I was wrong, and all the mizar modes work fine with ocaml-3.09.3
and hol_version 2.20++. I can successfully paste in these 5 commands:
hol_light> ocaml
#use "hol.ml";;
#load "unix.cma";;
#use "miz3/miz3.ml";;
#use "JohnTarskiGeometry.ml";;
where JohnTarskiGeometry.ml (incl below) is the combination of your
two code fragments, included below. Thanks, that's real progress!
But I have serious questions about the coding below.
It didn't work to substitute your Mizar mode Examples/mizar.ml. Your
Tarski code chugged away but hung for hours. Mizarlight/make.ml also
didn't work, failing to prove your EquivReflexive, with error message
Unbound value thm.
So Freek's miz3 was the big winner!
My only bug report (for Mizarlight) is from the older
hol_version 2.20, included below.
Thanks for your new miz3 code, which is quite readable, and runs fine,
together with your (not so readable) earlier code, which amounts to
1) Proving Tarski's axioms as theorems in the coordinate plane R^2
2) using these axiom-theorems to prove Tarski's theorems.
We're not actually deducing consequences of Tarski's axioms here.
We're proving theorems in R^2, where all of Tarski's theorems (or
Hilbert's) are clearly true. That's not what want. For one thing, we
miss out on applying Tarski's axioms to hyperbolic geometry, as Tim
did on the Isabelle list (I can't read his code).
You and Freek didn't define the Mizar datatype `struct', which is what
I use: A Plane is a struct, a set with a 4-ary Betweenness relation
and 3-ary Equidistant relation.
BTW Hilbert and Birkhoff both prove that with enough axioms including
the parallel postulate, there's a unique model R^2, so there's nothing
unrigorous about working in coordinates, at least if you understand
this result, which Hartshorne does a pretty good job explaining.
I don't know what the plan to do this in miz3 is, though. Do we still
use newdefinition to define the axioms? Can we stack the axioms and
definitions together into something like a Isabelle locale and invoke
it when we want to prove theorems? BTW my first Mizar success was
really ugly: I had one theorem
AXIOM_1 and ... AXIOM_1 implies lemma1, lemma2, ... lemma17
and the proof was a mile long. I finally stumbled on my also
inelegant solution of making each axioms into a theorem.
-------------- hol_version 2.20 mizar bug report --------------
hol_light> make
hol_light> ocaml
#use "hol.ml";;
It took 5 minutes, and I got the message
Camlp4 Parsing version 3.09.3
#use "Mizarlight/make.ml";;
This didn't work, and I got the error message
Warning: inventing type variables
0..0..solved at 2
- : thm = |- ?x. !y. P x ==> P y
- : unit = ()
val holby_prover : thm list -> (string * thm) list * term -> goalstate =
<fun>
File "/home/richter/HOL/SOURCE/hol_light/Mizarlight/duality_holby.ml", line 8,
characters 0-14:
Unbound value current_prover
Error in included file
/home/richter/HOL/SOURCE/hol_light/Mizarlight/duality_holby.ml
- : unit = ()
Yours worked fine, and I wasn't before smart enough to try this:
hol_light> ocaml
#use "hol.ml";;
#use "Examples/mizar.ml";;
Freek's miz3 works fine, with your unix.cma trick above.
----------- Your miz3 Tarski geometry code JohnTarskiGeometry.ml -----------
(* ----------------------------------------------------------------------- *)
(* Define a new type "Plane" in bijection with real^2. *)
(* ----------------------------------------------------------------------- *)
needs "Multivariate/determinants.ml";;
let Plane_TYBIJ =
let th = prove(`?x:real^2. T`,REWRITE_TAC[]) in
let def = new_type_definition "Plane" ("planify","coords") th in
REWRITE_RULE[] def;;
(* ----------------------------------------------------------------------- *)
(* Define notions of congruence and between-ness as Euclidean equivalents. *)
(* ----------------------------------------------------------------------- *)
parse_as_infix("===",(12, "right"));;
let Congruent_DEF = new_definition
`a,b === c,d <=> dist(coords a,coords b) = dist(coords c,coords d)`;;
let Between_DEF = new_definition
`Between (a,b,c) <=> between (coords b) (coords a,coords c)`;;
(* ----------------------------------------------------------------------- *)
(* Simple tactic to switch variables from "Plane" to "real^2". *)
(* ----------------------------------------------------------------------- *)
let PLANE_COORD_TAC =
let PLANE_QUANT_THM = MESON[Plane_TYBIJ]
`((!x. P x) <=> (!x. P(planify x))) /\
((?x. P x) <=> (?x. P(planify x)))`
and PLANE_EQ_THM = MESON[Plane_TYBIJ] `planify x = planify y <=> x = y` in
REWRITE_TAC[PLANE_QUANT_THM; Congruent_DEF; Between_DEF; PLANE_EQ_THM;
Plane_TYBIJ];;
(* ----------------------------------------------------------------------- *)
(* Derivation of the axioms. *)
(* ----------------------------------------------------------------------- *)
let AXIOM_1 = prove
(`!a b. a,b === b,a`,
PLANE_COORD_TAC THEN NORM_ARITH_TAC);;
let AXIOM_2 = prove
(`!a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s`,
PLANE_COORD_TAC THEN NORM_ARITH_TAC);;
let AXIOM_3 = prove
(`!a b c. a,b === c,c ==> a = b`,
PLANE_COORD_TAC THEN NORM_ARITH_TAC);;
let AXIOM_4 = prove
(`!a q b c. ?x. Between(q,a,x) /\ a,x === b,c`,
PLANE_COORD_TAC THEN GEOM_ORIGIN_TAC `a:real^2` THEN REPEAT GEN_TAC THEN
REWRITE_TAC[DIST_0] THEN ASM_CASES_TAC `q:real^2 = vec 0` THENL
[ASM_SIMP_TAC[BETWEEN_REFL; VECTOR_CHOOSE_SIZE; DIST_POS_LE];
EXISTS_TAC `--(dist(b:real^2,c) / norm(q) % q):real^2` THEN
REWRITE_TAC[between; DIST_0] THEN
REWRITE_TAC[dist; NORM_MUL; NORM_NEG; REAL_ABS_DIV; REAL_ABS_NORM;
VECTOR_ARITH `q - --(a % q) = (&1 + a) % q`] THEN
CONJ_TAC THENL
[MATCH_MP_TAC(REAL_RING `a = &1 + b ==> a * q = q + b * q`) THEN
SIMP_TAC[REAL_ABS_REFL; REAL_POS; REAL_LE_ADD; REAL_LE_DIV;
NORM_POS_LE];
ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0]]]);;
let EquivReflexive = thm `;
!a b. a,b === a,b
proof
let a b be Plane;
b,a === a,b by AXIOM_1;
thus a,b === a,b by AXIOM_2;
end`;;
let EquivSymmetric = thm `;
!a b c d. a,b === c,d ==> c,d === a,b
proof
let a b c d be Plane;
assume a,b === c,d [1];
a,b === a,b by EquivReflexive;
thus c,d === a,b by 1, AXIOM_2;
end`;;
let EquivTransitive = thm `;
!a b p q r s : Plane. a,b === p,q /\ p,q === r,s ==> a,b === r,s
proof
let a b p q r s be Plane;
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, AXIOM_2;
end`;;
let Baaa_THM = thm `;
!a b. Between (a,a,a) /\ a,a === b,b
proof
let a b be Plane;
?x. Between (a,a,x) /\ a,x === b,b by AXIOM_4;
consider x such that Between (a,a,x) /\ a,x === b,b [1];
a = x by 1, AXIOM_3;
thus Between (a,a,a) /\ a,a === b,b by 1;
end`;;
------------------------------------------------------------------------------
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
