The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I've been toying around with the idea of making the standard
additional axioms into typeclasses.  e.g.

Class Classic : Prop :=
classic : forall P:Prop, P \/ ~P.

Class ProofIrrelevance : Prop :=
proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.

Require ClassicalFacts.

Instance classic_proof_irrel `{Classic} : ProofIrrelevance :=
ClassicalFacts.proof_irrelevance_cci classic.

So this way, if you prove lemma A using just proof_irrelevance, and
then lemma B which uses lemma A and also classic, then you can end up
with lemma B depending only on Classic; whereas with the current Axiom
approach, Print Assumptions B would include both classic and the
redundant proof_irrelevance.

I think the down side, though, would be that any cycles in the facts
you choose to make into instances would cause infinite loops in
instance resolution. (e.g. FunctionalExtensionality ->
PropExtensionality -> Extensionality_Ensembles, but also
Extensionality_Ensembles -> PropExtensionality)
-- 
Daniel Schepler