Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Wed, 22 Apr 92 15:06:14 EDT
From: sentot@ca.on.ora (Sentot Kromodimoeljo)
Message-Id: <9204221906.AA22627@alpha.ora.on.ca>
To: info-hol@edu.uidaho.cs.ted
Subject: Solution to Jeff's challenge in Eves


  The following is the script for a somewhat cleaned up version of our
(mainly Mark Saaltink's) solution to Jeff's challenge problem in Eves.
Each declaration is followed by the proof commands that are required
to discharge the declaration's proof obligation.  The entire thing is
about 200 lines and takes about 2 minutes to run on an Eves built on
top of AKCL on a SparcStation-2.

  The entire development of the script took about 2.5 hours which
includes proving all of the needed lemmas.  Most of the lemmas are
fairly general and ought to be included in the Eves standard library.

----------------------------

(function exp (b e)
    ((measure e))
  (if (> e 0)
      (* b (exp b (- e 1)))
      1))
(REDUCE)

(grule exp-type (b e)
  (implies (in b (int))
	   (= (type-of (exp b e)) (int))))
(PROVE-BY-INDUCTION)

(rule exp-by-1 (b)
  (implies (in b (int))
	   (= (exp b 1) b)))
(REDUCE)

(rule exp-1 (e)
  (= (exp 1 e)
     1))
(PROVE-BY-INDUCTION)

(grule *-non-negative (x y)
  (implies (and (>= x 0) (>= y 0))
           (>= (* x y) 0)))
(REDUCE)

(rule exp-plus (base e1 e2)
  (implies (and (<= 0 e1)
		(<= 0 e2)
		(in base (int)))
	   (= (exp base (+ e1 e2))
	      (* (exp base e1) (exp base e2)))))
(PROVE-BY-INDUCTION)
(EQUALITY-SUBSTITUTE)
(REWRITE)

(grule exp-nonnegative (b e)
  (implies (>= b 0)
	   (>= (exp b e) 0)))
(PROVE-BY-INDUCTION)

(grule exp-positive (b e)
  (implies (>= b 1)
	   (>= (exp b e) 1)))
(PROVE-BY-INDUCTION)

(axiom div-mod-fact (x d)
  (implies (and (>= x 0)
		(>= d 1))
	   (and (= x (+ (* d (div x d)) (mod x d)))
		(<= 0 (mod x d))
		(< (mod x d) d))))
(INDUCT)
(WITH-ENABLED (DIV MOD) (REDUCE))

(grule div-mod-1 (x d)
  (implies (and (>= x 0)
		(>= d 1))
	   (= x (+ (* d (div x d)) (mod x d)))))
(USE DIV-MOD-FACT (X X)(D D))
(SIMPLIFY)

(grule div-mod-2 (x d)
  (implies (and (>= x 0)
		(>= d 1))
	   (<= 0 (mod x d))))
(USE DIV-MOD-FACT (X X)(D D))
(SIMPLIFY)

(grule div-mod-3 (x d)
  (implies (and (>= x 0)
		(>= d 1))
	   (<= (mod x d) (- d 1))))
(USE DIV-MOD-FACT (X X)(D D))
(SIMPLIFY)

(axiom *-monotonic (x y z)
  (implies (and (= (type-of x) (int))
		(= (type-of y) (int))
		(>= z 1))
	   (= (>= x y) (>= (* z x) (* z y)))))
(SPLIT (>= X Y))
(SIMPLIFY)
(SPLIT (>= (* Z (- X Y)) 0))
(SIMPLIFY)
(REARRANGE)
(SIMPLIFY)

(axiom div-mod-4-lemma (d x r)
  (implies (and (= (type-of d) (int))
		(= (type-of x) (int))
		(= (type-of r) (int))
		(= (+ (* d x) r) 0)
		(< (negate d) r)
		(< r d))
	   (and (= r 0)
		(= x 0))))
(USE *-MONOTONIC (Z D) (X X) (Y 1))
(USE *-MONOTONIC (Z D) (X -1) (Y X))
(REARRANGE)
(SIMPLIFY)

(axiom div-mod-4 (x d q r)
  (implies (and (>= x 0)
		(>= d 1)
		(= (type-of q) (int))
		(= x (+ r (* d q)))
		(<= 0 r)
		(< r d))
	   (and (= q (div x d))
		(= r (mod x d)))))
(USE DIV-MOD-4-LEMMA (D D) (X (- (DIV X D) Q)) (R (- (MOD X D) R)))
(REARRANGE)
(REWRITE)

(grule div-nonnegative (x d)
  (implies (and (>= x 0)
		(>= d 1))
	   (>= (div x d) 0)))
(WITH-ENABLED (DIV) (PROVE-BY-INDUCTION))

(axiom *-distributes-over-+ (x y z)
  (implies (and (= (type-of x) (int))
		(= (type-of y) (int))
		(= (type-of z) (int)))
	   (= (* x (+ y z))
	      (+ (* x y) (* x z)))))
(SIMPLIFY)

(axiom div-div-fact (x y z)
  (implies (and (>= x 0)
		(> y 0)
		(> z 0))
	   (and (= (div (div x y) z)
		   (div x (* y z)))
		(= (mod x (* y z))
		   (+ (* y (mod (div x y) z)) (mod x y))))))
(USE DIV-MOD-4
     (D (* Y Z))
     (X X)
     (Q (DIV (DIV X Y) Z))
     (R (+ (* Y (MOD (DIV X Y) Z)) (MOD X Y))))
(USE *-DISTRIBUTES-OVER-+
     (X Y)
     (Y (MOD (DIV X Y) Z))
     (Z (* Z (DIV (DIV X Y) Z))))
(USE *-MONOTONIC (Z Y) (X (- Z 1)) (Y (MOD (DIV X Y) Z)))
(REARRANGE)
(REWRITE)


(rule div-div (x y z)
  (implies (and (>= x 0)
		(> y 0)
		(> z 0))
	   (= (div (div x y) z)
	      (div x (* y z)))))
(USE DIV-DIV-FACT (X X)(Y Y)(Z Z))
(SIMPLIFY)

(rule div-product (x y d)
  (implies (and (>= d 1)
		(>= x 0)
		(>= y 0))
	   (= (div (+ y (* d x)) d)
	      (+ x (div y d)))))
(USE DIV-MOD-4 (X (+ (* D X) Y)) (D D) (Q (+ X (DIV Y D))) (R (MOD Y D)))
(REARRANGE)
(REWRITE)

(axiom hol-problem ()
  (all (A B C n i)
    (implies (and (>= a 0)
		  (>= b 0)
		  (>= c 0)
		  (>= n 0)
		  (>= i 0)
		  (< i n))
	     (= (+ (DIV (+ (* (EXP 2 (- n i)) (* A (MOD B (EXP 2 i))))
			   (DIV C (EXP 2 i)))
			2)
		   (* (MOD (DIV B (EXP 2 i)) 2) (* A (EXP 2 (- n 1)))))
		(+ (* (EXP 2 (- n (+ i 1))) (* A (MOD B (EXP 2 (+ i 1)))))
		   (DIV C (EXP 2 (+ i 1))))))))
(OPEN)
(INVOKE (EXP 2 (- N I)))
(USE DIV-DIV-FACT (X B) (Y (EXP 2 I)) (Z 2))
(USE EXP-PLUS (BASE 2) (E1 (- (- N I) 1)) (E2 I))
(USE *-DISTRIBUTES-OVER-+
     (X (* A (EXP 2 (- (- N I) 1))))
     (Y (MOD B (EXP 2 I)))
     (Z (* (EXP 2 I) (MOD (DIV B (EXP 2 I)) 2))))
(REARRANGE)
(REWRITE)
(EQUALITY-SUBSTITUTE)
(REWRITE)

------------------------------

/sentot