Stream: Hierarchy Builder devs & users

Topic: Possibility of drop-in replacements in HB


view this post on Zulip Xuanrui Qi (Oct 30 2023 at 06:46):

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?

view this post on Zulip Pierre Roux (Oct 30 2023 at 07:43):

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.

view this post on Zulip Xuanrui Qi (Oct 30 2023 at 08:56):

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.

view this post on Zulip Pierre Roux (Oct 30 2023 at 09:25):

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.

view this post on Zulip Xuanrui Qi (Oct 31 2023 at 04:03):

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

view this post on Zulip Pierre Roux (Oct 31 2023 at 07:08):

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.

view this post on Zulip Karl Palmskog (Oct 31 2023 at 07:35):

SProp_subType sounds like something useful to have around...

view this post on Zulip Pierre Roux (Oct 31 2023 at 07:40):

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

view this post on Zulip Karl Palmskog (Oct 31 2023 at 08:10):

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.

view this post on Zulip Xuanrui Qi (Oct 31 2023 at 19:00):

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

view this post on Zulip Pierre Roux (Oct 31 2023 at 19:22):

Indeed my bad, I misread Prop.

view this post on Zulip Reynald Affeldt (Nov 01 2023 at 01:55):

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?

view this post on Zulip Cyril Cohen (Nov 02 2023 at 07:13):

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.


Last updated: Apr 21 2024 at 01:02 UTC