The Coq mailing list

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

Hi,

> is it possible to experiment with Proof Irrelevance and Eta in the
> conversion rule?
> 
> I would like to write some proofs using this but axiomatizing seems to make
> things extremely awkward because reduction is lost. Is there any nice way I
> can test out my idea?

Adding eta to the conversion rule in Coq is under investigation. It is
technically not very difficult. As Coq relies on a syntax-directed
presentation of the Calculus of Inductive Constructions, it should be
enough to eta-expand on the fly this term that does not start with a
lambda in case a conversion between a term starting with a lambda and
a term not starting with a lambda is requested (this has then to be
done for the four different conversion/unification functions of Coq).

Adding proof-irrelevance to the conversion rule in Coq has been
investigated for a long time now but some technical problems remain
(afair, the main problem is that due to the "Prop subset of Type"
subtyping rule, some opportunities to equate two proofs may fail to be
cost-free detected) and the project is temporarily suspended.

In particular, I know no ready-to-use way to experiment eta and
proof-irrelevance in your developments (though these are extensions we
really would like to integrate to the Calculus of Inductive
Constructions).

Hugo Herbelin