defmax-nat

(in-package "ACL2")

(defxdoc+ defmax-nat-implementation
  :parents (defmax-nat)
  :short "Implementation of @(tsee defmax-nat)."
  :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 defmax-nat),
      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+ defmax-nat-input-processing
  :parents (defmax-nat-implementation)
  :short "Input processing performed by @(tsee defmax-nat)."
  :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 defmax-nat-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+ defmax-nat-event-generation
  :parents (defmax-nat-implementation)
  :short "Event generation performed by @(tsee defmax-nat)."
  :order-subtopics t
  :default-parent t)

(define defmax-nat-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"))
      (uboundp (add-suffix-to-fn f ".UBOUNDP"))
      (existsp (add-suffix-to-fn f ".EXISTSP"))
      (existsp-witness (add-suffix-to-fn existsp "-WITNESS"))
      (uboundp-witness (add-suffix-to-fn uboundp "-WITNESS"))
      (uboundp-necc (add-suffix-to-fn uboundp "-NECC"))
      (existsp-suff (add-suffix-to-fn existsp "-SUFF"))
      (pkgwit (pkg-witness (symbol-package-name f)))
      (booleanp-of-uboundp (packn-pos (list 'booleanp-of uboundp) pkgwit))
      (booleanp-of-existsp (packn-pos (list 'booleanp-of existsp) pkgwit))
      (maybe-natp-of-f (packn-pos (list 'maybe-natp-of- f) pkgwit))
      (natp-of-f-equal-existsp (packn-pos (list 'natp-of- f '-equal- existsp) pkgwit))
      (natp-of-f-when-existsp (packn-pos (list 'natp-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))
      (uboundp-of-f-when-existsp (packn-pos (list uboundp '-of- f '-when- 'existsp) 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))
      (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))
      (ubound-geq-member (packn-pos (list f '.ubound-geq-member) pkgwit))
      (ubound-nonmember-gt-member (packn-pos (list f '.ubound-nonmember-gt-member) pkgwit))
      (find-max (packn-pos (list f '.find-max) pkgwit))
      (find-max-uboundp-preservation (packn-pos (list f '.find-max-uboundp-preservation) pkgwit))
      (elementp-of-find-max (packn-pos (list f '.elementp-of-find-max) pkgwit))
      (uboundp-of-find-max (packn-pos (list f '.uboundp-of-find-max) pkgwit))
      (existsp-when-nonempty-and-bounded (packn-pos (list f '.existsp-when-nonempty-and-bounded)
          pkgwit))
      (equal-when-member-and-ubound (packn-pos (list f '.equal-when-member-and-ubound) pkgwit))
      (elementp-events `((defun ,ELEMENTP
           ,X1...XN-Y
           (declare (xargs :guard (and ,GUARD (natp ,Y))))
           ,BODY) ,@(AND VERIFY-GUARDS `((VERIFY-GUARDS ,ELEMENTP)))
          (in-theory (disable ,ELEMENTP))))
      (uboundp-events `((defun-sk ,UBOUNDP
           ,X1...XN-Y
           (declare (xargs :guard (and ,GUARD (natp ,Y)) :verify-guards nil))
           (forall (,Y1)
             (impliez (and (natp ,Y1) (,ELEMENTP ,@X1...XN ,Y1))
               (>= (nfix ,Y) ,Y1)))
           :rewrite (implies (and (,UBOUNDP ,@X1...XN-Y)
               (natp ,Y1)
               (,ELEMENTP ,@X1...XN ,Y1))
             (>= (nfix ,Y) ,Y1))) ,@(AND VERIFY-GUARDS `((VERIFY-GUARDS ,UBOUNDP)))
          (defthm ,BOOLEANP-OF-UBOUNDP
            (booleanp (,UBOUNDP ,@X1...XN-Y)))
          (in-theory (disable ,UBOUNDP ,UBOUNDP-NECC))))
      (existsp-events `((defun-sk ,EXISTSP
           ,X1...XN
           (declare (xargs :guard ,GUARD :verify-guards nil))
           (exists (,Y)
             (and (natp ,Y)
               (,ELEMENTP ,@X1...XN-Y)
               (,UBOUNDP ,@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-NATP-OF-F
              (maybe-natp (,F ,@X1...XN))
              :hints (("Goal" :in-theory (enable maybe-natp ,EXISTSP)))))
          (defthm ,MAYBE-NATP-OF-F (maybe-natp (,F ,@X1...XN)))
          (local (defthm ,NATP-OF-F-EQUAL-EXISTSP
              (equal (natp (,F ,@X1...XN)) (,EXISTSP ,@X1...XN))
              :hints (("Goal" :in-theory (enable ,EXISTSP)))))
          (defthm ,NATP-OF-F-EQUAL-EXISTSP
            (equal (natp (,F ,@X1...XN)) (,EXISTSP ,@X1...XN)))
          (defthm ,NATP-OF-F-WHEN-EXISTSP
            (implies (,EXISTSP ,@X1...XN) (natp (,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 ,UBOUNDP-OF-F-WHEN-EXISTSP
              (implies (,EXISTSP ,@X1...XN)
                (,UBOUNDP ,@X1...XN (,F ,@X1...XN)))
              :hints (("Goal" :in-theory (enable ,EXISTSP)))))
          (defthm ,UBOUNDP-OF-F-WHEN-EXISTSP
            (implies (,EXISTSP ,@X1...XN)
              (,UBOUNDP ,@X1...XN (,F ,@X1...XN))))
          (local (defthm ,F-GEQ-WHEN-EXISTSP-LINEAR
              (implies (and (,EXISTSP ,@X1...XN)
                  (,ELEMENTP ,@X1...XN ,Y1)
                  (natp ,Y1))
                (>= (,F ,@X1...XN) ,Y1))
              :rule-classes :linear :hints (("Goal" :use (,UBOUNDP-OF-F-WHEN-EXISTSP (:instance ,UBOUNDP-NECC (,Y (,F ,@X1...XN))))))))
          (defthm ,F-GEQ-WHEN-EXISTSP-LINEAR
            (implies (and (,EXISTSP ,@X1...XN)
                (,ELEMENTP ,@X1...XN ,Y1)
                (natp ,Y1))
              (>= (,F ,@X1...XN) ,Y1))
            :rule-classes :linear)
          (local (defthm ,F-GEQ-WHEN-EXISTSP-REWRITE
              (implies (and (,EXISTSP ,@X1...XN)
                  (,ELEMENTP ,@X1...XN ,Y1)
                  (natp ,Y1))
                (>= (,F ,@X1...XN) ,Y1))
              :hints (("Goal" :by ,F-GEQ-WHEN-EXISTSP-LINEAR))))
          (defthm ,F-GEQ-WHEN-EXISTSP-REWRITE
            (implies (and (,EXISTSP ,@X1...XN)
                (,ELEMENTP ,@X1...XN ,Y1)
                (natp ,Y1))
              (>= (,F ,@X1...XN) ,Y1)))
          (local (defthm ,F-LEQ-WHEN-EXISTSP-LINEAR
              (implies (and (,EXISTSP ,@X1...XN)
                  (,UBOUNDP ,@X1...XN ,Y1)
                  (natp ,Y1))
                (<= (,F ,@X1...XN) ,Y1))
              :rule-classes :linear :hints (("Goal" :in-theory (disable ,F)
                 :use (:instance ,UBOUNDP-NECC (,Y1 (,F ,@X1...XN)) (,Y ,Y1))))))
          (defthm ,F-LEQ-WHEN-EXISTSP-LINEAR
            (implies (and (,EXISTSP ,@X1...XN)
                (,UBOUNDP ,@X1...XN ,Y1)
                (natp ,Y1))
              (<= (,F ,@X1...XN) ,Y1))
            :rule-classes :linear)
          (local (defthm ,F-LEQ-WHEN-EXISTSP-REWRITE
              (implies (and (,EXISTSP ,@X1...XN)
                  (,UBOUNDP ,@X1...XN ,Y1)
                  (natp ,Y1))
                (<= (,F ,@X1...XN) ,Y1))
              :hints (("Goal" :by ,F-LEQ-WHEN-EXISTSP-LINEAR))))
          (defthm ,F-LEQ-WHEN-EXISTSP-REWRITE
            (implies (and (,EXISTSP ,@X1...XN)
                (,UBOUNDP ,@X1...XN ,Y1)
                (natp ,Y1))
              (<= (,F ,@X1...XN) ,Y1)))
          (in-theory (disable ,F))))
      (existsp-when-non-empty-and-bounded-events `((local (defthm ,UBOUND-GEQ-MEMBER
             (implies (and (natp ,Y0)
                 (,ELEMENTP ,@X1...XN ,Y0)
                 (natp ,Y1)
                 (,UBOUNDP ,@X1...XN ,Y1))
               (>= ,Y1 ,Y0))
             :rule-classes nil
             :hints (("Goal" :use (:instance ,UBOUNDP-NECC (,Y ,Y1) (,Y1 ,Y0)))))) (local (defthm ,UBOUND-NONMEMBER-GT-MEMBER
              (implies (and (natp ,Y0)
                  (,ELEMENTP ,@X1...XN ,Y0)
                  (natp ,Y1)
                  (,UBOUNDP ,@X1...XN ,Y1)
                  (not (,ELEMENTP ,@X1...XN ,Y1)))
                (> ,Y1 ,Y0))
              :rule-classes nil
              :hints (("Goal" :use ,UBOUND-GEQ-MEMBER))))
          (local (defun ,FIND-MAX
              (,@X1...XN ,Y1 ,Y0)
              (declare (xargs :hints (("Goal" :use ,UBOUND-NONMEMBER-GT-MEMBER))))
              (if (and (natp ,Y0)
                  (,ELEMENTP ,@X1...XN ,Y0)
                  (natp ,Y1)
                  (,UBOUNDP ,@X1...XN ,Y1))
                (if (,ELEMENTP ,@X1...XN ,Y1)
                  ,Y1
                  (,FIND-MAX ,@X1...XN (1- ,Y1) ,Y0))
                0)))
          (local (defthm ,FIND-MAX-UBOUNDP-PRESERVATION
              (implies (and (natp ,Y0)
                  (,ELEMENTP ,@X1...XN ,Y0)
                  (natp ,Y1)
                  (,UBOUNDP ,@X1...XN ,Y1)
                  (not (,ELEMENTP ,@X1...XN ,Y1)))
                (,UBOUNDP ,@X1...XN (1- ,Y1)))
              :hints (("Goal" :expand ((,UBOUNDP ,@X1...XN (1- ,Y1)))
                 :use (:instance ,UBOUNDP-NECC
                   (,Y ,Y1)
                   (,Y1 (,UBOUNDP-WITNESS ,@X1...XN (1- ,Y1))))))))
          (local (defthm ,ELEMENTP-OF-FIND-MAX
              (implies (and (natp ,Y0)
                  (,ELEMENTP ,@X1...XN ,Y0)
                  (natp ,Y1)
                  (,UBOUNDP ,@X1...XN ,Y1))
                (,ELEMENTP ,@X1...XN (,FIND-MAX ,@X1...XN ,Y1 ,Y0)))
              :hints ('(:use (:instance ,UBOUNDP-NECC (,Y ,Y1) (,Y1 0))) '(:use (:instance ,UBOUNDP-NECC (,Y 0) (,Y1 ,Y0))))))
          (local (defthm ,UBOUNDP-OF-FIND-MAX
              (implies (and (natp ,Y0)
                  (,ELEMENTP ,@X1...XN ,Y0)
                  (natp ,Y1)
                  (,UBOUNDP ,@X1...XN ,Y1))
                (,UBOUNDP ,@X1...XN (,FIND-MAX ,@X1...XN ,Y1 ,Y0)))
              :hints ('(:use (:instance ,UBOUNDP-NECC (,Y ,Y1) (,Y1 0))) '(:use (:instance ,UBOUNDP-NECC (,Y 0) (,Y1 ,Y0))))))
          (local (defthm ,EXISTSP-WHEN-NONEMPTY-AND-BOUNDED
              (implies (and (natp ,Y0)
                  (,ELEMENTP ,@X1...XN ,Y0)
                  (natp ,Y1)
                  (,UBOUNDP ,@X1...XN ,Y1))
                (,EXISTSP ,@X1...XN))
              :rule-classes nil
              :hints (("Goal" :use (:instance ,EXISTSP-SUFF (,Y (,FIND-MAX ,@X1...XN ,Y1 ,Y0)))))))
          (defthm ,EXISTSP-WHEN-NONEMPTY-AND-BOUNDED
            (implies (and (natp ,Y0)
                (,ELEMENTP ,@X1...XN ,Y0)
                (natp ,Y1)
                (,UBOUNDP ,@X1...XN ,Y1))
              (,EXISTSP ,@X1...XN))
            :rule-classes nil)))
      (equal-when-member-and-bound `((local (defthm ,EQUAL-WHEN-MEMBER-AND-UBOUND
             (implies (and (natp ,Y)
                 (,ELEMENTP ,@X1...XN ,Y)
                 (,UBOUNDP ,@X1...XN ,Y))
               (equal (,F ,@X1...XN) ,Y))
             :rule-classes nil
             :hints (("Goal" :in-theory (disable ,F-GEQ-WHEN-EXISTSP-REWRITE)
                :use ((:instance ,EXISTSP-WHEN-NONEMPTY-AND-BOUNDED
                   (,Y0 ,Y)
                   (,Y1 ,Y)) (:instance ,F-GEQ-WHEN-EXISTSP-REWRITE (,Y1 ,Y))
                  (:instance ,UBOUNDP-NECC (,Y1 (,F ,@X1...XN)))))))) (defthm ,EQUAL-WHEN-MEMBER-AND-UBOUND
            (implies (and (natp ,Y)
                (,ELEMENTP ,@X1...XN ,Y)
                (,UBOUNDP ,@X1...XN ,Y))
              (equal (,F ,@X1...XN) ,Y))
            :rule-classes nil))))
    `(encapsulate nil
      (set-verify-guards-eagerness 0)
      ,@ELEMENTP-EVENTS
      ,@UBOUNDP-EVENTS
      ,@EXISTSP-EVENTS
      ,@F-EVENTS
      ,@EXISTSP-WHEN-NON-EMPTY-AND-BOUNDED-EVENTS
      ,@EQUAL-WHEN-MEMBER-AND-BOUND)))

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

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