MRG home page · Research · Publications · Projects · Software · People

Lemma Speculation Results

Our experiments has highlighted limitations of lemma speculation. It is not as widely applicable as believed at the start of the project. The evaluation set thus contains the 18 theorems below. Lemma speculation has problems when no ripple-steps are possible between application of the lemma and fertilisation, which will cause the technique to fail with an underspecified lemma.

Theorems 1 - 7:
These theorems come from the evaluation set for lemma speculation in CLAM 3.
Ireland, A. and Bundy, A. Productive use of failure in inductive proof. Journal of Automated Reasoning, 1996.

Theorem Speculated lemma(s) Proved lemma ? Time (sec.)
1 x + (Suc x) = Suc(x + x) Suc(x + y) = Suc(y) + x yes 6
2 even(x + x) x + (Suc x) = Suc(x + x) no 4
3 even(len(l @ l)) len(l @ (h # l)) = Suc(len(l @ l)) no 13
len(l @ (h # l)) = len(h # (l @ l))
4 rev((rev l) @ m) = (rev m) @ l rev(h # l) @ m = rev l @ (h # m) yes 8
5 rev(rev(l @ m)) = rev(rev l) @ rev(rev m) rev(l @ [h]) = h # rev l yes < 1
6 rev(rev l) @ m = rev(rev(l @ m)) rev(l @ [h]) = h # rev l yes < 1
7 rotate (len l) (l @ m) = m @ l fail - 7

Theorems 8 - 11:
Higher-order theorems about lists. Theorem 8 comes from Isabelle's list library, while the other theorems have been constructed by hand.

Theorem Speculated lemma(s) Proved lemma ? Time (sec.)
8 rev(concat l) = concat(map rev (rev l)) fail - 8
9 len(concat (map f l)) = len(maps f l) fail - 1
10 foldl (λ x y. y + x) n ((rev l) @ m) =
foldl (λ x y. y + x) n (m @ l)
foldl (λ x y. y + x) n (l @ (h # m)) =
foldl (λ x y. y + x) h (n # (l @ m)
no 137
11 foldl (λ x y. x + len y) n ((rev l) @ m) =
foldl (λ x y. x + len y) n (m @ l)
foldl (λ x y. x + len y) n (l @ (h # m)) =
foldl (λ x y. x + len y) h (n # (l @ m)
no 34

Theorems 12 - 13:
Theorems about inequalities.

Theorem Speculated lemma(s) Proved lemma ? Time (sec.)
12 x ≤ (y + x) Suc z ≤ a + (Suc z) = z ≤ Suc(a + z) yes 44
13 count n l ≤ count n (l @ m) fail - 23

Theorems 14 - 18:
Theorems from alternative formalisations of Peano arithmetic. These are seemingly the same theorems, but with different definitions of addition, multiplication and exponentiation. The different theories will force different proofs for the theorems.

The variants of addition considered are:
a1: 0 + y = y
Suc x + y = Suc(x + y)
a2: x + 0 = x
x + Suc y = Suc(x + y)
a3: 0 + y = y
Suc x + y = x + Suc y
a4: x + 0 = x
x + Suc y = Suc x + y

The test-set in alternative variants of Peano arithmetic comes from: Dixon, L. A proof-planning framework for Isabelle. PhD Thesis, University of Edinburgh, 2005.

Theorem Def. of + Speculated lemma(s) Proved lemma ? Time (sec.)
14 a + (a + b) = b + (a + a) a1 fail - < 1
15 a + (0 + a) = a + a a1 fail - < 1
16 a + (0 + a) = a + a a2 Suc x + y = x + Suc y yes* < 1
17 a + (0 + a) = a + a a3 fail - < 1
18 a + (0 + a) = a + a a4 fail - < 1
* Note: After finding the lemma for theorem 16, weak fertilisation can be applied to the original goal. Although the speculated lemma can be proved automatically, there is however also a sub-goal remaining after fertilisation: Suc(b + b) = Suc b + b, which IsaPlanner cannot prove as it lacks capabilities to generalise variables apart.


Webpage maintained by Moa Johansson
Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland
Tel: +44 (0)131 650 2733      Fax: +44 (0)131 650 6899
Please send corrections and suggestions for this page to the DReaM Support Team
Unless explicitly stated otherwise all material on this web site is copyright © The University of Edinburgh.