## Stream: math-comp users

### Topic: Question abount finType

#### walker (Nov 01 2022 at 23:07):

in some data type I am defining... `m1 !! k` means look fo rkey k in m1 and : `m2 ⊈ₘ m1` is defind as `~ m2 ⊆ₘ m1` and `m2 ⊆ₘ m1` is defined as `forall k v, m2 !! k = Some v -> m1 !! k = Some v`

So I was I was struggling something that looks like follows:

``````m2 ⊈ₘ m1 -> (exists k : KT e,  m1 !! k = None /\ m2 !! k <> None
``````

This basically boils to something that is like `(~(forall .....) -> (exists k : KT e, m1 !! k = None /\ m2 !! k <> None)`

Based on my understanding there is no way to move from `~forall` to `exists` constructively but it seams that finType have some reflections that does the job by what it seams to be computational version of forall exists.

I wanted to confirm my assumption that this packed class will help me the way I think it will.

p.s. m1, m2 are finite maps with `eqType` keys and values.

#### Paolo Giarrusso (Nov 01 2022 at 23:54):

I think it's sufficient if the key type is a `finType`?

#### abab9579 (Nov 02 2022 at 00:32):

This is not directly related to `finType`, but I do not think your result holds.
The map `m1 = { 1 -> 1 }` and `m2 = { 1 -> 2 }`are not included in each other, but they have the same support:
`m1 !! k = None <-> m2 !! k = None` holds for any key.

#### Paolo Giarrusso (Nov 02 2022 at 00:34):

right, one needs to adjust the result

#### Paolo Giarrusso (Nov 02 2022 at 00:35):

and I must correct what I said for a different reason: given `T : finType`,`~(forall x : T, P x) -> ∃ x : T, ~ P x` requires `P` to be decidable

#### Paolo Giarrusso (Nov 02 2022 at 00:56):

`m2 ⊈ₘ m1` should only implies there's a key where the map differs, and you can find it by iterating over `T`'s elements and comparing the map entries

Last updated: Jul 25 2024 at 17:02 UTC