The Coq mailing list

[James McKinna <james AT dcs.st-and.ac.uk>]

[NB This reply comes rather a long time after Gang Chen's
original enquiry; the delay in responding is due to my having
recently changed my affiliation from the University of Durham to
the University of St.Andrews. Please note my new e-mail address
as above. JHM]

GANGCHEN5 AT aol.com
 wrote, some time ago:

> Given an inductive definition:
>
> ...
>
> I want to prove that each pair of two constructors are
> different. ...

> Question:
> Are there simpler or general proofs for this problem ?
>
> ...

Using a tactic, Discriminate, which other correspondents have
noted as a potential solution, corresponds to working at the
meta-level of provability for the type theory of Coq (I stand
corrected if this tactic is in fact implemented definitionally,
as below). Given sufficient strength in the type theory
(typically one more level of universes, and Type-level
elimination for equality), one can do a little better, and
construct the matrix of discrimination statements as a type
family internally.

The construction looks roughly like this:

For Inductive D := c1 ... | c2 ... | ... | ck ...

construct the family D-Disc indexed over (d, d':D), using D-rect
(we need Type-level elimination), such that

D-Disc (ci s) (ci t)  definitionally equals (iota-reduces to)  "s
= t"
       for i = 1, 2, ..., k, ...

D-Disc (ci s) (cj t)  definitionally equals (iota-reduces to)
"False"
       for i =/= j

In the case of constructors ci being constants, replace the
equality "s=t" between terms (in general, equality of vectors of
terms) with "True". Now, you may further prove

  D-disc : (d,d':D)(d = d') -> D-Disc d d'

either: by double recursion on d,d': D (mirroring the double
recursion used in defining D-Disc), using reflexivity proofs on
the diagonal, and inversion to rule out as impossible the
off-diagonal cases;

or, better: by eliminating the equality directly, and proving
(d:D)D-Disc d d by a single induction on d:D.

The general method which you seek is now internalized, for any
terms d, d':D via the *term* D-disc d d', and by iota-reduction
in the system. Of course, for arbitrary inductive types, it
requires some meta-programming to construct D-Disc and D-disc. If

your type theory, and its universes, are further capable of
internalizing the scheme for inductive definitions, then these
meta-programs may themselves be internalizable.

I first saw such a construction by Claire Jones for the LEGO
system in the early 1990s, with various subsequent refinements
and re-implementation by Conor McBride in Oleg (in particular
CPS-lifting the equation "s=t"), and now in the implementation of

our language EPIGRAM, where these definitions take an obvious,
and very unimaginative, form.

Best wishes,

James McKinna
School of Computer Science
University of St. Andrews
North Haugh
St. Andrews
Fife KY16 9SS
SCOTLAND