The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

> Definitional "proof irrelevance" (DPI) is one way to
> tackle this problem: wasn't there a plan to have this
> in Coq? How's it going? Of course, DPI is incompatible
> with case analysis on proofs, as happens in the
> computational behaviour of equality elimination, so it
> makes things more complex, requiring computation and
> definitional equality to be defined mutually. 

Yes, it would be very convenient (and natural) to have definitional
proof irrelevance in Coq. The local expert is Benjamin
Werner. Matthieu Sozeau, who started to investigate how it could be
implemented, was also involved, together with Arnaud Spiwack.

As far as I remember, the loss of an effective proof while computing
with equality elimination could indeed be addressed by triggering the
reduction only in case of definitional equality of the two terms being
compared (actually, reasoning in Oury's extended Calculus of
Constructions to make equality elimination commute with the context
may perhaps provide a solution too).

To tell the truth, I'm not so sure about what was actually
blocking. One of the main problems was the loss of the effective proof
of Acc that is used for triggering the reduction of fixpoints. There
were several solutions to address it but I don't remember if one
emerged from the others.

I think to remember there were also complex technical issues with the
Prop <= Type subtyping (difficulty to cheaply detect, say, that a
polymorphic "f: forall A:Type, A -> A" becomes a proof when
instantiated on a proposition), but here again, I don't know if it was
blocking. I think we should indeed take stock of the state of the art
on DPI.

> Just adding K in some (computational) form is much cheaper!  I know
> there were some other proposals which would effectively repair the
> computational behaviour of JMeq: it would be good to know the state
> of play.

There were several proposals here.

The clearest one is probably the one by Pierre Corbineau which exactly
provides the computational behaviour of JMeq by a simple change of the
"return" clause.

There is also a proposal by Bruno Barras (I think derived from a trick
by Thorsten Altenkirch) but I think to remember that Bruno told me
that the exact logical strength of this proposal was unclear.

Finally, there is a more general proposal to support Agda-style
pattern-matching (see the proceedings of TYPES'08) but the
implementation, planned at some time, was suspended in the hope of
finding a more expressive pattern-matching typing rule and the problem
now connects to the question of extensional equality.

Then, here also, we need to review the state of the art of the
question.

Hugo