uninterpreted-fn-cp

(in-package "SMT")

(include-book "std/util/bstar" :dir :system)

(include-book "xdoc/top" :dir :system)

(include-book "std/util/define" :dir :system)

(include-book "pseudo-lambda-lemmas")

(include-book "hint-please")

(include-book "hint-interface")

(include-book "computed-hints")

(defsection uninterpreted-fn-cp
  :parents (verified)
  :short "Verified clause-processor for proving return types of uninterpreted
  functions."
  (defevaluator ev-uninterpreted
    ev-lst-uninterpreted
    ((not x) (if x
        y
        z)
      (hint-please hint)))
  (def-join-thms ev-uninterpreted)
  (define lambda->actuals-fix
    ((formals symbol-listp) (actuals pseudo-term-listp))
    :returns (new-actuals pseudo-term-listp)
    (b* ((formals (symbol-list-fix formals)) (actuals (pseudo-term-list-fix actuals))
        (len-formals (len formals))
        (len-actuals (len actuals))
        ((if (equal len-formals len-actuals)) actuals))
      nil))
  (define lambda->formals-fix
    ((formals symbol-listp) (actuals pseudo-term-listp))
    :returns (new-formals symbol-listp)
    (b* ((formals (symbol-list-fix formals)) (actuals (pseudo-term-list-fix actuals))
        (len-formals (len formals))
        (len-actuals (len actuals))
        ((if (equal len-formals len-actuals)) formals))
      nil))
  (local (in-theory (enable lambda->formals-fix
        lambda->actuals-fix)))
  (defprod lambda-binding
    :parents (uninterpreted-fn-cp)
    ((formals symbol-listp
       :default nil
       :reqfix (lambda->formals-fix formals actuals)) (actuals pseudo-term-listp
        :default nil
        :reqfix (lambda->actuals-fix formals actuals)))
    :require (equal (len formals) (len actuals)))
  (deflist lambda-binding-list
    :parents (lambda-binding)
    :elt-type lambda-binding
    :pred lambda-binding-listp
    :true-listp t)
  (defprod fhg-single-args
    :parents (uninterpreted-fn-cp)
    ((fn func-p :default nil) (actuals pseudo-term-listp :default nil)
      (fn-returns-hint-acc hint-pair-listp :default nil)
      (fn-more-returns-hint-acc hint-pair-listp
        :default nil)
      (lambda-acc lambda-binding-listp :default nil)))
  (local (defthm symbol-listp-of-append-of-symbol-listp
      (implies (and (symbol-listp x) (symbol-listp y))
        (symbol-listp (append x y)))))
  (local (defthm crock0
      (implies (and (fhg-single-args-p args)
          (not (equal (func->name (fhg-single-args->fn args))
              'quote)))
        (pseudo-term-listp (list (cons (func->name (fhg-single-args->fn args))
              (fhg-single-args->actuals args)))))))
  (local (defthm crock1
      (implies (and (pseudo-term-listp x)
          (pseudo-term-listp y))
        (pseudo-term-listp (append x y)))))
  (define generate-fn-hint-pair
    ((hypo hint-pair-p) (args fhg-single-args-p)
      (flag symbolp))
    :returns (fn-hint-pair hint-pair-p)
    :guard-debug t
    (b* ((hypo (hint-pair-fix hypo)) (args (fhg-single-args-fix args))
        (flag (symbol-fix flag))
        ((hint-pair h) hypo)
        ((fhg-single-args a) args)
        ((func f) a.fn)
        (formals f.flattened-formals)
        (returns f.flattened-returns)
        ((unless (equal (len returns) 1)) (prog2$ (er hard?
              'smt-goal-generator=>generate-fn-hint-pair
              "User ~
                defined function with more than one returns is not supported ~
                currently. ~%The function ~q0 has returns ~q1."
              f.name
              returns)
            (make-hint-pair)))
        ((unless (equal (len formals) (len a.actuals))) (prog2$ (er hard?
              'smt-goal-generator=>generate-fn-hint-pair
              "Number ~
                of formals and actuals don't match. ~%Formals: ~q0, actuals: ~q1."
              formals
              a.actuals)
            (make-hint-pair)))
        ((if (equal f.name 'quote)) (prog2$ (er hard?
              'smt-goal-generator=>generate-fn-hint-pair
              "Function name can't be 'quote.")
            (make-hint-pair)))
        ((unless (or (equal flag 'more-returns)
             (and (consp h.thm) (symbolp (car h.thm))))) (prog2$ (er hard?
              'smt-goal-generator=>generate-fn-hint-pair
              "Returns should have consp h.thm.~%")
            (make-hint-pair)))
        (thm (if (equal flag 'more-returns)
            `((lambda (,@SMT::FORMALS ,@SMT::RETURNS) ,SMT::H.THM) ,@SMT::A.ACTUALS
              (,SMT::F.NAME ,@SMT::A.ACTUALS))
            `(,(CAR SMT::H.THM) (,SMT::F.NAME ,@SMT::A.ACTUALS)))))
      (change-hint-pair h :thm thm)))
  (define generate-fn-returns-hint
    ((returns decl-listp) (args fhg-single-args-p))
    :returns (fn-hint-lst hint-pair-listp)
    :measure (len returns)
    (b* ((returns (decl-list-fix returns)) (args (fhg-single-args-fix args))
        ((fhg-single-args a) args)
        ((unless (consp returns)) a.fn-returns-hint-acc)
        ((cons first rest) returns)
        ((decl d) first)
        ((hint-pair h) d.type)
        (hypo (change-hint-pair h
            :thm `(,SMT::H.THM ,SMT::D.NAME)))
        (first-hint-pair (generate-fn-hint-pair hypo
            args
            'returns)))
      (generate-fn-returns-hint rest
        (change-fhg-single-args a
          :fn-returns-hint-acc (cons first-hint-pair a.fn-returns-hint-acc)))))
  (define generate-fn-more-returns-hint
    ((more-returns hint-pair-listp) (args fhg-single-args-p))
    :returns (fn-hint-lst hint-pair-listp)
    :measure (len more-returns)
    (b* ((more-returns (hint-pair-list-fix more-returns)) (args (fhg-single-args-fix args))
        ((fhg-single-args a) args)
        ((unless (consp more-returns)) a.fn-more-returns-hint-acc)
        ((cons first rest) more-returns)
        (first-hint-pair (generate-fn-hint-pair first
            args
            'more-returns)))
      (generate-fn-more-returns-hint rest
        (change-fhg-single-args a
          :fn-more-returns-hint-acc (cons first-hint-pair a.fn-more-returns-hint-acc)))))
  (define generate-fn-hint
    ((args fhg-single-args-p))
    :returns (fn-hint-lst fhg-single-args-p)
    (b* ((args (fhg-single-args-fix args)) ((fhg-single-args a) args)
        ((func f) a.fn))
      (change-fhg-single-args a
        :fn-returns-hint-acc (generate-fn-returns-hint f.returns a)
        :fn-more-returns-hint-acc (generate-fn-more-returns-hint f.more-returns
          a))))
  (defprod fhg-args
    :parents (uninterpreted-fn-cp)
    ((term-lst pseudo-term-listp :default nil) (fn-lst func-alistp :default nil)
      (fn-returns-hint-acc hint-pair-listp :default nil)
      (fn-more-returns-hint-acc hint-pair-listp
        :default nil)
      (lambda-acc lambda-binding-listp :default nil)))
  (encapsulate nil
    (local (defthm lemma-1
        (implies (fhg-args-p x)
          (pseudo-term-listp (fhg-args->term-lst x)))))
    (local (defthm lemma-2
        (implies (and (pseudo-term-listp y) (consp y))
          (pseudo-termp (car y)))))
    (local (defthm lemma-3
        (implies (and (pseudo-termp z)
            (consp z)
            (not (equal (car z) 'quote)))
          (pseudo-term-listp (cdr z)))))
    (local (defthm not-symbolp-then-consp-of-pseudo-termp
        (implies (and (pseudo-termp x) (not (symbolp x)))
          (consp x))))
    (defthm not-symbolp-then-consp-of-car-of-fhg-args->term-lst
      (implies (and (fhg-args-p args)
          (consp (fhg-args->term-lst args))
          (not (symbolp (car (fhg-args->term-lst args)))))
        (consp (car (fhg-args->term-lst args)))))
    (local (defthm lemma-4
        (implies (and (pseudo-term-listp y) (consp y))
          (pseudo-term-listp (cdr y)))))
    (defthm pseudo-term-listp-of-cdr-of-fhg-args->term-lst
      (implies (and (fhg-args-p args)
          (consp (fhg-args->term-lst args)))
        (pseudo-term-listp (cdr (fhg-args->term-lst args)))))
    (defthm pseudo-term-listp-of-cdar-of-fhg-args->term-lst
      (implies (and (fhg-args-p args)
          (consp (fhg-args->term-lst args))
          (not (symbolp (car (fhg-args->term-lst args))))
          (not (equal (car (car (fhg-args->term-lst args)))
              'quote)))
        (pseudo-term-listp (cdr (car (fhg-args->term-lst args))))))
    (local (defthm lemma-5
        (implies (and (pseudo-termp z)
            (not (symbolp z))
            (not (pseudo-lambdap (car z))))
          (symbolp (car z)))
        :hints (("Goal" :in-theory (enable pseudo-termp pseudo-lambdap)))))
    (defthm symbolp-of-caar-of-fhg-args->term-lst
      (implies (and (fhg-args-p args)
          (consp (fhg-args->term-lst args))
          (not (symbolp (car (fhg-args->term-lst args))))
          (not (pseudo-lambdap (car (car (fhg-args->term-lst args))))))
        (symbolp (car (car (fhg-args->term-lst args))))))
    (local (defthm lemma-6
        (implies (and (pseudo-termp x)
            (pseudo-lambdap (car x)))
          (equal (len (cadar x)) (len (cdr x))))
        :hints (("Goal" :in-theory (enable pseudo-lambdap pseudo-termp)))))
    (defthm len-equal-of-formals-of-pseudo-lambdap-and-actuals
      (implies (and (fhg-args-p args)
          (consp (fhg-args->term-lst args))
          (pseudo-lambdap (car (car (fhg-args->term-lst args)))))
        (equal (len (cadr (car (car (fhg-args->term-lst args)))))
          (len (cdr (car (fhg-args->term-lst args)))))))
    (local (defthm lemma-7
        (implies (and (func-alistp x)
            (assoc-equal key x))
          (func-p (cdr (assoc-equal key x))))))
    (defthm lemma-8
      (implies (and (fhg-args-p args)
          (consp (fhg-args->term-lst args))
          (assoc-equal (car (car (fhg-args->term-lst args)))
            (fhg-args->fn-lst args)))
        (func-p (cdr (assoc-equal (car (car (fhg-args->term-lst args)))
              (fhg-args->fn-lst args)))))
      :hints (("Goal" :in-theory (disable lemma-7)
         :use ((:instance lemma-7
            (key (car (car (fhg-args->term-lst args))))
            (x (fhg-args->fn-lst args)))))))
    (local (defthm lemma-9
        (implies (and (func-alistp x)
            (assoc-equal key x))
          (consp (assoc-equal key x)))))
    (defthm lemma-10
      (implies (and (fhg-args-p args)
          (consp (fhg-args->term-lst args))
          (assoc-equal (car (car (fhg-args->term-lst args)))
            (fhg-args->fn-lst args)))
        (consp (assoc-equal (car (car (fhg-args->term-lst args)))
            (fhg-args->fn-lst args))))
      :hints (("Goal" :in-theory (disable lemma-9)
         :use ((:instance lemma-9
            (key (car (car (fhg-args->term-lst args))))
            (x (fhg-args->fn-lst args))))))))
  (define generate-fn-hint-lst
    ((args fhg-args-p))
    :parents (uninterpreted-fn-cp)
    :short "@(call generate-fn-hint-lst) generate auxiliary hypotheses from ~
           function expansion"
    :returns (fn-hint-lst fhg-args-p)
    :measure (acl2-count (fhg-args->term-lst args))
    :verify-guards nil
    (b* ((args (fhg-args-fix args)) ((fhg-args a) args)
        ((unless (consp a.term-lst)) a)
        ((cons term rest) a.term-lst)
        ((if (symbolp term)) (generate-fn-hint-lst (change-fhg-args a :term-lst rest)))
        ((if (equal (car term) 'quote)) (generate-fn-hint-lst (change-fhg-args a :term-lst rest)))
        ((cons fn-call fn-actuals) term)
        ((if (pseudo-lambdap fn-call)) (b* ((lambda-formals (lambda-formals fn-call)) (lambda-body (lambda-body fn-call))
              (lambda-actuals fn-actuals)
              (lambda-bd (make-lambda-binding :formals lambda-formals
                  :actuals lambda-actuals))
              ((unless (mbt (lambda-binding-p lambda-bd))) a)
              (a-1 (generate-fn-hint-lst (change-fhg-args a
                    :term-lst (list lambda-body)
                    :lambda-acc (cons lambda-bd a.lambda-acc))))
              (a-2 (generate-fn-hint-lst (change-fhg-args a-1
                    :term-lst lambda-actuals))))
            (generate-fn-hint-lst (change-fhg-args a-2 :term-lst rest))))
        ((unless (mbt (symbolp fn-call))) a)
        (fn (assoc-equal fn-call a.fn-lst))
        ((unless fn) (b* ((a-1 (generate-fn-hint-lst (change-fhg-args a :term-lst fn-actuals))))
            (generate-fn-hint-lst (change-fhg-args a-1 :term-lst rest))))
        (f (cdr fn))
        (as-1 (generate-fn-hint (make-fhg-single-args :fn f
              :actuals fn-actuals
              :fn-returns-hint-acc a.fn-returns-hint-acc
              :fn-more-returns-hint-acc a.fn-more-returns-hint-acc
              :lambda-acc a.lambda-acc)))
        ((fhg-single-args as-1) as-1)
        (a-1 (change-fhg-args a
            :fn-returns-hint-acc as-1.fn-returns-hint-acc
            :fn-more-returns-hint-acc as-1.fn-more-returns-hint-acc))
        (a-2 (generate-fn-hint-lst (change-fhg-args a-1 :term-lst fn-actuals))))
      (generate-fn-hint-lst (change-fhg-args a-2 :term-lst rest))))
  (verify-guards generate-fn-hint-lst)
  (defprod uninterpreted
    ((returns hint-pair-listp) (more-returns hint-pair-listp)))
  (define uninterpreted-fn-helper
    ((cl pseudo-term-listp) (smtlink-hint smtlink-hint-p))
    :returns (uninterpreted uninterpreted-p)
    (b* ((cl (pseudo-term-list-fix cl)) (smtlink-hint (smtlink-hint-fix smtlink-hint))
        ((smtlink-hint h) smtlink-hint)
        (fn-lst (make-alist-fn-lst h.functions))
        (g (disjoin cl))
        (args (generate-fn-hint-lst (make-fhg-args :term-lst (list g)
              :fn-lst fn-lst
              :fn-returns-hint-acc nil
              :fn-more-returns-hint-acc nil
              :lambda-acc nil)))
        ((fhg-args a) args)
        (fn-returns-hint-lst a.fn-returns-hint-acc)
        (fn-more-returns-hint-lst a.fn-more-returns-hint-acc))
      (make-uninterpreted :returns fn-returns-hint-lst
        :more-returns fn-more-returns-hint-lst)))
  (define uninterpreted-subgoals
    ((hint-pair-lst hint-pair-listp) (g pseudo-termp)
      (tag symbolp))
    :returns (mv (list-of-h-thm pseudo-term-list-listp)
      (list-of-not-hs pseudo-term-listp))
    :measure (len hint-pair-lst)
    (b* ((hint-pair-lst (hint-pair-list-fix hint-pair-lst)) (g (pseudo-term-fix g))
        ((unless (or (equal tag :return) (equal tag :more-return))) (prog2$ (er hard?
              'uninterpreted-fn-cp=>uninterpreted-subgoals
              "Tag not supported: ~q0"
              tag)
            (mv nil nil)))
        ((unless (consp hint-pair-lst)) (mv nil nil))
        ((cons first-hinted-h rest-hinted-hs) hint-pair-lst)
        (h (hint-pair->thm first-hinted-h))
        (h-hint (hint-pair->hints first-hinted-h))
        (merged-hint-please-in-theory (treat-in-theory-hint '(hint-please) h-hint))
        (merged-type-hyp-in-theory (treat-in-theory-hint '(type-hyp)
            merged-hint-please-in-theory))
        (merged-expand (treat-expand-hint '((:free (x) (hide x)))
            merged-type-hyp-in-theory))
        (first-h-thm (if (equal tag :return)
            `((hint-please ',SMT::MERGED-EXPAND) (type-hyp (hide (cons ,SMT::H 'nil)) ',SMT::TAG)
              ,SMT::G)
            `((hint-please ',SMT::MERGED-HINT-PLEASE-IN-THEORY) ,SMT::H
              ,SMT::G)))
        (first-not-h-clause (if (equal tag :return)
            `(not (type-hyp (hide (cons ,SMT::H 'nil)) ',SMT::TAG))
            `(not ,SMT::H)))
        ((mv rest-h-thms rest-not-h-clauses) (uninterpreted-subgoals rest-hinted-hs
            g
            tag)))
      (mv (cons first-h-thm rest-h-thms)
        (cons first-not-h-clause rest-not-h-clauses)))
    ///
    (defthm uninterpreted-subgoals-correctness
      (implies (and (pseudo-termp g)
          (alistp b)
          (hint-pair-listp hint-pair-lst)
          (ev-uninterpreted (disjoin (mv-nth 1
                (uninterpreted-subgoals hint-pair-lst
                  g
                  tag)))
            b)
          (ev-uninterpreted (conjoin-clauses (mv-nth 0
                (uninterpreted-subgoals hint-pair-lst
                  g
                  tag)))
            b))
        (ev-uninterpreted g b))
      :hints (("Goal" :induct (uninterpreted-subgoals hint-pair-lst
           g
           tag)))))
  (local (defthm crock3
      (implies (pseudo-term-list-listp x)
        (true-listp x))))
  (local (defthm crock4
      (implies (and (pseudo-term-list-listp x)
          (pseudo-term-list-listp y))
        (pseudo-term-list-listp (append x y)))))
  (local (defthm crock5
      (implies (and (pseudo-term-listp x)
          (pseudo-term-listp y))
        (pseudo-term-listp (append x y)))))
  (define uninterpreted-fn-cp
    ((cl pseudo-term-listp) (smtlink-hint t))
    :returns (subgoal-lst pseudo-term-list-listp)
    :guard-debug t
    (b* (((unless (pseudo-term-listp cl)) nil) ((unless (smtlink-hint-p smtlink-hint)) (list cl))
        (g (disjoin cl))
        ((smtlink-hint h) smtlink-hint)
        (uninterpreted (uninterpreted-fn-helper cl h))
        (hinted-ts-returns (uninterpreted->returns uninterpreted))
        (hinted-ts-more-returns (uninterpreted->more-returns uninterpreted))
        ((mv list-of-returns-t-thm
           list-of-returns-not-ts) (uninterpreted-subgoals hinted-ts-returns
            g
            :return))
        ((mv list-of-more-returns-t-thm
           list-of-more-returns-not-ts) (uninterpreted-subgoals hinted-ts-more-returns
            g
            :more-return))
        (list-of-t-thm (append list-of-returns-t-thm
            list-of-more-returns-t-thm))
        (list-of-not-ts (append list-of-returns-not-ts
            list-of-more-returns-not-ts))
        (next-cp (if h.custom-p
            (cdr (assoc-equal 'uninterpreted-custom
                *smt-architecture*))
            (cdr (assoc-equal 'uninterpreted
                *smt-architecture*))))
        ((if (null next-cp)) (list cl))
        (the-hint `(:clause-processor (,SMT::NEXT-CP clause ',SMT::H state)))
        (cl0 `((hint-please ',SMT::THE-HINT) ,@SMT::LIST-OF-NOT-TS
            ,SMT::G)))
      `(,SMT::CL0 ,@SMT::LIST-OF-T-THM)))
  (local (in-theory (enable uninterpreted-fn-cp)))
  (defthm correctness-of-uninterpreted-fn-cp
    (implies (and (pseudo-term-listp cl)
        (alistp b)
        (ev-uninterpreted (conjoin-clauses (uninterpreted-fn-cp cl smtlink-hint))
          b))
      (ev-uninterpreted (disjoin cl) b))
    :hints (("Goal" :in-theory (disable uninterpreted-subgoals-correctness)
       :use ((:instance uninterpreted-subgoals-correctness
          (g (disjoin cl))
          (hint-pair-lst (uninterpreted->returns (uninterpreted-fn-helper cl smtlink-hint)))
          (tag :return)
          (b b)) (:instance uninterpreted-subgoals-correctness
           (g (disjoin cl))
           (hint-pair-lst (uninterpreted->more-returns (uninterpreted-fn-helper cl smtlink-hint)))
           (tag :more-return)
           (b b)))))
    :rule-classes :clause-processor))