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.
You can define it as Definition A_both : Type := {a : A_f | g (proj1_sig a) = true}.
. Is that what you're looking for?
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
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!
Jake has marked this topic as resolved.
Last updated: Sep 30 2023 at 06:01 UTC