universal-equiv - ACL2 Book

Included Books

equality top

other

(in-package "ACL2")

include-book

(include-book "clause-processors/equality" :dir :system)

include-book

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

other

(set-state-ok t)

other

(defsection def-universal-equiv
  :parents (macro-libraries)
  :short "A macro for defining universally quantified equivalence relations."
  :long "<p>It is often useful to introduce equivalence relations such as:</p>

<blockquote>
<i>A === B when for every possible element E, A and B agree on E.</i>
</blockquote>

<p>For some particular notion of what <i>agree</i> means.  This macro gives you
a quick way to introduce such a relation, using @(see defun-sk), and then
automatically prove that it is an equivalence relation.  For instance, an
equivalence such as:</p>

@({
    (defun-sk foo-equiv (a b)
      (forall (x y z)
              (and (bar-equiv (foo a x y)
                              (foo b x y))
                   (baz-equiv (fa a z)
                              (fa b z)))))
})

<p>Can be introduced using:</p>

@({
    (def-universal-equiv foo-equiv (a b)
      :qvars (x y z)
      :equivs ((bar-equiv (foo a x y))
               (baz-equiv (fa a z))))
})

<p>When called with @(':defquant t'), we use @(see defquant) instead of @(see
defun-sk).  This requires that the WITNESS-CP book be included.</p>

<p>Note that @(':qvars') may be omitted, in which case there is no
quantifier (@(see defun-sk)) introduced.  This can be used as a shortcut to
prove that a fixing function induces an equivalence relation, e.g.,</p>

@({
  (def-universal-equiv gfix-equiv
    :equiv-terms ((equal (gfix x))))
 })
<p>produces</p>
@({
 (defun gfix-equiv (x y)
  (equal (gfix x) (gfix y)))

 (defequiv gfix-equiv)
 })

<p>(with appropriate hints to ensure that the @('defequiv') succeeds).</p>")

universal-equiv-equivtermsfunction

(defun universal-equiv-equivterms
  (var1 var2 equivs)
  (if (atom equivs)
    nil
    (let* ((equivname (caar equivs)) (term1 (cadar equivs))
        (term2 (esc-substitute term1 (list (cons var1 var2)))))
      (cons (list equivname term1 term2)
        (universal-equiv-equivterms var1 var2 (cdr equivs))))))

universal-equiv-multi-qvar-bindingsfunction

(defun universal-equiv-multi-qvar-bindings
  (n qvars witnesscall)
  (if (atom qvars)
    nil
    (cons `(,(CAR QVARS) (mv-nth ,N ,WITNESSCALL))
      (universal-equiv-multi-qvar-bindings (1+ n)
        (cdr qvars)
        witnesscall))))

universal-equiv-qvar-bindingsfunction

(defun universal-equiv-qvar-bindings
  (witness var1 var2 qvars)
  (let ((qvars (if (and (consp qvars) (not (consp (cdr qvars))))
         (car qvars)
         qvars)) (term (list witness var1 var2)))
    (if (atom qvars)
      (list (list qvars term))
      (universal-equiv-multi-qvar-bindings 0 qvars term))))

universal-equiv-formfunction

(defun universal-equiv-form
  (equivname qvars
    equivs
    defquant
    witness-dcls
    witness-dcls-p
    parents
    parents-p
    already-definedp
    short
    long
    state)
  (declare (xargs :mode :program))
  (let* ((equivterms `(and . ,(UNIVERSAL-EQUIV-EQUIVTERMS 'X 'Y EQUIVS))) (witness (intern-in-package-of-symbol (concatenate 'string (symbol-name equivname) "-WITNESS")
          equivname))
      (equivname-necc (intern-in-package-of-symbol (concatenate 'string (symbol-name equivname) "-NECC")
          equivname))
      (equivname-refl (intern-in-package-of-symbol (concatenate 'string (symbol-name equivname) "-REFL")
          equivname))
      (equivname-symm (intern-in-package-of-symbol (concatenate 'string (symbol-name equivname) "-SYMM")
          equivname))
      (equivname-trans (intern-in-package-of-symbol (concatenate 'string (symbol-name equivname) "-TRANS")
          equivname))
      (parents (if parents-p
          parents
          (or (get-default-parents (w state)) '(undocumented))))
      (long (or long
          (and parents
            (concatenate 'string
              "<p>This is a universal equivalence, introduced
                     using @(see acl2::def-universal-equiv).</p>"))))
      (long (and long
          (concatenate 'string
            long
            "@(def "
            (full-escape-symbol equivname)
            ")"))))
    `(defsection ,EQUIVNAME
      ,@(AND PARENTS `(:PARENTS ,PARENTS))
      ,@(AND SHORT `(:SHORT ,SHORT))
      ,@(AND LONG `(:LONG ,LONG))
      ,@(AND (NOT ALREADY-DEFINEDP)
       (LIST
        (IF QVARS
            (IF DEFQUANT
                `(DEFQUANT ,EQUIVNAME (X Y) (FORALL ,QVARS ,EQUIVTERMS)
                  ,@(AND WITNESS-DCLS-P `(:WITNESS-DCLS ,WITNESS-DCLS)))
                `(DEFUN-SK ,EQUIVNAME (X Y) ,@WITNESS-DCLS
                           (FORALL ,QVARS ,EQUIVTERMS)))
            `(DEFUN ,EQUIVNAME (X Y) ,EQUIVTERMS))))
      (in-theory (disable ,@(AND QVARS (LIST EQUIVNAME-NECC)) ,EQUIVNAME))
      (local (defthm ,EQUIVNAME-REFL
          (,EQUIVNAME x x)
          :hints (("goal" :in-theory (enable ,EQUIVNAME)))))
      (local (defthm ,EQUIVNAME-SYMM
          (implies (,EQUIVNAME x y) (,EQUIVNAME y x))
          :hints (("goal" ,@(IF QVARS
      `(:USE
        ((:INSTANCE ,EQUIVNAME-NECC
          ,@(UNIVERSAL-EQUIV-QVAR-BINDINGS WITNESS 'Y 'X QVARS)))
        :EXPAND ((,EQUIVNAME Y X)))
      `(:IN-THEORY (ENABLE ,EQUIVNAME)))))))
      (local (defthm ,EQUIVNAME-TRANS
          (implies (and (,EQUIVNAME x y) (,EQUIVNAME y z))
            (,EQUIVNAME x z))
          :hints (("goal" ,@(IF QVARS
      `(:USE
        ((:INSTANCE ,EQUIVNAME-NECC
          ,@(UNIVERSAL-EQUIV-QVAR-BINDINGS WITNESS 'X 'Z QVARS))
         (:INSTANCE ,EQUIVNAME-NECC
          ,@(UNIVERSAL-EQUIV-QVAR-BINDINGS WITNESS 'X 'Z QVARS) (X Y) (Y Z)))
        :EXPAND ((,EQUIVNAME X Z)))
      `(:IN-THEORY (ENABLE ,EQUIVNAME)))))))
      (defequiv ,EQUIVNAME))))

def-universal-equivmacro

(defmacro def-universal-equiv
  (name &key
    qvars
    equiv-terms
    defquant
    (witness-dcls 'nil witness-dcls-p)
    (parents 'nil parents-p)
    already-definedp
    short
    long)
  `(make-event (let ((form (universal-equiv-form ',NAME
           ',QVARS
           ',EQUIV-TERMS
           ',DEFQUANT
           ',WITNESS-DCLS
           ',WITNESS-DCLS-P
           ',PARENTS
           ',PARENTS-P
           ',ALREADY-DEFINEDP
           ',SHORT
           ',LONG
           state)))
      (value form))))