Stream: math-comp users

Topic: Question abount finType


view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 01 2022 at 23:54):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 02 2022 at 00:34):

right, one needs to adjust the result

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 14:01 UTC