https://dl.dropbox.com/u/34693999/nonobv.pdf
Rob, thanks for the acknowledgment and modifying your proof 2 of Los's Logic
result. Sorry for posting my code yesterday with my Isabelle-type fonts still
in. I'm including the version which runs in HOL Light. I recommend you learn
miz3, and I coded up your proof 2 in miz3 to get you started. I didn't
understand your declarative ProofPower proof 2 formalization, but I know mine
is a lot shorter.
A word about "the eye of the beholder." Your proof 2 is a simplification of
your proof 1, but I still don't see its intuition. I haven't understood your
proof 3 yet. So I'm naturally amazed at your work! The intuition for my proof
below is that Q is almost ~P, so let's work the special case of Q = ~P, which
has an intuitive proof. Since I only thought of this after staring at your
proofs for a long time, I have no confidence that I would actually have done
this without seeing your proofs first.
Here's something miz3 cases & skeletons which Freek explained to me that's not
in his paper arxiv.org/pdf/1201.3601. It pays to write an outline of your
proof before filling in the steps. So when I first started coding up your
proof 2, I got this far without thinkingl:
horizon := 0;;
let RobProof2LosLogic_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. P x y);
consider a b such that
~P a b /\ ~P b a [notPab] by -, Psym;
Q a b /\ Q b a [Qab] by -, Psym, PunionQ;
!x y. Q x y
proof
let x y be A;
cases;
suppose P x a /\ P b y;
qed by -;
suppose ~P x a /\ ~P b y;
qed by -;
suppose P x a /\ ~P b y;
qed by -;
suppose ~P x a /\ P b y;
qed by -;
end;
qed by -`;;
Miz3 gives me "#1 inference error" after each "qed by -;" of of the 4 cases,
because I haven't written in the proofs yet. But you'll notice that that the
proof of "!x y. Q x y" ends with "end;" and not "qed by -;" Otherwise I would
get a "#9 syntax error mizar." The reason, Freek explains, I think, is that
proving each case exhausts the thesis, so "qed" (which means "thus thesis;
end;") wouldn't make sense: there's no thesis anymore! Writing outline proofs
first is especially helpful if you have nested cases.
Here's my miz3 formalization of your proof 2, which took 40 minutes after I
finished the above outline proof. I agree that your case (iii) is very
similar to your case (iv), but it took me a while to see it. You might want to
rewrite your proof a bit. Your phrase "x exchanged for y" isn't quite accurate.
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
let RobProof2LosLogic_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. P x y);
consider a b such that
~P a b /\ ~P b a [notPab] by -, Psym;
Q a b /\ Q b a [Qab] by -, Psym, PunionQ;
!x y. Q x y
proof
let x y be A;
cases;
suppose P x a /\ P b y [PxyPby];
~P x y
proof
assume P x y [Con];
P a x /\ P y b by PxyPby, Psym;
P a b by -, Con, Ptrans;
qed by -, notPab;
Q x y by -, PunionQ;
qed by -;
suppose ~P x a /\ ~P b y;
Q x a /\ Q b y by -, PunionQ;
qed by -, Qab, Qtrans;
suppose P x a /\ ~P b y [Pxy_notPby];
~P x b
proof
assume P x b;
P a b by -, Pxy_notPby, Psym, Ptrans;
qed by -, notPab;
Q x b /\ Q b y by -, Pxy_notPby, PunionQ;
qed by -, Qtrans;
suppose ~P x a /\ P b y;
P y b /\ ~P a x [Pyb_notPax] by -, Psym;
~P y a
proof
assume P y a;
P a b by -, Psym, Pyb_notPax, Ptrans;
qed by -, notPab;
Q x a /\ Q a y by Pyb_notPax, -, Psym, PunionQ;
qed by -, Qtrans;
end;
qed by -`;;
--
Best,
Bill
Here's my proof from yesterday that I think is more intuitive, in spite of the
fact that MESON worked about 10 times harder to prove it. Our two proofs are
about the same length, if you subtract my comments and extra blank lines.
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
let SymTransImpliesSkewTrans_THM = thm `;
let P be A->A->bool;
assume ! x y z. P x y /\ P y z ==> P x z [Ptrans];
assume !x y. P x y ==> P y x [Psym];
thus ! x y z. P x y /\ ~P y z ==> ~P x z
proof
! x y z. P y x /\ ~P y z ==> ~P x z by Ptrans;
qed by -, Psym`;;
(* That was an comprehensible result I detected in your proof. The next result
solves Los's problem in case Q = ~P. *)
let RobLosPnotP_THM = thm `;
let P be A->A->bool;
assume ! x y z. P x y /\ P y z ==> P x z [Ptrans];
assume ! x y z. ~P x y /\ ~P y z ==> ~P x z [notPtrans];
assume !x y. P x y ==> P y x [Psym];
thus (!x y. P x y) \/ (!x y. ~P x y)
proof
! x y z. P x y /\ ~P y z ==> ~P x z by Ptrans, Psym,
SymTransImpliesSkewTrans_THM;
! x y z. ~P y z ==> ~P x z [almost_done] by -, notPtrans;
assume ~(!x y. P x y);
consider a b such that
~P a b [notPab] by -;
~P b a [notPba] by -, Psym;
!x y. ~P x y
proof
let x y be A;
~P x a /\ ~P y b by notPba, notPab, almost_done;
qed by -, Psym, notPab, notPtrans;
qed by -`;;
(* My proof below of Los's result is more complicated than I'd like, but it's a
straightforward modification of the above comprehensible proof. The MESON
solved at number 108 is a bit lower than the the above proof, and I get a
strange error miz3 message for I believe some step of the proof:
Warning: No useful-looking instantiations of lemma
*)
let LosLogic_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
! x y z. ~P x y /\ ~P y z ==> Q x z /\ Q z x [nearnotPtrans] by
PunionQ, Qtrans, Psym;
! x y z. P x y /\ ~P y z ==> ~P x z /\ ~P z x by Ptrans, Psym,
SymTransImpliesSkewTrans_THM, Psym;
! x y z. P x y /\ ~P y z ==> Q x z /\ Q z x by -, PunionQ;
! x y z. ~P y z ==> Q x z /\ Q z x [good_enough] by nearnotPtrans, -;
assume ~(!x y. P x y);
consider a b such that
~P a b /\ ~P b a [notPab] by -, Psym;
Q a b /\ Q b a [Qab] by -, Psym, PunionQ;
!x y. Q x y
proof
let x y be A;
Q x a /\ Q b y by notPab, good_enough;
qed by -, Qab, Qtrans;
qed by -`;;
------------------------------------------------------------------------------
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
