Elimination with a Motive
Conor McBride
University of Durham
Abstract: I spent my PhD escaping `traditional' elimination rules for inductive
datatypes in favour of pattern-matching, demonstrating the relationship
between the two. However, the Stockholm Syndrome(*) set in, and I became
rather attached to the kind of rule I was supposed to be making redundant.
In this talk, I shall explain why.
My question is this: how should we exploit assumptions?
One answer is to prove specific consequences of them: for example, we may
deduce from a conjunction that each conjunct holds, or that equal conses
give rise to equal heads and tails. In practice, such theorems give rise
to forward steps in a proof, unmotivated by the goal at hand.
On the other hand, elimination rules for datatypes look like this:
all Phi. (all y... Phi t[y...])-> ... all x. Phi x
Here Phi abstracts `the goal at hand': it is the `motive' for the
elimination. The subgoals so generated not only expose the `predecessors'
of the , they also yield more specific applications of Phi, rewriting the
goal in the light of the new information available. The rule explains the
leverage that the assumption x gives us on an arbitrary goal.
I shall outline a tactic to apply rules in this style, and give a variety
of examples characterizing data, relations and programs. I aim to convince
you that elimination is best done with a motive.
(*) prisoner begins to like captor
Back to schedule.
Marieke Huisman