; What's New in ACL2?
; Matt Kaufmann (and J Moore)
; ACL2 Workshop 2007, November 16, 2007

; Note: I have a lot to cover, so I'd appreciate holding of till the
; final session today for general discussion of ACL2 issues, such as
; the location of the next workshop.  But, of course, I'm happy to
; answer questions.

; Version 3.3 was released last week.

; In short: The release notes show what's new, and we encourage you to
; read them.  Note that :doc note-3-3 refers to :doc note-3-2-1, which
; has changes from Version 3.2 (4/07) to Version 3.2.1 (8/07); but I
; won't discuss that here.

; Thanks to everyone for the feedback!  As you can see in the release
; notes, it's led to a lot of improvements.

; NEXT, I'll highlight some items on the note-3-3 web page.  An
; alternative (but with fewer links) is to use the Emacs Info version
; of the documentation -- you can use meta-x acl2-info (see (1)
; below).

;;;;;

; Some side comments:

; (1) Emacs support for ACL2 keeps improving.  Consider using emacs
; and putting something like this in your .emacs file:

;    (load "/proj/acl2-sources/emacs/emacs-acl2.el")

; The top of emacs-acl2.el documents what is provided by this file.

; (2) (RESET-PREHISTORY) can be very useful during development, so
; that :ubt never takes you back before the start of what you're
; doing.  I used it in developing the rest of what I'll discuss in
; this talk.

; (3) I won't talk about clause-processors (see :DOC
; clause-processor), but with all the progress in automated tools
; reported at FMCAD this week, I hope efforts will continue to take
; advantage of this ability to connect external tools with ACL2, as
; for example Erik Reeber and Sudarshan Srinivasan have done.

;;;;;

; But mostly I want to discuss a new feature, gag-mode.  This is a
; short version of a demo talk I gave in the UT Austin ACL2 seminar on
; 10/17/07.  You can visit the seminar web page (linked to from the
; ACL2 home page) for notes from that talk.

; J and I are grateful for discussions about the design of gag-mode,
; in particular with Sandip Ray and Robert Krug.

; IMPORTANT: We currently intend to make gag-mode the default in the
; next ACL2 release.  So please let us know if you have any
; suggestions for improvements, or if there is any reason you are
; avoiding using it!

; To use it, just put this in your ~/acl2-customization.lisp file:

(set-gag-mode t) ; or, (set-gag-mode :goals)

; So what is gag-mode?  In a nutshell, it is a setting that is
; intended to restrict proof output to what is most useful.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma discovery.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(set-gag-mode t)
(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))))

; Note the hiding of sub-induction goals when they are pushed.

; Note the summary, which is printed even if all output is suppressed,
; an extreme version.

:pso ; Print Saved Output, if you want all the output after all

; Note that gag-mode printed only the so-called "key checkpoints":
; those goals stable under simplification that are not descendents of
; such.

(set-inhibit-output-lst '(prove proof-tree))
(thm (equal (rev (append x y)) (append (rev y) (rev x))))

; Now fix the proof by proving a relevant lemma based on a displayed
; "key checkpoint".

(defthm append-nil
  (implies (true-listp x)
           (equal (append x nil) x)))
(defthm true-listp-rev
  (true-listp (rev x)))
(thm (equal (rev (append x y)) (append (rev y) (rev x))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Now let's look at :or hints.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Re-start 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)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Using dmr with :goals setting
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

cd ~/acl2/v3-3/acl2-sources/books/workshops/2004/legato/support/
; Start up ACL2:
(rebuild "proof-by-generalization-mult.lisp" t)
(dmr-start)
(u)
(u)
(set-gag-mode :goals)
; Control-t 1 and then split the screen:
; Try aborting the following after going into induction -- summary
; still works.
; Note: Aborting doesn't give summary you'd expect unless you do:
;  (SET-DEBUGGER-ENABLE T)
; I hope to fix this for the next release.
(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)))

; [end]