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.

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

?

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.

right, one needs to adjust the result

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

`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: Nov 29 2023 at 19:01 UTC