Trivializing the Proof of Trivial Theorems

TRIVIALIZING THE PROOF OF TRIVIAL THEOREMS

Y. Kodratoff and J. Castaing

LRI, Bat. 490 - Universite de Paris-Sud -F. 91405 ORSAY CEDEX

ABSTRACT

Besides a definition of "trivial" theorem, this paper presents a sketch of our methodology for the generalization of recurrence proofs on "trivial" theorems but that lead, in a context of automatic theorem proving, to very length y (or even impossible to achieve) proofs.

This paper reduces to a description of a detailed example, we hope to make clear that our methodolo­

gy is of a much wider field of application.

I INTRODUCTION

In the field of theorem proving by induction, the need for an efficient generalization system has been expressed several times [2,3,5]. The methodo­ logy presented here differs from the one already used in existing systems [2,4]by two main features. First, our heuristics are driven by example proofs run on particular values of the variables (in this, we follow [6,7]. Second, instead of a progressive generalization expected to eventually reach a state where the theorem is provable, we go the otherway round: we "savagely" generalize the theorem into an expression which is (in general) FALSE, and use a progressive particularization expected to eventual­ ly reach a state where the theorem is TRUE (and provable). This coincidence of truth and provabili­ ty of a progressively particularized expression is implicitly part of our definition of "triviality".

II OUR DEFINITION OF A TRIVIAL THEOREM

II. I Sketch of our methodology

We suppose that we are ~n an environmen t of recursive definitions as in [I] (Burstall 69) and that we have at our disposal a well-founded orde­ ring. Let t(x) be a theorem to be proven by induc­ tion on x. Let s(x) be the successor of x in the well-founded ordering. An induction proof contains two steps. The first one is the basis case (which we consider here as already proven). The second tries to prove that t(x) implies t(s(x)). Let R be the set of rules we have at our disposal (section 3), and let tc(x)=R t(s(x)) be the expression one obtains after having applied R to t(s(x)). Definition: We say that t(x) r-matches tc(x) iff

1- there exists a substitution a such that Oo t(x)=tc(x) 2- oox is less than or equal to x in the well-foun­ ded ordering. Remark: This definition implies that the substitu­ tion x+s(x) is a failure of the r-matching.

It is clear that the r-matching of t(x) to­ wards tc(x) proves that the implication t(x)+t(s(x)) is valid in the theory. If the r-matching of t towards tc fails, we analyse the conditions at which it could succeed. These conditions are considered ag recursively generated new theorems to be proven by the same methodology.

II.2 Definition of "trivial"

The theorems we are able to prove are trivial in the following sense:

a- If the proposition to be proven is FALSE, it must "quickly" evaluate to FALSE for the first par­ ticular values of its variables. In the list domain these values are NIL, (CONS A NIL), (CONS B (CONS

A NIL)), ... where A, Bare atoms. b- When the matching of t towards tc fails then it often happens that the conditions which expresshow to avoid this failure are a system of equations (of the diophantine type) among a set of new varia­ bles. "Trivial" means also here that this system is "easy" to solve. The words quoted above, i.e, "quickly" and "easy" can have different definitions. In our system, we have chosen the following: "quickly" is "at once" (an untrue expression must evaluate to FALSE for the first element of thewe~ founded ordering) and "easy" means that only equa­ lity relationships linking the variables directly are allowed. Notice that even with that ground de­ finition of trivial, we are able to prove (trivial) theorems the proof of which is very difficult.

III THE REWRITING SYSTEM

The functions we are to uGe are given below under a case representation (Burstall 69). (EQL x y ) type : boolean (EQL NIL NIL ) = TRUE (EQL (CONS A x) NIL) = FALSE (EQL NIL (CONS A y)) = FALSE (EQL (CONS Ax) (CONS By)) (AND (EQN A B ) (EQL x y)) (AND x y ) type : boolean (AND TRUE y) = y (AND FALSE y) = FALSE (APP x y) type : list (APP NIL y) =y (APP (CONS Ax) y) = (CONS A (APP x y)) (REV x) type : list (REV NIL) = NIL (REV (CONS Ax)) = (APP (REV x) (CONS A NIL))

(FOO x y) type : list (FOO NIL y) = y (FOO (CONS A x)y) = (FOO x (CONS A y)) (EQN x y) type : boolean (EQN ZERO ZERO) = TRUE (EQN (SUCC x) ZERO) = FALSE (EQN ZERO (SUCC y)) =FALSE (EQN (SUCC x) (SUCC y)) = (EQN x y)

IV DESCRIPTION OF OUR METHODOLOGY

It consists of four steps, the first two of which will be exemplified by the proof of: t= (EQL (APP (rtEV x) (1'00 x tHL))

(FOO (APP x x) NIL)).

Assuming that the basis case has been proven, a recurrence proof of t consists of an induction step done by the substitution x+(CONS A x) and the rewritings of section III. This leads to: tc= (EQL (APP (APP (REV x) (CONS A NIL)) (FOO x (CONS A NIL))) (FOO (APP x (CONS A x)) (CONS A NIL)))

and the proof of tc under the hypothesis that t is TRUE is not at all trivial.

IV.I Step one

We "savagely" generalize the variables of t, giving a different name to all of them. The obtai­ ned expression, named Tl, is generally wrong. We particularize Tl so that it will eventually take the form tl which evaluates to TRUE (for the first values of its variables). As in section II.I, we compute tel and if there exists a substitution a: ao tl = tel, the problem is solved. Otherwise, we have to use step 2.

Example: The theorem t given above is savagely generalized to:

Tl= (EQL (APP (REV xl) (FOO x2 NIL))

(FOO(APP x3 x4) NIL)).

Let xil, Js is4, be an atom, we give to each varia­ ble xi the value (CONS xil NIL) and look for the conditions on the xil ins~ring that Tl takes the value TRUE. The expression of TI((CONS xi! NIL)) is equal to:

(EQL (APP (REV (CONS xll NIL)) (FOO (CONS X2f NIL) NIL)) (FOO (APP (CONS x31 NIL) (CONS x41 NIL)) NIL)). -

A call - by - name evaluation of the definitions given in section 3 leads to evaluate first the underlined fnnctional symbols, so that

Tl ((CONS xil NIL)) becorues

• (EQL (APP (APP (REV NIL) (CONS xll NIL)) (FOO (CONS x21 NIL)lNIL)) (FOO (CONS x31 (APP NIL (CONS x41 NIL))) NIL)).
• (EQL (APP(APP NIL (CONS xll NIL)) (FOO (CONS xrr-NIL) NIL)) (FOO (APP NIL (CONS x41 NIL)) (CONS x31 NIL))).
• (EQL (APP (CONS xll NIL) (FOO(CONS x21 NIL) NIL)) (FOO (CONS x41 NIL) (CONS x31 NIL))).
• (EQL (CONS xll (APP NIL (FOO (CONS x21 NIL) NIL))) (FOO NIL (CONS x41 (CONS x31 NIL)))).
• (EQL (CONS xll (APP NIL (FOO (CONS x21 NIL) NIL))) - (CONS x41 (CONS x31 NIL))).

-(AND (EQN xll x41) (EQL (APP NIL (FOO (CONS x21 NIL) NIL)) (CONS x31 NIL))).

The evaluation stops at this point since xi! and x41 are variables and we cannot evaluate (EQN x II x41). We therefore state that (EQN x II x41) is a condition for Tl ((CONS xi! NIL)) evaluating to TRUE. We replace (EQN xll x41) by TRUE and the evaluation proceeds on (and is left to the reader) up to the result:

-(AND (EQN x21 x31 (EQL NIL NIL)).

In the same way as above, we must have (EQN x21 x31) .From these conditions, we deduce that xi= x4 x2 = x3 which are put in Tl in order to obtain tl: tl= (EQL (APP (REV y) (FOO z NIL))

(FOO (APP z y) NIL)).

We leave to the reader to verify that tl cannot be trivially proven by induction on y (or z). We the­ refore proceed on to step 2.

IV.2 Step two:Obtaining new theorems.

Broadly speaking, we apply again the same strategy which is too much generalizing and then finding for particular values of the variables the conditions which bring the generalization to TRUE. In this step the generalization is made according to the following heuristics: the matching of tl to­ wards tel fails, and we mark the terms in tl that do not contain the recurrence variable and fail to match with tel. Each marked term is generalized to a different variable vl, ... vi and tl takes the form T2. In T2, we give particular values to the varia­ bles different from the vi's, and find conditions on the vi's so that these particular expressions evaluate to TRUE (as in step 1). Our triviality condition "insures" that the system of equations linking the vi's is easy to solve. The solution is put into T2 which becomes t2. If t2 does not match tc2, we recursively apply step 2 to t2 (obtaining t3 ... ). This step stops in two cases: either the theorem is proven or the failure of the matching is the same inti and ti+l. In the last case we proceed on to step 3.

Example: Choosing z as the inductive variable, so that z is replaced by (CONS A z) into tl tl= (EQL (APP (REV y) (FOO z NIL)) (FOO (APP z y) NIL)), we obtain tel= (EQL (APP (REV y) (FOO z (CONS A NIL)))

(FOO (APP z y) (CONS A NIL))) .

The r-matching of tl and tel fails because it would lead to the substitution NIL +(CONS A NIL), which is forbidden since the left part of a substitution must be a variable. As above explained, we replace the two occurences of NIL by two different varia­ bles vi and v2. We have

T2= (EQL (APP (REV y) (FOO z vi)) (FOO (APP z y)v2)) Giving to y and z the value NIL we obtain (as in step I) the condition (EQL vi v2) which is put into T2 in order to give t2:

t2= (EQL (APP (REV y) (FOO z u)) (FOO (APP z y) u)). The reader will find that inducting on z (which is replaced by (CONS A z) in t2), one obtains tc2 such that there exists a substitution a such that

aot2 = tc2, a= u+(CONS A u). This proves the induc­ tion step for t2, because u is not the induction variable. We assume here that the basis case has already been proven, so this ends the proof of t.

IV.3 Step three: Inducting lemmata from a partial matching.

We suppose that step I and step 2 failed and we must now prove the theorem t' obtained after applying step I and step 2. We restrict ourselves to the cases where the property to be proven about t' is not a unary operator. An instance of this operator is EQL of arity 2, when t' is con­ cerned with list equality. Lett' = (P Sl(x) Sn(x)) where xis the induction variable, and t'c = (P Scl(x) ... Scn(x)) such that t' does not match t'c. Let us suppose that one subterm Si(x) matches Sci(x) : there exists a substitution a such that ao Si (x) = Sci(x) and aox:O:x. It is evident that t'= (P 51 (x) ... Sn(x)) matches t" = (PaoSI(x) ... a oSn(x)). It follows that if we are able to prove the n-1 lemmata: a oSI(x) = Scl(x), ... a oSn(x) = Scn(x), we will have proven t'. This is really a heuristic since nothing proves that then lemmata are easy ones. Our simple remark is that this is the last hint one can find and is therefore worth trying.

IV.4 Step four: Inducting lemmata from a par­ ticular values of the induction variable.

We suppose that step 3 fails because no Si(x) matches an Sci(x). Let s(O) <s(s(O))< ... be the successive canonical forms of the well founded ordering. We write: (P 51(0), ... Sn(O)), (P Sl(s(O)) ... Sn(s(O))), ... and evaluate all the Si's with our rewriting rules. We attempt to match the evaluated Si(O) .nd Si(s(O)) (as we have already seen O+s(O) is excluded as a matching failure). If this succeeds for one i, a substitution a is found and used as in step 3.

V. CONCLUSION

Our main goal has not been to give a syntac­ tical characterization of the class of theorems we are able to prove in that way. Notice never­ theless, that improving our possibility to solve systems of equations and to detect our constant substitutions will extend the class of trivial theorems as defined here.