Subsingleton elimination and impredicativity for SProp, Prop and hProp #55

herbelin · 2021-03-04T22:25:51Z

This CEPS explores how to implement suggestions made in the SProp paper and suggestions to get an impredicative hProp suitable for working in impredicative HoTT.

Rendered here

text/section-goal-var-distinction.md

text/section-goal-vars-distinction.md

SkySkimmer · 2021-03-04T22:36:29Z

text/subsingleton-elimination.md

+
+## Generalize the syntactic criterion for being in `Prop` or `SProp`
+
+2. accept in `SProp` and `Prop` singleton types with arguments of the form `forall a:A, B` when `B` is recursively an `SProp` or `Prop`-subsingleton


Is it not already the case?

You're right.

Inductive I : Prop := C : (nat->True) -> I.

is recognized as subsingleton.

I had naively checked

Inductive I : Prop := C : (nat->unit) -> I.

which is not recognized as such for other reasons.

Let me fix the document.

SkySkimmer · 2021-03-04T22:40:27Z

text/subsingleton-elimination.md

+| Cn vars => body
+end
+```
+where, when `I` is `HProp`-truncated but the instance `I args` is an `HProp` proved by `u : forall x y:I args, x = y`, the elimination to `Type` is allowed.


If I is a truncation then x = y :> I _ is always inhabited, ie we can't express "I may be un-truncated" in terms of I.

Yes, my wording is wrong. The term u should be a proof of forall x y:I args, x = y where, in the proof, I is taken in Type, i.e. not truncated, even if in the match, it is truncated.

Maybe another criterion would be to prove that forall vars vars', vars = vars' but the equality is complicated to express when there are dependencies.

Actually, you have x = y :> I _ always inhabited for SProp but not for Prop (nor for HProp as the CEP is) because nothing enforces that Prop (or HProp in the proposal) is actually proof-irrelevant (there is a model of Prop which interprets it as impredicative Set for instance).

…ed in Prop for subsingleton elimination thanks to impredicativity).

SkySkimmer · 2021-03-04T22:46:36Z

text/subsingleton-elimination.md

+# Conclusion
+
+A few extensions could be done pretty easily:
+1. accept singleton types with all arguments in `SProp` to be in `SProp` (`True`, `and`, ...)


This is not especially useful as we already have records, and is not trivial to implement as the reduction rule for the match is something like

match p with conj x y => e end ====> e[x := match p with conj x _ => x end; y := match p with conj _ y => y end]

Maybe I'm overestimating the difficulty but I don't think I'm underestimating the usefulness.

I don't think I'm underestimating the usefulness.

Indeed, I forgot eta for non empty primitive records.

(Then, aren't we back to the practical question of letting existing libraries take benefit of primitive records?)

Maybe I'm overestimating the difficulty

Isn't there two levels?

Couldn't and be in SProp even with the usual (non proof-irrelevant) match reduction?

But more fundamentally, you're right that the good answer is probably more about stopping to distinguish between match-based and and projection-based and (or, if we don't unify them, to at least get rid of match-based and).

In particular, it is a bit misleading that and is accepted in SProp without being recognized as subsingleton. It should at least be discouraged.

Couldn't and be in SProp even with the usual (non proof-irrelevant) match reduction?

That would break decidability of typechecking (same as equality without reducing on reflexive proofs)

Couldn't and be in SProp even with the usual (non proof-irrelevant) match reduction?

That would break decidability of typechecking (same as equality without reducing on reflexive proofs)

I'm sorry, I fail to see the example. (By the way, do you have a copy of your PhD somewhere?)

Also, I added to the CEP a section on SProp subtype of Prop. Did I miss an issue with decidability?

How do you check

fun (x : and True True) (f : match x with conj _ _ => nat -> nat end) => f 0

?

(specifically it's not that it's undecidable, it's that I don't know how to decide it without the reduction)

Thanks. So what is the consensus about this situation? That we should reduce match of positive records as you gave above? Or that we should get rid of positive records at all?

Actually, coming back to this example, I would argue that the question of supporting the typing of fun (x : and True True) (f : match x with conj _ _ => nat -> nat end) => f 0 is not an SProp issue but an eta issue. From the moment we decide that eta is supported for positive records, match x with conj _ _ => nat -> nat end should reduce to nat -> nat, independently of the sort of and.

In particular, I guess that you would reduce also match x : and False True with conj _ _ => nat -> nat end, which I interpret as taking care here of the surface constructor of the proof of and, rather than ensuring that and False True is inhabited, i.e. to rely on eta.

SkySkimmer · 2021-03-04T22:54:17Z

text/subsingleton-elimination.md

+
+The "disjoint indices" extension would require some days of work:
+
+4. accept in `SProp` and `Prop` types with several constructors when (small) indices justify that the constructors are disjoint (section 5 of "Definitional Proof-Irrelevance without K")


I see this in 2 parts:

having indices at all (in the non 0 constructor case), in which case the implicit equality must be small (except for prop without -indices-matter)
this was actually already present in an early version of SProp, see https://github.com/coq/ceps/pull/37/files#diff-dce84f9d9bcdf12e5ebabb0ce1c8791176850fe3aa48a8e58f068d016c92a90dR255 Inductive universe levels and forced constructor arguments coq#7929 and https://github.com/coq/coq/blob/089f1504293559b4472f8f4f13c2a498a51a5d64/kernel/indtypes.ml#L116-L222 and related code in that branch

once we have indices, allowing multiple constructors when the indices force them to be disjoint

this was actually already present in an early version of SProp

And you removed it because it raised issues?

(except for prop without -indices-matter)

It would be nice to eventually have -indices-matter the default.

once we have indices, allowing multiple constructors when the indices force them to be disjoint

OK, thus there are plans?!

Incidentally, at some time, I tried using SProp to have irrelevant proofs of le but this was difficult (I should report about my experience; maybe I just don't know the good tricks...).

And you removed it because it raised issues?

It was somewhat incomplete (for instance extraction didn't handle it) and didn't seem all that useful.

OK, thus there are plans?!

It's just "if we do it, it will probably be something like this"

- taking into account proxys mentioned by Gaëtan for SProp - mentioning the SProp <= Prop issue - mentioning the eta for "match" issue reminded by Gaëtan - fixing some wrong item numbering

SkySkimmer · 2021-03-05T12:20:20Z

text/subsingleton-elimination.md

+
+In particular, we do not plan late detection of a parametric type in `Type` as an `SProp` liable to be considered impredicative. Late detection of a parametric type in `SProp` as a type supporting subsingleton elimination is the purpose of point 2 (once points 1 and 3 are achieved).
+
+## Subtyping of `SProp` in `Prop`


This will never happen in Coq (except as an unsafe option)
I'm not convinced that it's decidable, and even if it is, deciding a conversion a == b : A would need to do some check that there is no B : SProp such that a : B and b : B which sounds quite costly.

Wouldn't the mark computed for a and b be enough to know that a and b are in some SProp type B, independently on A?

Or are you talking about the cost of computing the mark for a sTrue when a is forall A:Type, A?

I probably don't have the whole picture in mind as much as you do, but at worst, I suspect that we could do it if the internal representation of terms kept track of subtyping, since that would not be different in fine, except that it is made automatically, than asking the user to add explicit Box coercions?

Marks only work when they're stable by substitution, subtyping breaks that.

For the reason above right? That if a is of type forall A:Type, A, it assumes that the sort of A is stable by substitution.

spitters · 2021-03-05T21:08:17Z

It would be good to record an intended semantics. E.g. the set model and a homotopic model.

herbelin · 2021-03-07T20:40:31Z

It would be good to record an intended semantics. E.g. the set model and a homotopic model.

That would be good yes. This could be a subsection of the reference manual? At least, proposing it as a PR would be a way to hopefully trigger a constructive discussion (since it is not clear even from the Coq-club discussion tonight that there is an agreement on extensional equality - which actually may be a problem as wrong as opposing intuitionistic and classical logic, i.e. that we may want to give different interpretations to a same symbol while there are actually different symbols involved).

spitters · 2021-03-08T11:31:31Z

There is a reference to Coquand's model of MLTT+sProp here. However, they don't work out the differences between Coq and MLTT.
https://dl.acm.org/doi/10.1145/3290316

mikeshulman · 2021-04-14T15:44:09Z

Just found this. i don't completely follow the HProp proposal; is the idea that there would be a single universe HProp, analogous to Prop, which would be impredicative, and that moreover any type in any universe that can be proven by the user to be an h-prop could itself be asserted to belong to HProp (rather than there being an equivalent copy of it that belongs to HProp)? If so, this seems like a variation on Voevodsky's resizing axiom for hprops, which as far as I know is not known to have any models, so I would be wary of implementing it.

herbelin · 2021-04-15T19:37:27Z

Good question. Let's write ↓A for the copy in HProp₀ (here HProp) of an h-prop_n A, and ↑ for the image back in h-prop_n. Is your question about whether ↑↓A=A and ↓↑A=A can be taken as definitional?

I guess you have in mind a model where ↑ is universe inclusion and, assuming EM, ↓A is True if A is inhabited and ↓A is False if not inhabited. Then, indeed ↑↓A is not definitional.

Couldn't we imagine a model where the coercions preserve contents and are definitional? Typically, what about a model with as many copies of True as inhabited h-prop_n types and as many copies of False as non-inhabited h-prop_n types, with the paths betwen the copy of True for A in h-prop_n and the copy of True for B in h-prop_m being (copies of) the paths between A and B seen in h-prop_max(n,m), and recursively? It is sketchy, but would there be a problem going in this direction?

Because, assuming such a model with definitional coercions, would there be things which we could do with A (seen in impredicative HProp₀) which we could not already do if we had instead an explicitly coerced ↓A, up to first applying ↑ to get back A in h-prop_n?

mikeshulman · 2021-04-15T19:47:45Z

as many copies of True as inhabited h-prop_n types

In all the models I'm familiar with, this many copies would have too high a cardinality to fit in HProp₀. For instance, in ZFC the number of singleton sets in a Grothendieck universe U has the same cardinality as U, since {x} is such a singleton for every x in U. Things get even worse in homotopical models, where you have the same number of contractible types that are not even isomorphic to each other.

herbelin · 2021-04-15T20:21:22Z

Are you talking about cardinality from inside or outside the theory? From outside the theory, there are only countable copies to consider.

Alternatively, how would you derive a contradiction from having an arbitrary number of copies, without anything (a priori) to observe the cardinality from inside?

For instance, there is no model of System F with a set-theoretic interpretation of the function type but there are term models, even term models which include an arbitrary cardinal of atoms (e.g. Miquel).

mikeshulman · 2021-04-16T03:11:57Z

I mean outside the type theory, in the set theory where we consider models. I'm not hugely familiar with System-F-style models, so it's possible you could play some game there. But it's also important to have set-theoretic and homotopy-theoretic models, and in those cases there are a proper class of unequal singleton sets. I'm not claiming I know how to derive a contradiction from this axiom inside type theory, just that I don't know how to build a set-theoretic or homotopy-theoretic model.

mikeshulman · 2021-04-16T03:35:30Z

I would be interested in seeing the details of a system-F-type model of this rule, though. Can you really cook things up so that {x:A & a=x}, for instance, always lies in the first universe, no matter what universe A lies in?

SkySkimmer · 2021-04-16T09:08:16Z

I don't understand the hprop proposal. Could you make some small example (pseudocode) script using it?