acl2-books-source 7.1-1 / usr / share / acl2-7.1 / books / demos / knuth-bendix-problem-1.lisp

This file is indexed.

/usr/share/acl2-7.1/books/demos/knuth-bendix-problem-1.lisp is in acl2-books-source 7.1-1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below. 

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
; Copyright (C) 2014, Regents of the University of Texas
; Written by Matt Kaufmann (original date March, 2014)
; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.

; An example illustrating the use GL to prove unbounded theorems

; In :doc TIPS we see the following, which points to the present file.

;   Also assure that subexpressions on the left hand
;   side of a rewrite rule are in simplified form; see community-books
;   example books/demos/knuth-bendix-problem-1.lisp.

; The following from :doc INTRODUCTION-TO-REWRITE-RULES-PART-2 also describes
; the situation discussed in this file.

;   Choose a Left-Hand Side Already in Simplest Form:

; I've inserted comments below that are intended to make this all clear.

(in-package "ACL2")

; Introduce three functions and two properties of them.

(defun foo (x)
  x)

(defun bar (x)
  x)

(defun h1 (x)
  x)

(defthm rule-1
  (equal (h1 (foo (bar x)))
         x))

(defthm rule-2
  (equal (foo (bar x))
         x))

; Include a book defining the MUST-FAIL macro.

(include-book "misc/eval" :dir :system)

(must-fail

; The following theorem illustrates the "Knuth-Bendix problem".  Since
; rewriting is inside-out, rule-2 simplifies the term (foo (bar a)) to a.  So
; we are left with the simplification checkpoint (equal (h1 a) a), and rule-1
; is useless in simplifying the call of h1 because of the disappearance of the
; argument (foo (bar a)) of h1.

 (thm (equal (h1 (foo (bar a)))
             (foo (bar a)))
      :hints (("Goal"
               :in-theory
               (union-theories '(rule-1 rule-2)
                               (theory 'ground-zero))))))

(must-fail

; If we enable only rule-1, then of course the call of h1 is simplified using
; rule-1, but the second argument of EQUAL is not simplified (because rule-2 is
; disabled).

 (thm (equal (h1 (foo (bar a)))
             (foo (bar a)))
      :hints (("Goal"
               :in-theory
               (union-theories '(rule-1)
                               (theory 'ground-zero))))))

(must-fail

; If we enable only rule-2, then we're back to the behavior of the first THM
; attempt, since in both cases, rule-1 does nothing.

 (thm (equal (h1 (foo (bar a)))
             (foo (bar a)))
      :hints (("Goal"
               :in-theory
               (union-theories '(rule-2)
                               (theory 'ground-zero))))))

; WARNING: The following proof succeeds but is not recommended.  The necessary
; use of subgoal hints for this solution (necessary, as shown above) suggests a
; problem with our set of rules: the left-hand side of rewrite rule rule-1 is
; not in simplest ("normal") form, because it can be simplified using rule-2.
; We succeed here only because we first apply rule-1 to simplify the call of h1
; and then, later, we apply rule-2 to simplify the second argument of EQUAL,
; that is, (foo (bar a)).  What we want instead (see below) is a set of rewrite
; rules whose left-hand sides are all in simplest form, to avoid this sort of
; subgoal-level micromanagement (which can get quite complex in large proofs).

(defthm ugly-success
  (equal (h1 (foo (bar a)))
         (foo (bar a)))
  :hints (("Goal"
           :in-theory
           (union-theories '(rule-1)
                           (theory 'ground-zero)))
          ("Goal'"
           :in-theory
           (union-theories '(rule-2)
                           (theory 'ground-zero))))
  :rule-classes nil)

; So here is a better solution (that is, better than using subgoal-level
; hints).  First, we fix rule-1 so that its left-hand side has been simplified
; using rule-2.

(defthm rule-1-better
  (equal (h1 x)
         x))

; Now we disable rule-1 so that we only need to think about its "better"
; version.  Since we are specifying user-defined rules explicitly (see the call
; of union-theories below), we don't actually need to do this here.  But in
; general, one may wish to do this kind of disable so that the current theorey
; (set of enabled rule) is nice.

(in-theory (disable rule-1))

; Finally, our original THM succeeds, using rule-1-better in place of rule-1.

(defthm pretty-success
  (equal (h1 (foo (bar a)))
         (foo (bar a)))
  :hints (("Goal"
           :in-theory
           (union-theories '(rule-1-better rule-2)
                           (theory 'ground-zero))))
  :rule-classes nil)

APT Browse - Built by Thomas Orozco.