A finite set of tuples with unique first element

Stream: new members

[Ömer Şakar]

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]

You should take a look at the alist type

[Mario Carneiro]

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

[Mario Carneiro]

tuple is just prod btw

[Ömer Şakar]

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]

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

[Alex J. Best]

Yes its in mathlib, docs at docs#alist

[Ömer Şakar]

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

[Ömer Şakar]

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]

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]

Your map is isomorphic to list (α × β)

[Ömer Şakar]

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]

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]

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

[Yakov Pechersky]

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

[Ömer Şakar]

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]

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]

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]

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)