acl2-books-source 8.0dfsg-1 / usr / share / acl2-8.0dfsg / books / misc / problem13.lisp

This file is indexed.

/usr/share/acl2-8.0dfsg/books/misc/problem13.lisp is in acl2-books-source 8.0dfsg-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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
; Matyas Sustik
; November, 2001

; The following question was posted on the University of Texas
; Computer Science problem web page (located at
; http://www.cs.utexas.edu/users/xli/prob/) numbered problem 13:

; Let f be a function from naturals to naturals.  (Note that naturals
; are non-negative integers.)  It is given that:
;   Property P:: for every n, f^2(n) < f(n + 1) holds.
; Here f^2(n) means applying f twice on n, that is, f(f(n)).
; Prove that f is the identity function.
; Generalization: Prove that f is the identity function given that:
;   Property Q:: for every n exists an i >= 2 such that f^i(n) < f(n + 1).
; (Similarly, f^i(n) means applying f i times on n.)

; For a classical proof of the theorem visit to the above mentioned
; web page.  The article posted at that location contains several
; versions of ACL2 verified proofs about the P and the Q properties.
; Here I include the strongest result only.  I wish to say thanks to
; Peter Manolios who followed upon the first version of the proof
; posted to the ACL2 meeting list.

(in-package "ACL2")

; The following includes help ACL2 with arithmetic:
(include-book "arithmetic/equalities" :dir :system)
(include-book "arithmetic/inequalities" :dir :system)
(include-book "ordinals/e0-ordinal" :dir :system)
(set-well-founded-relation e0-ord-<)

; A shorthand for naturals:
(defabbrev np (x)
  (and (integerp x)
       (>= x 0)))

; This form introduces a constrained f function with the
; Q property.  The 'iterated' version is also defined and
; it is called g.  The existence of i in the Q-property
; for a given n is captured by the Q-witness function.
; The type-prescription rules help ACL2 to reason more
; efficiently.
(encapsulate
 (((f *) => *)
  ((Q-witness *) => *))
  (local (defun f (n) (nfix n)))
  (defthm range-f
    (and (integerp (f n))
         (>= (f n) 0))
    :rule-classes :type-prescription)
  (defun g (i n)
    (if (zp (nfix i))
	(nfix n)
      (g (+ -1 (nfix i)) (f n))))  ;tail recursiveness is important
  (local (defun Q-witness (n) (declare (ignore n)) 2))
  (defthm Q-witness-type
    (and (integerp (Q-witness n))
	 (<= 2 (Q-witness n)))
    :rule-classes :type-prescription)
  (defthm Q-property
    (< (g (Q-witness n) n) (f (+ 1 (nfix n))))
    :rule-classes nil))

; This function describes an induction scheme which is
; used in the following theorem.  To admit the function
; we had to provide a measure to prove termination.
(defun ind-hint (x y i)
  (declare (xargs  :measure (if (or (zp x) (zp i))
				0
			      (cons x i))))
  (if (or (zp x) (zp i))
      (list x y i)
    (list (ind-hint (+ -1 x)
		      (+ -1 y)
		      (Q-witness (+ -1 y)))
	  (ind-hint x
		      (f y)
		      (+ -1 i)))))

; This is the main lemma.
(defthm f-i-x->=-x-lemma
  (implies (and (np x)
		(np y)
		(np i)
		(<= 1 i)
		(<= x y))
	   (<= x (g i y)))
  :hints (("goal"
           :induct (ind-hint x y i))
	  ("subgoal *1/2'"
	   :use (:instance Q-property
			   (n (+ -1 y)))))
  :rule-classes nil)

(defthm f-i-x->=-x
  (implies (np i)
           (<= (nfix x) (g i x)))
  :hints (("Goal"
	   :use (:instance f-i-x->=-x-lemma
			   (y x))))
  :rule-classes nil)

(defthm f-lower-bound
  (<= (nfix n) (f n))
  :hints (("Goal"
	   :use (:instance f-i-x->=-x-lemma
			   (x n)
			   (y n)
			   (i 1))))
  :rule-classes nil)

(defthm f-monotonicity-lemma
  (implies (np n)
	   (< (f n) (f (+ 1 n))))
  :hints (("Goal"
	   :use (Q-property
		 (:instance f-i-x->=-x
			    (x (f n))
			    (i (+ -1 (Q-witness n))))))))

(defun nat-ind (x)
  (if (zp x)
      x
    (nat-ind (- x 1))))

(defthm f-monotonicity
  (implies (and (np x)
                (np y)
                (<= x y))
           (<= (f x) (f y)))
  :hints (("goal"
           :induct (nat-ind y))
          ("subgoal *1/2.1"
           :use ((:instance f-monotonicity-lemma (n (- y 1)))))))

(defthm Q-witness-less-than-two
  (and (equal (<= 2 (Q-witness n)) t)
       (equal (< (Q-witness n) 2) nil))
  :hints (("Goal"
	   :use Q-witness-type)))

(defthm g-f-rewrite
  (implies (integerp n)
	   (equal (g i (f n))
		  (g (+ 1 (nfix i)) n)))
  :hints (("Goal"
	   :expand (g (+ 1 (nfix i)) n))))

; We need to disable g, otherwise ACL2 goes into an infinite
; loop when tries to rewite a formula with g in it.
(in-theory (disable g))

(defthm f-upper-bound
  (implies (np n)
	   (<= (f n) n))
  :hints (("Goal"
	   :in-theory (disable f-monotonicity)
	   :use (Q-property
		 (:instance f-monotonicity
			    (x (+ 1 n))
			    (y (f n)))
		 (:instance f-i-x->=-x
			    (x (f (f n)))
			    (i (+ -2 (Q-witness n)))))))
  :rule-classes nil)

; This is the main theorem.
(defthm f-is-id
  (implies (np n)
	   (equal (f n) n))
  :hints (("Goal"
	   :use (f-lower-bound f-upper-bound))))

APT Browse - Built by Thomas Orozco.