Playing around with Finset (Finset Char)

Stream: new members

[Antoine Meyer]

Hi,

Trying to learn some Lean by playing around with finite automata, I've been attempting to define finite sets (of, say, Char) as subsets of other finite sets. This seemed necessary to specify the initial and final states and the transition function of a finite automaton over some fixed alphabet and set of states.

Doing this involves cumbersome notation, in particular to write down small examples, because one has to prove that each element indeed belong to the enclosing finite set.

Here is a short excerpt of what I've come up with :

import Mathlib.Data.Finset.Basic

def Aabcd   : Finset Char := {'a', 'b', 'c', 'd'}

-- attempt 1 : would be ideal, but fails with
--   failed to synthesize Singleton Char (Finset { x // x ∈ Aabcd })
--   failed to synthesize Insert Char (Finset { x // x ∈ Aabcd })
def Aac1   : Finset Aabcd  := {'a', 'c'}

-- attempt 2 : ok but really cumbersome
def Aac2  : Finset Aabcd  := {⟨'a', by decide⟩, ⟨'c', by decide⟩}

-- attempt 3 : fails with
--   failed to synthesize Singleton Char (Multiset { x // x ∈ Aabcd })
--   failed to synthesize Insert Char (Multiset { x // x ∈ Aabcd })
def Aac3  : Finset Aabcd  := ⟨{'a', 'c'}, by decide⟩

-- attempt 4 : ok but possibly not very idiomatic...
def finset_cast (s : Finset α) {t : Finset α} (h : s ⊆ t) : Finset t :=
  let f : s → t := fun ⟨x, hx⟩ => ⟨x, h hx⟩
  let hf : (Multiset.map f s.val.attach).Nodup := by
    apply Multiset.Nodup.map
    . simp [Function.Injective, f]
    . rw [Multiset.nodup_attach]
      exact s.nodup
  ⟨s.val.attach.map f, hf⟩

def Aac4 : Finset Aabcd  := finset_cast {'a', 'c'} (by decide)

Is there an elegant / idiomatic way to omit the (by decide) parts in these examples? Or ideally, to make the syntax in attempt 1 above trigger some kind of automatic coercion or dependent coercion? Or is the "Finset over a Finset" approach a really bad idea?

Thanks!

(PS : I've never really introduced myself here, is it something people still do, or has this channel been converted to a noob-questions channel?)

[Bjørn Kjos-Hanssen]

Instead of working with Char you could use Fin 4 and then Aac1 would be ({0,2} : Set (Fin 4)).
Or you could define a new type T containing elements a,b,c,d and then do {a,c} : Set T.
Char is not really a thing in mathematics so if we're doing mathematics it is probably best avoided.

[Antoine Meyer]

Thanks Bjørn. I’ll experiment with your suggestions using Fin and Set.

Still, I’d be curious to know about my original question, if only to learn about this kind of coercions.

To be honest I don’t really care that much about Char, it could be any arbitrary type. It’s just convenient to be able to use letters when working with automata (whether or not that can be considered real math).