Tactical theorem proving

Logics can be defined in STELF in such a way that it may not be possible to do proof search by the fixed search strategy of STELF’s logic programming engine. In these cases, tactical theorem provers can be written that may still be able to prove many theorems. This article defines two approaches to writing these tactical theorem provers.

Logic definition

When we introduce numbers with addition on this wiki (see for example natural numbers), we usually define a judgmental definition of addition and then prove that it has the properties we desire. This will be a rather different presentation, more in line with the Zermelo Frankel case study. This is a signature for an object language (a logic) that has addition as a primitive operation.

We define a type for numbers num, and then make addition a primitive operation. We also define propositions; the only proposition we define here is equality of two numbers.

%sort num %.
%name num %.
%term + %pi num %-> num %-> num %.
%prec %left 10 + %.
%term 0 num %.
%term 1 num %.
%sort prop %.
%term == %pi num %-> num %-> prop %.
%prec %none 5 == %.

We can create a valid proposition that may be obviously untrue; for instance, (0 == 1) is a valid object of type prop. Therefore, we create pf, which is a particular little logic which will allow us to prove a large number of theorems about addition based on a small number of axioms. Eight axioms are defined below:

%sort pf {_ prop} %.
%term refl pf (N == N) %.
%term symm %pi (pf (N1 == N2)) %-> (pf (N2 == N1)) %.
%term trans %pi (pf (N1 == N2)) %-> (pf (N2 == N3)) %-> (pf (N1 == N3)) %.
%term plus_assoc pf (N1 + N2 + N3 == N1 + (N2 + N3)) %.
%term plus_comm pf (N1 + N2 == N2 + N1) %.
%term plus_zero pf (N1 + 0 == N1) %.
%term plus_cong %pi (pf (N1 == N1')) %-> (pf (N2 == N2')) %-> (pf (N1 + N2 == N1' + N2')) %.
%term plus_elim1 %pi (pf (N1 + N2 == N1 + N2')) %-> (pf (N2 == N2')) %.
%freeze pf %.

We freeze the type family pf to prevent any more axioms from being defined, but we can still define (many!) more theorems using the axioms (for instance, the complement to plus_elim1.

%define plus_elim2 (%pi (pf (N1 + N2 == N1' + N2)) %-> (pf (N1 == N1'))) [p1 pf (N1 + N2 == N1' + N2)] plus_elim1 (trans (trans plus_comm p1) plus_comm) %.

Tactical theorem proving

Motivation: “flattening” a numeric formula

Say we want to define a predicate mklist that takes some numeric formula num and applies associativity exhaustively to “flatten” the formula into a list, for instance transforming (a + (b + c) + d) into (a + b + c + d) - addition was defined to be left-associative, so this is the same as (((a + b) + c) + d).

The list type family below will do this when run as a logic program.

%sort list {_ num} {_ num} %.
%mode list %in %out %.
%term list-swap %pi (list (A + (B + C)) D) %<- (list (A + B + C) D) %.
%term list-step %pi (list (A + C) (B + C)) %<- (list A B) %.
%term list-stop list A A %.

Returning a proof of equality

The operation of list may seem a bit mysterious - how do we know that the straightened out formula is equal to the old one? By using STELF’s dependent types, we can define a new type family mklist which operates in the same way but returns a proof that the two numeric formulas are equal. We do not prove that the second formula is flattened, just that it is equal to the first formula.

%sort mklist {A} {B} {_ pf (A == B)} %.
%mode mklist %in %out %out %.
%term mklist-swap
  %pi (mklist (A + (B + C)) D (trans (symm plus_assoc) Pf))
  %<- (mklist (A + B + C) D (%the (pf (A + B + C == D)) Pf)) %.
%term mklist-step
  %pi (mklist (A + C) (B + C) (plus_cong Pf refl))
  %<- (mklist A B (%the (pf (A == B)) Pf)) %.
%term mklist-stop mklist A A refl %.

Using the tactical theorem prover

We can then use %define and %solve to create a proof that (a + (b + c) + d == a + b + c + d). In order for mklist to terminate, it must be given a ground term, so we introduce a four atomic terms a through d. The proof Pf must be explicitly allowed to rely on those terms, which is why (Pf a b c d) is written instead of just Pf.

%define p1 = Pf %solve _ : {a} {b} {c} {d} mklist (a + (b + c) + d) _ (Pf a b c d) %.

Tactics with %clause

Another way to achieve the same goal is to define (list A B) as (pf (A == B)), which we do for list' below.

%define list' (%pi num %-> num %-> %type) [a] [b] pf (a == b) %.
%mode list %in %out %.

Then, we have to justify each clause of the logic in the same way as we justified plus_elim2 above. We have to write the %clause because, if we do not, then STELF will not use the definitions in logic programming search.

%clause list'-swap (%pi (list' (A + (B + C)) D) %<- (list' (A + B + C) D)) [Pf pf (A + B + C == D)] trans (symm plus_assoc) Pf %.
%clause list'-step (%pi (list' (A + C) (B + C)) %<- (list' A B)) [Pf pf (A == B)] plus_cong Pf refl %.
%clause list'-stop (list' A A) refl %.

Now we do not need to use %define; p2 proves the same thing as p1 above.

%solve p2 : {a} {b} {c} {d} list' (a + (b + c) + d) _ %.

This is not the recommended style for a number of reasons (metatheoretic parts of STELF like totality assertions won’t work with %clause), but a few large examples such as the big algebraic solver have been written in this style.