Introduction-to-apply$
Background knowledge on how to use apply$, defwarrant, etc.
Background and Organization
Apply$ is the ACL2 version of LISP's apply function. It takes a
``function'' and a list of argument values, applies the function to the
arguments, and returns the result. For example, (apply$ 'expt (list 2
8)) returns 256.
A good introduction to the basic ideas and challenges of adding
apply$ to ACL2 is the paper ``Limited
Second-Order Functionality in a First-Order Setting'' by Matt Kaufmann
and J Strother Moore, Journal of Automated Reasoning, Springer,
64, pp 391-422, 2018. We refer to the paper simply as ``the paper.''
Some aspects of the paper are no longer accurate because the implementation
of apply$ has matured since 2018. But as a basic introduction, rather
than a reference guide or user's manual, the paper is a good place to start.
It provides motivations and challenges, succinct and precise definitions of
relevant concepts, lots of examples, a model and meta-level proof that the
extended theory is consistent, and a discussion of the limitations and of
related work. The model described in the paper is illustrated concretely in
the certified books under books/projects/apply-model/. See the
README file there.
The current documentation topic takes a slightly more informal approach
but covers much of the same ground. In particular, after some preliminary
remarks we coach you through a few simple simple exercises involving
apply$ and related concepts. During these exercises we draw your
attention to some basic lessons to keep in mind. At the end of this topic we
list some simple challenge problems.
This topic links to reference-level documentation for apply$ and
those other concepts. But if you are just getting started with apply$
we recommend that you work your way through this topic, including doing the
examples described below, without following all the links.
Challenges and Basic Solutions
The unreachable goal of this work is to allow the ACL2 user to pass
`functions' as objects and to apply them. That goal is unreachable because
ACL2 remains a first order system. However, we can identify a certain
syntactic class of ordinary ACL2 objects, called the `tame
functions' (which are in fact not functions but are merely symbols and
list expressions) and we can allow names of functions with certain tameness
properties to be passed around and used as functions.
By the way, in this documentation topic we tend to display certain symbols
sometimes in uppercase and sometimes in lowercase. They denote the same
symbol. But we use uppercase when we're using the symbol as a quoted
constant to be passed to apply$ and we use lowercase when we're using
the symbol as a function symbol in a term.
``Tameness'' imposes strict rules on how functional arguments are used.
We'll discuss it further below.
The fundamental question raised by apply$ is ``How can apply$
know the correspondence between an ordinary ACL2 object, like a symbol or a
list, and the ACL2 function the user means to apply?'' For example, if the
user defines the function my-append, how can apply$ know that
(apply$ 'MY-APPEND (list a b)) should expand to (my-append a b)?
The ACL2 primitives can be built in. The logical definition of apply$
includes a big case split that recognizes about 800 ACL2 primitives, so that
for example:
(apply$ 'car (list a)) = (car a)
and
(apply$ 'assoc-equal (list a b)) = (assoc-equal a b).
But user-defined functions are problematic because once apply$ has been
defined in the ACL2 sources it cannot be extended to handle new symbols.
Intuitively, if you have defined the n-ary function foo then you
would expect (apply$ 'foo (list a1...an)) to be (foo a1...an). One
way to arrange that might be to leave apply$ undefined on the symbol
foo but to assume, as by a new axiom or hypothesis,
forall a1...an : (apply$ 'foo (list a1...an)) = (foo a1...an).
It will turn out that using new axioms for this purpose is a bad idea.
Hiding the link between apply$ and new symbols in axioms raises a
problem with ACL2's notion of local. This is called ``the LOCAL
problem'' and we illustrate it later in this doc topic. But for that reason,
the suppositions extending apply$ will take the form of hypotheses to be
added to conjectures in which the behavior of apply$ on new symbols is
important. These hypotheses are called ``warrants.''
Warrant (Merriam-Webster): (noun) a commission or document giving
authority to do something....
In our case, a warrant for fn gives apply$ permission to apply
fn under some circumstances, by asserting a universally quantified
conditional equality about apply$'s behavior on 'fn. It also tells
apply$ and the tameness predicates things like how many arguments
fn takes and how it uses them by asserting the badge of
'fn. The badge of fn is an ACL2 object that contains various
tokens interpretable by apply$ and the tameness predicates.
But there is a fundamental logical problem: it is not always possible to
satisfy such suppositions. There may be no way that apply$ could handle
fn. An example of a fn for which that hypothesis is unsatisfiable
is
(defun russell (x y) (not (apply$ x (list y y)))).
This definition of russell is not recursive: it does not call itself.
So this definition is admissible. But if we had a warrant for apply$
and that warrant were as simple as
forall x,y : (apply$ 'russell (list x y)) = (russell x y)
then we would have this classical problem with self-reference:
(russell 'russell 'russell)
= {def russell}
(not (apply$ 'russell (list 'russell 'russell)))
= {warrant russell}
(not (russell 'russell 'russell))
which is contradictory.
This problem is addressed by introducing the notion of ``tameness.''
Tameness is a syntactic property of terms and functions that implies that it
is ok to ``extend'' apply$ to handle them.
It should be pretty clear that if the user defines an ACL2 function that
in no way depends on apply$, e.g., a function like:
(defun sq (x) (* x x))
then the hypothesis
forall x : (apply$ 'SQ (list x)) = (sq x)
is satisfiable: we could have introduced sq before apply$ and
then defined apply$ in the first place to handle that particular
symbol.
Sq is a particularly simple example of a tame function. One
challenge in this work has been to extend the notion of tameness so that it
includes a lot of what a normal ACL2 programmer might want in apply$
while maintaining the soundness of the resulting theory.
For example, consider the following function, which maps a given function
over a list and collects the results.
(defun my-collect$ (fn lst)
(if (endp lst)
nil
(cons (apply$ fn (list (car lst)))
(my-collect$ fn (cdr lst)))))
Our definition of tameness considers (my-collect$ 'SQ lst) to be a
tame expression, even though my-collect$ calls apply$. The reason we
can allow this is that in this particular call of my-collect$ the function
to be applied is itself tame. But if (my-collect$ 'SQ lst) is a tame
expression, then '(LAMBDA (LST) (MY-COLLECT$ 'SQ LST)) is a tame
function and thus
(my-collect$ '(LAMBDA (LST) (MY-COLLECT$ 'SQ LST)) z)
is a tame expression. So, for example, at the top-level of ACL2 one
can do this:
ACL2 !>(my-collect$ '(LAMBDA (LST) (MY-COLLECT$ 'SQ LST))
'((1 2 3) (4 5 6) (7 8 9)))
((1 4 9) (16 25 36) (49 64 81))
Of course, this presumes we have defined sq and my-collect$ and have
analyzed them to make sure they have the appropriate tameness properties.
(Note that my-collect$ is not tame, but the way it uses its ``functional''
argument is crucial to the tameness of (my-collect$ 'SQ lst).) To use
apply$ to full advantage we need to have analyzed every relevant
function definition so we know which arguments are treated like functions and
whether they are used in accordance with our restrictions. So if you're
defining a function you intend to apply$ it is convenient to define it
with the new command defun$, which is just an ordinary defun
followed by a defwarrant command. If you've already defined the
function and then realize you wish to apply$ it, you can call
defwarrant yourself.
Defwarrant analyzes a :logic mode definition and
produces a badge and a warrant, if possible. Also relevant is the defbadge command which issues a badge for a function (if possible) but does
not issue a warrant. Its primary purpose is to allow :program mode
functions to be analyzed and badged so they can be safely executed by
apply$ at the top-level ACL2 loop. But the present discussion focuses
primarily on the logical machinery, which requires warrants.
We explain further via an annotated example, starting from scratch but
from the basic background just sketched. For many additional examples, see
community-books books/projects/apply/report.lisp which is a
certified book containing the examples in the paper.
Note carefully: the directory books/projects/apply-model/,
mentioned earlier in conjunction with the paper, is different from the
directory books/projects/apply/ just mentioned! The former directory
concerns the logical foundations of apply$ as they stood when the paper
was written. The latter is more directly relevant to ACL2 users and provides
useful lemmas about apply$ as it is axiomatized and implemented today.
It also includes many example theorems.
Exercises and Lessons
To get started, fire up your ACL2 and define two ordinary ACL2 functions,
one that squares its argument and the other that reverses its argument. We
show the ACL2 prompt below in front of each form we expect you to execute.
ACL2 !>(defun sq (x) (* x x))
ACL2 !>(defun rev (x)
(if (endp x)
nil
(append (rev (cdr x)) (list (car x)))))
Lesson 0: Learn about apply$ by reading this tutorial
introduction. But this tutorial mentions many undefined concepts: tameness,
warrants, badges, ilks. These concepts are intertwined with apply$ and
warrants through mutual recursion, constraints, rewrite rules, etc.. So we
decided not to try to define them here as we go along, though the links
provided do provide definitive descriptions. So please tolerate the use of
undefined words here — we'll try to give you a sense of what they
mean.
Lesson 1: To use apply$, be sure to include the following book
of lemmas. These lemmas are important not just to proving theorems about
apply$ but to defining functions that use apply$.
ACL2 !>(include-book "projects/apply/top" :dir :system)
Lesson 2: To allow apply$ to ``work'' on a function symbol the
symbol must be ``warranted.'' Actually, of course, you can pass anything to
apply$ and the axioms will reduce it to some value: ACL2 is untyped and
all functions are total! But apply$ won't work in the logic as you
expect if the first argument to apply$ is not warranted! (And
apply$ won't work as you expect for top-level evaluation if its first
argument is not at least badged.) To issue warrants (and badges) for sq
and rev do:
ACL2 !>(defwarrant sq)
ACL2 !>(defwarrant rev)
Defwarrant checks that its argument, fn, is a defined
function symbol that satisfies certain restrictions on how it uses its
arguments, restrictions that enable us to define the tameness predicates and
that allow apply$ to ``work'' without causing logical contradictions.
Defwarrant causes an error if fn does not obey our rules. But if
defwarrant does not cause an error it produces a ``badge'' for fn
that describes which formals are treated as ``functions.'' Henceforth, we'll
say such formals have ``ilk'' :FN. In addition to computing a
badge, non-erroneous calls of defwarrant introduce a “warrant function” for fn. The warrant function for fn
is a 0-ary function named apply$-warrant-fn. A call of the
warrant function, i.e., the term (apply$-warrant-fn) is
called the “warrant” for fn and if the warrant for
fn is included among the hypotheses of a conjecture then (apply$
'fn (list a1 ... an)) can expand to (fn a1
... an), provided the ai meet the tameness requirements required by
fn's badge.
Lesson 3: We'll say more about tameness, badges, and warrants
later. You already know that warrants can only be issued for :logic
mode functions because the function symbol is used as a function in the
logical definition of the warrant. But you might as well learn four major
limitations of apply$:
(i) Apply$ does not take state or stobj arguments and so
cannot call any function that takes STATE or stobj arguments. (ii)
Apply$ cannot call a function whose measure, well-founded relation, or
domain predicate depends on apply$. (iii) Apply$ cannot call a
function that itself uses apply$ unless that function's measure is a
natural number or a lexicographic combination of naturals formed with
llist as defined in the Community Books at books/ordinals/. (iv)
Apply$ cannot call a function that itself uses apply$ if that
function was defined mutually recursively. Another way of saying all this is
that defwarrant will cause an error if you try to warrant a function
violating (i), (ii), (iii) or (iv).
Lesson 4: If you want to define a function and immediately call
defwarrant on it you can use the handy macro defun$. We'll use
defun$ freely below.
Lesson 5: You can define functions that take warranted
``functions'' as arguments and apply$ them. Here is a function that
applies its first argument to every element of its second argument and
collects the results. We sometimes call functions like my-collect$
``mapping functions'' because they map another function over some range. We
would call them ``functionals'' except that suggests ACL2 is higher-order and
it is not! So we most often call them scions of apply$. In
ordinary English usage, a ``scion'' is a descendent of an important family or
individual; our scions are ``descendents'' of apply$ and inherit its
power and restrictions.
ACL2 !>(defun$ my-collect$ (fn lst)
(if (endp lst)
nil
(cons (apply$ fn (list (car lst)))
(my-collect$ fn (cdr lst)))))
In this definition, the first argument has ilk :FN because it is used
exclusively as a ``function:'' it reaches the first argument of apply$
and is untouched otherwise. The second argument has ilk NIL and we say
it's ``ordinary.'' It is never used as a function.
Note: We define my-collect$ with defun$ simply to illustrate
defun$. Unless we mean to pass my-collect$ to apply$ or to
some scion in the future, there is no reason to have a warrant for
my-collect$. Had we defined my-collect$ with the ordinary
defun and realized later that we want to pass 'MY-COLLECT$ into a
slot of ilk :FN, we could get a warrant for my-collect$ by calling
(defwarrant my-collect$).
Actually, the function collect$ is pre-defined in ACL2 and behaves
like my-collect$. We chose to introduce my-collect$ simply to
illustrate that new scions can be introduced and used. Here's another useful
pre-defined scion. You won't need to define it in your ACL2 session to use
it.
(defun$ always$ (fn lst)
(if (endp lst)
t
(and (apply$ fn (list (car lst)))
(always$ fn (cdr lst)))))
It checks that every element of lst satisfies its :FN argument
fn.
The reason that both collect$ and always$ are pre-defined is
that they are part of the support for the loop$ statment.
Lesson 6: You can run scions on warranted function symbols:
ACL2 !>(my-collect$ 'SQ '(1 -2 3 -4))
(1 4 9 16)
ACL2 !>(my-collect$ 'rev '((1 2 3) (4 5 6) (7 8 9)))
((3 2 1) (6 5 4) (9 8 7))
You might wonder why you can run my-collect$ on 'SQ — which
evaluates apply$ on 'SQ — without explicitly acknowledging
the warrant that links (apply$ 'SQ (list a)) to (sq a). The reason
is that evaluation in ACL2's top-level read-eval-print loop assumes all
existing warrants are provided. Warrants only become important when we start
dealing with proofs.
Lesson 7: You can run scions on tame quoted LAMBDA objects.
These LAMBDA objects can even include calls of scions, provided
they are tame.
ACL2 !>(my-collect$
(lambda$ (x) (CONS 'SQUARES (MY-COLLECT$ 'SQ x)))
'((1 2 3) (4 5 6)))
((SQUARES 1 4 9) (SQUARES 16 25 36))
Note that the ``function symbols'' in the ``body'' of a quoted LAMBDA
object may reach apply$ as the LAMBDA object is applied.
LAMBDA objects are just quoted list expressions that start with the
symbol LAMBDA and look like lambda-expressions. But quoted LAMBDA
objects have to have fully translated bodies and meet other restrictions so
apply$ can interpret them. You cannot use macros like + or
cond and must you quote all constants. We urge you not to try to type
quoted LAMBDA objects by hand! Instead, we provide a macro, lambda$, that allows you to write lambda expressions in untranslated
form.
Lesson 8: There are three very similar looking but very different
notions used in this documentation: lambda expressions, LAMBDA objects,
and lambda$ expressions. Read carefully! See lambda for some
definitions and disambiguation help. The LAMBDA objects reaching
apply$ must be fully translated (and tame) to be handled correctly. The
special macro lambda$ will translate for you.
; Don't type quoted LAMBDA objects like this!
ACL2 !>(my-collect$ '(LAMBDA (x)
(IF (< x '0) (BINARY-* '10 x) (SQ x)))
'(1 -2 3 -4))
(1 -20 9 -40)
; Type this instead!
ACL2 !>(my-collect$ (lambda$ (x)
(if (< x 0) (* 10 x) (sq x)))
'(1 -2 3 -4))
(1 -20 9 -40)
Lesson 9: Almost all ACL2 primitives are known to apply$. For
a complete list of the built-ins evaluate
(append '(BADGE TAMEP TAMEP-FUNCTIONP SUITABLY-TAMEP-LISTP
APPLY$ EV$)
(strip-cars *badge-prim-falist*))
You can freely use these ACL2 primitives with apply$ and in your
lambda$ expressions, without warrants.
Lesson 10: You can prove and use theorems about scions.
ACL2 !>(defthm my-collect$-append
(equal (my-collect$ fn (append a b))
(append (my-collect$ fn a)
(my-collect$ fn b))))
ACL2 !>(thm (equal (my-collect$ (lambda$ (x) (* x x))
(append c d))
(append (my-collect$ (lambda$ (x) (* x x)) c)
(my-collect$ (lambda$ (x) (* x x)) d))))
Notice that the lemma my-collect$-append talks about an arbitrary
fn. The definition of apply$ is completely irrelevant to this
theorem! Once my-collect$-append has been proved can be instantiated
with anything for fn. This is demonstrated when the thm above is
proved: the proof is just to rewrite with my-collect$-append. Notice
that the only function being apply$'d in the thm above is the
primitive multiplication function, which is built into apply$.
Lesson 11: But when your theorems depend on the behavior of
apply$ on particular user-defined functions, you will need to provide
hypotheses stipulating the behavior of apply$ on those values. Those
hypotheses are the warrants for the (non-primitive) function symbols
involved. Here is an example: Recall the function sq defined and
warranted above. We might wish to prove that if lst is a list of
integers then (my-collect$ 'SQ lst) is a list of natural numbers. We
can use always$ to express the notions of ``list of integers'' and
``list of naturals.'' We could try to state the conjecture this way:
ACL2 !>(thm (implies (always$ 'INTEGERP lst)
(always$ 'NATP (my-collect$ 'SQ lst)))).
But the attempt to prove that formula will fail because it depends on the
fact that the sq of an integer is a natural and on the assumption
that (apply$ 'SQ (list x)) is (sq x). That assumption
is what the warrant for sq tells us. Thus, the warrant for
sq is required as a hypothesis! The following theorem can be
proved.
ACL2 !>(defthm all-natp-collect$-sq
(implies (and (warrant sq)
(always$ 'INTEGERP lst))
(always$ 'NATP (collect$ 'SQ lst))))
Note that we don't need to provide warrants for integerp or natp
because they are ACL2 primitives and thus built into the behavior of
apply$. But we must provide the warrant for sq because we know the
proof depends on (apply$ 'sq (list x1 ...)) simplifying to (sq
x1).
The macro form (warrant f1 ... fk) expands to the conjunction of the
warrants for the fis. That is
(warrant f1 ... fk)
=
(and (apply$-warrant-f1)
...
(apply$-warrant-fk)).
If you attempt a proof and it fails, and you see among the checkpoints
terms of the form (apply$ 'fn (list a1 ... an)), then you probably
forgot to call defwarrant on fn and apply$ doesn't know what
to do with that symbol! If, on the other hand, you see a forcing-round checkpoint that is attempting to prove a warrant, like
(apply$-warrant-fn), then you probably forgot to add the warrant for
fn to the hypotheses of the conjecture you're trying to prove.
Lesson 12: Warrants solve the ``LOCAL problem.'' Imagine the
trouble we'd be in if the theorem above did not require a warrant on sq.
We could get away with this:
(encapsulate nil
(local (defun sq (x) (* x x)))
(defthm unwarranted-all-natp-collect$-sq
(implies (always$ 'INTEGERP lst)
(always$ 'NATP (collect$ 'SQ lst)))))
(defun sq (x) (* x x x))
(thm (implies (always$ 'INTEGERP lst)
(always$ 'NATP (collect$ 'SQ lst))))
This would be a disaster because the final thm is invalid since
(sq -2) here is -8 and yet the thm is trivially proved by
appealing to the unwarranted theorem exported from the encapsulate.
If we could prove the unwarranted theorem we could export it because it
does not mention or depend on the locally defined function sq, it just
mentions the constant symbol 'SQ. Fortunately, we cannot actually
prove the unwarranted version of the theorem because there is no a
priori connection between (apply$ 'SQ (list x)) and (sq x).
And if we add the warrant for sq to the defthm in the encapsulate
we can prove the theorem but then we cannot export it because the warrant
ancestrally depends on locally defined function sq.
Lesson 13: While we may have given the impression that we've
provided a convenient fragment of second-order functionality in ACL2 its
limitations will annoy you! For example, when ACL2 tries to use the
lemma
(defthm all-natp-collect$-sq
(implies (and (warrant sq)
(always$ 'INTEGERP lst))
(always$ 'NATP (collect$ 'SQ lst))))
it just employs its usual first-order matching algorithm. Thus, the lemma
won't apply to
(always$ 'NATP (collect$ (lambda$ (x) (* x x)) lst))
because the constant symbol 'SQ is not the same as the constant
list generated by translating lambda$ expression,
'(LAMBDA (X) (BINARY-* X X)), even though they are equivalent
if understood as functions. See the discussion at fn-equal.
Lesson 14: Recall Lesson 0! Before you start to use apply$
outside of this simple demo script, we advise you to read the documentation
for apply$.
An Advanced Lesson: We conclude this tutorial by defining one of
the most useful scions and proving a couple of theorems illustrating its
flexibility: foldr.
ACL2 !>(defun$ foldr (lst fn init)
(if (endp lst)
init
(apply$ fn
(list (car lst)
(foldr (cdr lst) fn init)))))
Note that foldr maps over the list in its first argument, applying
its second argument to two things: successive elements of the list and the
result of recursively calling itself on the rest of the list. It returns its
third argument when the list is empty.
When its functional argument is CONS foldr is just the
concatenation of its other two arguments:
ACL2 !>(defthm foldr-cons
(equal (foldr x 'CONS y)
(append x y)))
We do not need a warrant for cons because it is built into
apply$. In fact, the built-ins don't have warrants but if you
unnecessarily list a primitive in a warrant expression, like (warrant
foldr cons), it just ignores the primitives that are built into
apply$.
By supplying a certain lambda expression we can use foldr to
reverse its first argument:
ACL2 !>(defthm foldr-can-be-rev
(implies (warrant foldr)
(equal (foldr x
(lambda$ (x y)
(FOLDR y 'CONS (CONS x nil)))
nil)
(rev x))))
Note that the lambda$ expression calls FOLDR. Because of this,
we must provide the warrant for foldr since that inner foldr will
be applied by the outer foldr. This illustrates an important point made
in Lesson 7 above: scions can apply other scions, including themselves, as
long as the applications are tame.
Some Practice Problems
There is no better way to learn than to practice. So here are a few
challenge problems. The answers can be found in
books/projects/apply/answers-to-doc-intro-to-apply.lisp.
Problem 1: Assume fn is a binary relation. Define
(insert$ e lst fn) to insert e into the list lst in front of
the first element, d, in lst such that (fn e d) is true.
Problem 2: Define (sort$ lst fn) to be an insertion sort
algorithm for the binary relation fn, e.g., to successively insert each
element into the recursively sorted remaining elements. (Note: There is no
assurance that sort$ will actually produce a list ordered by fn
because we don't know that fn is an ordering relation.)
Problem 3: Study the four examples below, which illustrate perhaps
surprising properties of our ``insertion sort'' function. (If your
definitions don't have these properties you should back up and redefine your
functions as we vaguely described above!)
(defthm examples-of-sort$
(and (equal (sort$ '(1 3 -7 0 23) '<)
'(-7 0 1 3 23))
(equal (sort$ '(1 3 -7 0 23)
(lambda$ (x y) t))
'(1 3 -7 0 23))
(equal (sort$ '(1 3 -7 0 23)
(lambda$ (x y) nil))
'(23 0 -7 3 1))
(equal (sort$ '(1 a 2 x b 3 4 y c)
(lambda$ (x y) (symbolp x)))
'(a x b y c 4 3 2 1)))
:rule-classes nil)
Problem 4: Prove the following theorem suggested especially by the
last example above. To state this theorem we first introduce the familiar
reverse function, rev.
(defun rev (x)
(if (endp x)
nil
(append (rev (cdr x))
(list (car x)))))
and we use the pre-defined function (when$ fn lst) which computes the
elements of lst satisfying the unary-function fn, in the order in
which they occur, e.g., (when$ '(1 a 2 b) 'symbolp) is '(a b).
Prove
(defthm sort$-lambda-symbolp
(implies (true-listp lst)
(equal (sort$ lst (lambda$ (x y) (symbolp x)))
(append (when$ 'symbolp lst)
(rev
(when$
(lambda$ (x y) (not (symbolp x)))
lst))))))
Lemmas will be needed.
Problem 5: Define (orderedp$ lst fn) to check whether fn
holds between each adjacent pair of elements in lst. Test your function
with
(defthm examples-of-orderedp$
(and (orderedp$ '(1 3 5 7) '<)
(not (orderedp '(1 3 3 5 7) '<)))
:rule-classes nil)
Problem 6: You might hope that (orderedp$ (sort$ lst fn) fn)
is a theorem. But it is not as is easily shown by the example
(orderedp$ (sort$ '(3 1 5 3 7) '<) '<). If you try to prove the
conjecture and inspect the output you'll see that the proof fails because we
do not know that (or (fn x y) (fn y x)) is true. That is, we don't know
that fn is Strongly Connected. How could we, since the
conjecture is claimed for all fn?
Unfortunately, it is awkward to state that fn is a strongly connected
relation in ACL2's first-order quantifier-free language. This is a good
example of the limitations of ACL2's support for second-order functions!
But we can prove versions of the conjecture for concrete strongly
connected fns. The relation named before-dayp, below, is strongly
connected, as demonstrated by the events following its definition.
Carry out these events.
(defun beforep (x y lst)
(if (and (member x lst)
(member y lst))
(member y (member x lst))
t))
(defun before-dayp (x y)
(beforep x y '(mon tue wed thu fri sat sun)))
(defthm before-dayp-strongly-connected
(implies (not (before-dayp x y))
(before-dayp y x)))
(in-theory (disable before-dayp))
Now, prove the version of (orderedp$ (sort$ lst fn) fn) for the
instance in which fn is 'before-dayp.
