		Search-engine friendly clone of the ACL2 documentation.

Soft-macros

Defequal

Introduce an equality between functions.

Introduction

In a first-order language like the one of ACL2, a second-order equality (i.e. an equality between two functions) cannot be expressed directly as a second-order assertion of the form

(equal f g)

but it can be expressed as a first-order assertion of the form

(forall (x1 ... xn) (equal (f x1 ... xn) (g x1 ... xn)))

This macro generates such expression of equality, as a defun-sk2, which already includes a rewrite rule from f to g; the macro also generates an rewrite rule from g to f. It also generates a theory invariant preventing both rewrite rules from being simultaneously enabled.

Thus, this macro automates the boilerplate of function equalities, and provides some support for reasoning about them. This macro may be extended with additional reasoning support.

General Form

(defequal name
          :left ...                  ; no default
          :right ...                 ; no default
          :vars ...                  ; default :auto
          :enable ...                ; default nil
          :verify-guards ...         ; default t
          :left-to-right-name ...    ; default :auto
          :left-to-right-enable ...  ; default nil
          :right-to-left-name ...    ; default :auto
          :right-to-left-enable ...  ; default nil
          :print ...                 ; default :result
          :show-only ...             ; default nil
  )

Inputs

name

Specifies the name of the generated function.
It must be a symbol.
In the rest of this documentation page, let name be the name of this function.

:left — no default
:right — no default

Specify the functions to use as the left-hand and right-hand sides of the equality.
Each must be an existing function symbol. It may be a SOFT function variable, a SOFT second-order function, a regular first-order function, etc.
The two functions must have the same arity, which must not be 0.
At least one of the two functions must be a function variable or a second-order function.
If the :verify-guards input (see below) is t, the two functions must have guard t and be guard-verified. Support for more general guards may be added in the future.
In the rest of this documentation page, let left and right be the names of these functions, and let n be their arity.

:vars — default :auto

Specifies the variables to use in the quantification.
It must be one of the following:
A list of distinct symbols that are legal variables. Its length must be n.
:auto, to use the list of symbols (x1 ... xn), all in the same package as name.
In the rest of this documentation page, let x1, ..., xn be these variables.

:enable — default nil.

Specifies whether name should be enabled.
It must be one of the following:
t, to enable it.
nil, to disable it.

:verify-guards — default t.

Specifies whether name should be guard-verified.
It must be one of the following:
t, to guard-verify it.
nil, to not guard-verify it.
Unless both left and right have guard t, this should be set to nil.

:left-to-right-name — default :auto

Specifies the name of the theorem that rewrites left to right.
It must be one of the following:
:auto, to use the name obtained by concatenating the name of left, `-to-', and the name of right, in the same package as name.
Any other symbol, to use as the name of the theorem.
In the rest of this documentation page, let left-to-right be the name of this theorem.

:left-to-right-enable — default nil.

Specifies whether left-to-right should be enabled.
It must be one of the following:
t, to enable it.
nil, to disable it.
If this is t, :right-to-left-enable must be nil.

:right-to-left-name — default :auto

Specifies the name of the theorem that rewrites left to right.
It must be one of the following:
:auto, to use the name obtained by concatenating the name of left, `-to-', and the name of right, in the same package as name.
Any other symbol, to use as the name of the theorem.
In the rest of this documentation page, let right-to-left be the name of this theorem.

:right-to-left-enable — default nil.

Specifies whether right-to-left should be enabled.
It must be one of the following:
t, to enable it.
nil, to disable it.
If this is t, :left-to-right-enable must be nil.

:print — default :result

Specifies what is printed on the screen (see screen printing).
It must be one of the following:
nil, to print nothing (not even error output).
:error, to print only error output (if any).
:result, to print, besides any error output, also the results of defequal. This is the default value of the :print input.
:info, to print, besides any error output and the results, also some additional information about the internal operations of defequal.
:all, to print, besides any error output, the results, and the additional information, also ACL2's output in response to all the submitted events.
If the call of defequal is redundant, an indication to that effect is printed on the screen, unless :print is nil.

:show-only — default nil

Determines whether the event expansion of defequal is submitted to ACL2 or just printed on the screen:
nil, to submit it.
t, to just print it. In this case: the event expansion is printed even if :print is nil (because the user has explicitly asked to show the event expansion); the resulting events are not re-printed separately (other than their appearance in the printed event expansion) even if :print is :result or :info or :all; no ACL2 output is printed for the event expansion even if :print is :all (because the event expansion is not submitted). If the call of defequal is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

Generated Events

name

Function that expresses the equality of left and right:
(defun-sk2 name ()
  (forall (x1 ... xn)
          (equal (left x1 ... xn)
                 (right x1 ... xn)))
  :rewrite :direct
  :thm-name left-to-right)
Note the generation of left-to-right as a direct rewrite rule. See next item.

left-to-right

Theorem that rewrites left to right:
(defthm left-to-right
  (implies (name)
           (equal (left x1 ... xn)
                  (right x1 ... xn))))
This is generated by the defun-sk2. See previous item.

right-to-left

Theorem that rewrites right to left:
(defthm right-to-left
  (implies (name)
           (equal (right x1 ... xn)
                  (left x1 ... xn))))
This is generated by the defun-sk2. See previous item.

Redundancy

A call of defequal is redundant if and only if it is identical to a previous successful call of defequal whose :show-only input is not t, except that the two calls may differ in their :print and :show-only inputs. These inputs do not affect the generated events, and thus they are ignored for the purpose of redundancy.

A call of defequal whose :show-only input is t does not generate any event. Thus, no successive call may be redundant with such a call.

Subtopics

Defequal-implementation: Implementation of defequal.