defmin-int

(in-package "ACL2")

(defxdoc+ defmin-int-implementation
  :parents (defmin-int)
  :short "Implementation of @(tsee defmin-int)."
  :long (topstring (p "The implementation functions have formal parameters
     consistently named as follows:")
    (ul (li "@('state') is the ACL2 @(see state).")
      (li "@('ctx') is the context used for errors.")
      (li "@('f'),
      @('y'),
      @('x1...xn'),
      @('body'),
      @('guard'), and
      @('verify-guards')
      are the honomynous inputs to @(tsee defmin-int),
      where @('x1...xn') is shown as @('(x1 ... xn')) in the documentation.
      They have no types before being processed,
      then they acquire types implied by their validation.")))
  :order-subtopics t)

(defxdoc+ defmin-int-input-processing
  :parents (defmin-int-implementation)
  :short "Input processing performed by @(tsee defmin-int)."
  :long (topstring-p "Currently this validates the inputs lightly.
    It should be improved to do a more thorough validation.")
  :order-subtopics t
  :default-parent t)

(define defmin-int-process-inputs
  (f y x1...xn body guard verify-guards ctx state)
  :returns (mv erp (nothing null) state)
  :short "Process all the inputs."
  :long (topstring-p "We just check that the inputs have the right types.
    We do not check the @('body') and @('guard') inputs,
    since those are untranslated term,
    for which we do not quite have a ``type'' readily available.")
  (declare (ignore body guard))
  (b* (((er &) (ensure-value-is-symbol$ f "The first input" t nil)) ((er &) (ensure-value-is-symbol$ y "The second input" t nil))
      ((er &) (ensure-value-is-symbol-list$ x1...xn
          "The third input"
          t
          nil))
      ((er &) (ensure-value-is-boolean$ verify-guards
          "The :VERIFY-GUARDS input"
          t
          nil)))
    (value nil)))

(defxdoc+ defmin-int-event-generation
  :parents (defmin-int-implementation)
  :short "Event generation performed by @(tsee defmin-int)."
  :order-subtopics t
  :default-parent t)

(define defmin-int-gen-everything
  ((f symbolp) (y symbolp)
    (x1...xn symbol-listp)
    body
    guard
    (verify-guards booleanp))
  :returns (event "A @(tsee pseudo-event-formp).")
  :mode :program :short "Generate the top-level event."
  :long (topstring-p "The events are generated inside an @(tsee encapsulate).
    Some events are only local, just used to prove the first helper theorem
    @('f.existsp-when-nonempty-and-bounded').
    The exported theorems that have hints are generated
    first locally with the hints,
    then non-locally and redundantly without hints,
    to keep the history ``cleaner''.")
  (b* ((y0 (genvar y (symbol-name y) 0 (list* y x1...xn))) (y1 (genvar y (symbol-name y) 1 (list* y y0 x1...xn)))
      (x1...xn-y (rcons y x1...xn))
      (elementp (add-suffix-to-fn f ".ELEMENTP"))
      (lboundp (add-suffix-to-fn f ".LBOUNDP"))
      (existsp (add-suffix-to-fn f ".EXISTSP"))
      (existsp-witness (add-suffix-to-fn existsp "-WITNESS"))
      (lboundp-witness (add-suffix-to-fn lboundp "-WITNESS"))
      (lboundp-necc (add-suffix-to-fn lboundp "-NECC"))
      (existsp-suff (add-suffix-to-fn existsp "-SUFF"))
      (pkgwit (pkg-witness (symbol-package-name f)))
      (booleanp-of-lboundp (packn-pos (list 'booleanp-of lboundp) pkgwit))
      (booleanp-of-existsp (packn-pos (list 'booleanp-of existsp) pkgwit))
      (maybe-integerp-of-f (packn-pos (list 'maybe-integerp-of- f) pkgwit))
      (integerp-of-f-equal-existsp (packn-pos (list 'integerp-of- f '-equal- existsp) pkgwit))
      (integerp-of-f-when-existsp (packn-pos (list 'integerp-of- f '-when- existsp) pkgwit))
      (f-iff-existsp (packn-pos (list f '-iff- existsp) pkgwit))
      (not-f-when-not-existsp (packn-pos (list 'not- f '-when-not- existsp) pkgwit))
      (elementp-of-f-when-existsp (packn-pos (list elementp '-of- f '-when- existsp) pkgwit))
      (lboundp-of-f-when-existsp (packn-pos (list lboundp '-of- f '-when- 'existsp) pkgwit))
      (f-leq-when-existsp-linear (packn-pos (list f '-leq-when- existsp '-linear) pkgwit))
      (f-leq-when-existsp-rewrite (packn-pos (list f '-leq-when- existsp '-rewrite) pkgwit))
      (f-geq-when-existsp-linear (packn-pos (list f '-geq-when- existsp '-linear) pkgwit))
      (f-geq-when-existsp-rewrite (packn-pos (list f '-geq-when- existsp '-rewrite) pkgwit))
      (lbound-leq-member (packn-pos (list f '.lbound-leq-member) pkgwit))
      (lbound-nonmember-gt-member (packn-pos (list f '.lbound-nonmember-gt-member) pkgwit))
      (find-min (packn-pos (list f '.find-min) pkgwit))
      (find-min-lboundp-preservation (packn-pos (list f '.find-min-lboundp-preservation) pkgwit))
      (elementp-of-find-min (packn-pos (list f '.elementp-of-find-min) pkgwit))
      (lboundp-of-find-min (packn-pos (list f '.lboundp-of-find-min) pkgwit))
      (existsp-when-nonempty-and-bounded (packn-pos (list f '.existsp-when-nonempty-and-bounded)
          pkgwit))
      (equal-when-member-and-lbound (packn-pos (list f '.equal-when-member-and-lbound) pkgwit))
      (elementp-events `((defun ,ELEMENTP
           ,X1...XN-Y
           (declare (xargs :guard (and ,GUARD (integerp ,Y))))
           ,BODY) ,@(AND VERIFY-GUARDS `((VERIFY-GUARDS ,ELEMENTP)))
          (in-theory (disable ,ELEMENTP))))
      (lboundp-events `((defun-sk ,LBOUNDP
           ,X1...XN-Y
           (declare (xargs :guard (and ,GUARD (integerp ,Y)) :verify-guards nil))
           (forall (,Y1)
             (impliez (and (integerp ,Y1) (,ELEMENTP ,@X1...XN ,Y1))
               (<= (ifix ,Y) ,Y1)))
           :rewrite (implies (and (,LBOUNDP ,@X1...XN-Y)
               (integerp ,Y1)
               (,ELEMENTP ,@X1...XN ,Y1))
             (<= (ifix ,Y) ,Y1))) ,@(AND VERIFY-GUARDS `((VERIFY-GUARDS ,LBOUNDP)))
          (defthm ,BOOLEANP-OF-LBOUNDP
            (booleanp (,LBOUNDP ,@X1...XN-Y)))
          (in-theory (disable ,LBOUNDP ,LBOUNDP-NECC))))
      (existsp-events `((defun-sk ,EXISTSP
           ,X1...XN
           (declare (xargs :guard ,GUARD :verify-guards nil))
           (exists (,Y)
             (and (integerp ,Y)
               (,ELEMENTP ,@X1...XN-Y)
               (,LBOUNDP ,@X1...XN-Y)))) ,@(AND VERIFY-GUARDS `((VERIFY-GUARDS ,EXISTSP)))
          (defthm ,BOOLEANP-OF-EXISTSP
            (booleanp (,EXISTSP ,@X1...XN)))
          (in-theory (disable ,EXISTSP ,EXISTSP-SUFF))))
      (f-events `((defun ,F
           ,X1...XN
           (declare (xargs :guard ,GUARD))
           (if (,EXISTSP ,@X1...XN)
             (,EXISTSP-WITNESS ,@X1...XN)
             nil)) ,@(AND VERIFY-GUARDS `((VERIFY-GUARDS ,F)))
          ,@(AND (NULL X1...XN) `((IN-THEORY (DISABLE (:E ,F)))))
          (local (defthm ,MAYBE-INTEGERP-OF-F
              (maybe-integerp (,F ,@X1...XN))
              :hints (("Goal" :in-theory (enable maybe-integerp ,EXISTSP)))))
          (defthm ,MAYBE-INTEGERP-OF-F
            (maybe-integerp (,F ,@X1...XN)))
          (local (defthm ,INTEGERP-OF-F-EQUAL-EXISTSP
              (equal (integerp (,F ,@X1...XN)) (,EXISTSP ,@X1...XN))
              :hints (("Goal" :in-theory (enable ,EXISTSP)))))
          (defthm ,INTEGERP-OF-F-EQUAL-EXISTSP
            (equal (integerp (,F ,@X1...XN)) (,EXISTSP ,@X1...XN)))
          (defthm ,INTEGERP-OF-F-WHEN-EXISTSP
            (implies (,EXISTSP ,@X1...XN) (integerp (,F ,@X1...XN)))
            :rule-classes :type-prescription)
          (local (defthm ,F-IFF-EXISTSP
              (iff (,F ,@X1...XN) (,EXISTSP ,@X1...XN))
              :hints (("Goal" :in-theory (enable ,EXISTSP)))))
          (defthm ,F-IFF-EXISTSP
            (iff (,F ,@X1...XN) (,EXISTSP ,@X1...XN)))
          (defthm ,NOT-F-WHEN-NOT-EXISTSP
            (implies (not (,EXISTSP ,@X1...XN)) (not (,F ,@X1...XN)))
            :rule-classes :type-prescription)
          (local (defthm ,ELEMENTP-OF-F-WHEN-EXISTSP
              (implies (,EXISTSP ,@X1...XN)
                (,ELEMENTP ,@X1...XN (,F ,@X1...XN)))
              :hints (("Goal" :in-theory (enable ,EXISTSP)))))
          (defthm ,ELEMENTP-OF-F-WHEN-EXISTSP
            (implies (,EXISTSP ,@X1...XN)
              (,ELEMENTP ,@X1...XN (,F ,@X1...XN))))
          (local (defthm ,LBOUNDP-OF-F-WHEN-EXISTSP
              (implies (,EXISTSP ,@X1...XN)
                (,LBOUNDP ,@X1...XN (,F ,@X1...XN)))
              :hints (("Goal" :in-theory (enable ,EXISTSP)))))
          (defthm ,LBOUNDP-OF-F-WHEN-EXISTSP
            (implies (,EXISTSP ,@X1...XN)
              (,LBOUNDP ,@X1...XN (,F ,@X1...XN))))
          (local (defthm ,F-LEQ-WHEN-EXISTSP-LINEAR
              (implies (and (,EXISTSP ,@X1...XN)
                  (,ELEMENTP ,@X1...XN ,Y1)
                  (integerp ,Y1))
                (<= (,F ,@X1...XN) ,Y1))
              :rule-classes :linear :hints (("Goal" :in-theory (disable ,F)
                 :use (,LBOUNDP-OF-F-WHEN-EXISTSP (:instance ,LBOUNDP-NECC (,Y (,F ,@X1...XN))))))))
          (defthm ,F-LEQ-WHEN-EXISTSP-LINEAR
            (implies (and (,EXISTSP ,@X1...XN)
                (,ELEMENTP ,@X1...XN ,Y1)
                (integerp ,Y1))
              (<= (,F ,@X1...XN) ,Y1))
            :rule-classes :linear)
          (local (defthm ,F-LEQ-WHEN-EXISTSP-REWRITE
              (implies (and (,EXISTSP ,@X1...XN)
                  (,ELEMENTP ,@X1...XN ,Y1)
                  (integerp ,Y1))
                (<= (,F ,@X1...XN) ,Y1))
              :hints (("Goal" :by ,F-LEQ-WHEN-EXISTSP-LINEAR))))
          (defthm ,F-LEQ-WHEN-EXISTSP-REWRITE
            (implies (and (,EXISTSP ,@X1...XN)
                (,ELEMENTP ,@X1...XN ,Y1)
                (integerp ,Y1))
              (<= (,F ,@X1...XN) ,Y1)))
          (local (defthm ,F-GEQ-WHEN-EXISTSP-LINEAR
              (implies (and (,EXISTSP ,@X1...XN)
                  (,LBOUNDP ,@X1...XN ,Y1)
                  (integerp ,Y1))
                (>= (,F ,@X1...XN) ,Y1))
              :rule-classes :linear :hints (("Goal" :in-theory (disable ,F)
                 :use (:instance ,LBOUNDP-NECC (,Y1 (,F ,@X1...XN)) (,Y ,Y1))))))
          (defthm ,F-GEQ-WHEN-EXISTSP-LINEAR
            (implies (and (,EXISTSP ,@X1...XN)
                (,LBOUNDP ,@X1...XN ,Y1)
                (integerp ,Y1))
              (>= (,F ,@X1...XN) ,Y1))
            :rule-classes :linear)
          (local (defthm ,F-GEQ-WHEN-EXISTSP-REWRITE
              (implies (and (,EXISTSP ,@X1...XN)
                  (,LBOUNDP ,@X1...XN ,Y1)
                  (integerp ,Y1))
                (>= (,F ,@X1...XN) ,Y1))
              :hints (("Goal" :by ,F-GEQ-WHEN-EXISTSP-LINEAR))))
          (defthm ,F-GEQ-WHEN-EXISTSP-REWRITE
            (implies (and (,EXISTSP ,@X1...XN)
                (,LBOUNDP ,@X1...XN ,Y1)
                (integerp ,Y1))
              (>= (,F ,@X1...XN) ,Y1)))
          (in-theory (disable ,F))))
      (existsp-when-non-empty-and-bounded-events `((local (defthm ,LBOUND-LEQ-MEMBER
             (implies (and (integerp ,Y0)
                 (,ELEMENTP ,@X1...XN ,Y0)
                 (integerp ,Y1)
                 (,LBOUNDP ,@X1...XN ,Y1))
               (<= ,Y1 ,Y0))
             :rule-classes nil
             :hints (("Goal" :use (:instance ,LBOUNDP-NECC (,Y ,Y1) (,Y1 ,Y0)))))) (local (defthm ,LBOUND-NONMEMBER-GT-MEMBER
              (implies (and (integerp ,Y0)
                  (,ELEMENTP ,@X1...XN ,Y0)
                  (integerp ,Y1)
                  (,LBOUNDP ,@X1...XN ,Y1)
                  (not (,ELEMENTP ,@X1...XN ,Y1)))
                (< ,Y1 ,Y0))
              :rule-classes nil
              :hints (("Goal" :use ,LBOUND-LEQ-MEMBER))))
          (local (defun ,FIND-MIN
              (,@X1...XN ,Y1 ,Y0)
              (declare (xargs :measure (nfix (- ,Y0 ,Y1))
                  :hints (("Goal" :use ,LBOUND-NONMEMBER-GT-MEMBER))))
              (if (and (integerp ,Y0)
                  (,ELEMENTP ,@X1...XN ,Y0)
                  (integerp ,Y1)
                  (,LBOUNDP ,@X1...XN ,Y1))
                (if (,ELEMENTP ,@X1...XN ,Y1)
                  ,Y1
                  (,FIND-MIN ,@X1...XN (1+ ,Y1) ,Y0))
                0)))
          (local (defthm ,FIND-MIN-LBOUNDP-PRESERVATION
              (implies (and (integerp ,Y0)
                  (,ELEMENTP ,@X1...XN ,Y0)
                  (integerp ,Y1)
                  (,LBOUNDP ,@X1...XN ,Y1)
                  (not (,ELEMENTP ,@X1...XN ,Y1)))
                (,LBOUNDP ,@X1...XN (1+ ,Y1)))
              :hints (("Goal" :expand ((,LBOUNDP ,@X1...XN (1+ ,Y1)))
                 :use (:instance ,LBOUNDP-NECC
                   (,Y ,Y1)
                   (,Y1 (,LBOUNDP-WITNESS ,@X1...XN (1+ ,Y1))))))))
          (local (defthm ,ELEMENTP-OF-FIND-MIN
              (implies (and (integerp ,Y0)
                  (,ELEMENTP ,@X1...XN ,Y0)
                  (integerp ,Y1)
                  (,LBOUNDP ,@X1...XN ,Y1))
                (,ELEMENTP ,@X1...XN (,FIND-MIN ,@X1...XN ,Y1 ,Y0)))
              :hints ('(:use (:instance ,LBOUNDP-NECC (,Y ,Y1) (,Y1 0))) '(:use (:instance ,LBOUNDP-NECC (,Y 0) (,Y1 ,Y0))))))
          (local (defthm ,LBOUNDP-OF-FIND-MIN
              (implies (and (integerp ,Y0)
                  (,ELEMENTP ,@X1...XN ,Y0)
                  (integerp ,Y1)
                  (,LBOUNDP ,@X1...XN ,Y1))
                (,LBOUNDP ,@X1...XN (,FIND-MIN ,@X1...XN ,Y1 ,Y0)))
              :hints ('(:use (:instance ,LBOUNDP-NECC (,Y ,Y1) (,Y1 0))) '(:use (:instance ,LBOUNDP-NECC (,Y 0) (,Y1 ,Y0))))))
          (local (defthm ,EXISTSP-WHEN-NONEMPTY-AND-BOUNDED
              (implies (and (integerp ,Y0)
                  (,ELEMENTP ,@X1...XN ,Y0)
                  (integerp ,Y1)
                  (,LBOUNDP ,@X1...XN ,Y1))
                (,EXISTSP ,@X1...XN))
              :rule-classes nil
              :hints (("Goal" :use (:instance ,EXISTSP-SUFF (,Y (,FIND-MIN ,@X1...XN ,Y1 ,Y0)))))))
          (defthm ,EXISTSP-WHEN-NONEMPTY-AND-BOUNDED
            (implies (and (integerp ,Y0)
                (,ELEMENTP ,@X1...XN ,Y0)
                (integerp ,Y1)
                (,LBOUNDP ,@X1...XN ,Y1))
              (,EXISTSP ,@X1...XN))
            :rule-classes nil)))
      (equal-when-member-and-bound `((local (defthm ,EQUAL-WHEN-MEMBER-AND-LBOUND
             (implies (and (integerp ,Y)
                 (,ELEMENTP ,@X1...XN ,Y)
                 (,LBOUNDP ,@X1...XN ,Y))
               (equal (,F ,@X1...XN) ,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 ,@X1...XN)))))))) (defthm ,EQUAL-WHEN-MEMBER-AND-LBOUND
            (implies (and (integerp ,Y)
                (,ELEMENTP ,@X1...XN ,Y)
                (,LBOUNDP ,@X1...XN ,Y))
              (equal (,F ,@X1...XN) ,Y))
            :rule-classes nil))))
    `(encapsulate nil
      (set-verify-guards-eagerness 0)
      ,@ELEMENTP-EVENTS
      ,@LBOUNDP-EVENTS
      ,@EXISTSP-EVENTS
      ,@F-EVENTS
      ,@EXISTSP-WHEN-NON-EMPTY-AND-BOUNDED-EVENTS
      ,@EQUAL-WHEN-MEMBER-AND-BOUND)))

(define defmin-int-fn
  (f y x1...xn body guard verify-guards ctx state)
  :returns (mv erp (event "A @(tsee pseudo-event-formp).") state)
  :mode :program :parents (defmin-int-implementation)
  :short "Process the inputs and generate the event to submit."
  (b* (((er &) (defmin-int-process-inputs f
         y
         x1...xn
         body
         guard
         verify-guards
         ctx
         state)) (event (defmin-int-gen-everything f
          y
          x1...xn
          body
          guard
          verify-guards)))
    (value event)))

(defsection defmin-int-macro-definition
  :parents (defmin-int-implementation)
  :short "Definition of the @(tsee defmin-int) macro."
  :long (topstring (p "Submit the event generated by @(tsee defmin-int-fn).")
    (@def "defmin-int"))
  (defmacro defmin-int
    (f y x1...xn body &key (guard 't) (verify-guards 't))
    `(make-event (defmin-int-fn ',F
        ',Y
        ',X1...XN
        ',BODY
        ',GUARD
        ',VERIFY-GUARDS
        (cons 'defmin-int ',F)
        state))))