Remove dependency on proof irrelevence axiom

[roconnor-blockstream]

This is a small clean up that removes the already rare uses of the proof irrelevance axiom.

[xavierleroy]

Apologies for taking so long to acknowledge this proposal. It's instructive to see how to get rid of proof irrelevance and how it "costs" in terms of proof effort. Thanks a lot for your work pushing the proofs through!

In the end I'm not sure yet what to conclude from this experiment. If we really want to avoid the proof irrelevance axiom, perhaps it would be better to use Boolean equalities in dependent types, i.e. replace {x : A | P x} with {x : A | decide (P x) = true} where decide is the one from the DecidableClass library.

But is it really worth getting rid of proof irrelevance? Currently CompCert uses functional extensionality and proof irrelevance axioms, and I thought those two axioms are uncontroversial (and possibly even provable in a future HoTT-infused Coq).

[xavierleroy]

Also: this set of axioms (functional extensionality + proof irrelevance) was agreed a long time ago with @andrew-appel as a common basis for CompCert and for VST. I see VST uses proof irrelevance quite a lot.

[roconnor-blockstream]

I created this patch because I was trying to understand where CompCert was relying on proof irrelevance. In my experience, proof irrelevance is usually not necessary. I consider using proof irrelevance a kind of code smell because it means you are making computationally relevant data inaccessible, and there is a reasonable chance that later on you will decide you need that data accessible afterall. I was surprised when I saw CompCert was relying on it and I wanted to explore where it was needed. As you can see, my conclusion is that it isn't really needed at all and was, in fact, very easy to remove.

Most of the places that CompCert uses proof irrelevence is for propositions that are already provably irrelevant. The only exception was the inductive definition of perm_order which is a Prop that isn't proof irrelevant. However, this inductive definition for perm_order seems like an anomaly to me. Every other proposition in CompCert, such as perm_order' and perm_order'' etc., seems to be defined recursively rather than inductively.

Regarding if it would be better "to use Boolean equalities in dependent types", I don't think that follows. The two definitions you suggest are isomorphic and each form has its advantages and disadvantages (which is why in SSReflect's library usually both forms of predicates, logical and computational, are defined and related to each other by a reflection principle).

While the axioms used by CompCert are uncontroversial from a logical standpoint, the use of axioms get in the way of reduction and eliminate CIC's canonicity property. I suppose we are all hoping that a computational form of Univalance will be discovered to make functional extensionality reducible.

OTOH I don't believe that proof irrelevance is something that will be provable with HOTT. I'm not an expert, but my understanding is that HOTT only has proof irrelevance for hProps, which are types where irrelevance essentially holds by definition. However, interpreting Coq's Prop type as hProp seems to be problematic with respect to singleton elimination (see https://homotopytypetheory.org/2012/01/22/univalence-versus-extraction/.) In fact, proof irrelevance implies UIP which contradicts Univalence, IIUC.

Generally speaking, I think it is good form to only use Props that are in fact hProp, which is what this patch proposes by replacing the definition of perm_order.

Regarding VST, because it is VST that depends on CompCert rather than vice versa, I feel that the fact that VST uses Proof Irrelevence doesn't obligate CompCert to also make use of Proof Irrelevence. I think a reasonable outcome here is to keep proof_irr in Axioms.v and simply never make use of it in CompCert. That way you avoid polluting other projects depending on CompCert with this particular axiom (after all, Coq can track uses of axioms on a per definition level rather than on a per module level).

I agree that the argument to remove the use of proof-irrelevance isn't very strong. All the axioms used by CompCert, functional extensionality, EqDep.eq_rect_eq, and proof irrelevence could, in principle, be removed; it just so happens that proof irrelevence is by far easiest to remove. I think of this patch as perhaps a first step to removing all uses of axioms to achieve the canonicity property. However, even then, the use of Opaque terms in Coq means that having canonicity property arguably really provide you with much value. Removing proof irrelevence and EqDep.eq_rect_eq would make CompCert compatible with the Univalence axiom IIUC, which is maybe worth something.

Perhaps ultimately it is just aesthetically displeasing to depend on Axioms and if it is easy to remove the use of one of them, then maybe this is an improvement. However, not merging this PR seems to be reasonable choice if you think reducing axiom dependencies isn't worthwhile (though I still think your definition of perm_order really ought to be changed).

[xavierleroy]

Thanks for the extra explanations, very useful.

I care much more about specifications than about proofs. CompCert tries hard to use the specification styles most appropriate for what needs to be specified. Quite often (as in PL mechanization in general) inductive predicates are best, but sometimes functions with results in Prop are clearer.

For perm_order the inductive presentation is just fine and in no way "ought to be changed", as you write.

More generally, I certainly don't want to be forced into changing specifications just to get the uniqueness of proofs property. That's just a failure of proof engineering. I'll gladly take the smell of the proof irrelevance axiom instead.

If I mentioned the SSR-style use of decide P = true in place of P, it's because it's a (the?) systematic way to work around this uniqueness-of-proofs issues without changing the specs.

[roconnor-blockstream]

Your comments are fair.

I believe that you will eventually come to regret accepting non-proof irrelevent definitions in Prop, such as perm_order in your development if you start making more of them (I know that I regret my uses in my earlier proof developments in Coq). I believe you haven't encountered issues yet because, as it turns out, perm_order is the sole proposition that you use that has violated this property, and the current use of perm_order is relatively limited in scope.

However I think your decision here is reasonable, and I'm quiet happy you have considered my PR even if it is rejected.