Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 9 Sep 1993 15:05:42 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA24944; Thu, 9 Sep 93 06:49:59 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from air52.larc.nasa.gov by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA24940; Thu, 9 Sep 93 06:49:57 -0700 Received: by air52.larc.nasa.gov (5.65.1/lanleaf2.4) id AA02413; Thu, 9 Sep 93 09:47:50 -0400 Message-Id: <9309091347.AA02413@air52.larc.nasa.gov> Date: Thu, 9 Sep 93 09:47:50 -0400 From: Victor "A." Carreno To: joyce@cs.ubc.ca, borm@cs.ubc.ca Subject: Re: a little proof challenge In-Reply-To: Mail from 'Jeffrey Joyce ' dated: 8 Sep 93 17:15 -0700 Cc: info-hol@cs.uidaho.edu, vac@air16.larc.nasa.gov This is another answer to Jeff's challenge. The thinking goes as follows: After stripping the goal you have: "?v w. !y z. (P x /\ Q y) ==> ((P v \/ R w) /\ (R z ==> Q v))" If there is no "v" that satisfies Q (!v.~Q v) then the theorem is trivialy true since the antecedent of the implication is allways false. If there is a "v" that satisfies Q then pick that "v" so (R z ==> Q v) will be true. However the "v" that makes Q true might make P false. In that case you must pick a "w" that makes R true. If there is no "w" that makes R true then R is always false and (R z ==> Q v) is always true. In that case you can pick "v" to be "x". REPEAT STRIP_TAC THEN ASM_CASES_TAC "?w.(R:**->bool) (w:**)" THENL [POP_ASSUM (STRIP_ASSUME_TAC) THEN ASM_CASES_TAC "?v.(Q:*->bool) (v:*)" THEN POP_ASSUM (STRIP_ASSUME_TAC o (CONV_RULE (TRY_CONV NOT_EXISTS_CONV))) THEN EXISTS_TAC "v:*" THEN EXISTS_TAC "w:**" THEN (TRY (STRIP_TAC THEN STRIP_TAC)) THEN ASM_REWRITE_TAC[] ;POP_ASSUM (STRIP_ASSUME_TAC o (CONV_RULE NOT_EXISTS_CONV)) THEN EXISTS_TAC "x:*" THEN EXISTS_TAC "w:**" THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN RES_TAC] It took me about 45 minutes to think what I wanted to do. After that about 10 hours in HOL to write the code. (more like 30 minutes but I type slowly) Victor.