Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Sun, 9 Oct 1994 11:33:32 +0100
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA01241;
          Sun, 9 Oct 1994 04:34:13 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from sirius.brunel.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA01237;
          Sun, 9 Oct 1994 04:34:11 -0600
Received: from pinky.ahl.co.uk by sirius.brunel.ac.uk with SMTP (PP) 
          id <07034-0@sirius.brunel.ac.uk>; Sun, 9 Oct 1994 11:27:48 +0100
From: Simon Finn <simon@ahl.co.uk>
Received: from alpha.ahl.co.uk by Pinky.ahl.co.uk; Sun, 9 Oct 94 11:29:01 BST
Date: Sun, 9 Oct 1994 11:28:31 +0000
Message-Id: <350.9410091028@alpha.ahl.co.uk>
To: info-hol@leopard.cs.byu.edu
Subject: Re: A Little Puzzle.
Content-Type: X-sun-attachment
Content-Length: 2510

----------
X-Sun-Data-Type: text
X-Sun-Data-Description: text
X-Sun-Data-Name: text
X-Sun-Charset: us-ascii
X-Sun-Content-Lines: 32



> Certainly the easy thing is to Skolemise.   From a logical point
> of view this is extravagant.  The correct way to prove this is
> to use a $\exists$-elimination rule like
>                          F(x)
>                           .
>                           .
>          (\exists y)(Fy)  p
>          ------------------
>                   p
> 

That's essentially how I did the proof in LAMBDA. The key step is
using the rule "anyImpR", which is almost always useful when reasoning
about "any" expressions:

> p anyImpR;
2: G // H |- exists x. P#(x)
1: G // H |- forall x. P#(x) ->> Q#(x)
   -----------------------------------
   G // H |- Q#(any x. P#(x))


The rest of the proof is just routine instantiation and rewriting
(which could undoubtably be tidied up somewhat).

Acknowledgement: the precise form of the rule "anyImpR" was suggested
by Holger Busch of Siemens.


Simon Finn (Abstract Hardware Ltd.)
----------
X-Sun-Data-Type: default
X-Sun-Data-Description: default
X-Sun-Data-Name: proof
X-Sun-Charset: us-ascii
X-Sun-Content-Lines: 47



pushGoal libPenv "G // H |- \
\forall g, f. (forall x, y. (g x == g y) ->> (f x == f y)) \
\                 ->> \
\              exists h. forall x. h(g x) == f x";

at simpR;
at (chooseInstantiateTac libPenv "h" "fn b => any c. exists a. g' a == b /\\ f' a == c");
at (rewriteTac []);

(* ...
*******   LEVEL 1.4   *******
1: G // forall x,y. g' x == g' y ->> f' x == f' y $ H
   |- (any c. exists a. g' a == g' x' /\ f' a == c) == f' x'
   ---------------------------------------------------------
   G // H
   |- forall g,f.
        (forall x,y. g x == g y ->> f x == f y)
        ->> exists h. forall x. h (g x) == f x
... *)

apprl anyImpR;
(* ...
*******   LEVEL 1.5   *******
2: G // forall x,y. g' x == g' y ->> f' x == f' y $ H
   |- exists x1,a. g' a == g' x' /\ f' a == x1
1: G // forall x,y. g' x == g' y ->> f' x == f' y $ H
   |- forall x1. (exists a. g' a == g' x' /\ f' a == x1) ->> x1 == f' x'
   ---------------------------------------------------------------------
   G // H
   |- forall g,f.
        (forall x,y. g x == g y ->> f x == f y)
        ->> exists h. forall x. h (g x) == f x
.... *)

(* subgoal 1 *)
at simpR; 
at (chooseExLTac ["a"]);
htog 1;
at (chooseAllLTac libPenv ["a'","x'"]);
at(rewriteTac[]);

(* subgoal 2 *)
at (chooseExRTac libPenv ["f' x'","x'"]);
at(rewriteTac[]);