Chris, your MESON example was illuminating, and I hope someone can tell me what
it means. Paste this code from p 36 of John's tutorial into the HOL Light
window:
MESON[]
`(!x y z. P x y /\ P y z ==> P x z) /\
(!x y z. Q x y /\ Q y z ==> Q x z) /\
(!x y. P x y ==> P y x) /\
(!x y. P x y \/ Q x y)
==> (!x y. P x y) \/ (!x y. Q x y)`;;
MESON solves this logic puzzle (which I still haven't yet solved) quite
quickly, and it writes
...solved at 23107
And we can easily make this a no-tactics miz3 theorem with a 1-line proof:
let LosLogic_THM = thm `;
let x y be A;
let P Q be A->A->bool;
assume ! x y z. P x y /\ P y z ==> P x z [H1];
assume ! x y z. Q x y /\ Q y z ==> Q x z [H2];
assume !x y. P x y ==> P y x [H3];
assume !x y. P x y \/ Q x y [H4];
thus (!x y. P x y) \/ (!x y. Q x y)
proof
qed by H1, H2, H3, H4`;;
The miz3 proof is almost as quick, with a MESON `solved at' number of 23088.
The clear moral of your example is that if one uses no-tactics miz3 to solve
logic puzzle like this, then miz3 (using MESON) can astound us, proving things
we can't easily prove by ourselves.
Now it's dimly possible that one would actually want to have a proof like that
in Hilbert axiomatic geometry code, as I have other set-theoretic proofs
similarly using A and A->bool, e.g. this one with a MESON `solved at' number of
32:
parse_as_infix("NOTIN",(11, "right"));;
let NOTIN = new_definition
`!a:A l:A->bool. a NOTIN l <=> ~(a IN l)`;;
let BiggerThanSingleton_THM = thm `;
let p be A->bool;
let x be A;
assume x IN p [H1];
assume ~(p = {x}) [H2];
thus ? a . a IN p /\ ~(a = x)
proof
{x} SUBSET p by H1, SING_SUBSET;
~(p SUBSET {x}) by -, H2, SUBSET_ANTISYM;
consider a such that
a IN p /\ a NOTIN {x} [X1] by -, SUBSET, NOTIN;
~(a = x) by -, IN_SING, NOTIN;
qed by -, X1`;;
But these MESON `solved at' numbers seem very small to me. My record for a
MESON `solved at' number is 310649, achieved in the proof of a result that
looks pretty obvious, that the supplement of an angle is well-defined up to
angle congruence:
SupplementsCongAnglesCong_THM : thm =
|- !alpha beta alpha' beta'.
alpha Suppl alpha' /\ beta Suppl beta'
==> alpha === beta
==> alpha' === beta'
And I claim any of you could understand my proof, in
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
in spite of the fact that MESON worked to hard to prove it. So Michael's
`sweet spot' seems to be about what you want to use no-tactics miz3 for. Why
am I hitting the sweet spot with my geometry code? And Michael, do they play
baseball in Australia?
The question of course arises of whether miz3 could have proven my Hilbert
axiomatic geometry results with much shorter proofs than I gave. I'm very
skeptical that it could have, because I typically evaluate my proof a zillion
times before it works, at first with no proof at all beyond
proof
qed by -`;;
And I always have a #1 inference error after the final qed until I've written
in what I call a proof, and removed the zillion obvious blunders that miz3
detected for me. In fact, let's try the above one right now:
let SupplementsCongAnglesCong_THM = thm `;
let alpha beta alpha' beta' be point_set;
assume alpha Suppl alpha' /\ beta Suppl beta' [H1];
assume alpha === beta [H2];
thus alpha' === beta'
proof
qed by -`;;
miz3 instantly calculated my #1 inference error, with MESON getting only up to
49.
--
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
