The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/18/2014 03:11 PM, Daniel Schepler wrote:
> 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.

While I have no opinion on this particular issue, I didn't know that 
Print Assumptions would ever print out something less than the 
transitive closure of the assumptions in certain cases (as in the 
typeclasses case you describe).  If that's true, is there some way to 
force Print Assumptions to print out the transitive closure?

Otherwise, for people who are using Print Assumptions as a way to check 
if inconsistent assumptions are being used together, this could be a 
problem.

-- Jonathan