From e95693984ed565a8264eccd021b1dccf2a09246f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 4 Mar 2021 23:19:29 +0100 Subject: [PATCH] Proposal on subsingleton elimination and hProp --- text/subsingleton-elimination.md | 176 +++++++++++++++++++++++++++++++ 1 file changed, 176 insertions(+) create mode 100644 text/subsingleton-elimination.md diff --git a/text/subsingleton-elimination.md b/text/subsingleton-elimination.md new file mode 100644 index 00000000..4e0b3b71 --- /dev/null +++ b/text/subsingleton-elimination.md @@ -0,0 +1,176 @@ +- Title: Extended subsingleton elimination and subsingleton impredicativity, the case of `SProp`, `Prop` and `hProp` + +- Driver: Hugo Herbelin + +- Status: Draft + +----- + +# Bibliography + + - [Definitional Proof-Irrelevance without K](https://hal.inria.fr/hal-01859964v2/document), Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau + - This [Coq-club thread](https://sympa.inria.fr/sympa/arc/coq-club/2021-02/msg00092.html) on HoTT support + +# Summary + +The declaration of an inductive type in `SProp` and `Prop` can be seen as a truncation with respect to classes of formulas which we shall respectively call `SProp` and `Prop`. + +These classes are superset defined by syntactic criteria: +- for `SProp`, as described in "Definitional Proof-Irrelevance without K": + - inductive types with at most one constructor whose components are recursively in `SProp` (section 3 of the paper), otherwise said inductive types generated by: + - `False` + - `True` + - any type previously declared in `SProp` + - any sigma-type of such types (without recursivity nor indices) + - inductive types with disjoint indices (sections 5 and 6 of the paper), a priori to be taken in small types, i.e. hsets +- for actual `SProp`, as implemented in Coq 8.12: + - only the empty inductive type (possibly with indices) +- for `Prop`: inductive types possibly with indices with at most one possibly-recursive constructor whose components are recursively in `Prop`, otherwise said inductive types generated by: + - `False` + - `True` + - any type previously declared in `Prop` (e.g. `ex A P`) + - any sigma-type of such types, as in `and`, possibly recursive as in `Acc`, possibly with indices as in `eq`. + +These truncations are automatically considered as eliminable when the truncated type is syntactically recognized as belonging to the class (so-called "singleton elimination", which we could more accurately call "subsingleton elimination"). + +The classes `Prop` and `SProp` are impredicative, in the sense that a dependent product of codomain `Prop` or `SProp` is again in the class. + +This CEPS is about three distinct extensions: +- extending the definition of `Prop` and `SProp` classes with new syntactically decidable criteria +- extending the dynamic detection of subsingleton elimination +- adding a new class `HProp` providing an impredicative universe of subsingleton types; this extra `HProp` class would provide a variant of HoTT with impredicative `hProp` (`hProp := { A:Type & forall x y:A, x = y }`), alternative to using an axiom of resizing + +# Details of the current situation + +We review the current situation for `Prop` and `SProp`. + +## `Prop` + +Sort-polymorphism makes that inductive types are syntactically recognized in `Prop` after instantiation of parameters. For instance, `prod True True` is recognized as impredicative after instantiation: +``` +Check Type -> prod True True. +(* Type -> True * True + : Prop *) +``` +Similarly in contexts where a `Prop` is expected: +``` +Check and (prod True True) True +(* True * True /\ True + : Prop *) +``` +Contrastingly, subsingleton elimination is not recomputed dynamically: +``` +Inductive PROD A B : Prop := PAIR : A -> B -> PROD A B. +Check fun x : PROD True True => match x with PAIR _ _ _ _ => 0 end. +(* Elimination of an inductive object of sort Prop is not allowed on a predicate in sort Set *) +``` +which would actually be easy to address (see item 3 of the next section). + +## Actual `SProp` + +Actual `SProp` has no template polymorphism. Its subsingleton elimination is restricted to `False` so that dynamic computation of subsingleton elimination does not matter. + +We do not recommend template polymorphism for `SProp` (since template polymorphism is already planned to be superseded with universe polymorphism). + +In particular, we do not plan late detection of a parametric type in `Type` as an `SProp, nor late detection of a parametric type in `SProp` as supporting subsingleton type. + +# Detailed design for the `Prop` and `SProp` extensions + +## Uniformizing the treatment between `Prop` and `SProp` + +1. accept singleton types with all arguments in `SProp` to be in `SProp` as it is the case for `Prop`, the only difference being that recursive arguments are excluded; the indices should be in small types (i.e. `Prop` or `Set`) + +## 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 +3. 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") + +## Dynamically recognizing subsingleton elimination for `Prop` and `SProp` in `match` + +4. This would require calling the subsingleton elimination checker dynamically when typing `match`. + +# Detailed design for the `HProp` addition + +Belonging to `HProp` is not decidable, so exactly characterizing `HProp` requires user-provided data. + +There are two solutions: +- either we retarget `Prop` to include `HProp` (simpler) +- or we keep `Prop` as it is and add a new subuniverse `HProp` (less change of habits) + +Both solutions follow the same way. Below, we assume the latter. To get the former, just use `Prop` instead of `HProp`. + +We shall avoid relying on template polymorphism. However, we may consider a `cast` of the form: +``` +(t : HProp by p) +``` +which forces the type-checker to recognize a type as being in a smaller universe than decidably detectable. + +The status of casts in the implementation is however fragile, so this may require some clarification of casts first. + +## New command to support arbitrary `HProp` + +We propose a new command: +``` +Subsingleton id context : ishProp A := proof. +``` +which recast the type of `A` from `context -> Type` to `context -> HProp` so that it is latter considered impredicative. + +An alternative is to have a modifier to definitions in the form: +``` +Subsingleton id context := def : HProp by proof. +``` +But then, we probably want also: +``` +Subsingleton id context := def : Hprop. +Proof. +the proof of being hProp +Qed. +``` +which may be complicated. + +If `HProp` is made distinct from `Prop`, new declarations `Inductive ... : ... -> HProp` would be accepted too. When to tell that the type has subsingleton elimination? There is a proposal in the next section. + +## Dynamic detection of subsingleton elimination + +We propose an extension of `match` of the following form: +``` +match t as id in I params return typ by u with +| C1 vars => body +... +| 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. + +# Side remark on template polymorphism for `Prop` + +Instances of parametric types which are not in `Prop` in the general case are automatically recognized as belonging to the `Prop` class (and treated as subsingleton for `match` and as impredicative in function types) when the parameters are themselves in `Prop`. This is typically the case of `prod A B` which behaves as `and A B` when `A` and `B` are in `Prop`. + +Template polymorphism induces a view where an inductive type in `Prop` does not necessarily mean explicitly `Prop`-truncated. It is so only when the original type is not a syntactic `Prop`-subsingleton. + +Without template polymorphism, explicit coercions from `prod A B` to `and A B` should be inserted (when `A` and `B` are `Prop`), and explicit Prop-boxing of `prod A B` should be done to make `prod A B` behave impredicatively. + +# Issues with extraction of `HProp` + +Types in `HProp` which are not in the current syntactic class `Prop` could simply be extracted as if they were types. + +# Conclusion + +A few extensions could be done pretty easily: +1. accept singleton types with all arguments in `SProp` to be in `SProp` (`True`, `and`, ...) +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 +4. dynamically recognize subsingleton elimination for `Prop` and `SProp` in `match` + +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") + +The support for `HProp` distinct from `Prop` would require introducing the new subuniverse `HProp` at many places of the code and may be costly. + +However, scaling `Prop` to `HProp` would only require the new independent commands: + +5. `Subsingleton ...` +6. `match ... by p with ... end` +7. `(t : HProp by p)` + +and each of them are worth a design discussion.