Constructing useful lemmas

Question

In the tutorial Programming and Proving in Isabelle/HOL there's a step-by-step explanation of the proof of reversing a list twice yields the original list (2.2.4 The Proof Process).

theorem rev_rev [simp]: "rev(rev xs) = xs"
apply(induction xs)
apply(auto)

Following the auto step one subgoal remains:

1. V x1 xs.
     rev (rev xs) = xs =⇒
     rev (app (rev xs) (Cons x1 Nil)) = Cons x1 xs

The author then says "In order to simplify this subgoal further, a lemma suggests itself.", and presents the rev_app lemma below:

lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"

Is it just intuition and practice, just like in pen and paper proofs, that enables one to see how subgoal 1. could be simplified and come up with a lemma like rev_app? I simply can't recognize how this lemma suggests itself.

larsrh larsrh · Accepted Answer · 2018-10-10T14:51:04

That is indeed tricky for people unfamiliar with formal proof developments. Over time, one will learn many heuristic approaches to come up with potential lemmas.

In this case (purely equational reasoning) the heuristic usually works by looking at the involved constants of the subgoals.

The main lemma, for example, describes a rev/rev property. The subgoal however needs something about rev/app. This is what tells you that you need a lemma about these two.

The remainder can, unfortunately, be only be described as "human ingenuity": to see that rev(app xs ys) = app (rev ys) (rev xs) is a reasonable property on rev/app.

There is various research on detecting such properties automatically, for example IsaHipster.

Constructing useful lemmas

1 Answers