Tactical theorem proving

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

Logics can be defined in Twelf in such a way that it may not be possible to do proof search by the fixed search strategy of Twelf'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.

num : type. %name num N.
+ : num -> num -> num. %infix left 10 +.
0 : num.
1 : num.

prop : type.
== : num -> num -> prop. %infix 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:

pf : prop -> type.

refl : pf (N == N).
symm : pf (N1 == N2) -> pf (N2 == N1).
trans : pf (N1 == N2) -> pf (N2 == N3) -> pf (N1 == N3).

plus_assoc : pf (N1 + N2 + N3 == N1 + (N2 + N3)).
plus_comm : pf (N1 + N2 == N2 + N1).
plus_zero : pf (N1 + 0 == N1).
plus_cong : pf (N1 == N1') -> pf (N2 == N2') -> pf (N1 + N2 == N1' + N2').
plus_elim1 : 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.

plus_elim2 : 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.

list : num -> num -> type.
%mode list +A -B.

list-swap : list (A + (B + C)) D
	     <- list (A + B + C) D.
list-step : list (A + C) (B + C)
	     <- list A B.
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 Twelf'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.

mklist : {A}{B} pf (A == B) -> type.
%mode mklist +A -B -Pf.

mklist-swap : mklist (A + (B + C)) D (trans (symm plus_assoc) Pf)
		<- mklist (A + B + C) D (Pf: pf (A + B + C == D)).
mklist-step : mklist (A + C) (B + C) (plus_cong Pf refl)
		<- mklist A B (Pf: pf (A == B)).
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).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%solve {a:num} {b:num} {c:num} {d:num} mklist (a + (b + c) + d) (N1 a b c d) (Pf a b c d). OK p1 : {n:num} {n1:num} {n2:num} {n3:num} pf (n + (n1 + n2) + n3 == n + n1 + n2 + n3) = [n:num] [n1:num] [n2:num] [n3:num] plus_cong (trans (symm plus_assoc) (plus_cong (plus_cong refl refl) refl)) refl. _ : {a:num} {b:num} {c:num} {d:num} mklist (a + (b + c) + d) (a + b + c + d) (plus_cong (trans (symm plus_assoc) (plus_cong (plus_cong refl refl) refl)) refl) = [a:num] [b:num] [c:num] [d:num] mklist-step (mklist-swap (mklist-step (mklist-step mklist-stop))).

%% OK %%

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.

list' : num -> num -> type = [a][b] pf (a == b).
%mode list +A -B.

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 Twelf will not use the definitions in logic programming search.

list'-swap : list' (A + (B + C)) D
	     <- list' (A + B + C) D 
  = [Pf: pf (A + B + C == D)] (trans (symm plus_assoc) Pf).

list'-step : list' (A + C) (B + C)
	     <- list' A B
  = [Pf: pf (A == B)] (plus_cong Pf refl).

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) _.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%solve {a:num} {b:num} {c:num} {d:num} list' (a + (b + c) + d) (N1 a b c d). OK p2 : {a:num} {b:num} {c:num} {d:num} list' (a + (b + c) + d) (a + b + c + d) = [a:num] [b:num] [c:num] [d:num] list'-step (list'-swap (list'-step (list'-step list'-stop))).

%% OK %%

This is not the recommended style for a number of reasons (metatheoretic parts of Twelf 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.