Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
To: borm@cs.ubc.ca
Cc: info-hol@cs.uidaho.edu
Subject: Re: a little proof challenge
In-Reply-To: Your message of "08 Sep 93 17:15:00 PDT." <7637*joyce@cs.ubc.ca>
Date: Thu, 09 Sep 93 14:32:53 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:199040:930909133302"@cl.cam.ac.uk>


Jeff Joyce writes:

| One of my students, Eric Borm, has come up with the following theorem
| which has been nasty to other theorem-provers.  If anyone is interested
| in trying to prove this theorem in HOL, we would be interested in 
| the result -- in addition to the proof script, we'd be interested in
| some account of the amount of effort required  to prove it.  The
| proof script is likely to be very short -- it's more a matter of
| the effort required to find the script.

I came up with the following simple, crude proof. It took me 15 minutes,
rather a long time for such a short script, but I did fly back from the
US six hours ago... I'd be interested in more details of the problems
encountered in using other provers.

John.

let JEFF = PROVE
 ("!P Q R.
    !x:*. ?v. ?w. !y. !z:**.
      ((P x /\ Q y) ==> ((P v \/ R w)  /\ (R z ==> Q v)))",
  REPEAT GEN_TAC THEN
  MAP_EVERY ASM_CASES_TAC ["!p:*. ~(P p)"; "!q:*. ~Q q"; "!r:**. ~R r"] THEN
  ASM_REWRITE_TAC[] THEN TRY(UNDISCH_TAC "!r:**. ~R r") THEN
  EVERY_ASSUM(CHOOSE_TAC o REWRITE_RULE[] o CONV_RULE NOT_FORALL_CONV) THENL
   [DISCH_TAC THEN EXISTS_TAC "p:*"; MAP_EVERY EXISTS_TAC ["q:*"; "r:**"]] THEN
  ASM_REWRITE_TAC[]);;