ezyang’s blog

the arc of software bends towards understanding

Elimination with a Motive (in Coq)

Elimination rules play an important role in computations over datatypes in proof assistants like Coq. In his paper "Elimination with a Motive", Conor McBride argued that "we should exploit a hypothesis not in terms of its immediate consequences, but in terms of the leverage it exerts on an arbitrary goal: we should give elimination a motive." In other words, proofs in a refinement setting (backwards reasoning) should use their goals to guide elimination.

I recently had the opportunity to reread this historical paper, and in the process, I thought it would be nice to port the examples to Coq. Here is the result:


It's basically a short tutorial motivating John Major equality (also known as heterogenous equality.) The linked text is essentially an annotated version of the first part of the paper—I reused most of the text, adding comments here and there as necessary. The source is also available at:


6 Responses to “Elimination with a Motive (in Coq)”

  1. Pseudonym says:

    For obvious (or perhaps not so obvious) reasons, and_elim should read:

    Lemma and_elim : forall { A B C : Prop }, A /\ B -> (A -> B -> C) -> C.

    You used parentheses rather than braces. You want the propositions to be implicit for maximal usefulness.

  2. Oops, good catch.

  3. ja says:

    One other problem with dependent induction in coq is how often it changes. This makes it brittle, and proofs using it may not survive coq version changes.

  4. tbelaire says:

    Could you explain `Vect_elim` in more detail? What’s going on with the {} and the @P? I’m still just learning Coq. I tried googling, but it’s surprisingly hard to google about syntax for Coq.

  5. tbelaire: Curly braces indicate that an argument is implicit, and prefixing a function/constructor with @ is how you explicitly pass implicit arguments.

  6. tbelaire says:


Leave a Comment