walker (Nov 01 2022 at 23:07): 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: Oct 13 2024 at 01:02 UTC