[acl2/acl2] 9266b9: Improved handling of contradictions by tau (thanks...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 9266b9fb86a55b9112c005a37b90ed834d9a0996
https://github.com/acl2/acl2/commit/9266b9fb86a55b9112c005a37b90ed834d9a0996
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2017-06-11 (Sun, 11 Jun 2017)

Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp

Log Message:
-----------
Improved handling of contradictions by tau (thanks to code from J Moore).

Recently I checked in a change with the following paragraph from :doc
note-7-5:

A bug that was in the [tau-system] is illustrated by the following
example sent by Grant Passmore, in which tau discovers that the
function being defined always returns nil, hence implies
everything. Tau no longer causes an error in this situation.

(defun f (x) (> x 0))
(defun g (x) (< x 0))
(defun h (x) (and (f x) (g x)))

I made a further commit a few moments ago
(00403f44a0f0ec627f4a5a9aaec12b63b1b2e80d) that unfortunately failed
to mention an improvement, by incorporating code supplied by J. Here
is an addition made to the paragraph above (from :doc note-7-5) that
explains this improvement.

Moroever, tau ``knows'' that the function h above is contradictory,
as evidenced by the successful proof of the thm below.

(thm
(implies (h x) (consp x))
:hints (("Goal" :in-theory '((:e tau-system)))))

[GitHub]

Branch: refs/heads/testing