Tactical theorem proving
From The Twelf Project
| 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.
Contents |
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.5R3, Aug 30, 2005 (%trustme)%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.
%clause list'-swap : list' (A + (B + C)) D <- list' (A + B + C) D = [Pf: pf (A + B + C == D)] (trans (symm plus_assoc) Pf). %clause list'-step : 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) _.Twelf 1.5R3, Aug 30, 2005 (%trustme)%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 %%
