find-minimal-2d

(in-package "ACL2")

(encapsulate ((fmla (x y) t))
  (local (defun fmla (x y) (* x y)))
  (defthm integerp-fmla
    (implies (and (integerp x) (integerp y))
      (integerp (fmla x y)))
    :rule-classes :type-prescription))

(defun find-minimal2
  (x loy hiy min)
  (declare (xargs :measure (nfix (- (+ 1 (ifix hiy)) (ifix loy)))))
  (cond ((not (and (integerp loy) (integerp hiy))) min)
    ((> loy hiy) min)
    (t (find-minimal2 x
        (+ 1 loy)
        hiy
        (if (or (null min) (< (fmla x loy) min))
          (fmla x loy)
          min)))))

(defun find-minimal1
  (lox hix loy hiy min)
  (declare (xargs :measure (nfix (- (+ 1 (ifix hix)) (ifix lox)))))
  (cond ((not (and (integerp lox) (integerp hix))) min)
    ((> lox hix) min)
    (t (find-minimal1 (+ 1 lox)
        hix
        loy
        hiy
        (find-minimal2 lox loy hiy min)))))

(defun find-minimal
  (lox hix loy hiy)
  (find-minimal1 lox hix loy hiy nil))

(defthm find-minimal2-decreases
  (implies (and min (integerp x))
    (<= (find-minimal2 x loy hiy min) min))
  :rule-classes :linear)

(defthm integerp-find-minimal2
  (implies (and (integerp x)
      (integerp loy)
      (integerp hiy)
      (or (null min) (integerp min)))
    (equal (integerp (find-minimal2 x loy hiy min))
      (if (null min)
        (<= loy hiy)
        t))))

(defthm non-nil-find-minimal2
  (implies (and (integerp x) (integerp loy) (integerp hiy))
    (iff (find-minimal2 x loy hiy min) (or min (<= loy hiy)))))

(defthm find-minimal1-decreases
  (implies (and min
      (integerp lox)
      (integerp hix)
      (integerp loy)
      (integerp hiy))
    (<= (find-minimal1 lox hix loy hiy min) min))
  :rule-classes :linear)

(defthm integerp-find-minimal1
  (implies (and (integerp lox)
      (integerp hix)
      (integerp loy)
      (integerp hiy)
      (or (null min) (integerp min)))
    (equal (integerp (find-minimal1 lox hix loy hiy min))
      (if (null min)
        (and (<= lox hix) (<= loy hiy))
        t))))

(defun below-all2
  (min x loy hiy)
  (declare (xargs :measure (nfix (- (+ 1 (ifix hiy)) (ifix loy)))))
  (cond ((not (and (integerp loy) (integerp hiy))) t)
    ((> loy hiy) t)
    ((<= min (fmla x loy)) (below-all2 min x (+ 1 loy) hiy))
    (t nil)))

(defun below-all1
  (min lox hix loy hiy)
  (declare (xargs :measure (nfix (- (+ 1 (ifix hix)) (ifix lox)))))
  (cond ((not (and (integerp lox) (integerp hix))) t)
    ((> lox hix) t)
    ((below-all2 min lox loy hiy) (below-all1 min (+ 1 lox) hix loy hiy))
    (t nil)))

(defthm below-all2-find-minimal2
  (implies (and (integerp x)
      (integerp loy)
      (integerp hiy)
      (or (null xxx) (integerp xxx)))
    (below-all2 (find-minimal2 x loy hiy xxx) x loy hiy)))

(defthm below-all2-trans
  (implies (and (<= min1 min2) (below-all2 min2 x loy hiy))
    (below-all2 min1 x loy hiy))
  :rule-classes nil)

(defthm below-all1-find-minimal1
  (implies (and (integerp lox)
      (integerp hix)
      (integerp loy)
      (integerp hiy)
      (or (null xxx) (integerp xxx)))
    (below-all1 (find-minimal1 lox hix loy hiy xxx)
      lox
      hix
      loy
      hiy))
  :hints (("Goal" :induct (find-minimal1 lox hix loy hiy xxx)) ("Subgoal *1/2" :use ((:instance below-all2-trans
         (x lox)
         (min1 (find-minimal1 (+ 1 lox)
             hix
             loy
             hiy
             (find-minimal2 lox loy hiy xxx)))
         (min2 (find-minimal2 lox loy hiy xxx))))
      :do-not '(generalize))))

(defthm below-all2-is-a-universal-quantifier
  (implies (and (below-all2 min x loy hiy)
      (integerp x)
      (integerp loy)
      (integerp hiy)
      (integerp y)
      (<= loy y)
      (<= y hiy))
    (<= min (fmla x y)))
  :rule-classes :linear)

(defthm below-all1-is-a-universal-quantifier
  (implies (and (below-all1 min lox hix loy hiy)
      (integerp lox)
      (integerp hix)
      (integerp loy)
      (integerp hiy)
      (integerp x)
      (<= lox x)
      (<= x hix)
      (integerp y)
      (<= loy y)
      (<= y hiy))
    (<= min (fmla x y)))
  :rule-classes nil)

(defthm find-minimal-correct
  (implies (and (integerp lox)
      (integerp hix)
      (integerp loy)
      (integerp hiy)
      (integerp x)
      (<= lox x)
      (<= x hix)
      (integerp y)
      (<= loy y)
      (<= y hiy))
    (and (integerp (find-minimal lox hix loy hiy))
      (<= (find-minimal lox hix loy hiy) (fmla x y))))
  :hints (("Goal" :use (:instance below-all1-is-a-universal-quantifier
       (min (find-minimal lox hix loy hiy)))))
  :rule-classes nil)