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.

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:

def-listp-rule theorems will be instantiated by std::deflist and fty::deflistdef-listfix-rule theorems will be instantiated by fty::deflist, pertaining to the list-fix function it introducesdef-projection-rule theorems will be instantiated by std::defprojectiondef-mapappend-rule theorems will be instantiated by std::defmapappend.

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.

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 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

(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))))

Note: All of these are symbols in the ACL2 package.

element-p-of-nil is true if NIL is known to be an elementnot-element-p-of-nil is true if NIL is known not to be an element. Note: mutually exclusive withelement-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 byNOT of some predicate, which may affect the correct formulation of rewrite rulestrue-listp is true if the list recognizer is strict, i.e., implies true-listpsingle-var is true if the list recognizer has no parameters other than the list variablecheap 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.

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

(local (ruletable-delete-tags! acl2::listp-rules (:osets)))

On the other hand, in the unlikely event that you only wanted the rules
tagged with

(local (ruletable-keep-tags! acl2::listp-rules (:osets)))

- 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.