John, here's a much shorter version of my bug report yesterday. I
don't of course know that this is a bug in miz3 or HOL Light, as I
haven't mastered the documentation for either, but miz3 isn't doing
what I think it should do, and it's a serious matter to me.
(* Paste in these 4 commands, with 2 copy/pastes
cd ~/hol_light; ocaml
#use "hol.ml";;
#load "unix.cma";;
loadt "miz3/miz3.ml";;
and then paste in the following file. *)
horizon := 0;;
new_type("point",0);;
new_type_abbrev("point_set",`:point->bool`);;
new_constant("Between",`:point#point#point->bool`);;
new_constant("Line",`:point_set->bool`);;
let Collinear_DEF = new_definition
`Collinear (A,B,C) <=>
?l. Line l /\ A IN l /\ B IN l /\ C IN l`;;
let I1 = new_axiom
`!A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;;
let B1 = new_axiom
`! A B C. Between (A,B,C) ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
Between (C,B,A) /\ Collinear (A,B,C)`;;
(* This next proof works fine, returning
0..0..1..5..12..27..50..88..138..212..321..453..695..1034..1503..2194..solved
at 2319
val I1unhappy_THM : thm = |- !A B C. Between (A,B,C) ==> A = A
#
That's evidence for a bug in miz3. I think I should have gotten a #1
inference error after line 2 of the proof. Distinct doesn't include
the needed assumption for I1, ~(A = B). Axiom B1, cited on line 1,
does compute ~(A = B), but with horizon = 0 I don't think this result
should have been available to justify line 2.
*)
let I1unhappy_THM = thm `;
let A B C be point;
assume Between (A,B,C) [H1];
thus A = A
proof
~(B = C) [Distinct] by H1, B1;
consider p such that
Line p /\ A IN p /\ B IN p by Distinct, I1;
qed by -`;;
(*
This of course doesn't work, yielding the error
#1 :: 1: inference error
after line 1 of the proof.
*)
let I1not_unhappy_THM = thm `;
let A B C be point;
assume Between (A,B,C) [H1];
thus A = A
proof
consider p such that
Line p /\ A IN p /\ B IN p by I1;
qed by -`;;
!horizon;;
(*
As expected, this command yields
val it : int = 0
Let's check that axiom B1 is working:
*)
let B1works_THM = thm `;
let A B C be point;
assume Between (A,B,C) [H1];
thus ~(A = B)
proof
~(A = B) /\ ~(A = C) /\ ~(B = C) /\
Between (C,B,A) /\ Collinear (A,B,C) by H1, B1;
qed by -`;;
(* Works fine!
B1works_THM : thm = |- !A B C. Between (A,B,C) ==> ~(A = B)
--
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
