Std/lists/abstract
Abstract theories for listp, projection, and mapappend functions
This book defines various generic functions:
- element-p
- element-fix
- element-equiv
- element-list-p
- element-list-fix
- element-list-equiv
- element-list-projection
- element-list-mapappend
The idea is that in other books, we can add various theorems about how these
generic functions behave in relation to other functions such as nth, index-of,
member, etc, which we can use in pluggable forms of std::deflist, std::defprojection, or std::defmapappend. However, as yet this
functionality is only implemented for std::deflist (and through std::deflist, also fty::deflist).
We'll describe in this documentation how to write theorems that can be
instantiated by std::deflist so that they can be used for arbitrary
typed lists. Eventually, this will also apply to std::defprojection and
std::defmapappend.
Writing Generic Typed-list Rules
Generic Rule Macros
Deflist creates theorems for each new list type it defines by instantiating
a list of theorems recorded in a table. To create a new theorem and add it to
that table so that it is available to deflist, use the def-listp-rule
macro, which is similar to defthm. There are other such macros for rules about
other kinds of functions as well:
These macros all take the same basic arguments as defthm but some
additional keyword arguments as well; the following shows an elaborate example.
(def-listp-rule element-list-p-when-not-consp-non-true-list
(implies (and (element-list-final-cdr-p t)
(not (consp x)))
(element-list-p x))
:hints (("goal" :expand ((element-list-p))))
:rule-classes :rewrite
:otf-flg nil
:requirement (not true-listp)
:name element-list-p-when-not-consp
:body (implies (not (consp x))
(element-list-p x))
:inst-rule-classes ((:rewrite :backchain-limit-lst 2))
:cheap-rule-classes ((:rewrite :backchain-limit-lst 0))
:tags (:basic))
To briefly describe the keyword arguments:
- :hints, :rule-classes, and :otf-flg are the same as in defthm and do not affect what is stored for later instantiation
- :requirement restricts this rule to only apply to certain kinds of
typed lists; see the section "Variants and Requirements" below
- :name overrides the theorem name template used by instantiations of
this theorem
- :body overrides the theorem body as the template to be used for
instantiations; see the "Variants and Requirements" section
- :inst-rule-classes overrides the rule-classes used by instantiations
of this theorem
- :cheap-rule-classes provide an alternative rule-classes if the option
:cheap t is given to deflist
- :tags are freeform annotations of the rules, which can be used to
disable in bulk certain sets of rules from being instantiated.
Variants and Requirements
Some theorems pertaining to typed lists are best phrased differently when:
- the list recognizer requires/does not require a NIL final cdr
- the list element recognizer is true of/is not true of NIL, or its value on
NIL is unknown or varies with other parameters.
The example def-listp-rule form above, here reproduced with irrelevant
parts removed, helps to show how we accommodate these variants:
(def-listp-rule element-list-p-when-not-consp-non-true-list
(implies (and (element-list-final-cdr-p t)
(not (consp x)))
(element-list-p x))
:requirement (not true-listp)
:name element-list-p-when-not-consp
:body (implies (not (consp x))
(element-list-p x)))
The :body shows the theorem that will be produced by instantiations of
this rule. However, this is only true when element-list-p is non-strict,
i.e. it allows a non-nil final cdr. The generic definition of element-list-p
accomodates both strict and non-strict versions by calling a constrained
function element-list-final-cdr-p on its final cdr. This function is
constrained to either be true on every input, or to only be true on NIL; thus,
it matches the two typical final cdr behaviors of list recognizers. To prove
that any non-cons is element-list-p, we need to assume we are in the non-strict
case -- where element-list-final-cdr-p is true of every input -- which, by
its constraint, is true iff (element-list-final-cdr-p t). To avoid
instantiating this rule on typed lists that are strict, we add the
:requirement field. In std::deflist, before instantiating a rule,
the :requirement field is evaluated with variables such as true-listp
bound to values based on the particular variant. Finally, the :name field
lets us consistently name the instantiated theorems when there are different
variants; e.g., for the strict case, we can have this other form that produces
a different theorem but uses the same naming convention:
(def-listp-rule element-list-p-when-not-consp-true-list
(implies (and (not (element-list-final-cdr-p t))
(not (consp x)))
(equal (element-list-p x) (not x)))
:requirement true-listp
:name element-list-p-when-not-consp
:body (implies (not (consp x))
(equal (element-list-p x)
(not x))))
List of requirement variables recognized by std::deflist
Note: All of these are symbols in the ACL2 package.
- element-p-of-nil is true if NIL is known to be an element
- not-element-p-of-nil is true if NIL is known not to be an element.
Note: mutually exclusive with element-p-of-nil, but both may be false in
cases where the status of NIL as an element is unknown or depends on other
input parameters.
- negatedp is true if we are creating a list that recognizes elements
defined by NOT of some predicate, which may affect the correct formulation
of rewrite rules
- true-listp is true if the list recognizer is strict, i.e., implies true-listp
- single-var is true if the list recognizer has no parameters other than the list variable
- cheap is true if the user gave an extra option requesting cheaper versions of some rules.
- simple is true if the element recognizer is a simple function, rather
than some more complicated term.
Using Tags to Disable Instantiation
Certain generic rules are tagged so as to group them with other rules. For
example, all the rules defined in "std/osets/element-list.lisp" are tagged
with :osets. This makes it easy to turn these rules off so that a
subsequent deflist form will not instantiate this set of rules. This form does
that:
(local (ruletable-delete-tags! acl2::listp-rules (:osets)))
On the other hand, in the unlikely event that you only wanted the rules
tagged with :osets you could do:
(local (ruletable-keep-tags! acl2::listp-rules (:osets)))
Subtopics
- Element-list-p
- Generic typed list recognizer function.
- Element-list-equiv
- Generic typed list equivalence relation
- Element-list-nonempty-p
- Generic typed list recognizer function.
- Elementlist-projection
- Generic projection over a typed list.
- Element-equiv
- Generic equivalence relation among typed list elements.
- Generic-eval-requirement
- Evaluate a requirement of a generic theorem for deflist/defprojection/defmapappend
- Element-list-fix
- Generic typed list fixing function.
- Elementlist-mapappend
- Generic mapappend over a typed list.
- Element-fix
- Generic fixing function for typed list elements.
- Outelement-list-p
- Generic recognizer for the output list type of a projection.
- Outelement-p
- Generic recognizer for the output element type of a projection.
- Element-xformer
- Generic transform to be projected over a typed list.
- Element-listxformer
- Generic element-list transform for mapappend
- Element-p
- Generic typed list element recognizer.
- Def-listp-rule
- Define a theorem and save it in a table, denoting that it is a rule
about element-list-p.
- Def-projection-rule
- Define a theorem and save it in a table, denoting that it is a rule
about elementlist-projection.
- Def-nonempty-listp-rule
- Define a theorem and save it in a table, denoting that it is a rule
about element-list-nonempty-p.
- Def-mapappend-rule
- Define a theorem and save it in a table, denoting that it is a rule
about elementlist-mapappend.
- Def-listfix-rule
- Define a theorem and save it in a table, denoting that it is a rule
about element-list-fix.
