Stream: Coq users

Topic: ✔ Assert member of one type is member of another

Jake (Oct 15 2022 at 21:23):

I have something like this:

Variables (A : Type) (f : A -> bool) (g : A -> bool).
Definition A_f : Type = {a : A | f a = true}.
Definition A_g : Type = {a : A | f g = true}.

then what I want to say is something like this (assuming that f and g are complicated):

Definition A_both : Type = {a : A_f | a in A_g}  (* can't actually do this *)

Is this the best way to do this? It's convenient to have things like A_f and A_g defined as types for other places in the code (namely functions), but then I'm not sure how (if it's possible) to assert that a member of one is a member of another. But maybe there's an entirely different way of doing this I'm unaware of.

Ana de Almeida Borges (Oct 15 2022 at 21:33):

You can define it as Definition A_both : Type := {a : A_f | g (proj1_sig a) = true}.. Is that what you're looking for?

Karl Palmskog (Oct 15 2022 at 21:37):

it's possible that what you want to do is akin to using subtypes in MathComp, see subType here and Chapter 7 in the MathComp book

Jake (Oct 15 2022 at 21:46):

Hmm. Seems like there isn't a super convenient built-in way of doing it then. I'll just stick with defining f externally then. Thanks though!

Notification Bot (Oct 16 2022 at 07:20):

Jake has marked this topic as resolved.

Last updated: Sep 30 2023 at 06:01 UTC