Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <04164-0@swan.cl.cam.ac.uk>; Sat, 1 Aug 1992 17:24:42 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08909; Sat, 1 Aug 92 09:14:13 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA08904; Sat, 1 Aug 92 09:14:06 -0700 Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <04098-0@swan.cl.cam.ac.uk>; Sat, 1 Aug 1992 17:04:25 +0100 To: gavan@za.ac.uct.mth.UCT_elc (Gavan Tredoux) Cc: info-hol@edu.uidaho.cs.ted Subject: Re: CHOOSE breaks In-Reply-To: Your message of Tue, 28 Jul 92 23:36:26. <9207282136.AA03441@UCT_elc.mth.uct.ac.za> Date: Sat, 01 Aug 92 17:04:19 +0100 From: John Harrison Message-Id: <"swan.cl.ca.100:01.07.92.16.04.28"@cl.cam.ac.uk> Gavan Tredoux writes: > In the process of complex proof, I've managed to break > REPEAT STRIP_TAC, due to an error in CHOOSE. Here's a > cut and paste of the error - the goal won't make much sense > because it depends on all sorts of theories. At the core of STRIP_TAC is STRIP_THM_THEN, which is defined by: let STRIP_THM_THEN = FIRST_TCL [CONJUNCTS_THEN; DISJ_CASES_THEN; CHOOSE_THEN];; Thus it just tries splitting apart conjunctions, doing case splits over disjunctions, and choosing Skolem constants. CHOOSE_THEN ttac (|- ?x. P[x]) (A ?- t) picks a variant of "x", by adding primes, so that it doesn't coincide with any free variables in A, P or t. The problem seems to be that in a theorem-continuation context, when a theorem is split into conjuncts by CONJUNCTS_THEN, the variants are chosen for the two conjuncts independently, because the intermediate result isn't actually put on the assumption list. This is probably too simplistic to be the whole story, because on that count I would expect the following to fail: #g "(?x. x = 1) /\ (?x. x = 2) ==> (1 = 2)";; "(?x. x = 1) /\ (?x. x = 2) ==> (1 = 2)" () : void #e STRIP_TAC;; OK.. "1 = 2" [ "x = 1" ] [ "x' = 2" ] An ad-hoc solution (particularly since I don't really understand the problem) is to rewrite STRIP_TAC using a function which "predicts" the variables chosen in one conjunct, and avoids them in the other. An attempt is given below, which seems to work on the examples posted by Roger and Tom. I don't know if this is correct, and it has the flaw of choosing variants unnecessarily for disjuncts. John. %----------------------------------------------------------------------------% % newfvs - New free variables from naive STRIP of A |- tm % %----------------------------------------------------------------------------% letrec newfvs tm = ($. o (I # newfvs) o dest_exists) tm ? ($@ o (newfvs # newfvs) o dest_conj) tm ? ($@ o (newfvs # newfvs) o dest_disj) tm ? [];; %----------------------------------------------------------------------------% % variants av vs - Sequentially picks variants % %----------------------------------------------------------------------------% letrec variants av vs = (let vh = variant av (hd vs) in vh.(variants (vh.av) (tl vs))) ? [];; %----------------------------------------------------------------------------% % XA_STRIP_THEN - Similar to REPEAT_TCL STRIP_THM_THEN. Avoids picking names % % in the "av" argument (only; i.e. it doesn't look at asl,w) % %----------------------------------------------------------------------------% letrec XA_STRIP_THEN av ttac th = let tm = concl th in (let v' = variant av (fst(dest_exists tm)) in X_CHOOSE_THEN v' (XA_STRIP_THEN (v'.av) ttac) th) ? (CONJUNCTS_THEN2 (XA_STRIP_THEN av ttac) (XA_STRIP_THEN (av@(variants av (newfvs (fst(dest_conj tm))))) ttac) th) ? (DISJ_CASES_THEN2 (XA_STRIP_THEN av ttac) (XA_STRIP_THEN (av@(variants av (newfvs (fst(dest_disj tm))))) ttac) th) ? ttac th;; %----------------------------------------------------------------------------% % STRIP_ASSUME_TAC2 - Like STRIP_ASSUME_TAC but without the bug(?) % %----------------------------------------------------------------------------% let STRIP_ASSUME_TAC2 th (asl,w) = let av = (thm_frees th)@(freesl(w.asl)) in XA_STRIP_THEN av ASSUME_TAC th (asl,w);; %----------------------------------------------------------------------------% % STRIP_TAC2 - Like STRIP_TAC but without the bug(?) % %----------------------------------------------------------------------------% let STRIP_TAC2 g = STRIP_GOAL_THEN STRIP_ASSUME_TAC2 g ? failwith `STRIP_TAC2`;;