For example, I want to use MathComp, but I want `subType`

to be `{x : T | P x}`

with `P : T -> Prop`

instead of `P : pred T`

. I want the rest of MathComp to be mostly unchanged, just drop-in replace `subType`

.

Is drop-in replacement of existing structures in HB currently possible?

Why would you want that? Note that currently, sig is an *instance* of `subType`

https://github.com/math-comp/math-comp/blob/19227db6deba63824dd266695e92b39b65cc8237/mathcomp/ssreflect/eqtype.v#L706 enabling to use it whenever a `subType`

is expected. In fact, sig is just a particular case of `subType`

. Another instance comes for example with `nat`

being a `subType`

of `int`

.

Happy to know that `sig`

is an instance of `subType`

, but what I want is something different. `subType`

still requires `P`

to be a `pred T`

, that is `T -> bool`

, and even if `sig`

is an instance, this requirement is not dropped. But I want to completely *replace* the definition of `subType`

(actually, `isSub`

) to change `P`

from a `pred T`

to a `T -> Prop`

.

Sometimes when I am doing proofs, I need to work with subtypes that are associated with a predicate that is not necessarily decidable (i.e. `T -> Prop`

), but the current MathComp definition of `subType`

makes it that a `subType`

is necessarily defined by a decidable predicate. One solution is of course introducing the law of excluded middle which makes every predicate computable, but in some of my use cases, I don't want LEM, so this is not possible.

I see. That's a very unusual use case as, usually, one either works on decidable things and enjoys the constructive logic development of mathcomp or wants classical logic and uses the boolp.v file from mathcomp analysis. It's the first time I hear of such a middle ground. In fact, it seems a very limited case: technically you could simply redevelop subType on Prop, this would probably be fairly easy but since Prop does not enjoy proof irrelevance, most of the nice properties will be lost. Maybe you should use SProp instead of Prop but my understanding is that it's currently still not very easy to use.

I'm fine with adding Prop irrelevance as an axiom, but anyways, I was mainly just illustrating a possible use case for such structure replacements

Then, the best solution for you is simply to implement some Prop_subType which should be fairly easy mimicking what's done in eqtype.v for subType.

SProp_subType sounds like something useful to have around...

Not so sure since it requires to assume prop irrelevance. Most users in this case are doing classical logic anyway.

I may be missing something here (and it was a while ago I looked at the SProp paper), but for SProp I thought the irrelevance was "built into" Coq, so no axioms were needed? I guess trusting the implementation amounts to an assumption, though.

For SProp no axioms are needed: "SProp" means strict, or irrelevant-by-definition Prop. Just that SProp isn't very easy to use yet!

Indeed my bad, I misread Prop.

Xuanrui Qi said:

For SProp no axioms are needed: "SProp" means strict, or irrelevant-by-definition Prop. Just that SProp isn't very easy to use yet!

What is lacking according to you? Library support?

Xuanrui Qi said:

For example, I want to use MathComp, but I want

`subType`

to be`{x : T | P x}`

with`P : T -> Prop`

instead of`P : pred T`

. I want the rest of MathComp to be mostly unchanged, just drop-in replace`subType`

.Is drop-in replacement of existing structures in HB currently possible?

It depends what exactly you mean by drop-in.

- Can you import mathcomp 2.1.0 as such and replace just this structure in your own dev? no.
- Can you push a PR to mathcomp and replace this structure with your suggestion without changing anything else? Yes if you assume proof irrelevance of Prop. No otherwise because "drop-in replacements" should be "logically equivalent" to previous structures. So that the theory is the same and so that the previous mixins could be turned into factories.

Alternatively we could make a new structure: proof irrelevant types and have predicates take values in that new structure. Then in your own dev you can deduce`Prop`

is an instance of proof irrelevant type from the axiom.

Last updated: Apr 21 2024 at 01:02 UTC