; Gag-mode
; Matt Kaufmann
; ACL2 seminar
; 10/17/07

; Acknowledgements: Lots of discussion with J Moore, of course; also Sandip Ray
; and Robert Krug.

; For this talk I'll use:
; /projects/acl2/devel/allegro-saved_acl2

; First, some miscellaneous observations:

; 1. (RESET-PREHISTORY) was useful in the patch file, so that :ubt never took
;    me back before the patch.

; 2. I re-did the whole thing after I realized that we want to see output as
;    the proof is going along.  (Duh!)

; 3. Then I made major further changes to take advantage of existing output,
;    which provides a nice structure.  It only begs to be gagged when
;    describing HOW top-level simplification checkpoints ultimate generate
;    goals to prove by induction; more on that during the talk.

; 4. Suggestion:  Put something like this in your .emacs:
;    (load "/projects/acl2/devel/emacs/emacs-acl2.el")

; Overview of output:

(set-gag-mode t)
(mini-proveall)

; Lemma discovery (and, explain the hiding of sub-induction goals when they are
; pushed):

(ubt! 'mem-del)
(thm (implies (and (perm x y)
                   (mem a x))
              (mem a y)))
(defthm mem-del
  (implies (mem a (del b x)) (mem a x)))
(thm (implies (and (perm x y)
                   (mem a x))
              (mem a y)))

; Another lemma discovery:

(ubt! 1)
(defun rev (x)
  (if (consp x)
      (append (rev (cdr x)) (cons (car x) nil))
    nil))
(thm (equal (rev (append x y)) (append (rev y) (rev x))))
(defthm append-nil
  (implies (true-listp x)
           (equal (append x nil) x)))
(thm (equal (rev (append x y)) (append (rev y) (rev x))))
(defthm true-listp-rev
  (true-listp (rev x)))
(thm (equal (rev (append x y)) (append (rev y) (rev x))))

; Fixing false theorem:

(set-gag-mode nil)
(thm (equal (rev (rev x)) x))
; One has to wade through the output to see that *1.2 was proved.
; Let's try with gag-mode.
(set-gag-mode t)
(thm (equal (rev (rev x)) x))

; Avoiding excessive junk.

(ubt! 1)
(thm (equal (append (append x x) x) (append x x x)))
(set-gag-mode nil)
(thm (equal (append (append x x) x) (append x x x)))

; Trivial failures:

(set-gag-mode nil)
(thm (equal (car (cons x y)) (cons x x)))

; Forcing and pso.

(ubt! 1)
(with-output :off :all (mini-proveall))
(ubt! 'force-test)
(set-gag-mode t)
(thm
 (and (implies (ends-in-a-0 x)
               (equal (app0 (rev0 x) 0) (rev0 x)))
      (implies (ends-in-a-0 y)
               (equal (app0 (rev0 y) 0) (rev0 y)))
      (implies (ends-in-a-0 z)
               (equal (app0 (rev0 z) 0) (rev0 z)))))

; Presumably inspection of [2]Goal suggests to enable
; ends-in-a-zero (if we know the problem).  Of, notice
; this if we use proof-trees:

; Presumably inspection from the proof-tree line
; c  1 |  |  [2]Subgoal *1/4' ELIM
; using control-z o will set us to add this hint:
; :HINTS (("[2]Goal" :IN-THEORY (ENABLE ENDS-IN-A-ZERO)))

; Now let's look at :or hints.

acl2
(set-gag-mode t)
(ld "hints/basic-tests.lisp" :dir :system :ld-pre-eval-print t)
; Notice the use of thm? and not-thm?.
; Here's a good one to focus on.
(thm
 (property ccc)
 :hints (("Goal" :or ((:induct (append ccc x))
                      (:in-theory (enable bbb)
                                  :use (:instance mum (x ddd)))))))

; Another example of lemma discovery; and, illustration of :goals.

cd /projects/acl2/devel/books/workshops/2004/legato/support/
(set-gag-mode :goals)
(ld "proof-by-generalization-mult.lisp" :ld-pre-eval-print t)
(ubt! 1)
(rebuild "proof-by-generalization-mult.lisp" 'MOD-+-1)
(u)
(u) ; get rid of lemma, HACK
(defthm mod-+-1
  (implies (and (equal (mod a 2) 0)
                (natp i)
                (integerp a))
           (equal (mod (+ 1 a) (expt 2 i))
                  (if (equal i 0)
                      0 (+ 1 (mod a (expt 2 i))))))
  :hints (("Goal" :induct (ind-hint i)
           :do-not '(generalize))))
; Notice introduction of j above.  I suspect that Legato's strategy was to
; allow elim as a "legitimate" processor.  Let's try looking at things that
; way.  (Question: Should I document this?)
(@ checkpoint-processors)
(assign checkpoint-processors (cdr (@ checkpoint-processors)))
(defthm mod-+-1
  (implies (and (equal (mod a 2) 0)
                (natp i)
                (integerp a))
           (equal (mod (+ 1 a) (expt 2 i))
                  (if (equal i 0)
                      0 (+ 1 (mod a (expt 2 i))))))
  :hints (("Goal" :induct (ind-hint i)
           :do-not '(generalize))))
; At this point the discovery of HACK becomes clear:
(defthm hack
(IMPLIES (AND (EQUAL (EXPT 2 I) (+ 1 J))
              (INTEGERP J)
              (INTEGERP K)
              (< -1 J)
              (NOT (ZP I))
              (NOT (EQUAL I 1)))
         (not (EQUAL (+ 1 (MOD J (EXPT 2 (+ -1 I))))
                     (MOD (+ 1 J) (EXPT 2 (+ -1 I)))))))

;;;; DMR

(ubt! 1)
(rebuild "proof-by-generalization-mult.lisp" t)
(dmr-start)
(u)
(u)
(set-gag-mode :goals)
; Control-t 1 and then split the screen:
(defthm wp-zcoef-g-multiplies
   (implies (and (not (zp x))
		 (integerp i)
		 (<= x i)
		 (natp f1)
		 (natp low)
		 (natp a)
		 (natp c)
		 (< low (expt 2 i))
		 (natp f2)
		 (< f2 (expt 2 i)))
	    (equal (wp-zcoef-g f1 x c low a result f2 i)
		   (equal
		    (+ (floor (+ low (* (expt 2 i) a) (* (expt 2 i) (expt 2 i) c))
			      (expt 2 x))
		       (* f2
			  (mod f1 (expt 2 (1- x)))
			  (floor (expt 2 i) (expt 2 (1- x)))))
		    result)))
   :hints (("Subgoal *1/2.16"
	    :nonlinearp t)
	   ("Subgoal *1/2.15.1"
	    :nonlinearp t)
	   ("Subgoal *1/2.14.1"
	    :nonlinearp t)
	   ("Subgoal *1/2.13.1"
	    :nonlinearp t)
	   ("Subgoal *1/2.12"
	    :nonlinearp t)
	   ("Subgoal *1/2.11.1"
	    :nonlinearp t)))

======================================================================
PROBABLY STOP HERE
======================================================================

; Some more output to look at:

(ubt! 1)
(defun rev (x)
  (if (consp x)
      (append (rev (cdr x)) (cons (car x) nil))
    nil))
(defaxiom silly
  (implies (and (consp x) (force (equal (car x) 17))
                (equal (append (append (cdr x) (cdr x))
                               (cdr x))
                       (append (cdr x) (cdr x) (cdr x))))
           (equal (append (append (cdr x) x) x)
                  (append (cdr x)
                          (cons (car x) (append (cdr x) x))))))
; Fails:
(thm (and (equal (append (append x x) x) (append x x x))
          (implies (true-listp x) (equal (rev (rev x)) x))
          (true-listp (append x nil)))
     :otf-flg t)