Follow

Coq sorts, rant

I urgently need a reminder why I shouldn't be allowed to destruct Prop to construct Set or Type. Because ATM it seems so stupid!

I can just redefine everything for a higher sort and throw the definitions from the standard, or any other library dependent on it, out the window. Just *why*?

Coq sorts, rant

@tfb I sometimes use tactics to construct definitions (because otherwise it's boring), and it's kind of anxious to end it with Defined, because the definition may in principle be not exactly what I meant it to be ((dis)trust to the automation).

Coq sorts, rant

@amiloradovsky In the Coq-Mode I keep thinking about making, there'd be a key binding to comment out the tactics-based proof and replace it with the generated definition.

re: Coq sorts, rant

@amiloradovsky I can give a very technical reason for this. There is an independent axiom called "proof irrelevance" which states that any Predicate in Prop has at least one proof (formally "forall (X : Prop) (x y : X), x = y"). The elim restriction guarantees us that we cannot contradict PI. While PI on its own is pretty uninteresting, it is also entailed when assuming the principle of the excluded middle (which we very much want to be at least a consistent axiom), so we need to make sure PI is consistent as well.

There are actually ways to show that even without additional axioms, the absence of the elim restriction would cause inconsistencies because of the impredicativity of Prop, but they are less straightforward.

There are actually ways to show that even without additional axioms, the absence of the elim restriction would cause inconsistencies because of the impredicativity of Prop, but they are less straightforward.

re: Coq sorts, rant

@amiloradovsky Whoops, "at least one proof" should of course be "at most one proof". That'd be terribly broken, otherwise.

re: Coq sorts, rant

@amiloradovsky Maybe another thing to note is that the entailment XM -> PI is because of the impredicativity of Prop (as far as I understand it). You can assume the Type equivalent of XM (forall (X : Type), X + ~X) without entailing the Type equivalent of PI (which would be horribly inconsistent).

re: Coq sorts

@abs So it is for a compatibility with classical logic, where we don't care about the #computability and #complexity and just assume everything is decidable. After all Coq is a proof assistant and not just a programming language; so we'd like to be able to encode the non-constructive proofs in it as well.

re: Coq sorts

@abs Then couple immediate thoughts/questions:

- if it is an optional restriction, why all the standard library is using it as the default?

- what should I use for (proof-relevant) dependent sums, instead of "exists", for example?

re: Coq sorts

@amiloradovsky I'm not sure what you mean with "optional restriction". Coq is inconsistent without it.

I'm also not sure why all of the standard library is using Prop (or why there is an impredicative universe at the bottom of the universe hierarchy to begin with). Its usefulness for code extraction as @tfb suggests seems like a very plausible reason.

You can use sig or sigT as an alternative to the existential quantifier in Type.

I'm also not sure why all of the standard library is using Prop (or why there is an impredicative universe at the bottom of the universe hierarchy to begin with). Its usefulness for code extraction as @tfb suggests seems like a very plausible reason.

You can use sig or sigT as an alternative to the existential quantifier in Type.

re: Coq sorts

@abs @tfb By optional restriction I meant that one should only use Prop/Set if they want to use the (proof irrelevance) axiom. Otherwise I see no reason to not formulate the constructions for Type or broadest universe possible.

I've just realized/recalled that `forall` and `exists` aren't entirely symmetric w.r.t. the implementation: `forall` is a very basic construction, used to define functions and inductive types, for instance, while `exists` is just a particular inductive type.

re: Coq sorts

re: Coq sorts

@amiloradovsky @tfb The benefit of Prop is that it is impredicative, so you don't have to worry about universe stuff as much. I think that's a huge reason why people use it.

re: Coq sorts

re: Coq sorts

@amiloradovsky @tfb Impredicative for Prop essentially means that you can quantify over anything you like and end up in Prop as long as your consequence lays in Prop.

This is not the case for Type, where the universe level of a definition might change depending on "what you use it on" which can lead to problems that can only be solved by complicated (and rather slow) mechanisms like universe polymorphism.

This is not the case for Type, where the universe level of a definition might change depending on "what you use it on" which can lead to problems that can only be solved by complicated (and rather slow) mechanisms like universe polymorphism.

functional.cafe is an instance for people interested in functional programming and languages.

Thomas@tfb@functional.cafeCoq sorts, rant

@amiloradovsky Because we care about extraction, and the distinction between programs where form matters and form-irrelevant proofs.

The standard library could work better with higher sorts, for sure.