Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: 15 Apr 92 2:46 +0100
From: Jeffrey Joyce <joyce@ca.ubc.cs>
To: info-hol <info-hol@edu.uidaho.cs.ted>
Message-Id: <4580*joyce@cs.ubc.ca>

In reply to Matt Kaufmann's request for challenging theorems ...
here is a (what I believe is) a theorem of natural number arithmetic
that exceeded my threshold for the amount of HOL-hacking effort that
I'm willing to invest in something of this size/complexity.

"!A B C n i.
  i < n ==>
  (((((2 EXP (n - i)) * (A * (B MOD (2 EXP i)))) + (C DIV (2 EXP i))) DIV
    2) +
   ((B DIV ((2 EXP i) MOD 2)) * (A * (2 EXP (n - 1)))) =
   ((2 EXP (n - (i + 1))) * (A * (B MOD (2 EXP (i + 1))))) +
   (C DIV (2 EXP (i + 1))))"

Here is a brief sketch of the proof,

    by using the fact that i < n to re-arrange the equation, then
    substracting (C DIV (2 EXP (i+1))) from both sides and then
    dividing both sides by ((2 EXP (n-(i+1))) * A),

       (B MOD (2 EXP i)) + ((B DIV (2 EXP i) MOD 2) * (2 EXP i))) =
       (B MOD (2 EXP (i+1)))

    by more arithmetic, etc...

The actual proof is more complicated than the above sketch suggests.
It depends on a number of lemmas about natural number arithmetic.

I sent the above maybe-theorem to Matt Kaufmann yesterday ... and
accordingly to Matt, it was a surprisingly difficult problem for BMTP.

If there are any HOL-hackers out there looking for a challenge, I'd
be interested in whether if anyone can prove this theorem with
HOL in under 4 hours and less than a page of ML source code.
Of course, I mean "can you develop the proof in HOL in less than 4
hours ?" rather than "is there a proof script which will run in less
than 4 hours ?")

If you'd like some context for this theorem, it is the key part of
one of the verification conditions for the following IMP program.
(where IMP is Mike Gordon's toy imperative language):

      {0 <= N and S < (2 EXP N) and B < (2 EXP N)}
      I := 0;
      WHILE not (I = N) DO
        BEGIN
          S := (S DIV 2) + (((B DIV (2 EXP I)) MOD 2) * A * (2 EXP (N-1)));
          I := I + 1;
        END
      {S = A * B}
      

 -- Jeff