The Coq mailing list

[C T McBride <c.t.mcbride AT durham.ac.uk>]

Hello all

On Wed, 11 Dec 2002, Cuihtlauac ALVARADO wrote:

> Hi,
> 
> >  > Inductive myEq:(A,B:Type)A->B->Prop :=
> >  >  myEq_refl: (C:Type)(x:C) (myEq C C x x).
> > 
> > This is known as John Major's  equality (the origin of this name is to
> > be found  is C. Mc Bride's  PhD thesis), and  this is part of  the Coq
> > standard library; see http://coq.inria.fr/library/Coq.Logic.JMeq.html
> 
> It's not exactly John Major equality, without Uniqueness of Identity
> Proofs axiom you cannot prove Leibniz elimination for this equality :
> 
>   (A:Type)(P:A->Prop)(x,y:A)(myEq A A x y)->(P x)->(P y)
> 
> Conor will correct me if I'm wrong, but John Major equality is really
> myEq + Leibniz Elimination (and regular elim of myEq to /dev/null).

Almost...

The elim rule I usually give for John Major equality is just the dependent
version of Leibniz Elimination:

   (A:Type)(x:A)(P:(y:A)(myEq A A x y)->Prop)(y:A)(q:myEq A A x y)
      (P x (myEq_refl A x))->(P y q)

From this, one may obviously derive Leibniz, but also that John Major
equality proofs are unique

   (A:Type)(x:A)(P:(myEq A A x x)->Prop)(q:myEq A A x x)    
     (P (myEq_refl A x))->(P q)

Dependent Leibniz elimination can be proven from non-dep Leibniz if you
keep the regular elim rule for myEq.

The regular elim rule for myEq does not follow from Dependent Leibniz,
but it's almost entirely useless anyway (unless you also have Leibniz).

> In the end Leibniz elimination for myEq is equivalent to UIP.

Yes, John Major equality is equivalent to adding UIP to the usual
equality. Going back to basics, John Major is just

  Eq (Ex A:Type. A) : (Ex A:Type. A)->(Ex A:Type. A)->Prop

with Ex curried out.

You can then derive the elim rule for John Major if you can prove

  (Eq (Ex A:Type. A) (A,a) (A,b)) -> (Eq A a b)

which is equivalent to UIP (Take A to be (Eq X x x)...).

We know [M. Hofmann] that UIP does not follow from the usual elim rule for
Eq. It is, however definable by pattern matching on dependent types [T.
Coquand].  Adding UIP (or, more conveniently, John Major) to the Calculus
of Inductive Constructions gives you all the structurally recursive
programs definable by pattern matching. Crucially, Leibniz elimination
for John Major equality allows you to use the regular elim rule for an
inductive family to eliminate a particular subfamily, by a trick James
McKinna taught me:

  if D : (is:Is)Type  (where by Is, I mean some index telescope)

  turn ? : (xs:Xs)(d:D ts)->P

  into ? : (is:Is)(d':D is)(xs:Xs)(d:D ts)(is = ts)->(d = d')->P

  then apply the regular D-elim

Cheers

Conor