problem13

other

(in-package "ACL2")

include-book

(include-book "arithmetic/equalities" :dir :system)

include-book

(include-book "arithmetic/inequalities" :dir :system)

include-book

(include-book "ordinals/e0-ordinal" :dir :system)

other

(set-well-founded-relation e0-ord-<)

npother

(defabbrev np (x) (and (integerp x) (>= x 0)))

range-fencapsulate

(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))))
  (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))

ind-hintfunction

(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)))))

f-i-x->=-x-lemmatheorem

(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)

f-i-x->=-xtheorem

(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)

f-lower-boundtheorem

(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)

f-monotonicity-lemmatheorem

(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))))))))

nat-indfunction

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

f-monotonicitytheorem

(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)))))))

q-witness-less-than-twotheorem

(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)))

g-f-rewritetheorem

(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))))

in-theory

(in-theory (disable g))

f-upper-boundtheorem

(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)

f-is-idtheorem

(defthm f-is-id
  (implies (np n) (equal (f n) n))
  :hints (("Goal" :use (f-lower-bound f-upper-bound))))

Included Books