# Inductive proofs in logical frameworks and logic programming

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.

## Introduction

Logical Frameworks (LF) and Logic Programming both regard logical formulas as programs and proof search as computation. The Twelf implementation of LF is built on top of a logic programming system. LF and logic programming can both be used to conduct inductive proofs. The styles of these proofs are different however. The inductive proof in Twelf is expressed constructively, as a computation that produces a proof object. Meta-theoretic reasoning is required to verify that the computation is total -- covering all the cases and terminating. Inductive proofs in a logic program are expressed declaratively and rely on the built-in proof search. Termination checking is not needed. Inductive proofs critically rely on hypothetical reasoning, solving goals under local assumptions. Formulas containing implication are not Horn-clause goals, and so out of scope for a pure, Horn-clause--based logic programming system. Prolog and Kanren do have (their own) facilities to solve goals under local assumptions. We describe and contrast these mechanisms.

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 Show
```
and 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:
Theorem

`mirror . mirror == id`
or: `mirror` is its own inverse.

## The mirror involution proof in Twelf

Twelf is an implementation of LF. It is particularly suitable for proving forall-exists formulas, of the form
```     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.

Version
The current version is 1.2, February 2010.
References
mirror.elf [3K]
Commented Twelf code

## ENKITEI-Prolog: Interactive proof system for natural deduction with inductive definitions

We introduce the interactive proof system Enkitei-Prolog that extends classical natural deduction (NK) with definitions, including inductive definitions. For the latter, the system can derive an induction principle and apply it. We illustrate Enkitei on the proof of the mirror involution theorem. The Enkitei proof differs from Twelf's proof in handling of definitions, in operating on judgements with explicit assumptions, and in being interactive. Enkitei builds a natural deduction derivation, using both intensional and extensional approaches to proving universally quantified formulas. Enkitei handles any first-order formulas, not limited to forall-exists ones.

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:

• incorporating definitions into NK;
• integrating the global environment -- Prolog's database of facts and clauses -- with local assumptions of a judgement;
• choosing the `right' eigen-variables;
• recognizing inductive definitions and introducing inductive hypotheses.

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
```
Version
The current version is 1.1, February 2010.
References
enkitei.prl [27K]
Extensively commented complete Prolog code, with explanations, tests and examples. It has been tested under SWI-Prolog, version 5.8.3.

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

## Eigen-variables: variables or constants?

In sequent and natural deduction calculi, to prove a universally quantified formula `forall X. g` we introduce a fresh constant `c` (which has not been used in the proof before) and attempt to prove the formula `g` with `X` replaced with `c`. Such a fresh constant is called ``eigen-variable.''

Most texts on deduction calculi (such as the ``Automated reasoning'' entry in the Stanford Encyclopedia of Philosophy) say nothing more about eigen-variables, leaving the reader to puzzle over the question why the name eigen-variable was chosen for constants.

The LICS2003 paper by Miller and Tiu is a rare text that describes the use of eigen-variables as variables, that is, to mark the place for substitution. Miller and Tiu point out that although Gentzen never substituted for eigen-variables when constructing proofs (so, eigen-variables were indeed constants), Gentzen did substitute for eigen-variables in meta-theory, when transforming proofs, e.g., to eliminate cuts. Miller and Tiu discuss extended sequent calculi that do treat eigen-variables as variables, and propose a sequent calculus that harmonizes the constant--variable treatment of eigen-variables.

In this article, we illustrate the constant--variable duality of eigen-variables on a simple example. We use classical natural deduction (NK) with equality rather than intuitionistic sequent calculus. Crucially however, our calculus, like that of Miller and Tiu, supports definitions. It is in the applications of definitions where the variable aspect of eigen-variables emerges. To be sure, we can treat eigen-variables ``classically'', as constants during the proof construction, all the time. In fact, we start with such a classical derivation. We then show the abbreviation of thus constructed proof, eliminating the use of equality and injectivity axioms. We replace the axioms with an inference rule that may treat eigen-variables as variables, substituting for them when applying definitions to hypotheses. The new inference rule is particularly easy to apply using unification. The simplified calculus underlies the Prolog implementation of Enkitei, a natural deduction proof system with equality and definitions.

We are interested in classical natural deduction proofs, that is, in finding a derivation for a judgement

```     hs |- g
```
where `g` is a formula and `hs` is a possibly empty set of formulas (assumptions). Formula `g` is an arbitrary first-order formula; `&` will stand for conjunction and `|` for disjunction.

Let us enter the following definitions:

```     nat(0).
nat(X) :- pos(X).
pos(s(X)) :- nat(X).
```
where `0` and `s` are function symbols (of arity zero and one, respectively), and `nat` and `pos` are predicate letters of arity one. `X` is a schematic variable. (The definitions are in fact inductive; however, we won't be concerned with induction here).

We may regard the definitions as axioms

```     forall U. nat(U) <-> U = 0 | pos(U)
forall U. pos(U) <-> exists V. U = s(V) & nat(V)
```
We shall also assume the following axioms of equality for terms (injectivity)
```     forall X Y. s(X) = s(Y) -> X = Y
forall X. not (s(X) = 0)
```
along with the standard introduction and elimination rules for equality:
equality introduction: for any term `t1`
```     [] |- t1 = t1
```
equality elimination: for any terms `t1`, `t2` and a formula `g`, the judgments
```     [] |- t1 = t2
[] |- g
```
let us derive `[] |- g{t1/t2}` where `g{t1/t2}` is `g` with every occurrence of `t1` replaced with `t2`.

Our running example will be proving the theorem `forall X. nat(s(X)) -> pos(s(X))` using the definitions of `nat` and `pos` shown earlier. We first demonstrate a ``classical'' derivation, using only the standard (and hence, boring) steps and indeed regarding the definitions as (domain) axioms. Thereby we demonstrate that we are not doing anything fishy; mainly, we will get an idea for short-cutting the most tedious steps.

Our goal is to derive the judgement

```     [] |- forall X. nat(s(X)) -> pos(s(X))
```
By appealing to the forall-introduction rule of NK we convert our goal to
```     [] |- nat(s(c)) -> pos(s(c))
```
where `c` is a fresh constant, the function symbol of arity 0 -- the eigen-variable. After the implication introduction rule of NK, the goal judgement becomes
```     nat(s(c)) |- pos(s(c))
```
The axiom for `pos` (after instantiating `U` with `s(c)`) lets us conclude
```     exists V. s(c) = s(V) & nat(V) |- pos(s(c))
```
We could then prove our goal judgment by the cut rule if we could prove
```     nat(s(c)) |- exists V. s(c) = s(V) & nat(V).
```

Let us indeed prove the latter judgment. We instantiate `V` to be `c`, converting the goal to

```     nat(s(c)) |- s(c) = s(c) & nat(c)
```
The formula `s(c)=s(c)` holds by reflection, and we only need to prove
```     nat(s(c)) |- nat(c)
```
We may try the `nat` axiom in the way we have just used the `pos` axiom, to re-write the conclusion of the judgement. It is easy to see that it won't do us any good. We have to re-write the assumption of the judgement.

The `nat` axiom after instantiating `U` with `s(c)` lets us conclude

```     nat(s(c)) |- s(c) = 0 | pos(s(c))
```
If we could only prove
```     (s(c) = 0 | pos(s(c))) |- nat(c)
```
we would derive the desired judgement, again by applying cut. We hence need to prove two judgements:
```     s(c) = 0  |- nat(c)
pos(s(c)) |- nat(c)
```
We get the first by contradiction (from the axiom `not(s(c)=0))`. For the latter, we apply the axiom `pos` to the assumption (as we have applied `nat` just before), giving us this judgement to prove:
```     exists V. s(c) = s(V) & nat(V) |- nat(c)
```
or, after the existential elimination:
```     s(c) = s(d) & nat(d) |- nat(c)
```
where `d` is another eigen-variable. Applying the injectivity gives us
```     c = d & nat(d) |- nat(c)
```
which is derivable by the equality elimination rule. We are done.

That was messy, wasn't it? Let us attempt to generalize and simplify the derivation steps. Suppose we have the following definition

```     p(0).
p(X) :- q(X).
```
where `p` and `q` are some predicates. We can write the definition in the form of an axiom
```     forall U. p(U) <-> U = 0 | q(U)
```
Suppose we wish to prove the judgement `hs |- p(c)` (where `c` is a constant; it could have been any term). If we follow the boring steps above we convert the judgement to
```     hs |- (c = 0 | q(c)).
```
and then elect to continue the proof search with `hs |- q(c)`. We could obtained the latter judgement directly, if we unified `p(c)` with the head of the `p` definition in its original clausal form. There is no surprise here: the `direct' step is mere resolution. We stress that in this step, `c` is treated as a constant, not subject to substitutions.

Let us take a different judgement: `hs, p(c) |- g` where `g` is some formula. The boring steps of using the definition of `p` in its axiomatic form gives us two new judgements to prove

```     c=0  |- g
q(c) |- g
```
The first judgement after the equality elimination rule becomes `[] |- g{c/0}`. Again, we could have obtained the two judgements in one step, if we unified `p(c)` against the two clauses of `p`'s original definition. If more than one clause unify, we obtain more than one judgement to prove. If none unify, we obtain the proof by contradiction. Crucially, during this step, `c` is being treated as a variable. It is now subject to substitution.

To summarize: when applying a definition to the conclusion of a judgement, we treat an eigen-variable as a constant during unification. When applying a definition to an assumption of a judgement, we treat eigen-variables as variables, subject to unification and substitution.

The new rules of applying definitions let us drop the axioms of equality. In other words, equality becomes definable:

```     eq(X,X).
```
We can prove, for example, that our defined equality is transitive. The goal
```     [] |- forall X Y Z. (eq(X,Y) & eq(Y,Z)) -> eq(X,Z)
```
after a series of introductions becomes
```     eq(c,d), eq(d,e) |- eq(c,e)
```
where `c`, `d`, and `e` are eigen-variables. We apply the definition of `eq` to the assumption, identifying eigen-variables `c` and `d` and obtaining
```     eq(c,e) |- eq(c,e)
```
which is the axiom. The Prolog Enkitei code have many more examples of applying definitions.

Classically, eigen-variables are constants, not to be substituted for during the proof construction. However, the equality elimination rule does permit replacement of arbitrary terms, which are not necessarily variables. This fact lets us design an alternative to equality axioms, relying on unification and treating eigen-variables as regular variables when operating on assumptions of a judgement. The alternative inference rule is especially useful when applying definitions.

References

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.

### Last updated June 7, 2010

This site's top page is http://okmij.org/ftp/

oleg-at-okmij.org