## Stream: new members

### Topic: A finite set of tuples with unique first element

#### Ömer Şakar (Jan 21 2021 at 18:21):

Hello:)

I am trying to make a finite set of pairs/tuples where the first element of the tuple is unique. I am trying different solutions such as using finite sets, finsets and making a subtype of finsets. The context where I need this is as follows. Suppose I have a map (or dictionary in Python terms) that is modeled as a list of "tuples" (see the inductive type map below) and the latest addition to the map is the key/value pair. I am trying to prove the property that the cardinality of the key is equal to the cardinality of the set of tuples (where the first element was unique).

inductive map {α β: Type} : Type
| nil : map
| build (a:α) (b:β) (m: map): map

inductive tuple {α β:Type}
| create (a:α) (b:β): tuple

def fst {α β:Type} : @tuple α β → α
| (tuple.create a _) := a

def snd {α β:Type} : @tuple α β → β
| (tuple.create _ b) := b


My latest approach is using a subtype of "a finset of tuple" where I then lift all the functions over the subtype (I hope that that sentence is correct).

def finsettuple_unique_key{α β: Type} (fs: finset $@tuple α β): Prop := ∀ t1 ∈ fs, ∀ t2 ∈ fs, t1 ≠ t2 → fst t1 ≠ fst t2 def fintupleset (α: Type) (β: Type) : Type := {fs: finset (@tuple α β) // finsettuple_unique_key fs}  With this subtype of finset, I can make a function that insert a value into the items set and a function that returns me the key/value pairs of a map (see below): def fintupleset_insert{α β: Type} [decidable_eq α] [decidable_eq$ @tuple α β] (t: @tuple α β) (fs: fintupleset α β): fintupleset α β :=
subtype.mk (
insert t (finset.filter (λt1, fst t ≠ fst t1) (subtype.val fs))
) (by sorry)   -- leaving out the proof as it is very long

def items {α β: Type} [decidable_eq α] [decidable_eq \$ @tuple α β] : @map α β → fintupleset α β
| map.nil := fintupleset_empty -- this is basically \empty
| (map.build a b m) := fintupleset_insert (tuple.create a b) (tmpitems m)


Now I have the problem that if I want to reason about the cardinality of this fintupleset, I cannot do that easily because if I use the fintupleset_insert I defined, it uses the insert and filter functions defined in the finset namespace and no lemmas seem to be defined that use both those functions (I also cannot seem to prove it, maybe due to inexperience).

Now my question is, is this approach using the fintupleset subtype a good approach? Or is there an approach I could take that would be easier?

#### Mario Carneiro (Jan 21 2021 at 18:23):

You should take a look at the alist type

#### Mario Carneiro (Jan 21 2021 at 18:24):

it implements essentially this idea, with a list (A x B) where the elements of A must be nodup

#### Mario Carneiro (Jan 21 2021 at 18:25):

tuple is just prod btw

#### Ömer Şakar (Jan 21 2021 at 18:34):

I think the reason I have my own tuple type is simply as practice (very simple practice, but I forgot about to do some basic stuff).

#### Ömer Şakar (Jan 21 2021 at 18:35):

I can't seem to easily find something on alist like documentation or its definition. Is it part of mathlib?

#### Alex J. Best (Jan 21 2021 at 18:36):

Yes its in mathlib, docs at docs#alist

#### Ömer Şakar (Jan 21 2021 at 18:38):

Aa, yes this is exactly what I was looking for. Thank you!

#### Ömer Şakar (Jan 21 2021 at 19:28):

Maybe I was a bit too enhousiastic, how does one use alist? I am trying to say that my items function returns an alist, but I cannot seem to construct it.

I would expect this to work, but I see that the types are not entirely correct:

def items {α β: Type} {γ : α → β} [decidable_eq α]: @map α β → alist γ
| map.nil := ∅
| (map.build a b m) := insert a b (items m)


Maybe I can phrase the question differently, how do I insert a key/value pair a\->b into an alist al?

#### Yakov Pechersky (Jan 21 2021 at 19:39):

import data.list.alist

variables {α : Type} {β : Type}

inductive map {α β: Type} : Type
| nil : map
| build (a:α) (b:β) (m: map): map

def map_to_alist_keep [decidable_eq α] : (@map α β) → alist (λ (a : α), β)
| map.nil := ∅
| (map.build a b m) := if a ∈ map_to_alist_keep m
then map_to_alist_keep m
else (map_to_alist_keep m).insert a b

def map_to_alist_overwrite [decidable_eq α] : (@map α β) → alist (λ (a : α), β)
| map.nil := ∅
| (map.build a b m) := (map_to_alist_overwrite m).insert a b


#### Yakov Pechersky (Jan 21 2021 at 19:42):

Your map is isomorphic to list (α × β)

#### Ömer Şakar (Jan 21 2021 at 19:45):

Yes, that was the idea:) but that was before I knew of the existence of alist. But I now see me misreading the argument of alist. It is a function from \a to the type \b. Thank you again:)

#### Yakov Pechersky (Jan 21 2021 at 19:45):

def list_to_alist_keep [decidable_eq α] : list (α × β) → alist (λ (a : α), β) :=
list.foldr (λ ⟨a, b⟩ al, if a ∈ al then al else al.insert a b) ∅

def list_to_alist_overwrite [decidable_eq α] : list (α × β) → alist (λ (a : α), β) :=
list.foldr (λ ⟨a, b⟩ al, al.insert a b) ∅


#### Yakov Pechersky (Jan 21 2021 at 19:46):

Yes, alist can be dependently typed on the value, based on the key. But in your case, they're independent.

#### Yakov Pechersky (Jan 21 2021 at 19:46):

(of course, foldr or foldl will depend on how you construct your list of tuples)

#### Ömer Şakar (Jan 21 2021 at 19:48):

Yakov Pechersky said:

Yes, alist can be dependently typed on the value, based on the key. But in your case, they're independent.

Yes, I forgot that it can be dependently typed.

#### Ömer Şakar (Jan 21 2021 at 19:49):

Is it correct that you cannot reason about the length of this alist? So, that probably means you have to use the underlying list I guess

#### Mario Carneiro (Jan 21 2021 at 20:41):

I'm not sure what you are getting at - the length of the alist is l.entries.length, although there should be a function for that

#### Ömer Şakar (Jan 27 2021 at 19:41):

Hmm, there does not seem to be a function, but I can just use l.entries.length (sorry for the late reply, forgot to check Zulip)

Last updated: May 08 2021 at 18:17 UTC