gtests

(in-package "GL")

(include-book "hyp-fix")

(include-book "gtypes")

(include-book "tools/mv-nth" :dir :system)

(local (include-book "gtype-thms"))

(local (include-book "bfr-reasoning"))

(set-inhibit-warnings "theory")

(define mk-g-bdd-ite
  (bdd then else hyp)
  (let ((test (hf bdd)))
    (cond ((th test) then)
      ((fh test) else)
      (t (mk-g-ite (mk-g-boolean bdd) then else))))
  ///
  (defcong bfr-hyp-equiv
    equal
    (mk-g-bdd-ite bdd then else hyp)
    4
    :hints (("Goal" :in-theory (enable true-under-hyp false-under-hyp))))
  (defthm mk-g-bdd-ite-correct
    (implies (double-rewrite (bfr-hyp-eval hyp (car env)))
      (equal (generic-geval (mk-g-bdd-ite bdd then else hyp)
          env)
        (if (bfr-eval bdd (car env))
          (generic-geval then env)
          (generic-geval else env))))
    :hints (("Goal" :in-theory (enable true-under-hyp false-under-hyp)) (bfr-reasoning)))
  (defthm mk-g-bdd-ite-of-bfr-hyp-fix
    (equal (mk-g-bdd-ite bdd
        then
        else
        (bfr-hyp-fix hyp))
      (mk-g-bdd-ite bdd then else hyp)))
  (defthm gobj-depends-on-of-mk-g-bdd-ite
    (implies (and (not (pbfr-depends-on k p bdd))
        (not (gobj-depends-on k p then))
        (not (gobj-depends-on k p else)))
      (not (gobj-depends-on k
          p
          (mk-g-bdd-ite bdd then else hyp))))
    :hints (("Goal" :in-theory (enable mk-g-bdd-ite)))))

(with-output :off (prove event)
  (define gtests
    (x hyp)
    :returns (mv nonnilp
      unknownp
      unknown-obj
      same-hyp)
    :verify-guards nil
    (let* ((hyp (hyp-norm hyp)))
      (if (atom x)
        (mv (hf (if x
              t
              nil))
          (hf nil)
          nil
          hyp)
        (pattern-match x
          ((g-concrete obj) (mv (hf (if obj
                  t
                  nil))
              (hf nil)
              nil
              hyp))
          ((g-boolean bool) (mv (hf bool) (hf nil) nil hyp))
          ((g-integer &) (mv (hf t) (hf nil) nil hyp))
          ((g-apply & &) (mv (hf nil) (hf t) x hyp))
          ((g-var &) (mv (hf nil) (hf t) x hyp))
          ((g-ite test then else) (b* (((mv cc uc oc hyp) (gtests test hyp)) ((mv contra1 hyp undo1) (bfr-assume (bfr-or cc uc) hyp))
                ((when contra1) (b* ((hyp (bfr-unassume hyp undo1)))
                    (gtests else hyp)))
                ((mv c1 u1 o1 hyp) (gtests then hyp))
                (hyp (bfr-unassume hyp undo1))
                ((mv contra0 hyp undo0) (bfr-assume (bfr-or (hf (bfr-not cc)) uc)
                    hyp))
                ((when contra0) (b* ((hyp (bfr-unassume hyp undo0)))
                    (mv (hf c1) (hf u1) o1 hyp)))
                ((mv c0 u0 o0 hyp) (gtests else hyp))
                (hyp (bfr-unassume hyp undo0))
                ((when (and (eq uc nil) (eq u1 nil) (eq u0 nil))) (mv (hf (bfr-ite cc c1 c0))
                    nil
                    nil
                    hyp))
                (known-ans (hf (bfr-ite cc c1 c0)))
                (unknown (hf (cond ((eq uc t) (bfr-or (bfr-or u1 u0)
                          (bfr-xor c1 c0)))
                      ((eq uc nil) (bfr-ite cc u1 u0))
                      (t (bfr-ite uc
                          (bfr-or (bfr-or u1 u0)
                            (bfr-xor c1 c0))
                          (bfr-ite cc u1 u0)))))))
              (if (eq unknown nil)
                (mv known-ans unknown nil hyp)
                (b* ((unknown-cond (mk-g-bdd-ite uc
                       oc
                       (mk-g-boolean cc)
                       hyp)) (unknown-obj1 (mk-g-bdd-ite u1
                        o1
                        (mk-g-boolean c1)
                        hyp))
                    (unknown-obj0 (mk-g-bdd-ite u0
                        o0
                        (mk-g-boolean c0)
                        hyp))
                    (unknown-obj (mk-g-ite unknown-cond
                        unknown-obj1
                        unknown-obj0)))
                  (mv known-ans unknown unknown-obj hyp)))))
          (& (mv (hf t) (hf nil) nil hyp)))))
    ///
    (verify-guards gtests
      :hints (("Goal" :in-theory (disable gtests))))
    (def-hyp-congruence gtests
      :pres-hints (("Goal" :in-theory (disable (:d gtests))
         :induct (gtests x hyp)) '(:expand ((gtests x hyp))))
      :hyp-fix-hints (("goal" :expand ((gtests x hyp) (gtests x (bfr-hyp-fix hyp))))))))

(in-theory (disable (:definition gtests)))

(local (progn (defthmd bfr-eval-nonnil-forward
      (implies (bfr-eval x y) x)
      :rule-classes :forward-chaining)
    (local (in-theory (enable bfr-eval-nonnil-forward)))
    (defun-nx gnuo-ind
      (x hyp)
      (let ((hyp (lbfr-hyp-fix hyp)))
        (if (atom x)
          hyp
          (pattern-match x
            ((g-ite test then else) (b* ((?ign (gnuo-ind test hyp)) ((mv ?cc ?uc ?oc ?hypx) (gtests test hyp))
                  ((mv ?contra1 hyp1 ?undo1) (bfr-assume (bfr-or cc uc) hyp))
                  ((mv ?contra0 hyp0 ?undo0) (bfr-assume (bfr-or (hf (bfr-not cc)) uc)
                      hyp)))
                (if contra1
                  (gnuo-ind else hyp)
                  (if contra0
                    (gnuo-ind then hyp1)
                    (list (gnuo-ind then hyp1)
                      (gnuo-ind else hyp0))))))
            (& hyp)))))
    (local (in-theory (disable (:definition generic-geval)
          bfr-eval
          bfr-eval-list
          bfr-eval-booleanp)))))

(local (progn (defthm gtests-hyp-fixedp
      (and (hyp-fixedp (mv-nth 0 (gtests x hyp))
          hyp)
        (hyp-fixedp (mv-nth 1 (gtests x hyp))
          hyp))
      :hints (("goal" :induct (gnuo-ind x hyp)
         :in-theory (enable (:i gtests))
         :expand ((gtests x hyp))) (and stable-under-simplificationp
          '(:in-theory (enable hyp-fixedp)))))
    (add-bfr-pat (mv-nth 0 (gtests . &)))
    (add-bfr-pat (mv-nth 1 (gtests . &)))
    (local (bfr-reasoning-mode t))
    (local (in-theory (disable* hyp-fix-of-hyp-fixedp
          (:type-prescription bfr-eval)
          (:type-prescription true-under-hyp)
          (:type-prescription false-under-hyp)
          (:type-prescription q-implies-fn)
          (:type-prescription bfr-ite-fn)
          (:type-prescription booleanp)
          equal-of-booleans-rewrite
          default-car
          default-cdr
          bfr-eval-nonnil-forward
          hons-assoc-equal
          not)))
    (local (in-theory (enable true-under-hyp-point
          false-under-hyp-point)))
    (local (in-theory (disable gtests
          generic-geval
          double-containment
          tag-when-atom
          generic-geval-non-cons)))
    (local (in-theory (disable bfr-assume-correct
          true-under-hyp-point
          false-under-hyp-point
          true-listp
          mv-nth-cons-meta
          (:t mk-g-bdd-ite)
          (:t mk-g-boolean)
          (:t bfr-hyp-fix)
          (:t bfr-hyp-eval)
          sets-are-true-lists)))
    (defthm gtests-correct
      (mv-let (cc uc uo)
        (gtests x hyp)
        (implies (bfr-hyp-eval hyp (car env))
          (iff (generic-geval x env)
            (if (bfr-eval uc (car env))
              (generic-geval uo env)
              (bfr-eval cc (car env))))))
      :hints (("Goal" :induct (gnuo-ind x hyp)
         :expand ((gtests x hyp) (generic-geval x env)
           (generic-geval nil env))
         :in-theory (disable bfr-assume-correct
           true-under-hyp-point
           false-under-hyp-point)
         :do-not-induct t) (and stable-under-simplificationp
          '(:in-theory (e/d (bfr-assume-correct)
              (true-under-hyp-point false-under-hyp-point)))))
      :rule-classes nil)))

(defthm gobj-depends-on-of-gtests
  (implies (not (gobj-depends-on k p x))
    (mv-let (cc uc uo)
      (gtests x hyp)
      (and (not (pbfr-depends-on k p cc))
        (not (pbfr-depends-on k p uc))
        (not (gobj-depends-on k p uo)))))
  :hints (("goal" :induct (gnuo-ind x hyp)
     :expand ((gtests x hyp))
     :in-theory (e/d nil))))

(defthm gtests-nonnil-correct
  (b* (((mv ?nonnil ?unknown ?obj) (gtests x hyp)))
    (implies (and (not (bfr-eval unknown (car env)))
        (bfr-hyp-eval hyp (car env)))
      (equal (bfr-eval nonnil (car env))
        (if (generic-geval x env)
          t
          nil))))
  :hints (("goal" :use ((:instance gtests-correct))
     :in-theory (enable (:type-prescription bfr-eval)))))

(defthm gtests-obj-correct
  (b* (((mv ?nonnil ?unknown ?obj) (gtests x hyp)))
    (implies (and (bfr-eval unknown (car env))
        (bfr-hyp-eval hyp (car env)))
      (iff (generic-geval obj env)
        (generic-geval x env))))
  :hints (("goal" :use ((:instance gtests-correct)))))

(defthm bfr-assume-of-gtests-possibly-true
  (b* (((mv nonnil unknown &) (gtests obj hyp)) ((mv & hyp1 &) (bfr-assume$a (bfr-binary-or nonnil unknown)
          hyp)))
    (implies (and (generic-geval obj env)
        (bfr-hyp-eval hyp (car env)))
      (bfr-hyp-eval hyp1 (car env)))))

(defthm bfr-assume-of-gtests-possibly-false
  (b* (((mv nonnil unknown &) (gtests obj hyp)) ((mv & hyp1 &) (bfr-assume$a (bfr-binary-or (bfr-not nonnil) unknown)
          hyp)))
    (implies (and (not (generic-geval obj env))
        (bfr-hyp-eval hyp (car env)))
      (bfr-hyp-eval hyp1 (car env)))))