This document describes a toy example of how ACL2’s “constrained functions” feature can be used to verify some higher-order statements, despite ACL2 being a first-order theorem prover.
Suppose we have a function called
Let
$f$ be a function that satisfies the following three properties:
- The empty list is unchanged by
$f$ .- A single-element list is unchanged by
$f$ .- Appending two lists and passing the result through
$f$ is equivalent to passing each of the two lists through$f$ first and then appending them in the opposite order.Then
$f$ is identically equal to the$reverse$ function on all input lists.
How can this proposition be proved (or disproved)?
In a higher-order theorem prover like Coq, Agda, Idris, Isabelle/HOL,
HOL4, etc., one might state something like “for all
However, in ACL2, functions are not terms in the logic, and so we
cannot have propositions parametrized over functions in this way. But
we do have a handy mechanism called encapsulate which allows us to
“fake it” to some extent.
Let’s begin. First, let’s define our basic
(defun app (x y)
(if (atom x)
y
(cons (car x) (app (cdr x) y))))
(defun rev (x)
(if (atom x)
nil
(app (rev (cdr x)) (list (car x)))))If functions are not terms in the logic, what exactly does submitting
a defun form mean? It introduces a new axiom into the logic, which
equates applications of the function name to its arguments on the left
hand side, to the expanded body on the right hand side. So the above
defun forms introduced the following axioms into the logic:
(equal (app x y)
(if (atom x) y (cons (car x) (app (cdr x) y))))
(equal (rev x)
(if (atom x) nil (app (rev (cdr x)) (list (car x)))))This is one way to introduce information about a function into the
logic. Another way, of course, is to prove theorems about the
function. For example, I might prove that if x is an atom, then
(rev x) is nil:
(defthm dumb-theorem
(implies (atom x)
(equal (rev x) nil))Once ACL2 is satisfied that the statement is derivable from the current axioms, it adds it as a new axiom.
A perhaps unsurprising fact about ACL2 is that in order to prove theorems about a function, you must first have defined the function. After all, you can’t pass the function in as a parameter to the theorem you’re trying to prove, because ACL2 is a first order theorem prover, as mentioned above.
But if you think about a function definition merely as a way to
introduce an axiom about the function’s name, one might wonder why we
couldn’t introduce (implies (atom x) (equal (rev x) nil)) into the
logic without having to introduce (equal (rev x) ...) first.
What encapsulate allows us to do is exactly that… sort of.
Basically it lets us create an environment in which rev is defined
and some theorems are proved about it, but then the definitional axiom
of rev is removed when exiting the environment, with the other
theorems about rev remaining. At this point, rev has become a
constrained function.
(Note: Why is it OK to simply remove an axiom from the logic? Well, we certainly won’t introduce any inconsistency by doing so, so why not?)
So what’s the point of doing this? Well, think back to the statement
we wanted to formalize. “Let encapsulate form, we will essentially have three pieces of
information and no more, just as in the original English formulation
– and we have done so without appealing to quantification over
functions in the logic.
(Isabelle users might gain some intuition for what is going on here by
thinking about the difference between
We begin the encapsulate form, as follows:
(encapsulate
(((f *) => *))Here we have declared that we are going to define a constrained
function called f, which will accept one argument and return one
result (in ACL2, functions can of course take multiple arguments, but
they can also “return multiple results” in some cases, so this is
important to specify).
Normally it’s not important to declare this kind of stuff before
defining a function, but as the definitional axiom is going to be
rescinded later, the system needs to at least retain knowledge of what
ways of applying the function are valid. For example, it needs to be
able to cry foul if we later say something involving, say, (f x y).
We define our function f as follows.
(local
(defun f (x)
(rev x)))The local wrapper indicates that the axiom introduced by this
defun will be rescinded once we exit the encapsulate.
Why define f as equal to rev? Remember that f is supposed to
represent an arbitrary function that satisfies three properties. But
in order to add that knowledge to the logic, we need to provide a
particular f as a witness that it is even possible to satisfy those
three properties. Thankfully, rev does satisfy the three properties
(as we would expect!).
This is a disadvantage of our approach – as we encode our properties
of f as axioms in the logic, they had better be satisfiable,
otherwise we’re making the logic inconsistent. In a higher-order
logic, we could easily prove a vacuous theorem like “if 3 is an even
number then 5 = 7” without introducing inconsistency into the logic
itself, as the contradiction is contained within the hypotheses of a
particular proposition.
Now that we’ve defined our witness f, namely rev, we proceed to
show that f satisfies the three properties we desire:
(local
(defthm true-listp-rev
(true-listp (rev x))))
(local
(defthm app-nil
(implies (true-listp x)
(equal (app x nil) x))))
(defthm f-0
(equal (f nil)
nil))
(defthm f-1
(equal (f (list x))
(list x)))
(defthm f-app
(implies (and (true-listp x)
(true-listp y))
(equal (app (f x) (f y))
(f (app y x)))))Note that we needed a couple small lemmas first, in order to show that
rev indeed satisfied the three properties. Since they don’t involve
f, it doesn’t really matter whether we put them in a local wrapper
or not (in the sense that it won’t affect what we remember about f
after leaving the encapsulate), but we won’t need them again so we
might as well make them local here.
At this point we know four things about f (by which I mean the logic
contains four axioms involving f):
(equal (f x) (rev x))
(equal (f nil) nil)
(equal (f (list x)) (list x))
(implies (and (true-listp x) (true-listp y))
(equal (app (f x) (f y)) (f (app x y))))Now we close the encapsulate…
)… and only the latter three axioms remain.
Now, can we prove the statement we were originally considering? Are
those three properties sufficient for us to determine that f is
identical to rev, at least when considering lists as input?
We can answer this question by attempting to re-prove the axiom we
lost, (equal (f x) (rev x)), from the axioms we have remaining.
Here’s how I did it:
(defthm f-cons
(implies (true-listp y)
(equal (f (cons x y))
(app (f y) (list x))))
:hints (("Goal"
:use (:instance f-app
(x y)
(y (list x))))))
(defthm f-rev-equivalent
(implies (true-listp x)
(equal (f x)
(rev x))))(Note that I had to add the hypothesis (true-listp x), otherwise the
statement isn’t quite true – one could imagine a function f that
acted like rev when the input was a true list, but returned the
string “fnord” on any other input, for example. ACL2 is an untyped
logic, folks!)