Elimination with a Motive Export

@incollection{citeulike:5129236, 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.}, author = {Mcbride, Conor}, citeulike-article-id = {5129236}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/3-540-45842-5_13}, citeulike-linkout-1 = {http://www.springerlink.com/content/vbpg19305t46f6dm}, doi = {10.1007/3-540-45842-5_13}, journal = {Types for Proofs and Programs}, keywords = {data-type, dependent-types, elimination, motive, project-pre-phd, proof, theorem-prover, types}, pages = {727}, posted-at = {2009-07-12 23:05:37}, priority = {0}, title = {Elimination with a Motive}, url = {http://dx.doi.org/10.1007/3-540-45842-5_13}, year = {2002} }

TY - CHAP ID - citeulike:5129236 L3 - citeulike-article-id:5129236 N2 - 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. JF - Types for Proofs and Programs EP - 727 TI - Elimination with a Motive SP - 727 KW - data-type KW - dependent-types KW - elimination KW - motive KW - project-pre-phd KW - proof KW - theorem-prover KW - types AU - Mcbride, Conor PY - 2002/// UR - http://dx.doi.org/10.1007/3-540-45842-5_13 ER -