defmin-int-template

(in-package "ACL2")

(include-book "std/basic/defs" :dir :system)

(encapsulate (((xp *) => *)) (local (defun xp (x) x)))

(encapsulate (((elementp * *) =>
     *
     :formals (x y)
     :guard (and (xp x) (integerp y))))
  (local (defun elementp (x y) (cons x y))))

(defun-sk lboundp
  (x y)
  (declare (xargs :guard (and (xp x) (integerp y))))
  (forall (y1)
    (impliez (and (integerp y1) (elementp x y1))
      (<= (ifix y) y1)))
  :rewrite (implies (and (lboundp x y) (integerp y1) (elementp x y1))
    (<= (ifix y) y1)))

(defthm booleanp-of-lboundp (booleanp (lboundp x y)))

(in-theory (disable lboundp lboundp-necc))

(defun-sk existsp
  (x)
  (declare (xargs :guard (xp x)))
  (exists (y) (and (integerp y) (elementp x y) (lboundp x y)))
  :skolem-name existsp-witness)

(defthm booleanp-of-existsp (booleanp (existsp x)))

(in-theory (disable existsp existsp-suff))

(defun f
  (x)
  (declare (xargs :guard (xp x)))
  (if (existsp x)
    (existsp-witness x)
    nil))

(defthm maybe-integerp-of-f
  (maybe-integerp (f x))
  :hints (("Goal" :in-theory (enable maybe-integerp existsp))))

(defthm integerp-of-f-equal-existsp
  (equal (integerp (f x)) (existsp x))
  :hints (("Goal" :in-theory (enable existsp))))

(defthm integerp-of-f-when-existsp
  (implies (existsp x) (integerp (f x)))
  :rule-classes :type-prescription)

(defthm f-iff-existsp
  (iff (f x) (existsp x))
  :hints (("Goal" :in-theory (enable existsp))))

(defthm not-f-when-not-existsp
  (implies (not (existsp x)) (not (f x)))
  :rule-classes :type-prescription)

(defthm elementp-of-f-when-existsp
  (implies (existsp x) (elementp x (f x)))
  :hints (("Goal" :in-theory (enable existsp))))

(defthm lboundp-of-f-when-existsp
  (implies (existsp x) (lboundp x (f x)))
  :hints (("Goal" :in-theory (enable existsp))))

(defthm f-leq-when-existsp-linear
  (implies (and (existsp x) (elementp x y1) (integerp y1))
    (<= (f x) y1))
  :rule-classes :linear :hints (("Goal" :in-theory (disable f)
     :use (lboundp-of-f-when-existsp (:instance lboundp-necc (y (f x)))))))

(defthm f-leq-when-existsp-rewrite
  (implies (and (existsp x) (elementp x y1) (integerp y1))
    (<= (f x) y1))
  :hints (("Goal" :by f-leq-when-existsp-linear)))

(defthm f-geq-when-existsp-linear
  (implies (and (existsp x) (lboundp x y1) (integerp y1))
    (>= (f x) y1))
  :rule-classes :linear :hints (("Goal" :in-theory (disable f)
     :use (:instance lboundp-necc (y1 (f x)) (y y1)))))

(defthm f-geq-when-existsp-rewrite
  (implies (and (existsp x) (lboundp x y1) (integerp y1))
    (>= (f x) y1))
  :hints (("Goal" :by f-geq-when-existsp-linear)))

(in-theory (disable f))

(defthm lbound-leq-member
  (implies (and (integerp y0)
      (elementp x y0)
      (integerp y1)
      (lboundp x y1))
    (<= y1 y0))
  :rule-classes nil
  :hints (("Goal" :use (:instance lboundp-necc (y y1) (y1 y0)))))

(defthm lbound-nonmember-lt-member
  (implies (and (integerp y0)
      (elementp x y0)
      (integerp y1)
      (lboundp x y1)
      (not (elementp x y1)))
    (< y1 y0))
  :rule-classes nil
  :hints (("Goal" :use lbound-leq-member)))

(defun find-min
  (x y1 y0)
  (declare (xargs :measure (nfix (- y0 y1))
      :hints (("Goal" :use lbound-nonmember-lt-member))))
  (if (and (integerp y0)
      (elementp x y0)
      (integerp y1)
      (lboundp x y1))
    (if (elementp x y1)
      y1
      (find-min x (1+ y1) y0))
    0))

(defthm find-min-lboundp-preservation
  (implies (and (integerp y0)
      (elementp x y0)
      (integerp y1)
      (lboundp x y1)
      (not (elementp x y1)))
    (lboundp x (1+ y1)))
  :hints (("Goal" :expand ((lboundp x (1+ y1)))
     :use (:instance lboundp-necc
       (y y1)
       (y1 (lboundp-witness x (1+ y1)))))))

(defthm elementp-of-find-min
  (implies (and (integerp y0)
      (elementp x y0)
      (integerp y1)
      (lboundp x y1))
    (elementp x (find-min x y1 y0)))
  :hints ('(:use (:instance lboundp-necc (y y1) (y1 0))) '(:use (:instance lboundp-necc (y 0) (y1 y0)))))

(defthm lboundp-of-find-min
  (implies (and (integerp y0)
      (elementp x y0)
      (integerp y1)
      (lboundp x y1))
    (lboundp x (find-min x y1 y0)))
  :hints ('(:use (:instance lboundp-necc (y y1) (y1 0))) '(:use (:instance lboundp-necc (y 0) (y1 y0)))))

(defthm existsp-when-nonempty-and-bounded
  (implies (and (integerp y0)
      (elementp x y0)
      (integerp y1)
      (lboundp x y1))
    (existsp x))
  :rule-classes nil
  :hints (("Goal" :use (:instance existsp-suff (y (find-min x y1 y0))))))

(defthm equal-when-member-and-lbound
  (implies (and (integerp y) (elementp x y) (lboundp x y))
    (equal (f x) y))
  :rule-classes nil
  :hints (("Goal" :in-theory (disable f-leq-when-existsp-rewrite
       f-geq-when-existsp-rewrite)
     :use ((:instance existsp-when-nonempty-and-bounded (y0 y) (y1 y)) (:instance f-leq-when-existsp-rewrite (y1 y))
       (:instance lboundp-necc (y1 (f x)))))))