On a simple example, we contrast the style of inductive proofs conducted in logical frameworks, logic and functional logic programs. We highlight hypothetical reasoning in logic programming, solving goals under local assumptions. Hypothetical reasoning in Prolog requires building a meta-circular interpreter, using Prolog's meta-call mechanism.
Our running example is a simple inductive proof that the mirror operation on binary trees is involution, that is, is its own inverse. Formally (in Haskell notation, which is quite close to the mathematical one), we define the inductive datatype of binary trees
data Btree a = Leaf a | Node (Btree a) (Btree a) deriving Showand the operation to produce the mirror image of the tree, by recursively exchanging left and right branches:
mirror :: Btree a -> Btree a
mirror (Leaf x) = Leaf x
mirror (Node t1 t2) = Node (mirror t2) (mirror t1)
Here is a sample btree and the result of applying the mirror operation to it, once and twice:
-- A sample btree
btree1 = Node
(Node (Leaf 0) (Leaf 1))
(Leaf 2)
btree1' = mirror btree1
-- Node (Leaf 2) (Node (Leaf 1) (Leaf 0))
btree1'' = mirror btree1'
-- The same as btree1
We see that applying mirror twice yields the original tree. That is the general result we wish to prove:
mirror . mirror == id
or: mirror is its own inverse.
forall X. exists Y. prop (X,Y).Many theorems can be stated in this way, for example, the theorem that there is an infinite number of primes:
forall X:prime. exists Y:prime. Y > X.A constructive proof of such a formula is a computational procedure that given any
X will produce, in finite time, Y so that prop(X,Y) holds. In the case of the infinitude of primes, such a procedure was proposed by Euclid.
To formulate the mirror involution theorem, we first define the type of binary trees with two constructors leaf and node.
btree: type.
leaf: nat -> btree.
node: btree -> btree -> btree.
We then define the mirror operation. It is written as a binary relation, relating a tree with its mirror image. The mode declaration however makes mirror a function: the first argument of the mirror relation is the input and the second argument is the output:
mirror: btree -> btree -> type.
%mode mirror +B1 -B2.
mr-l: mirror (leaf N) (leaf N).
mr-b: mirror (node B1 B2) (node B2' B1')
<- mirror B1 B1'
<- mirror B2 B2'.
%worlds () (mirror _ _).
%total {B1} (mirror B1 _).
The labels mr-l and mr-b name the two clauses of the mirror function. We also regard the labels as the two constructors of the proof object of the type mirror B1 B2, witnessing that B2 is the mirror image of B1. We assert that mirror is a total function on binary trees; Twelf agrees.
We now state the main theorem: mirror is its own inverse. The theorem is written as a forall-exists formula:
mirror-inv-thm: mirror B B' -> mirror B' B -> type.
%mode mirror-inv-thm +P1 -P2.
(The variables B and B' are implicitly universally quantified.) In full, the formula is
forall B:btree, B':btree, P1:mirror B B'. exists P2:mirror B' B. true.In words: for all binary trees
B and B' such that B' is the mirror image of B, there exists a proof that B is the mirror image of B'.
We write the constructive proof of that formula as a computational procedure that computes the proof of mirror B' B from the proof of mirror B B'. In other words, to prove the involution theorem stated as the type of mirror-inv-thm, we have to show how to construct the inhabitants of the type mirror-inv-thm:
-: mirror-inv-thm mr-l mr-l.
-: mirror-inv-thm (mr-b P1L P1R) (mr-b P2R P2L)
<- mirror-inv-thm P1L P2L
<- mirror-inv-thm P1R P2R.
%worlds () (mirror-inv-thm _ _).
%total {P1} (mirror-inv-thm P1 _).
Twelf type-checks the two clauses, verifying that the two cases, if terminate, do indeed produce the proof of mirror B' B from the proof of mirror B B'. To complete the proof, we assert on the last line that there are no other cases and that the computation always terminates. Twelf admits the totality assertion, thus verifying the proof. The overall proof appears so simple because the complex part -- verifying termination by structural induction -- is done by the meta-theoretical engine of Twelf.
Enkitei is an interactive system: it displays the current judgements and lets the user apply deduction steps by entering various tactics. A tactic can prove the current goal, produce a new one, or split the current goal into subgoals. The proof concludes when there are no more goals.
Although Enkitei is written in Prolog, it cannot use Prolog directly to prove judgements. After all, Enkitei deals with arbitrary first-order logic formulas, not restricted to Horn clauses. All in all, Enkitei had to solve the following problems:
The (very long) comments in the source code explain how all these problems have been solved. We extensively rely on Prolog's meta-call facilities. One may regard Enkitei as a greatly extended, stepping meta-circular Prolog interpreter. The code contains many tests and examples, including inductive proofs from Pierce's Software Foundations course.
The first example proves that zero is the right unit of addition. We define natural numbers and the addition relation, by consulting the following Prolog program.
nat(z).
nat(s(N)) :- nat(N).
plus(z,N,N).
plus(s(N),M,s(R)) :- plus(N,M,R).
Here is the transcript of the proof session. User's input is after the prompt Command >.
?- main( forall(N, nat(N) -> plus(N,z,N)) ).
eigenvars: []
================
forall(_G2202, (nat(_G2202)->plus(_G2202, z, _G2202)))
Command >intros. % apply introduction rules as far as possible.
nat(_G2238)
eigenvars: [_G2238]
================
plus(_G2238, z, _G2238)
Command >induction.
eigenvars: [z]
================
plus(z, z, z)
plus(_G2489, z, _G2489)
nat(_G2489)
eigenvars: [s(_G2489)]
================
plus(s(_G2489), z, s(_G2489))
Command >simpl. % ask Prolog to prove the goal in judgement 1. It succeeds.
plus(_G2489, z, _G2489)
nat(_G2489)
eigenvars: [s(_G2489)]
================
plus(s(_G2489), z, s(_G2489))
Command >constructor. % unfold the definition of plus in the goal.
plus(_G2489, z, _G2489)
nat(_G2489)
eigenvars: [s(_G2489)]
================
plus(_G2489, z, _G2489)
Command >assumption. % search for the goal among assumptions, so to prove it.
QED
To prove the mirror theorem, we enter the following Prolog program, defining binary trees, the mirror relation and the theorem.
btree(leaf(_)).
btree(node(X,Y)) :- btree(X), btree(Y).
mirror(leaf(X),leaf(X)).
mirror(node(X,Y),node(Y1,X1)) :- mirror(X,X1), mirror(Y,Y1).
% The theorem: mirror is involutive
thm(BT) :- mirror(BT,BT1), mirror(BT1,BT).
Here is the abbreviated transcript of the proof session.
?- main( forall(B, btree(B) -> thm(B)) ).
Command >intros.
btree(_G2236)
eigenvars: [_G2236]
================
thm(_G2236)
Command >induction.
eigenvars: [leaf(_G2557)]
================
thm(leaf(_G2557))
thm(_G2523)
thm(_G2528)
btree(_G2523)
btree(_G2528)
eigenvars: [node(_G2523, _G2528)]
================
thm(node(_G2523, _G2528))
Command >simpl. % ask Prolog to solve the first goal, proving the judgement.
Command >destruct. move(3). destruct. % unfold thm in assumptions.
mirror(_G2806, _G2807)
mirror(_G2807, _G2806)
mirror(_G2818, _G2819)
mirror(_G2819, _G2818)
btree(_G2818)
btree(_G2806)
eigenvars: [_G2807, _G2819, node(_G2818, _G2806)]
================
thm(node(_G2818, _G2806))
Command >constructor. intros. constructor. intros. % unfold thm.
mirror(_G2806, _G2807)
mirror(_G2807, _G2806)
mirror(_G2818, _G2819)
mirror(_G2819, _G2818)
btree(_G2818)
btree(_G2806)
eigenvars: [_G2807, _G2819, node(_G2818, _G2806)]
================
mirror(_G2818, _G3106)
mirror(_G2806, _G2807)
mirror(_G2807, _G2806)
mirror(_G2818, _G2819)
mirror(_G2819, _G2818)
btree(_G2818)
btree(_G2806)
eigenvars: [_G2807, _G2819, node(_G2818, _G2806)]
================
mirror(_G2806, _G3105)
mirror(_G2806, _G2807)
mirror(_G2807, _G2806)
mirror(_G2818, _G2819)
mirror(_G2819, _G2818)
btree(_G2818)
btree(_G2806)
eigenvars: [_G2807, _G2819, node(_G2818, _G2806)]
================
mirror(node(_G3105, _G3106), node(_G2818, _G2806))
Command >assumption. assumption. % prove the first two judgements.
mirror(e99, e96)
mirror(e96, e99)
mirror(e98, e97)
mirror(e97, e98)
btree(e98)
btree(e99)
eigenvars: [e96, e97, node(e98, e99)]
================
mirror(node(e96, e97), node(e98, e99))
Command >constructor. intros. assumption. assumption. % prove the rest.
QED
Benjamin C. Pierce et al. Software Foundations. Course Notes, 2009.
< http://www.seas.upenn.edu/~cis500/current/sf/html/ >
The Coq Team: Coq Reference Manual, v8.1
< http://coq.inria.fr/V8.1/refman/Reference-Manual002 >
Specifically:
Chapter 4: Calculus of Inductive Constructions
Chapter 8: Tactics
Frederic Portoraro: Automated Reasoning
The Stanford Encyclopedia of Philosophy (Winter 2008 Edition), Edward N. Zalta (ed.).
< http://plato.stanford.edu/archives/win2008/entries/reasoning-automated/ >
Dale Miller and Alwen Tiu: A proof theory for generic judgments. An extended abstract.
Proceedings of LICS 2003, Phokion Kolaitis, ed. Ottawa, July 2003, pp. 118-127.
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML