Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: info-hol@cs.byu.edu
Subject: At a Los for something to do? (III)
Date: Tue, 26 Sep 1995 12:31:18 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:166970:950926113134"@cl.cam.ac.uk>


Having finally despaired of getting my message out from Finland, here's
an attempt from my old account!

I thought some of you might like to try your hand at the following little
logical puzzle. It was shown to me by Andrzej Trybulec, and I believe it's
originally due to Los.

Suppose P and Q are two binary relations, both transitive and at least one of
them symmetric. Then if for every x and y, either P x y or Q x y, one or other
of P and Q must be universally true. In HOL-speak:

  |- (!x y z. P x y /\ P y z ==> P x z) /\
     (!x y z. Q x y /\ Q y z ==> Q x z) /\
     (!x y. P x y ==> P y x) /\
     (!x y. P x y \/ Q x y) ==>
     (!x y. P x y) \/ (!x y. Q x y)

To start the ball rolling, here's an entry for the worst possible HOL proof. We
do a bit of quantifier manipulation to put it in prenex form with all the
universal quantifiers outside the existential ones. Using a classic result of
Bernays and Schoenfinkel, such assertions (with no function symbols) can be
reduced to proving a propositional tautology (32 variables in our case). This
is then solved using my BDD package.

This is a very bad proof because it doesn't give any intuition as to why the
result is true. What's more, it takes several minutes because the tautology
checking is slow. However it does illustrate a decision procedure which is a
classic in the automated theorem proving literature; see for example:

  @ARTICE{wang-mm,
          author          = "Hao Wang",
          title           = "Toward Mechanical Mathematics",
          journal         = "IBM Journal of research and development",
          year            = 1960,
          volume          = 4,
          pages           = "2--22"}

And it's nice to know that even in HOL, we can occasionally use a
sledgehammer approach. Here's the HOL proof (with the BDD stuff etc. taken for
granted -- maybe the TAUT library would work too):

  fun Union l = itlist union l [];;

  fun choose n l =
    if n = 0 then [[]] else
    let val subcase = choose (n - 1) l
     in Union (map (fn t => map (fn r => (t::r)) subcase) l)
    end;

  fun SIMPLE_EXISTS v th =
    EXISTS (mk_exists(v,concl th),v) th;

  fun SIMPLE_CHOOSE v th =
    CHOOSE(v,ASSUME (mk_exists(v,hd(hyp th)))) th;

  fun SIMPLE_DISJ_CASES th1 th2 =
    DISJ_CASES (ASSUME(mk_disj(hd(hyp th1),hd(hyp th2)))) th1 th2;

  val BERNAYS_SCHOENFINKEL_TAC =
    REWRITE_TAC[FORALL_SIMP, EXISTS_SIMP] THEN
    (fn (asl,w) =>
       let val (avs,abod) = strip_forall w
           val (evs,bod) = strip_exists abod
           val eth = DISCH_ALL(itlist SIMPLE_EXISTS evs (ASSUME bod))
           val coms = choose (List.length evs) avs
           val ith = end_itlist SIMPLE_DISJ_CASES
             (map (fn c => UNDISCH (INST (zip c evs) eth)) coms)
           val jth = DISCH_ALL ith
        in ([(asl,hd(hyp ith))],fn [th] => GENL avs (MP jth th))
       end);

  val LOS = prove
   (%`(!x y z. P x y /\ P y z ==> P x z) /\
      (!x y z. Q x y /\ Q y z ==> Q x z) /\
      (!x y. P x y ==> P y x) /\
      (!(x:'a) y. P x y \/ Q x y)
      ==> (!x y. P x y) \/ (!x y. Q x y)`,
    REWRITE_TAC[TAUT (%`(a ==> b) = ~a \/ b`)] THEN
    CONV_TAC (REDEPTH_CONV (NOT_FORALL_CONV ORELSEC
                            NOT_EXISTS_CONV ORELSEC
                       GEN_REWRITE_CONV I empty_rewrites [DE_MORGAN_THM])) THEN
    CONV_TAC (REDEPTH_CONV (RIGHT_OR_FORALL_CONV ORELSEC
                    LEFT_OR_FORALL_CONV)) THEN
    CONV_TAC (REDEPTH_CONV (OR_EXISTS_CONV ORELSEC
                            REWR_CONV DISJ_ASSOC)) THEN
    CONV_TAC (REDEPTH_CONV LEFT_OR_EXISTS_CONV) THEN
    BERNAYS_SCHOENFINKEL_TAC THEN
    CONV_TAC(EQT_INTRO o BDD_TAUT));;

The BDD stuff should appear (in cleaned-up form) in the next hol90 release. If
anyone desperately wants the source now, send me email.

John.

=========================================================================
John Harrison                   | email: jharriso@ra.abo.fi
Ebo Akademi University          | web:   http://www.abo.fi/~jharriso/
Department of Computer Science  | phone: +358 (9)21 265-4674
Lemminkdisenkatu 14a            | fax:   +358 (9)21 265-4732
20520 Turku                     | home:  +358 (9)21 2316132
FINLAND                         | time:  UTC+2:00
=========================================================================