Soundness Example: Functional Instantiation Bug

;;;============================================================================

;;;
;;; A bug in ACL2 (2.5 and 2.6). Proving "0=1".
;;; Francisco J. Martin-Mateos
;;; email: Francisco-Jesus.Martin@cs.us.es
;;; Dpt. of Computer Science and Artificial Intelligence
;;; University of SEVILLE
;;;
;;;============================================================================

;;;   I've found a bug in ACL2 (2.5 and 2.6). The following events prove that
;;; "0=1".

(in-package "ACL2")

(encapsulate
 (((g1) => *))

 (local
  (defun g1 ()
    0))

 (defthm 0=g1
   (equal 0 (g1))
   :rule-classes nil))

(defun g1-lst (lst)
  (cond ((endp lst) (g1))
 (t (g1-lst (cdr lst)))))

(defthm g1-lst=g1
  (equal (g1-lst lst) (g1)))

(encapsulate
 (((f1) => *))

 (local
  (defun f1 ()
    1)))

(defun f1-lst (lst)
  (cond ((endp lst) (f1))
 (t (f1-lst (cdr lst)))))

(defthm f1-lst=f1
  (equal (f1-lst lst) (f1))
  :hints (("Goal"
    :use (:functional-instance g1-lst=g1
          (g1 f1)
          (g1-lst f1-lst)))))

(defthm 0=f1
  (equal 0 (f1))
  :rule-classes nil
  :hints (("Goal"
    :use (:functional-instance 0=g1
          (g1 f1)))))

(defthm 0=1
  (equal 0 1)
  :rule-classes nil
  :hints (("Goal"
    :use (:functional-instance 0=f1
          (f1 (lambda () 1))))))

;;;   The theorem F1-LST=F1 is not proved via functional instantiation but it
;;; can be proved via induction. So, the constraints generated by the
;;; functional instantiation hint has not been proved. But when the theorem
;;; 0=F1 is considered, the constraints generated in the functional
;;; instantiation hint are bypassed because they ".. have been proved when
;;; processing the event F1-LST=F1", and the theorem is proved !!!. Finally,
;;; an instance of 0=F1 can be used to prove 0=1.

;;;============================================================================