elems of Fintype

Stream: new members

[Simon Daniel]

Hello, i wondered if a function exists that converts a Fintype to List of all its elements. I try to store values associated to all Fintype Values

def toList (ft: Type) [Fintype ft] (mapping: ft -> α): List (ft × α) :=
  (Fintype.elems ft).toList.map (fun x => (x, mapping x))

[Eric Wieser]

You maybe want FinEnum instead of Fintype; the former specifies an order

[Simon Daniel]

correct i didnt know about FinEnum.
is there a way to auto derive FinEnum like Fintype https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/DeriveFintype.html to define a FinEnum?

inductive Enum:Type
| A | B | C
deriving FinEnum

[Simon Daniel]

seems like this already has been discussed on Zulip and you suggested it alongside the derive Fintype feature Github
so i guess it does not exist yet in mathlib4

[Kyle Miller]

There are functions like docs#Finset.sort to give a List.

The fundamental problem here is that a Finset is a list without any order (it's defined as a quotient type of lists-up-to-permutation), and to extract that list you have to normalize it somehow.

To #xy, do you need a List? Or can you stick with Finset?

[Simon Daniel]

I want to map from a finite Type to a Network Socket. My Problem is by simply defining a function from my Type to a Socket such a function would Always create a new Socket . I want to init my Sockets once and preserve that State in a List so i can do lookups later to use them

[Matt Diamond]

it sounds like order doesn't matter, only that something is a member of a collection and can be searched for, so it doesn't necessarily need to be a list... it could be a hashmap or a finmap or something

[Simon Daniel]

yea but somehow i would have to fill this (hash) map with a proof that all elements from my type are part of the key set.
thats how im tried it

def Socket:= Unit
def init_socket (_address: Unit): IO Socket := return ()

def init_network (α:Type) [FinEnum α] (adress_of: α -> Unit): IO (List (α × Socket2)) := do
  let all_elems: List α := FinEnum.toList α   -- supposed to be the list of all α
  let init_progs: List (IO Socket2) := all_elems.map (fun x => init_socket (adress_of x))
  -- then execute all progs

def prog: IO Unit := do
  let net <- init_network Unit (fun _ => ())
  -- so now i can lookup Sockets by my supplied Type α = Unit
  let some_sock := (net.lookup ()) -- would need a proof that all α are in the list...

[Simon Daniel]

i use alpha to be able to supply different enums for Socket/Location names. for example

inductive Location
| alice | eve | bob

inductive Location2
| client | server

[Matt Diamond]

could you post a #mwe or is it too complex?

[Simon Daniel]

it should come down to this as a #mwe, however im not sure yet wether the concept of my "collection" makes sense. alpha again has to be some finite type

structure collection (α: Type) (β: α -> Type) [DecidableEq α] where
  data: List (Σ (v:α), β v)
  complete: ∀ (v:α), (data.dlookup v).isSome

def construct_collection [DecidableEq α]  (β: α -> Type) (f: (v:α) -> β v): collection α β :=
  ⟨
    sorry, sorry -- not sure how to get here if even possible
  ⟩

-- so i can define

def f {α: Type}  {β: α -> Type} [DecidableEq α]  (v:α) (c:collection α β) : β v :=
  (c.data.dlookup v).get (by simp [c.complete])

[Matt Diamond]

maybe this is a silly suggestion but why not just use f: (v:α) -> β v as the collection? by definition it must have one and only one "entry" for each member of α

is the issue that you need it to be a stateful object that can be shared and mutated?

[Matt Diamond]

you could use docs#Function.update if you want to update an entry, maybe store the function using a state monad

[Simon Daniel]

yea the idea is that its a network socket gets connected, stored in the "collection" and later retrieved without the need of starting the connection again (so yea its stateful)

[Simon Daniel]

Matt Diamond said:

you could use docs#Function.update if you want to update an entry, maybe store the function using a state monad

sounds like it could work, ill look into that thanks!

[Eric Wieser]

From a performance perspective that's pretty bad because the data gets bigger every time you update the same entry

[Matt Diamond]

yeah... that's a good point...

[Matt Diamond]

@Simon Daniel Eric is right that it's not a great solution... maybe something like this would work better:

import Mathlib

structure collection (α: Type) (β: α -> Type) [DecidableEq α] where
  data: Finmap β
  complete: ∀ (k : α), (data.lookup k).isSome

def construct_collection [DecidableEq α] [Fintype α] (β: α -> Type) (f: (v : α) -> β v) : collection α β :=
{
  data := ⟨
    Finset.univ.val.map (fun k => ⟨k, f k⟩),
    by
      rw [← Multiset.nodup_keys]
      simp [Multiset.keys, Finset.univ.nodup]
  ⟩,
  complete := fun k => by
    rw [Finmap.lookup_isSome, Finmap.mem_def]
    simp [Multiset.keys]
}

def collection.update {α : Type} {β : α → Type} [DecidableEq α] (c : collection α β) (key : α) (newVal : β key)
  : collection α β :=
{
  data := c.data.insert key newVal,
  complete := fun k => by
    by_cases h : k = key
    · rw [h]; simp
    · simp [h, c.complete]
}

def f (α: Type)  (β: α -> Type) [DecidableEq α]  (v:α) (c:collection α β) : β v :=
  (c.data.lookup v).get (by simp [c.complete])

(It's all good if you don't use this... I was just bored so I decided to write the whole thing up.)

[Kyle Miller]

I should have mentioned that even though there's no FinEnum derive handler, you can make use of the same machinery underlying the Fintype derive handler, and write this:

import Mathlib

inductive Location
  | alice | eve | bob

instance : FinEnum Location :=
  FinEnum.ofEquiv _ (proxy_equiv% Location).symm

[Kyle Miller]

(If someone wanted to write the FinEnum handler, it shouldn't be very hard, especially if you rip out the part about enum types, but if you want you could make an efficient FinEnum instance for enum types using the constructor index.)

[Eric Wieser]

I think FinEnum is currently in need of an overhaul, almost all the instances go back and forth between indices and lists in an inefficient way

[Eric Wieser]

So I think building meta code beyond transporting along the equivalence may be a bad use of time since such a refactor might throw it all out

[Kyle Miller]

Ok, so you're supporting ripping out all the enum type handling code, right?

I guess one upgrade to proxy_equiv% would be to have it detect if it's for an enum type and create an equiv to Fin, and then there doesn't need to be any special handling.

[Kyle Miller]

I was just experimenting making a Listable class that produces a List of all elements of a type, adding just enough to get this derivation of a Listable instance to work for the Location type.

import Mathlib

class Listable (α : Type*) :=
  elems : List α
  nodup : elems.Nodup
  complete : ∀ x, x ∈ elems

instance {n : Nat} : Listable (Fin n) where
  elems := List.finRange n
  nodup := List.nodup_finRange n
  complete := List.mem_finRange

def Listable.ofEquiv (α : Type*) [Listable α] {β : Type*} (f : α ≃ β) : Listable β where
  elems := Listable.elems.map f
  nodup := Listable.nodup.map f.injective
  complete := by
    intro x
    rw [List.mem_map]
    use f.symm x, Listable.complete _, Equiv.apply_symm_apply _ _

instance : Listable Unit where
  elems := [()]
  nodup := by decide
  complete := by decide

instance {α β : Type*} [Listable α] [Listable β] : Listable (α ⊕ β) where
  elems := Listable.elems.map Sum.inl ++ Listable.elems.map Sum.inr
  nodup := by
    apply List.Nodup.append
      (Listable.nodup.map Sum.inl_injective) (Listable.nodup.map Sum.inr_injective)
    intro
    simp only [List.mem_map, forall_exists_index, and_imp, imp_false, ne_eq]
    intros
    subst_vars
    simp
  complete := by rintro (x | x) <;> simp [Listable.complete]

inductive Location
  | alice | eve | bob

instance : Listable Location :=
  Listable.ofEquiv _ (proxy_equiv% _)

[Kyle Miller]

And a couple more Listable instances for the rest of the proxy_equiv% system:

code

instance : Listable Empty where
elems := []
nodup := by decide
complete := by decide

-- TODO clean up the proofs
instance {α : Type} {β : α → Type} [Listable α] [∀ x, Listable (β x)] :
Listable ((x : α) × β x) where
elems := Listable.elems.bind fun x => Listable.elems.map fun y => ⟨x, y⟩
nodup := by
rw [List.nodup_bind]
constructor
· intros
exact List.Nodup.map sigma_mk_injective Listable.nodup
· have hnd : (Listable.elems : List α).Nodup := Listable.nodup
generalize h : (Listable.elems : List α) = xs
rw [h] at hnd
clear h
induction xs
· simp
next _ x xs ih =>
simp
simp at hnd
specialize ih hnd.2
simp [ih]
intros x' hx' _
simp
intros
subst_vars
simp
rintro rfl
simp [hx'] at hnd
complete := by
intro ⟨x, y⟩
simp only [List.mem_bind, List.mem_map, Sigma.mk.inj_iff]
use x, Listable.complete x, y, Listable.complete y

instance {p : Prop} [Decidable p]: Listable (PLift p) where
elems := if h : p then [PLift.up h] else []
nodup := by by_cases h : p <;> simp [h]
complete := by by_cases h : p <;> simp [h]

[Simon Daniel]

Matt Diamond said:

(It's all good if you don't use this... I was just bored so I decided to write the whole thing up.)

cool, looks like what i intended originally! is there a function on Sets/Multisets that lets me run them in the (IO) Monad like

def execute_set (set: Multiset (IO α)) : IO (Multiset α)  := do
  return set.map (fun x => do return <- x)

searching for moand in the Multiset docs didnt come up with something.
and thanks @Kyle Miller for sharing, Ill play around with FinEnums

[Matt Diamond]

I'm unsure if Multiset is a Traversable... I assume you want to use docs#sequence here

[Matt Diamond]

you might need a list to do that

[Kyle Miller]

I don't think it can be Traversable. It would have to choose an order to perform the IO actions in, and different orders of IO actions have different effects.

[Matt Diamond]

@Simon Daniel if you want it to be Traversable, perhaps docs#AList would be better than docs#Finmap

(or you could use Finmap and then convert it to a List right before executing it, assuming you have some way of sorting it)

[Simon Daniel]

i guess switching to FinEnum instances would add the ordering

[Simon Daniel]

maybe you can help with the AList construction from FinEnum...

structure collection (α: Type) (β: α -> Type) [DecidableEq α] where
  data: AList β
  complete: ∀ (k : α), (data.lookup k).isSome

def construct_collection [DecidableEq α] [FinEnum α] (β: α -> Type) (f: (v : α) -> β v) : IO (collection α β) := do
 return {
          data := ⟨
            let mset := (Finset.univ).val.map (fun k => ⟨k, f k⟩)
            mset -- from multiset to AList with FunEnum implied order?
            by
              rw [← Multiset.nodup_keys]
              simp [Multiset.keys, Finset.univ.nodup],
          ⟩,
          complete := fun k => by
            rw [AList.lookup_isSome, AList.mem_def]
            simp [Multiset.keys]
        }

[Matt Diamond]

you would create the AList data with (FinEnum.toList α).map (fun k => ⟨k, f k⟩)

[Matt Diamond]

def construct_collection [DecidableEq α] [FinEnum α] (β: α -> Type) (f: (v : α) -> β v) : IO (collection α β) :=
pure {
  data := ⟨
    (FinEnum.toList α).map (fun k => ⟨k, f k⟩),
    by simp [List.NodupKeys, List.keys, Function.comp]
  ⟩,
  complete := fun k => by
    simp [AList.lookup_isSome, AList.mem_keys, AList.keys, List.keys]
}

[Eric Wieser]

One thing that's not clear to me is whether FinEnum or its replacement should be a tuple, a list, or an array