		Search-engine friendly clone of the ACL2 documentation.

Equiv

A macro to prove that a universally quantified formula is a paramaterized equivalence relation

The quant::equiv macro can be used to prove that a universally quantified formula satisfies the properties of a parameterized equivalence relation. This macro is similar in nature to ACL2::def-universal-equiv except that parameterized equivalences are supported. If no paramaters are specified, however, we prove that the quantified formula is in fact a standard ACL2::equivalence relation.

Usage:

(include-book "coi/quantification/quantified-equivalence" :dir :system)
             
(defun foo-pred (x k a y n b)
  (declare (ignore k a n b))
  (equal x y))

(defun-sk foo (x k y n)
  (forall (a b) (foo-pred x k a y n b)))

;; The first argument is the name of the quantified formula.
;; The first argument list specifies the "equivalent" arguments
;; The second argument list specifies the parameters
(quant::equiv foo (x y) (k n)
  ;; Repeat the body from the defun-sk event
  (forall (a b) (foo-pred x k a y n b))
  ;; Since the formals to the actual quantified formula 
  ;; are not (x y k n) as we would otherwise assume from
  ;; the arguments above we must specifify the actual
  ;; order of the formal arguments.
  :formals (x k y n))

(in-theory (disable foo))

;; This now proves automatically
(defthm equivalance-relation-properties
   (and
    (booleanp (foo x k y n))
    (foo x k x n)
    (implies
     (foo x k y n)
     (foo y k x n))
    (implies
     (and
      (foo x k y n)
      (foo y k z n))
     (foo x k z n))))