https://dl.dropbox.com/u/34693999/nonobv.pdf
Congratulations, Rob, I had no idea how to prove Los's non-obvious theorem
until I read your solution. I'm not quite satisfied with your exposition,
though, and here's a miz3 version of your proof not using your extension P',
reflexivity, domain P or range P (isn't dom = ran anyway?). The key is my
`a_works', which I learned from your proof.
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
let RobProofLosLogic_THM = thm `;
let P Q be A->A->bool;
assume ! x y z. P x y /\ P y z ==> P x z [Ptrans];
assume ! x y z. Q x y /\ Q y z ==> Q x z [Qtrans];
assume !x y. P x y ==> P y x [Psym];
assume !x y. P x y \/ Q x y [PunionQ];
thus (!x y. P x y) \/ (!x y. Q x y)
proof
assume ~(!x y. Q x y);
consider a b such that
~Q a b [notQab] by -;
P a b [Pab] by -, PunionQ;
! z. P a z [a_works]
proof
assume ~(! z. P a z);
consider z such that
~P a z [notPaz] by -;
~P b z
proof
assume P b z;
P a z by Pab, -, Ptrans;
qed by -, notPaz;
~P z b by -, Psym;
Q a z /\ Q z b by notPaz, -, PunionQ;
Q a b by -, Qtrans;
qed by -, notQab;
!x y. P x y
proof
let x y be A;
P a x /\ P a y by a_works, Psym;
P x y by -, Psym, Ptrans;
qed by -;
qed by -`;;
This is a great example of how it's OK for miz3 to have the theorem-proving
power that I was so afraid of. It seems ridiculous to worry that MESON
somehow used it's power to prove the theorem itself and so my proof is just
fluff that MESON is ignoring. I never asked miz3 to prove the theorem from the
assumptions. On top of that, miz3 verified this proof almost instantaneously,
writing
0..0..1..3..6..solved at 13
while John's proof converted to miz3 gets the MESON solved at number 23088:
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`;;
In this miz3 proof, I asked miz3 to verify the conclusion from the hypotheses.
In the proof, I never did, I only asked miz3 to verify a sequence of claims
that lead up to your proof.
--
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
