faig-equivs

(in-package "ACL2")

(defsection faig-equiv
  (def-universal-equiv faig-equiv
    :qvars env
    :equiv-terms ((equal (faig-eval x env)))
    :defquant t
    :witness-dcls ((declare (xargs :guard t :verify-guards nil)))
    :parents (faig)
    :short "We say the FAIGs @('X') and @('Y') are equivalent when they always
evaluate to the same value, per @(see faig-eval).")
  (verify-guards faig-equiv)
  (defcong faig-equiv
    equal
    (faig-eval x env)
    1
    :hints (("Goal" :in-theory (e/d (faig-equiv-necc) (faig-eval)))))
  (defthm faig-equiv-of-faig-fix
    (faig-equiv (faig-fix x) x)
    :hints (("Goal" :in-theory (enable faig-equiv)))))

(defsection faig-alist-equiv
  (def-universal-equiv faig-alist-equiv
    :qvars k
    :equiv-terms ((iff (hons-assoc-equal k x)) (faig-equiv (cdr (hons-assoc-equal k x))))
    :defquant t
    :witness-dcls ((declare (xargs :guard t :verify-guards nil)))
    :parents (faig)
    :short "We say the FAIG Alists @('X') and @('Y') are equivalent when they
bind the same keys to equivalent FAIGs, in the sense of @(see faig-equiv).")
  (verify-guards faig-alist-equiv)
  (defrefinement alist-equiv
    faig-alist-equiv
    :hints ((witness))))