NOTE-3-0-2

Major Section:  RELEASE-NOTES

NOTE: This is an annotated copy of :DOC NOTE-3-0-2.

Pkg-witness bug allowed proof of nil. This shows the delicacy of *1* functions.

Tracking of forcing is subtle.

(encapsulate
 ()


 (local (defun foo (x y)
          (declare (xargs :measure (acl2-count y)))
          (if (and (consp x) (consp y))
              (foo (cons x x) (cdr y))
            y)))


; So the following is redundant -- but it guesses a measure
; of (acl2-count x), which isn't right!
 (defun foo (x y)
   (if (and (consp x) (consp y))
       (foo (cons x x) (cdr y))
     y)))


; end of encapsulate


; Now we prove a non-theorem by exploiting the bug above,
; erroneously replacing formal y by a constant in the induction
; scheme hinted below.  (This should not be allowed, as y should be
; labeled as a measured formal.)


(defthm bad
  (atom x)
  :rule-classes nil
  :hints (("Goal" :induct (foo x '(3)))))


; It's easy to get a contradiction by instantiating the
; non-theorem just above.
(defthm contradiction
  nil
  :rule-classes nil
  :hints (("Goal" :use ((:instance bad (x '(7)))))))

We've previously talked about this one at some length.

Made nice :pl improvements.

:Ubu and :ubu! can be quite handy.

Illustrates how to do induction proofs by functional instantiation.

Please contribute books! It's pretty simple now; look for link with "How to Contribute" on home page.

Perhaps Sandip has a word to say about these?

You'll need to change any theory-invariant expressions to use ENS instead of THEORY.

Users have wanted defun-sk to create nicer rewrite rules. This still isn't the default, but at least now it's easy to get this behavior.

I could give a demo. This is nice if you have some preliminary stuff that you want to leave around.

; The "what could be considered a soundness hole" could be exploited as
; follows.

;     (in-package "ACL2")
;     
;     ; Portcullis commands:
;     #|
;     (set-ld-redefinition-action '(:warn! . :overwrite) state)
;     
;     (encapsulate
;      ()
;      (defun foo () t)
;      (local (defun foo () nil))
;      (defthm foo-prop
;        (equal (foo) nil)
;        :rule-classes nil))
;     |# ; |
;     
;     ; NOTE: After the above commands:
;     ; ACL2 !>(redefined-names state)
;     ; NIL
;     ; ACL2 !>
;     
;     ; Now execute:
;     
;     ; (certify-book "bad" 1)
;     
;     (defthm contradiction
;       nil
;       :hints (("Goal" :use foo-prop))
;       :rule-classes nil)

; After certifying the book we can do this:

; (include-book "bad")
; (thm nil :hints (("Goal" :use contradiction)))

The new axiom allows the obtaining of a canonical representative.

Note also expander.lisp.

This is a pretty sweeping change, since it lets you put almost anything into a book, even raw Lisp! I might discuss some of the sub-points just below.

A new event, remove-untouchable, can be used to give users access to system functions and data structures. We also fixed a bug in push-untouchable; and, it no longer is a no-op in :program mode. Thanks to Peter Dillinger for proposing remove-untouchable and suggesting that it and push-untouchable be functional in :program mode.

Raw-mode (see set-raw-mode) no longer disables certify-book. However, set-raw-mode is now disallowed unless there is an active ttag (see defttag). If you want to execute (set-raw-mode t) and there is no active ttag, consider executing (set-raw-mode-on!) instead.

Redefinition of system functions is disallowed unless there is an active ttag. However, redef! now introduces (defttag :redef!) in order to allow redefinition of system functions.

A new event, progn!, is a legal embedded event form that can go in books and both encapsulate and progn forms (see embedded-event-form), and is similar to progn except that it allows arbitrary forms. Thus, a progn! form is potentially dangerous and can only be evaluated if there is an active ttag.

See ttags-seen for information about how to find the ttags known in the current ACL2 world, and for related caveats.

A new book created with Peter Dillinger, books/misc/hacker.lisp, uses progn! to define utiliities with-raw-mode and with-redef-allowed, which respectively allow raw Lisp evaluation and redefinition to take place within a certifiable book (!).

(defstobj st fld)
(update-fld 3 st)
(certify-book "foo" 1) ; where foo.lisp contains (defstobj st fld)

Wow, this had been awaiting a fix for a long time.

This one is particularly useful for automatically-generated code when you don't want to use set-ignore-ok.

I'm sure Grant would like feedback.

Alex and Robert would probably like feedback.

o A new rule |(* (/ x) (/ (expt x n)))| in bind-free/collect.lisp, which is important for reducing collect-* expressions though it slowed down one proof (see comment above this rule in bind-free/collect.lisp).

o Slight improvements of rules integerp-mod and rationalp-mod in floor-mod/floor-mod.lisp.

o To avoid conflict with books/rtl/rel6/arithmetic/, renamed rule mod-minus to mod-neg in floor-mod/floor-mod.lisp, and renamed integerp-+-reduce-leading-constant to integerp-+-reduce-leading-rational-constant in bind-free/integerp.lisp.

Could be useful.