@InProceedings{10.1007/3-540-45842-5_13,
author="McBride, Conor",
editor="Callaghan, Paul
and Luo, Zhaohui
and McKinna, James
and Pollack, Robert
and Pollack, Robert",
title="Elimination with a Motive",
booktitle="Types for Proofs and Programs",
year="2002",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="197--216",
abstract="Elimination rules tell us how we may exploit hypotheses in the course of a proof. Many common elimination rules, such as ∨-elim and the induction principles for inductively defined datatypes and relations, are parametric in their conclusion. We typically instantiate this parameter with the goal we are trying to prove, and acquire subproblems specialising this goal to particular circumstances in which the eliminated hypothesis holds. This paper describes a generic tactic, Elim, which supports this ubiquitous idiom in interactive proof and subsumes the functionality of the more specific `induction' and `inversion' tactics found in systems like Coq and Lego[6][7][15]. Elim also supports user-derived rules which follow the same style.",
isbn="978-3-540-45842-5"
}

